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 …

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) )]$$…

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)\) …