Constraint system in STWO
…
How Powdr translates PIL to Plonky3 and what about to stwo —2
following the first post
got two tasks:
- generate trace from pil to stwo
- implement FrameworkEval trait, which is used by stwo to define constraint, to PowdrCircuit
let’s talk about generate trace first.
in stwo, the trace is in this format as showed in last post
ColumnVec<CircleEvaluation<SimdBackend, BaseField, BitReversedOrder>>how powdr …
How Powdr translates PIL to Plonky3 STARK—1
in Powdr, the proving function of Plonky3 is in function prove_with_key, in stark.rs
you can see the inputs for prove_with_key function has “air”, this is what used to define constraints, powdr gives “&circuit” to it, and it is a powdrcircuit, probably powdrcircuit applies the trait of AIR
so at this …
stwo fibonacci
it is about this example in stwo
two parameters:
FIB_SEQUENCE_LENGTH specifies the rounds of fibo sequence
LOG_N_INSTANCES as stwo use SIMD, data parallel data struct, this number specify how many instances of fibo sequences are proved at the same time. The data are packed in LOG_N_LANES chunks, which is 16 …
Stwo backend note2
following note1
packed31 is a vector of length 16
try to understand how the trace is generated
the bottom lines actually transfer the M31 values into circleDomain
from start:
N is log N instances
this code is to initialise the witness columns, later use to store the witness.
this code …
stwo backend note1
Powdr side
backend trait in powdr
- verify
- prove
- export_verification_key
how plonky3 implemented? this is in mod.rs
in mod.rs the backend trait is implemented for plonky3prover, in the prove function, it calls prove in stark.rs, where plonky3prover is implemented
so this prove function in stark.rs should be simliarly implemented in prover.rs …
About the repetition in GKR
There are different ways to describe the GKR algorithm
from Libra paper:
\(\tilde{V}_i(g) = \sum\limits_{x,y \in \{0,1\}^{s_{i+1}}} f_i(x,y)\)
\(= \sum\limits_{x,y \in \{0,1\}^{s_{i+1}}} \left( \widetilde{add}_{i+1}(g,x,y)(\tilde{V}_{i+1}(x) + \tilde{V}_{i+1}(y))\right.\)
\(\left. + \tilde{mult}_{i+1}(g,x,y)(\tilde{V}_{i+1}(x)\tilde{V}_{i+1}(y)) \right)\)
from hyrax paper:
$$\widetilde{V_0}(q’,q)=\sum\limits_{h’\in \{0,1\}^{b_N}}\sum\limits_{h_L\in \{0,1\}^{b_G}}\sum\limits_{h_R\in \{0,1\}^{b_G}}P_{q’,q,1}(h’,h_L,h_R)$$
$$=\sum\limits_{h’\in \{0,1\}^{b_N}}\sum\limits_{h_L\in \{0,1\}^{b_G}}\sum\limits_{h_R\in \{0,1\}^{b_G}}\widetilde{eq_1}(q’,h’)$$
$$\cdot [\widetilde{mul_1}(q,h_L,h_R)(\widetilde{V_1}(h’,h_L)\times \widetilde{V_1}(h’,h_R) )$$
$$+\widetilde{add_1}(q,h_L,h_R)(\widetilde{V_1}(h’,h_L)+ \widetilde{V_1}(h’,h_R) )]$$…
Powdr RISCV ZKVM start
hello world example
make the powdr-rs compiler up to date, pull the lasted changes in the repo, in powdr folder do the following:
cargo install --path ./cli-rs
use powdr-rs to compile rust file
powdr-rs compile riscv/tests/riscv_data/std_hello_world -o outputthis will generate asm in output, then use pil to compile the …
Libra GKR Prover
performance:
Prover is \(\mathcal{O}(C)\)
Verifier is \(\mathcal{O}(d\log C)\) for d-depth log-space uniform circuit.
note: in sumcheck/GKR context, the size of the circuit usually is described as \(2^l\), namely, the inputs of the circuit is \(2^l\), for a linear prover in this setting, has complexity \(\mathcal{O}(2^l)\), a logarithmic verifier has \(\mathcal{O}(l)\) …
VADCOP —2
Follow VADCOP —1
Instructions
an instruction consists of:
- a name
- a set of inputs (assignment registers or labels)
- a set of outputs (assignment registers)
- a set of powdr-pil constraints to activate when the instruction is called
- a set of links calling into functions/operations in submachines
//name of the instruction,