resources:
What is buses?
zkvm uses specialized component to offload some expensive computation outside of the main circuit (can I call it table here?), lookup is needed to prove the offloading process is correct: the inputs to the specialized circuit are consistent with what the main circuit put into this specialized component. They call it buses (why not just lookup?)
The difference between bus and lookup:
lookup is the process of checking one table belongs to another table, but buses is about checking there are correct input that is put into the sending table and receiving table. which means, suppose there 3 tables:
execution table \(t\), range check record \(r\), range table \(b\)
lookup: \(r \in b\), \(b \in t\)
buses: \(b \in t\)
Example from SP1 zkVM Design Concepts from Georg
in zkVM machine, Prover provides a big table of values. In Powdr there is concept of machine (in SP1 It is called chip), you can think of machine as a set of columns, the whole table can be partitioned to different machines.
The CPU is the main chip, having a column for each register, each row is the time step. For complicated instruction, CPU delegate it to specialized machines, and use lookup to guarantee the consistency.
and in CPU there will be a column instr_mul has only binary values, and the lookup operation’s goal is to prove (cpu.a, cpu.b, cpu.c) is in the multiplication table.
question here: why the blue and pink frame always need to consume a row alone?
The benefit here is now the multiplication machine only needs to be a table, without any computation. and the CPU is responsible to make sure that the right inputs are passed to the instruction.
The lookup operation basically is compiled to extra witness by added to the trace and some extra constraints. The exception here are these extra witness (columns) are interacting with all the machines.
The logup accumulator column is used to sum up some values. If lookup arguments hold, the logup accumulator column should be 0 at the end.
what is the cost to add more constraints (between cols and between rows?)
The sum can be pulled apart, you can compute the sum per machine, and get a partial sum for each machine. For example, you can just expose them as public inputs, and the verifier can just sum together the three values in the above example, and be convinced the lookup argument is satisfied.
This enable machines can have different number of rows.
What happens to the fixed columns then? fixed columns are known before inputs are known
- plonky3 has polynomials encoding is_first and is_last
- no latches if block size is 1
- fixed columns can be changed to witness columns + constraints
Continuations/sharding
the monolithic table can be split horizontally, but it can also be split vertically, then make proof for each chunk, expose the intermediate accumulator columns.
optimise it, to split bus sending to different machines
Example from polygon Miden VM
the example is a range checker using Logup
Notation: \(v\) is the value of column \(v\) in the current row, and \(v’\) as the value of column \(v\) in the next row
example 1: Simple range check
goal:
prove all the values in \(v\) are in range of 8-bit
Constraints:
- The value in the first row must be 0.
- The value in the last row must be 255.
- As we move from one row to the next, we can either keep the value the same or increment it by 1.
The last constraint is applied by:
\((v’-v)(v’-v-1)=0\)
Using logup:
we need to add one column \(b\) that will keep a running sum of the logarithmic derivative of the product of values in the \(v\) column. The constraint for this extra column \(b\) suppose to be:
\(b’=b+\frac{1}{(\alpha -v)}\)
remove the format of division, which is equivalent to:
\(b’ \cdot (\alpha -v)=b \cdot (\alpha – v) + 1\)
To check if other column \(x\) is a permutation of values in \(v\), we can compute the running sum of \(x\) the same way, then compare if the last value of the running sum is the same with \(b\)
Limitation:
can only do permutation check, which has limitation on the values (\(x\) needs contains all the values) and length of \(x\)
Example 2: range check with multiplicity
Add one more column \(m\) to keep track of the multiplicity of each value should be range-checked.
Constraint:
$$b’ = b + \frac{m}{\alpha – v}$$
Gains:
- We no longer need to pad the column we want to range-check with extra values because we can skip the values we don’t care about by setting the multiplicity to 0.
- We can range check as many unique values as there are rows in the trace, and there is essentially no limit to how many times each of these values can be range-checked. (The only restriction on the multiplicity value is that it must be less than the size of the set of lookup values. Therefore, for long traces where n>216, m<216 must hold, and for short traces m<n must be true.) (isn’t the sum of all the values \(m\) should be smaller than \(n\))
To be continued in next post