From lib.rs, there is test, checking prove simple:
check what this prove simple means
there are some prove and compile, prove recursion basic function in this file.
Compile:
In the compile function, there are two functions til now I think it …
Zero knowledge proof
About Keccak
Compiler Concept
Logup-GKR batching concept
Logup GKR in an example
traces:
\(a: [a_0,a_1,a_2,a_3,a_4,a_5,a_6,a_7]\)
\(b: [b_0,b_1,b_2,b_3,b_4,b_5,b_6,b_7]\)
goal:
prove logup relation:
\(\sum\limits_{i=0}^{i=7}\frac{1}{a_i+\alpha}=\sum\limits_{i=0}^{i=7}\frac{1}{b_i+\alpha}\)
what are available:
- commitments to the traces via FIR:
\(\text{commit}[a(x)]\)
\(\text{commit}[b(x)]\)
note: \(a(x),b(x)\) denote the polynomials’ evaluation in trace domain, \(x\) comes from cyclic group.
- GKR circuit: give a
logup GKR stwo implementation steps
Stwo logup-GKR : build test example
Stwo Logup with GKR: extra traces for GKR
GKR circuit:
a layer in GKR : proversrccorelookupsgkr_prover.rslayer
they take Mle: multi-linear extension as “input”.
Mle: corelookupsmle.rs
stored its evaluations on boolean hypercube, which is enough to uniquely determined the MLE
come back to the GKR layer struct, search where LogUpGeneric is used.…