Deep dive to InfoEvaluator of Stwo

The reason I write this is because I saw the verification sample ood points are related to InfoEvalator. InfoEvalator contains this mask or mask offset information which basically embedded the circuit information. This mask points of MleEvalProverComponent Start with component built when a component is buit, it takes a location_allocator, PowdrEval (type implement FrameworkEval), and logup_sums. -> new function of Component (trait FrameworkComponent): PowdrEval.evaluate function is called, upon infoevaluator, is where the mask_offset start building struct of Infoevaluator is defined as The important field mask_offsets is updated every time a new column, or new interaction is built, by calling function next_trace_mask or get_preprocessed_column mask_offset has this structure: it has three vectors to present pre-processed columns, let’s call them interation vector, interaction 0 is pre-processed, 1 is witness cols, 2 is for logup each interaction vector contains vectors to present columns. let’s call them column vectors each column vectors contains values …

Native logup implementation of Stwo backend Powdr

Powdr side: run test in pipeline (I changed the test so it can include stwo): #[test] fn witness_lookup() { let f = “pil/witness_lookup.pil”; let inputs = [3, 5, 2, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7] .into_iter() .map(GoldilocksField::from) .collect::<Vec<_>>(); let pipeline = make_prepared_pipeline(f, inputs, Default::default(), LinkerMode::Bus); test_mock_backend(pipeline); let inputs = [3, 5, 2, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7] .into_iter() .map(Mersenne31Field::from) .collect::<Vec<_>>(); let pipeline = make_prepared_pipeline(f, inputs, Default::default(), LinkerMode::Bus); test_stwo_pipeline(pipeline); } the witness_lookup.pil file: let N: int = 16; namespace std::convert(N); let fe = []; namespace std::prover(N); enum Query { Input(int, int), } namespace Quad(N); col fixed id(i) { i }; col fixed double(i) { i * 2 }; col witness input(i) query std::prelude::Query::Input(0, i + 1); col witness wdouble; col witness quadruple; [input, wdouble] in [id, double]; [wdouble, quadruple] in [id, double]; public out = quadruple(N-1); …

Bus in different field -1

the goal is to understand the extra cost (witness column) brought by using different field, in the bus part. start with lookup_via_challenges_range_constraint.asm use std::convert::fe; use std::protocols::lookup::lookup; use std::math::fp2::from_base; use std::prover::challenge; machine Main with degree: 8 { // Prove a correct decomposition of x into 3-bit limbs col fixed x = [1, 6, 23, 55, 63, 4, 1, 0]; col witness x_low, x_high; col fixed BIT3 = [0, 1, 2, 3, 4, 5, 6, 7]; lookup([x_low] in [BIT3]); lookup([x_high] in [BIT3]); x = x_low + 8 * x_high; } BN254 field run this command to spell out Logup constraint without field extension. cargo run pil test_data/std/lookup_via_challenges_range_constraint.asm -o output -f –field bn254 the generated …_opt.pil file: code and constraint explanation: Logup constraint: accumulator initiate: main::is_first * main::acc = 0; logup constraint: (std::prelude::challenge(0, 2) – main::x_low) * (std::prelude::challenge(0, 2) – main::BIT3) * (main::acc’ – main::acc) + main::multiplicities * (std::prelude::challenge(0, 2) – main::x_low) = …

Spartan 4

previous posts: ,, and Overview of spartan paper summarize again what spartan paper offer: transparent zksnark for arbitrarily NP statement sub-linear verification time optimal prover sub-linear verification,computation commitment for sparse multilinear polynomials recall in post 3, the remaining problems: use extractable polynomial commitment for multiliear polynomial \(\widetilde{Z}(r_y)\) to avoid \(O(|w|)\) communications other terms can be computed locally by verifier, namely, \(\widetilde{A},\widetilde{B},\widetilde{C}\) it is circuit information. section 6 of the paper discusses how to make the computation sublinear sub-linear verification is achieved by a public preprocessing step, in this pre-processing step, verifier basically need to evaluated the metrics \(\widetilde{A},\widetilde{B},\widetilde{C}\), but this evaluation can also be verifiably delegated to the prover, using the computation commitment. these computation commitments are commitments for sparse multilinear polynomials. Spark compiler to transform extractable polynomial commitment scheme for multilinear polynomials to one for sparse multilinear polynomials. consists of: extractable polynomial commitment scheme as black box special-purpose zkSNARK??? …

Spartan 3

following the previous posts about spartan: 1 and Chapter 5, A family of NIZKs with succinct interactive argument of knowledge from post 1 we get a goal to check \(\mathcal{Q}_{io}(\tau)=\sum\limits_{x\in \{0,1\}^s}\mathcal{G}_{io,\tau}(x)=\sum\limits_{x\in \{0,1\}^s}\widetilde{F}_{io}(x)\cdot \widetilde{eq}(\tau,x)=0\) where \(\tau\) is a random checking point. recall we have: \(\widetilde{F}_{io}(x)=\left(\sum\limits_{y\in\{0,1\}^s}\widetilde{A}(x,y)\cdot Z(y)\right)\cdot \left(\sum\limits_{y\in\{0,1\}^s}\widetilde{B}(x,y)\cdot Z(y)\right)\) let’s start from here to do further reduction. reduction step 1: use sum-check protocol to check \(\sum\limits_{x\in \{0,1\}^s}\mathcal{G}_{io,\tau}(x)=\sum\limits_{x\in \{0,1\}^s}\widetilde{F}_{io}(x)\cdot \widetilde{eq}(\tau,x)=0\) the last step of a sum-check protocol is an evaluation of a function in a random point. so the above claim can be reduced via sumcheck protocol to \(e_x\stackrel{?}{=}\mathcal{G}_{io,\tau}(r_x)\) where \(r_x\in \mathbb{F}^s\) to compute \(\mathcal{G}_{io,\tau}(r_x)\) is equivalent to compute \(\mathcal{G}_{io,\tau}(r_x)=\widetilde{F}_{io}(r_x)\cdot \widetilde{eq}(\tau,r_x)\) so let’s talk about computing \(\widetilde{F}_{io}(r_x)\) \(\widetilde{F}_{io}(r_x)=\left(\sum\limits_{y\in\{0,1\}^s}\widetilde{A}(r_x,y)\cdot Z(y)\right)\cdot \left(\sum\limits_{y\in\{0,1\}^s}\widetilde{B}(r_x,y)\cdot Z(y)\right)\) $$-\left(\sum\limits_{y\in\{0,1\}^s}\widetilde{C}(r_x,y)\cdot Z(y)\right)$$ The prover can then make three separate claims to \(\mathcal{V}\) : $$\bar{A}(r_x)=v_A,\bar{B}(r_x)=v_B,\bar{C}(r_x)=v_C$$ (why the tilde becomes bar? because the values here is the product of matrix and witness, namely \(\bar{A}(r_x)=\sum\limits_{y\in\{0,1\}^s}\widetilde{A}(r_x,y)\cdot …

On my way to review, about lookup –1

Trying to understand from this PR understanding lookup.asm let is_first: col = |i| if i == 0 { 1 } else { 0 }; the above line, defines fix column, fix columns are columns known during circuit setup, independent of the what the witness will be. “i” represent the row number. check here for more details. let alpha1: expr = challenge(0, 1); challenge built in function, Constructs a challenge object, essentially asking the verifier for a random number.The first argument is the proof stage and the second is the identifier of the challenge. some more explanation of challenger from Tibo “So basically you can think of witgen and proving as the same process:witgen phase 0 -> prove phase 0 -> witgen phase 1 -> prove phase 1 at the end of phase 0 proving, we draw randomness from the verifier and we use this randomness to run witness generation for …