Lookups

[eightfilms]

This will serve as a discussion for all lookup-related research on existing implementations.

To make use of our traces, we need to use lookups to reason about relationships and prove computation between them.

I'll write a new comment for each existing implementation so that we may reply and discuss under the relevant comment for each VM.

Each section will include a section on the algorithm and the actual code for reference.

[eightfilms]

OlaVM

OlaVM uses both inner table lookups and cross table lookups:

Inner Table Lookup (2 constraints)

A subset argument technology between columns I and T, proving that cells in column I all appear in column T at least once.

Algorithm

A quick and dirty summary of the image - given 2 columns I and T, we want to prove that all cells in column I appear in column T at least once. To achieve this, we need to implement and use a permutation argument.

source: page 137 of the OlaVM whitepaper V2

Code

The relevant code is found in eval_lookups() function:

In the implementation of that function you can see that the constraints are being enforced in a &mut ConstraintConsumer<P> where P is a PackedField. Note that PackedField here is a struct implemented in plonky2, but Ola is using a fork of plonky2 in their repo. Original vs fork. As far as I can tell there isn't a significant diff here when it comes to usage of plonky2.

pub(crate) fn eval_lookups<F: Field, P: PackedField<Scalar = F>, const COLS: usize>(
    vars: StarkEvaluationVars<F, P, COLS>,
    yield_constr: &mut ConstraintConsumer<P>,
    col_permuted_input: usize,
    col_permuted_table: usize,
) {

    // Other code above this line
    yield_constr.constraint(diff_input_prev * diff_input_table);
    // This is actually constraining the first row, as per the spec, since
    // `diff_input_table` is a diff of the next row's values. In the context of
    // `constraint_last_row`, the next row is the first row.
    yield_constr.constraint_last_row(diff_input_table);
  }

Cross Table Lookup

Mix of subset argument and permutation argument (This is basically a multiset check from what I can tell)

• When implementing STARK tables, Starky needs to define all the STARK cross table lookup relationships (which STARK table(s) each STARK table needs, what columns/rows are involved)

Algorithm

source: page 138 of OlaVM whitepaper V2

Code

The CrossTableLookup struct implementation can be found here, and there's actually some relevant tests found in the same file as well showing its usage, so this could be quite useful.

The usage of these cross table lookups can be found when constructing an OlaStark (which is basically a STARK proof of all the STARK table proofs) - source file here

[eightfilms]

Miden

Miden uses lookup arguments in the form of multiset checks, for 2 purposes (Multiset Checks - Polygon Wiki).

1. To prove the consistency of intermediate values that must persist between different cycles of the trace, without storing the full data in the execution trace (which would require adding more columns to the trace).
2. To prove correct interaction between two independent sections of the execution trace, e.g., between the main trace where the result of some operation is required, but would be expensive to compute, and a specialized component which can perform that operation cheaply.

Compared to Ola, the main difference seems to be that multiset equality check is implemented as a single running product column (which is not actually single, later on it is explained that each running product column needs to be represented by 2 columns for ~100-bit security)

(This info is found in the link above)

The first is achieved through virtual tables, while the second is achieved through a communication bus. Currently, there are 2 buses implemented (chiplets bus, range checker bus)

Essentially both seem like optimization techniques. Virtual tables trade off storing entire tables for storing extra rows + doing some computation to prove data consistency of this 'fake' table. The communication bus connects two sections of a trace, and operates on the Request/Response paradigm (eg. the stack can 'request' a 'response' from the Bitwise chiplet for a bitwise operation)

Constraints

The constraints for the communication bus can be found here.

Code

The ChipletsBus is basically the construct that tracks all the requests and responses to and from the stack and the chiplets (except the range checker). They use an AuxiliaryTrace, built by an AuxTraceBuilder to support this. This part is a bit confusing to me since there's a separate trace builder for different components (stack, chiplets, range checker)

[eightfilms]

Triton

As a disclaimer, TritonVM is using a different hash function (Tip5) instead of Poseidon. So I'm not entirely sure if this would be useful for our purposes.

They rely on Lookup Tables as well as Cascade Tables - this construction seems unique for the usage of the Tip5 hash. I'd have to read the Tip5 paper in detail to understand it but it seems like TLDR of the paper is that they did some benchmarking and found Tip5 to be much faster than Poseidon/Rescue-prime. Benchmarks are available in the paper. It's based on Marvellous design strategy (eg. Rescue-Prime) in contrast to Hades desgin strategy (eg. Poseidon).

One thing we could learn from them is their code quality, which is very nice imo:

Tables
Constraints

However, their constraints seem to be auto-generated by something called the constraint-evaluation-generator,

Out of curiosity there's also an example program found in a separate repository in triton-vm-scaffold.

[eightfilms]

Risc0

There isn't much to gather from their code since part of it seems like it's closed source. We can look at their Accum code to see how they deal with their grand product accumulation, as well as their verifier code, but beyond that there doesn't seem like much we can gather.