plonk in stwo
Trace table looks like this:
a_wire | a_val | b_wire | b_val | c_wire | c_val | multiplicity |
0 | 1 | 1 | 1 | 2 | 2 | 2 |
1 | 1 | 2 | 2 | 3 | 3 | 2 |
2 | 2 | 3 | 3 | 4 | 5 | 1 |
3 | 3 | 4 | 5 | 5 | 8 | 0 |
Constraints:
- gate at each row: c_val – op * (a_val + b_val)+ (E::F::one() – op) * a_val. * b_val
- copy constraints via logup lookup, by lookup.combine, which combining the values with their position in the trace.
kind of a clever way for lookup with pre-defined permutation.
two list:
- a list \(L_0\) that consists of:
(a_wire+a_val*random) for each pair of (a_wire,a_val) code reference
(b_wire +b_val*random) for each pair of (b_wire, b_val)
- a list \(L_1\) that consists of:
(c_wire +c_val*random) for each pair of (c_wire, c_val)
using logup to prove: \(L_0 \in L_1\) with the multiplicity of the record in \(L_1\) is [2,2,….,1,0] code reference
Conclusion and questions:
- list \(L_0\) has these three records, which are not in \(L_1\)
(0,1 ) (1,1 ) from (a_wire, a_val)
(1,1) from (b_wire,b_val)
how do they get handled? currently I am checking the details of logup implementation, specifically related to this code
- by combine (a_wire,a_val), it combines each value with its position in the trace, this seems can be used to implement the “next reference” and define the constraints between rows. but there might be problems, for example, the gap between each step is not necessary to be 1, can be 2, so the below trace can also pass verification successfully, I don’t know if this actually matters, skeptical about this method.
a_wire | a_val | b_wire | b_val | c_wire | c_val | multiplicity |
0 | 1 | 2 | 1 | 4 | 2 | 2 |
2 | 1 | 4 | 2 | 6 | 3 | 2 |
4 | 2 | 6 | 3 | 8 | 5 | 1 |
6 | 3 | 8 | 5 | 10 | 8 | 0 |
AIR for STARK
to define AIR arithmtization, not using the lookup way, I think this function and this function are needed to be defined. These two functions are related to step constraint evaluation, used for “next reference”. These functions are from the old fibonacci example, which use CpuBackend, the mask input (here and here ) are related to the next_interation_mask in EvalAtRow, which is for SIMD backend.
to implement these two functions, I start checking some details about circle stark. coset and vanishing polynomial on circle domain.
Questions
If there any SIMD based backend AIR airthmetization example, maybe I don’t need to get too deep into circle STARK?
or should just use next_interation_mask(0,[0,1]) for “next reference” and SIMD backend to start writing circuit?
Now I think I understand why Leo from STARWARE told me they expected user to use lookup to define constraints among rows. Using more lookup, which means using their GKR improved logup will gain more benefits, but as I describe in PLONK example, I am not sure it is the approach build AIR kink of thing?