arrabbiata/
witness.rs

1use ark_ec::CurveConfig;
2use ark_ff::PrimeField;
3use ark_poly::Evaluations;
4use kimchi::circuits::{domains::EvaluationDomains, gate::CurrOrNext};
5use log::debug;
6use mina_poseidon::constants::SpongeConstants;
7use num_bigint::{BigInt, BigUint};
8use num_integer::Integer;
9use o1_utils::field_helpers::FieldHelpers;
10use poly_commitment::{commitment::CommitmentCurve, ipa::SRS, PolyComm, SRS as _};
11use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
12
13use crate::{
14    challenge::{ChallengeTerm, Challenges},
15    column::Column,
16    curve::{ArrabbiataCurve, PlonkSpongeConstants},
17    interpreter::{Instruction, InterpreterEnv, Side, VERIFIER_STARTING_INSTRUCTION},
18    setup, NUMBER_OF_COLUMNS, NUMBER_OF_VALUES_TO_ABSORB_PUBLIC_IO,
19};
20
21/// A running program that the (folding) interpreter has access to.
22pub struct Program<
23    Fp: PrimeField,
24    Fq: PrimeField,
25    E: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>,
26> where
27    E::BaseField: PrimeField,
28    <<E as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
29{
30    /// Commitments to the accumulated program state.
31    ///
32    /// In Nova language, this is the commitment to the witness accumulator.
33    pub accumulated_committed_state: Vec<PolyComm<E>>,
34
35    /// Commitments to the previous program states.
36    ///
37    /// In Nova language, this is the commitment to the previous witness.
38    pub previous_committed_state: Vec<PolyComm<E>>,
39
40    /// Accumulated witness for the program state.
41    ///
42    /// In Nova language, this is the accumulated witness W.
43    ///
44    /// The size of the outer vector must be equal to the number of columns in
45    /// the circuit.
46    /// The size of the inner vector must be equal to the number of rows in
47    /// the circuit.
48    pub accumulated_program_state: Vec<Vec<E::ScalarField>>,
49
50    /// List of the accumulated challenges over time.
51    pub accumulated_challenges: Challenges<BigInt>,
52
53    /// Challenges during the last computation.
54    /// This field is useful to keep track of the challenges that must be
55    /// verified in circuit.
56    pub previous_challenges: Challenges<BigInt>,
57}
58
59impl<Fp: PrimeField, Fq: PrimeField, E: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>>
60    Program<Fp, Fq, E>
61where
62    E::BaseField: PrimeField,
63    <<E as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
64{
65    pub fn new(srs_size: usize, blinder: E) -> Self {
66        // Default set to the blinders. Using double to make the EC scaling happy.
67        let previous_committed_state: Vec<PolyComm<E>> = (0..NUMBER_OF_COLUMNS)
68            .map(|_| PolyComm::new(vec![(blinder + blinder).into()]))
69            .collect();
70
71        // FIXME: zero will not work.
72        let accumulated_committed_state: Vec<PolyComm<E>> = (0..NUMBER_OF_COLUMNS)
73            .map(|_| PolyComm::new(vec![blinder]))
74            .collect();
75
76        let mut accumulated_program_state: Vec<Vec<E::ScalarField>> =
77            Vec::with_capacity(NUMBER_OF_COLUMNS);
78        {
79            let mut vec: Vec<E::ScalarField> = Vec::with_capacity(srs_size);
80            (0..srs_size).for_each(|_| vec.push(E::ScalarField::zero()));
81            (0..NUMBER_OF_COLUMNS).for_each(|_| accumulated_program_state.push(vec.clone()));
82        };
83
84        let accumulated_challenges: Challenges<BigInt> = Challenges::default();
85
86        let previous_challenges: Challenges<BigInt> = Challenges::default();
87
88        Self {
89            accumulated_committed_state,
90            previous_committed_state,
91            accumulated_program_state,
92            accumulated_challenges,
93            previous_challenges,
94        }
95    }
96
97    /// Commit to the program state and updating the environment with the
98    /// result.
99    ///
100    /// This method is supposed to be called after a new iteration of the
101    /// program has been executed.
102    pub fn commit_state(
103        &mut self,
104        srs: &SRS<E>,
105        domain: EvaluationDomains<E::ScalarField>,
106        witness: &[Vec<BigInt>],
107    ) {
108        let comms: Vec<PolyComm<E>> = witness
109            .par_iter()
110            .map(|evals| {
111                let evals: Vec<E::ScalarField> = evals
112                    .par_iter()
113                    .map(|x| E::ScalarField::from_biguint(&x.to_biguint().unwrap()).unwrap())
114                    .collect();
115                let evals = Evaluations::from_vec_and_domain(evals, domain.d1);
116                srs.commit_evaluations_non_hiding(domain.d1, &evals)
117            })
118            .collect();
119        self.previous_committed_state = comms
120    }
121
122    /// Absorb the last committed program state in the correct sponge.
123    ///
124    /// For a description of the messages to be given to the sponge, including
125    /// the expected instantiation, refer to the section "Message Passing" in
126    /// [crate::interpreter].
127    pub fn absorb_state(&mut self, digest: BigInt) -> Vec<BigInt> {
128        let mut sponge = E::create_new_sponge();
129        let previous_state: E::BaseField =
130            E::BaseField::from_biguint(&digest.to_biguint().unwrap()).unwrap();
131        E::absorb_fq(&mut sponge, previous_state);
132        self.previous_committed_state
133            .iter()
134            .for_each(|comm| E::absorb_curve_points(&mut sponge, &comm.chunks));
135        let state: Vec<BigInt> = sponge
136            .sponge
137            .state
138            .iter()
139            .map(|x| x.to_biguint().into())
140            .collect();
141        state
142    }
143
144    /// Simulate an interaction with the verifier by requesting to coin a
145    /// challenge from the current prover sponge state.
146    ///
147    /// This method supposes that all the messages have been sent to the
148    /// verifier previously, and the attribute [self.prover_sponge_state] has
149    /// been updated accordingly by absorbing all the messages correctly.
150    ///
151    /// The side-effect of this method will be to run a permutation on the
152    /// sponge state _after_ coining the challenge.
153    /// There is an hypothesis on the sponge state that the inner permutation
154    /// has been correctly executed if the absorbtion rate had been reached at
155    /// the last absorbtion.
156    ///
157    /// The challenge will be added to the [self.challenges] attribute at the
158    /// position given by the challenge `chal`.
159    ///
160    /// Internally, the method is implemented by simply loading the prover
161    /// sponge state, and squeezing a challenge from it, relying on the
162    /// implementation of the sponge. Usually, the challenge would be the first
163    /// N bits of the first element, but it is left as an implementation detail
164    /// of the sponge given by the curve.
165    pub fn coin_challenge(&self, sponge_state: Vec<BigInt>) -> (BigInt, Vec<BigInt>) {
166        let mut sponge = E::create_new_sponge();
167        sponge_state.iter().for_each(|x| {
168            E::absorb_fq(
169                &mut sponge,
170                E::BaseField::from_biguint(&x.to_biguint().unwrap()).unwrap(),
171            )
172        });
173        let verifier_answer = E::squeeze_challenge(&mut sponge).to_biguint().into();
174        sponge.sponge.poseidon_block_cipher();
175        let state: Vec<BigInt> = sponge
176            .sponge
177            .state
178            .iter()
179            .map(|x| x.to_biguint().into())
180            .collect();
181        (verifier_answer, state)
182    }
183
184    /// Accumulate the program state (or in other words,
185    /// the witness), by adding the last computed program state into the
186    /// program state accumulator.
187    ///
188    /// This method is supposed to be called after the program state has been
189    /// committed (by calling [self.commit_state]) and absorbed (by calling
190    /// [self.absorb_state]). The "relation randomiser" must also have been
191    /// coined and saved in the environment before, by calling
192    /// [self.coin_challenge].
193    ///
194    /// The program state is accumulated into a different accumulator, depending
195    /// on the curve currently being used.
196    ///
197    /// This is part of the work the prover of the accumulation/folding scheme.
198    ///
199    /// This must translate the following equation:
200    /// ```text
201    /// acc_(p, n + 1) = acc_(p, n) * chal w
202    ///               OR
203    /// acc_(q, n + 1) = acc_(q, n) * chal w
204    /// ```
205    /// where acc and w are vectors of the same size.
206    pub fn accumulate_program_state(&mut self, chal: BigInt, witness: &[Vec<BigInt>]) {
207        let modulus: BigInt = E::ScalarField::modulus_biguint().into();
208        self.accumulated_program_state = self
209            .accumulated_program_state
210            .iter()
211            .zip(witness.iter()) // This iterate over the columns
212            .map(|(evals_accumulator, evals_witness)| {
213                evals_accumulator
214                    .iter()
215                    .zip(evals_witness.iter()) // This iterate over the rows
216                    .map(|(acc, w)| {
217                        let rhs: BigInt = (chal.clone() * w).mod_floor(&modulus);
218                        let rhs: BigUint = rhs.to_biguint().unwrap();
219                        let res = E::ScalarField::from_biguint(&rhs).unwrap();
220                        *acc + res
221                    })
222                    .collect()
223            })
224            .collect();
225    }
226
227    /// Accumulate the committed state by adding the last committed state into
228    /// the committed state accumulator.
229    ///
230    /// The commitments are accumulated into a different accumulator, depending
231    /// on the curve currently being used.
232    ///
233    /// This is part of the work the prover of the accumulation/folding scheme.
234    ///
235    /// This must translate the following equation:
236    /// ```text
237    /// C_(p, n + 1) = C_(p, n) + chal * comm
238    ///               OR
239    /// C_(q, n + 1) = C_(q, n) + chal * comm
240    /// ```
241    ///
242    /// Note that the committed program state is encoded in
243    /// [crate::NUMBER_OF_COLUMNS] values, therefore we must iterate over all
244    /// the columns to accumulate the committed state.
245    pub fn accumulate_committed_state(&mut self, chal: BigInt) {
246        let chal: BigUint = chal.to_biguint().unwrap();
247        let chal: E::ScalarField = E::ScalarField::from_biguint(&chal).unwrap();
248        self.accumulated_committed_state = self
249            .accumulated_committed_state
250            .iter()
251            .zip(self.previous_committed_state.iter())
252            .map(|(l, r)| l + &r.scale(chal))
253            .collect();
254    }
255}
256
257/// An environment is used to contain the state of a long "running program".
258///
259/// The running program is composed of two parts: one user application and one
260/// verifier application. The verifier application is used to encode the
261/// correctness of previous program states computations.
262///
263/// The term "app(lication) state" will be used to refer to the state of the
264/// user application, and the term "IVC state" will be used to refer to the
265/// state of the verifier application. The term program state will be used to refer to
266/// the state of the whole program.
267///
268/// The environment contains all the accumulators that can be picked for a given
269/// fold instance k, including the sponges.
270///
271/// The environment is run over big integers to avoid performing
272/// reduction at all step. Instead the user implementing the interpreter can
273/// reduce in the corresponding field when they want.
274///
275/// The environment is generic over two curves (called E1 and E2) that are
276/// supposed to form a cycle.
277pub struct Env<
278    Fp: PrimeField,
279    Fq: PrimeField,
280    E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>,
281    E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>,
282> where
283    E1::BaseField: PrimeField,
284    E2::BaseField: PrimeField,
285    <<E1 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
286    <<E2 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
287{
288    /// The relation this witness environment is related to.
289    pub indexed_relation: setup::IndexedRelation<Fp, Fq, E1, E2>,
290
291    /// Program state for curve E1
292    pub program_e1: Program<Fp, Fq, E1>,
293
294    /// Program state for curve E2
295    pub program_e2: Program<Fq, Fp, E2>,
296
297    // ----------------
298    // Data only used by the interpreter while building the witness over time
299    /// The index of the latest allocated variable in the circuit.
300    /// It is used to allocate new variables without having to keep track of the
301    /// position.
302    pub idx_var: usize,
303
304    pub idx_var_next_row: usize,
305
306    /// The index of the latest allocated public inputs in the circuit.
307    /// It is used to allocate new public inputs without having to keep track of
308    /// the position.
309    pub idx_var_pi: usize,
310
311    /// Current processing row. Used to build the witness.
312    pub current_row: usize,
313
314    /// State of the current row in the execution trace
315    pub state: [BigInt; NUMBER_OF_COLUMNS],
316
317    /// Next row in the execution trace. It is useful when we deal with
318    /// polynomials accessing "the next row", i.e. witness columns where we do
319    /// evaluate at ζ and ζω.
320    pub next_state: [BigInt; NUMBER_OF_COLUMNS],
321
322    /// While folding, we must keep track of the challenges the verifier would
323    /// have sent in the SNARK, and we must aggregate them.
324    // FIXME: nothing is done yet, and the challenges haven't been decided yet.
325    // See top-level documentation of the interpreter for more information.
326    pub challenges: Challenges<BigInt>,
327
328    /// Keep the current executed instruction.
329    /// This can be used to identify which gadget the interpreter is currently
330    /// building.
331    pub current_instruction: Instruction,
332
333    /// The sponges will be used to simulate the verifier messages, and will
334    /// also be used to verify the consistency of the computation by hashing the
335    /// public IO.
336    // IMPROVEME: use a list of BigInt? It might be faster as the CPU will
337    // already have in its cache the values, and we can use a flat array
338    pub sponge_e1: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH],
339    pub sponge_e2: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH],
340
341    /// Sponge state used by the prover for the current iteration.
342    ///
343    /// This sponge is used at the current iteration to absorb commitments of
344    /// the program state and generate the challenges for the current iteration.
345    /// The outputs of the sponge will be verified by the verifier of the next
346    /// iteration.
347    pub prover_sponge_state: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH],
348
349    /// Sponge state used by the verifier for the current iteration.
350    ///
351    /// This sponge is used at the current iteration to build the verifier
352    /// circuit. The state will need to match with the previous prover sopnge
353    /// state.
354    pub verifier_sponge_state: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH],
355
356    /// The current iteration of the IVC.
357    pub current_iteration: u64,
358
359    /// The digest of the program state before executing the last iteration.
360    /// The value will be used to initialize the execution trace of the verifier
361    /// in the next iteration, in particular to verify that the challenges have
362    /// been generated correctly.
363    ///
364    /// The value is a 128bits value.
365    pub last_program_digest_before_execution: BigInt,
366
367    /// The digest of the program state after executing the last iteration.
368    /// The value will be used to initialize the sponge before committing to the
369    /// next iteration.
370    ///
371    /// The value is a 128bits value.
372    pub last_program_digest_after_execution: BigInt,
373
374    /// The coin folding combiner will be used to generate the combinaison of
375    /// folding instances
376    pub r: BigInt,
377
378    /// Temporary registers for elliptic curve points in affine coordinates than
379    /// can be used to save values between instructions.
380    ///
381    /// These temporary registers can be loaded into the state by using the
382    /// function `load_temporary_accumulators`.
383    ///
384    /// The registers can, and must, be cleaned after the gadget is computed.
385    ///
386    /// The values are considered as BigInt, even though we should add some
387    /// type. As we want to apply the KISS method, we tend to avoid adding
388    /// types. We leave this for future work.
389    ///
390    /// Two registers are provided, represented by a tuple for the coordinates
391    /// (x, y).
392    pub temporary_accumulators: ((BigInt, BigInt), (BigInt, BigInt)),
393
394    /// Index of the values to absorb in the sponge
395    pub idx_values_to_absorb: usize,
396    // ----------------
397    /// The witness of the current instance of the circuit.
398    /// The size of the outer vector must be equal to the number of columns in
399    /// the circuit.
400    /// The size of the inner vector must be equal to the number of rows in
401    /// the circuit.
402    ///
403    /// The layout columns/rows is used to avoid rebuilding the witness per
404    /// column when committing to the witness.
405    pub witness: Vec<Vec<BigInt>>,
406
407    // --------------
408    // Inputs
409    /// Initial input
410    pub z0: BigInt,
411
412    /// Current input
413    pub zi: BigInt,
414    // ---------------
415}
416
417impl<
418        Fp: PrimeField,
419        Fq: PrimeField,
420        E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>,
421        E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>,
422    > InterpreterEnv for Env<Fp, Fq, E1, E2>
423where
424    E1::BaseField: PrimeField,
425    E2::BaseField: PrimeField,
426    <<E1 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
427    <<E2 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
428{
429    type Position = (Column, CurrOrNext);
430
431    /// For efficiency, and for having a single interpreter, we do not use one
432    /// of the fields. We use a generic BigInt to represent the values.
433    /// When building the witness, we will reduce into the corresponding field.
434    // FIXME: it might not be efficient as I initially thought. We do need to
435    // make some transformations between biguint and bigint, with an extra cost
436    // for allocations.
437    type Variable = BigInt;
438
439    fn allocate(&mut self) -> Self::Position {
440        assert!(self.idx_var < NUMBER_OF_COLUMNS, "Maximum number of columns reached ({NUMBER_OF_COLUMNS}), increase the number of columns");
441        let pos = Column::X(self.idx_var);
442        self.idx_var += 1;
443        (pos, CurrOrNext::Curr)
444    }
445
446    fn allocate_next_row(&mut self) -> Self::Position {
447        assert!(self.idx_var_next_row < NUMBER_OF_COLUMNS, "Maximum number of columns reached ({NUMBER_OF_COLUMNS}), increase the number of columns");
448        let pos = Column::X(self.idx_var_next_row);
449        self.idx_var_next_row += 1;
450        (pos, CurrOrNext::Next)
451    }
452
453    fn read_position(&self, pos: Self::Position) -> Self::Variable {
454        let (col, row) = pos;
455        let Column::X(idx) = col else {
456            unimplemented!("Only works for private inputs")
457        };
458        match row {
459            CurrOrNext::Curr => self.state[idx].clone(),
460            CurrOrNext::Next => self.next_state[idx].clone(),
461        }
462    }
463
464    fn write_column(&mut self, pos: Self::Position, v: Self::Variable) -> Self::Variable {
465        let (col, row) = pos;
466        let Column::X(idx) = col else {
467            unimplemented!("Only works for private inputs")
468        };
469        let (modulus, srs_size): (BigInt, usize) =
470            if o1_utils::is_multiple_of(self.current_iteration, 2) {
471                (
472                    E1::ScalarField::modulus_biguint().into(),
473                    self.indexed_relation.get_srs_size(),
474                )
475            } else {
476                (
477                    E2::ScalarField::modulus_biguint().into(),
478                    self.indexed_relation.get_srs_size(),
479                )
480            };
481        let v = v.mod_floor(&modulus);
482        match row {
483            CurrOrNext::Curr => {
484                self.state[idx].clone_from(&v);
485            }
486            CurrOrNext::Next => {
487                assert!(self.current_row < srs_size - 1, "The witness builder is writing on the last row. It does not make sense to write on the next row after the last row");
488                self.next_state[idx].clone_from(&v);
489            }
490        }
491        v
492    }
493
494    fn constrain_boolean(&mut self, x: Self::Variable) {
495        let modulus: BigInt = if o1_utils::is_multiple_of(self.current_iteration, 2) {
496            E1::ScalarField::modulus_biguint().into()
497        } else {
498            E2::ScalarField::modulus_biguint().into()
499        };
500        let x = x.mod_floor(&modulus);
501        assert!(x == BigInt::from(0_usize) || x == BigInt::from(1_usize));
502    }
503
504    fn constant(&self, v: BigInt) -> Self::Variable {
505        v
506    }
507
508    fn add_constraint(&mut self, _x: Self::Variable) {
509        unimplemented!("Only when building the constraints")
510    }
511
512    fn assert_zero(&mut self, var: Self::Variable) {
513        assert_eq!(var, BigInt::from(0_usize));
514    }
515
516    fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable) {
517        assert_eq!(x, y);
518    }
519
520    fn square(&mut self, pos: Self::Position, x: Self::Variable) -> Self::Variable {
521        let res = x.clone() * x.clone();
522        self.write_column(pos, res.clone());
523        res
524    }
525
526    /// Flagged as unsafe as it does require an additional range check
527    unsafe fn bitmask_be(
528        &mut self,
529        x: &Self::Variable,
530        highest_bit: u32,
531        lowest_bit: u32,
532        pos: Self::Position,
533    ) -> Self::Variable {
534        let diff: u32 = highest_bit - lowest_bit;
535        if diff == 0 {
536            self.write_column(pos, BigInt::from(0_usize))
537        } else {
538            assert!(
539                diff > 0,
540                "The difference between the highest and lowest bit should be greater than 0"
541            );
542            let rht = (BigInt::from(1_usize) << diff) - BigInt::from(1_usize);
543            let lft = x >> lowest_bit;
544            let res: BigInt = lft & rht;
545            self.write_column(pos, res)
546        }
547    }
548
549    // FIXME: for now, we use the row number and compute the square.
550    // This is only for testing purposes, and having something to build the
551    // witness.
552    fn fetch_input(&mut self, pos: Self::Position) -> Self::Variable {
553        let x = BigInt::from(self.current_row as u64);
554        self.write_column(pos, x.clone());
555        x
556    }
557
558    /// Reset the environment to build the next row
559    fn reset(&mut self) {
560        // Save the current state in the witness
561        self.state.iter().enumerate().for_each(|(i, x)| {
562            self.witness[i][self.current_row].clone_from(x);
563        });
564        // We increment the row
565        // TODO: should we check that we are not going over the domain size?
566        self.current_row += 1;
567        // We reset the indices for the variables
568        self.idx_var = 0;
569        self.idx_var_next_row = 0;
570        self.idx_var_pi = 0;
571        // We keep track of the values we already set.
572        self.state.clone_from(&self.next_state);
573        // And we reset the next state
574        self.next_state = core::array::from_fn(|_| BigInt::from(0_usize));
575    }
576
577    /// FIXME: check if we need to pick the left or right sponge
578    fn coin_folding_combiner(&mut self, pos: Self::Position) -> Self::Variable {
579        let r = if o1_utils::is_multiple_of(self.current_iteration, 2) {
580            self.sponge_e1[0].clone()
581        } else {
582            self.sponge_e2[0].clone()
583        };
584        let (col, _) = pos;
585        let Column::X(idx) = col else {
586            unimplemented!("Only works for private columns")
587        };
588        self.state[idx].clone_from(&r);
589        self.r.clone_from(&r);
590        r
591    }
592
593    fn load_poseidon_state(&mut self, pos: Self::Position, i: usize) -> Self::Variable {
594        let state = if o1_utils::is_multiple_of(self.current_iteration, 2) {
595            self.sponge_e1[i].clone()
596        } else {
597            self.sponge_e2[i].clone()
598        };
599        self.write_column(pos, state)
600    }
601
602    fn get_poseidon_round_constant(&self, round: usize, i: usize) -> Self::Variable {
603        if o1_utils::is_multiple_of(self.current_iteration, 2) {
604            E1::sponge_params().round_constants[round][i]
605                .to_biguint()
606                .into()
607        } else {
608            E2::sponge_params().round_constants[round][i]
609                .to_biguint()
610                .into()
611        }
612    }
613
614    fn get_poseidon_mds_matrix(&mut self, i: usize, j: usize) -> Self::Variable {
615        if o1_utils::is_multiple_of(self.current_iteration, 2) {
616            E1::sponge_params().mds[i][j].to_biguint().into()
617        } else {
618            E2::sponge_params().mds[i][j].to_biguint().into()
619        }
620    }
621
622    unsafe fn save_poseidon_state(&mut self, x: Self::Variable, i: usize) {
623        if o1_utils::is_multiple_of(self.current_iteration, 2) {
624            let modulus: BigInt = E1::ScalarField::modulus_biguint().into();
625            self.sponge_e1[i] = x.mod_floor(&modulus)
626        } else {
627            let modulus: BigInt = E2::ScalarField::modulus_biguint().into();
628            self.sponge_e2[i] = x.mod_floor(&modulus)
629        }
630    }
631
632    unsafe fn fetch_value_to_absorb(&mut self, pos: Self::Position) -> Self::Variable {
633        let (col, curr_or_next) = pos;
634        // Purely arbitrary for now
635        let Column::X(_idx) = col else {
636            panic!("Only private inputs can be accepted to load the values to be absorbed")
637        };
638        assert_eq!(
639            curr_or_next,
640            CurrOrNext::Curr,
641            "Only the current row can be used to load the values to be absorbed"
642        );
643        // FIXME: for now, we only absorb the commitments to the columns
644        let idx = self.idx_values_to_absorb;
645        let res = if idx < 2 * NUMBER_OF_COLUMNS {
646            let idx_col = idx / 2;
647            debug!("Absorbing the accumulator for the column index {idx_col}. After this, there will still be {} elements to absorb", NUMBER_OF_VALUES_TO_ABSORB_PUBLIC_IO - idx - 1);
648            if o1_utils::is_multiple_of(self.current_iteration, 2) {
649                let (pt_x, pt_y) = self.program_e2.accumulated_committed_state[idx_col]
650                    .get_first_chunk()
651                    .to_coordinates()
652                    .unwrap();
653                if o1_utils::is_multiple_of(idx, 2) {
654                    self.write_column(pos, pt_x.to_biguint().into())
655                } else {
656                    self.write_column(pos, pt_y.to_biguint().into())
657                }
658            } else {
659                let (pt_x, pt_y) = self.program_e1.accumulated_committed_state[idx_col]
660                    .get_first_chunk()
661                    .to_coordinates()
662                    .unwrap();
663                if o1_utils::is_multiple_of(idx, 2) {
664                    self.write_column(pos, pt_x.to_biguint().into())
665                } else {
666                    self.write_column(pos, pt_y.to_biguint().into())
667                }
668            }
669        } else {
670            unimplemented!("We only absorb the accumulators for now. Of course, this is not sound.")
671        };
672        self.idx_values_to_absorb += 1;
673        res
674    }
675
676    unsafe fn load_temporary_accumulators(
677        &mut self,
678        pos_x: Self::Position,
679        pos_y: Self::Position,
680        side: Side,
681    ) -> (Self::Variable, Self::Variable) {
682        match self.current_instruction {
683            Instruction::EllipticCurveScaling(i_comm, bit) => {
684                // If we're processing the leftmost bit (i.e. bit == 0), we must load
685                // the initial value into the accumulators from the environment.
686                // In the left accumulator, we keep track of the value we keep doubling.
687                // In the right accumulator, we keep the result.
688                if bit == 0 {
689                    if o1_utils::is_multiple_of(self.current_iteration, 2) {
690                        match side {
691                            Side::Left => {
692                                let pt = self.program_e2.previous_committed_state[i_comm].get_first_chunk();
693                                // We suppose we never have a commitment equals to the
694                                // point at infinity
695                                let (pt_x, pt_y) = pt.to_coordinates().unwrap();
696                                let pt_x = self.write_column(pos_x, pt_x.to_biguint().into());
697                                let pt_y = self.write_column(pos_y, pt_y.to_biguint().into());
698                                (pt_x, pt_y)
699                            }
700                            // As it is the first iteration, we must use the point at infinity.
701                            // However, to avoid handling the case equal to zero, we will
702                            // use a blinder, that we will subtract at the end.
703                            // As we suppose the probability to get a folding combiner
704                            // equals to zero is negligible, we know we have a negligible
705                            // probability to request to compute `0 * P`.
706                            // FIXME: ! check this statement !
707                            Side::Right => {
708                                let pt = self.indexed_relation.srs_e2.h;
709                                let (pt_x, pt_y) = pt.to_coordinates().unwrap();
710                                let pt_x = self.write_column(pos_x, pt_x.to_biguint().into());
711                                let pt_y = self.write_column(pos_y, pt_y.to_biguint().into());
712                                (pt_x, pt_y)
713                            }
714                        }
715                    } else {
716                        match side {
717                            Side::Left => {
718                                let pt = self.program_e1.previous_committed_state[i_comm].get_first_chunk();
719                                // We suppose we never have a commitment equals to the
720                                // point at infinity
721                                let (pt_x, pt_y) = pt.to_coordinates().unwrap();
722                                let pt_x = self.write_column(pos_x, pt_x.to_biguint().into());
723                                let pt_y = self.write_column(pos_y, pt_y.to_biguint().into());
724                                (pt_x, pt_y)
725                            }
726                            // As it is the first iteration, we must use the point at infinity.
727                            // However, to avoid handling the case equal to zero, we will
728                            // use a blinder, that we will subtract at the end.
729                            // As we suppose the probability to get a folding combiner
730                            // equals to zero is negligible, we know we have a negligible
731                            // probability to request to compute `0 * P`.
732                            // FIXME: ! check this statement !
733                            Side::Right => {
734                                let blinder = self.indexed_relation.srs_e1.h;
735                                let pt = blinder;
736                                let (pt_x, pt_y) = pt.to_coordinates().unwrap();
737                                let pt_x = self.write_column(pos_x, pt_x.to_biguint().into());
738                                let pt_y = self.write_column(pos_x, pt_y.to_biguint().into());
739                                (pt_x, pt_y)
740                            }
741                        }
742                    }
743                } else {
744                    panic!("We should not load the temporary accumulators for the bits different than 0 when using the elliptic curve scaling. It has been deactivated since we use the 'next row'");
745                }
746            }
747            Instruction::EllipticCurveAddition(i_comm) => {
748                // FIXME: we must get the scaled commitment, not simply the commitment
749                let (pt_x, pt_y): (BigInt, BigInt) = match side {
750                    Side::Left => {
751                        if o1_utils::is_multiple_of(self.current_iteration, 2) {
752                            let pt = self.program_e2.accumulated_committed_state[i_comm].get_first_chunk();
753                            let (x, y) = pt.to_coordinates().unwrap();
754                            (x.to_biguint().into(), y.to_biguint().into())
755                        } else {
756                            let pt = self.program_e1.accumulated_committed_state[i_comm].get_first_chunk();
757                            let (x, y) = pt.to_coordinates().unwrap();
758                            (x.to_biguint().into(), y.to_biguint().into())
759                        }
760                    }
761                    Side::Right => {
762                        if o1_utils::is_multiple_of(self.current_iteration, 2) {
763                            let pt = self.program_e2.previous_committed_state[i_comm].get_first_chunk();
764                            let (x, y) = pt.to_coordinates().unwrap();
765                            (x.to_biguint().into(), y.to_biguint().into())
766                        } else {
767                            let pt = self.program_e1.previous_committed_state[i_comm].get_first_chunk();
768                            let (x, y) = pt.to_coordinates().unwrap();
769                            (x.to_biguint().into(), y.to_biguint().into())
770                        }
771                    }
772                };
773                let pt_x = self.write_column(pos_x, pt_x.clone());
774                let pt_y = self.write_column(pos_y, pt_y.clone());
775                (pt_x, pt_y)
776            }
777            _ => unimplemented!("For now, the accumulators can only be used by the elliptic curve scaling gadget and {:?} is not supported. This should be changed as soon as the gadget is implemented.", self.current_instruction),
778        }
779    }
780
781    unsafe fn save_temporary_accumulators(
782        &mut self,
783        x: Self::Variable,
784        y: Self::Variable,
785        side: Side,
786    ) {
787        match side {
788            Side::Left => {
789                self.temporary_accumulators.0 = (x, y);
790            }
791            Side::Right => {
792                self.temporary_accumulators.1 = (x, y);
793            }
794        }
795    }
796
797    // It is unsafe as no constraint is added
798    unsafe fn is_same_ec_point(
799        &mut self,
800        pos: Self::Position,
801        x1: Self::Variable,
802        y1: Self::Variable,
803        x2: Self::Variable,
804        y2: Self::Variable,
805    ) -> Self::Variable {
806        let res = if x1 == x2 && y1 == y2 {
807            BigInt::from(1_usize)
808        } else {
809            BigInt::from(0_usize)
810        };
811        self.write_column(pos, res)
812    }
813
814    fn zero(&self) -> Self::Variable {
815        BigInt::from(0_usize)
816    }
817
818    fn one(&self) -> Self::Variable {
819        BigInt::from(1_usize)
820    }
821
822    /// Inverse of a variable
823    ///
824    /// # Safety
825    ///
826    /// Zero is not allowed as an input.
827    unsafe fn inverse(&mut self, pos: Self::Position, x: Self::Variable) -> Self::Variable {
828        let res = if o1_utils::is_multiple_of(self.current_iteration, 2) {
829            E1::ScalarField::from_biguint(&x.to_biguint().unwrap())
830                .unwrap()
831                .inverse()
832                .unwrap()
833                .to_biguint()
834                .into()
835        } else {
836            E2::ScalarField::from_biguint(&x.to_biguint().unwrap())
837                .unwrap()
838                .inverse()
839                .unwrap()
840                .to_biguint()
841                .into()
842        };
843        self.write_column(pos, res)
844    }
845
846    fn compute_lambda(
847        &mut self,
848        pos: Self::Position,
849        is_same_point: Self::Variable,
850        x1: Self::Variable,
851        y1: Self::Variable,
852        x2: Self::Variable,
853        y2: Self::Variable,
854    ) -> Self::Variable {
855        let modulus: BigInt = if o1_utils::is_multiple_of(self.current_iteration, 2) {
856            E1::ScalarField::modulus_biguint().into()
857        } else {
858            E2::ScalarField::modulus_biguint().into()
859        };
860        // If it is not the same point, we compute lambda as:
861        // - λ = (Y1 - Y2) / (X1 - X2)
862        let (num, denom): (BigInt, BigInt) = if is_same_point == BigInt::from(0_usize) {
863            let num: BigInt = y1.clone() - y2.clone();
864            let x1_minus_x2: BigInt = (x1.clone() - x2.clone()).mod_floor(&modulus);
865            // We temporarily store the inverse of the denominator into the
866            // given position.
867            let denom = unsafe { self.inverse(pos, x1_minus_x2) };
868            (num, denom)
869        } else {
870            // Otherwise, we compute λ as:
871            // - λ = (3X1^2 + a) / (2Y1)
872            let denom = {
873                let double_y1 = y1.clone() + y1.clone();
874                // We temporarily store the inverse of the denominator into the
875                // given position.
876                unsafe { self.inverse(pos, double_y1) }
877            };
878            let num = {
879                let a: BigInt = if o1_utils::is_multiple_of(self.current_iteration, 2) {
880                    let a: E2::BaseField = E2::get_curve_params().0;
881                    a.to_biguint().into()
882                } else {
883                    let a: E1::BaseField = E1::get_curve_params().0;
884                    a.to_biguint().into()
885                };
886                let x1_square = x1.clone() * x1.clone();
887                let two_x1_square = x1_square.clone() + x1_square.clone();
888                two_x1_square + x1_square + a
889            };
890            (num, denom)
891        };
892        let res = (num * denom).mod_floor(&modulus);
893        self.write_column(pos, res)
894    }
895
896    /// Double the elliptic curve point given by the affine coordinates
897    /// `(x1, y1)` and save the result in the registers `pos_x` and `pos_y`.
898    fn double_ec_point(
899        &mut self,
900        pos_x: Self::Position,
901        pos_y: Self::Position,
902        x1: Self::Variable,
903        y1: Self::Variable,
904    ) -> (Self::Variable, Self::Variable) {
905        let modulus: BigInt = if o1_utils::is_multiple_of(self.current_iteration, 2) {
906            E1::ScalarField::modulus_biguint().into()
907        } else {
908            E2::ScalarField::modulus_biguint().into()
909        };
910        // - λ = (3X1^2 + a) / (2Y1)
911        // We compute λ and use an additional column as a temporary value
912        // otherwise, we get a constraint of degree higher than 5
913        let lambda_pos = self.allocate();
914        let denom = {
915            let double_y1 = y1.clone() + y1.clone();
916            // We temporarily store the inverse of the denominator into the
917            // given position.
918            unsafe { self.inverse(lambda_pos, double_y1) }
919        };
920        let num = {
921            let a: BigInt = if o1_utils::is_multiple_of(self.current_iteration, 2) {
922                let a: E2::BaseField = E2::get_curve_params().0;
923                a.to_biguint().into()
924            } else {
925                let a: E1::BaseField = E1::get_curve_params().0;
926                a.to_biguint().into()
927            };
928            let x1_square = x1.clone() * x1.clone();
929            let two_x1_square = x1_square.clone() + x1_square.clone();
930            two_x1_square + x1_square + a
931        };
932        let lambda = (num * denom).mod_floor(&modulus);
933        self.write_column(lambda_pos, lambda.clone());
934        // - X3 = λ^2 - X1 - X2
935        let x3 = {
936            let double_x1 = x1.clone() + x1.clone();
937            let res = lambda.clone() * lambda.clone() - double_x1.clone();
938            self.write_column(pos_x, res.clone())
939        };
940        // - Y3 = λ(X1 - X3) - Y1
941        let y3 = {
942            let x1_minus_x3 = x1.clone() - x3.clone();
943            let res = lambda.clone() * x1_minus_x3 - y1.clone();
944            self.write_column(pos_y, res.clone())
945        };
946        (x3, y3)
947    }
948}
949
950impl<
951        Fp: PrimeField,
952        Fq: PrimeField,
953        E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>,
954        E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>,
955    > Env<Fp, Fq, E1, E2>
956where
957    E1::BaseField: PrimeField,
958    E2::BaseField: PrimeField,
959    <<E1 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
960    <<E2 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
961{
962    pub fn new(z0: BigInt, indexed_relation: setup::IndexedRelation<Fp, Fq, E1, E2>) -> Self {
963        let srs_size = indexed_relation.get_srs_size();
964        let (blinder_e1, blinder_e2) = indexed_relation.get_srs_blinders();
965
966        let mut witness: Vec<Vec<BigInt>> = Vec::with_capacity(NUMBER_OF_COLUMNS);
967        {
968            let mut vec: Vec<BigInt> = Vec::with_capacity(srs_size);
969            (0..srs_size).for_each(|_| vec.push(BigInt::from(0_usize)));
970            (0..NUMBER_OF_COLUMNS).for_each(|_| witness.push(vec.clone()));
971        };
972
973        // Initialize Program instances for both curves
974        let program_e1 = Program::new(srs_size, blinder_e1);
975        let program_e2 = Program::new(srs_size, blinder_e2);
976
977        // FIXME: challenges
978        let challenges: Challenges<BigInt> = Challenges::default();
979
980        // FIXME: use setup
981        let prover_sponge_state: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH] =
982            core::array::from_fn(|_| BigInt::from(0_u64));
983        let verifier_sponge_state: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH] =
984            core::array::from_fn(|_| BigInt::from(0_u64));
985
986        // FIXME: set this up correctly. Temporary as we're moving the initial
987        // transcript state into the setup
988        let sponge_e1 = indexed_relation.initial_sponge.clone();
989        let sponge_e2 = indexed_relation.initial_sponge.clone();
990
991        Self {
992            // -------
993            // Setup
994            indexed_relation,
995            // -------
996            // Program state for each curve
997            program_e1,
998            program_e2,
999            // ------
1000            // ------
1001            idx_var: 0,
1002            idx_var_next_row: 0,
1003            idx_var_pi: 0,
1004            current_row: 0,
1005            state: core::array::from_fn(|_| BigInt::from(0_usize)),
1006            next_state: core::array::from_fn(|_| BigInt::from(0_usize)),
1007
1008            challenges,
1009
1010            current_instruction: VERIFIER_STARTING_INSTRUCTION,
1011            sponge_e1,
1012            sponge_e2,
1013            prover_sponge_state,
1014            verifier_sponge_state,
1015            current_iteration: 0,
1016            // FIXME: set a correct value
1017            last_program_digest_before_execution: BigInt::from(0_u64),
1018            // FIXME: set a correct value
1019            last_program_digest_after_execution: BigInt::from(0_u64),
1020            r: BigInt::from(0_usize),
1021            // Initialize the temporary accumulators with 0
1022            temporary_accumulators: (
1023                (BigInt::from(0_u64), BigInt::from(0_u64)),
1024                (BigInt::from(0_u64), BigInt::from(0_u64)),
1025            ),
1026            idx_values_to_absorb: 0,
1027            // ------
1028            // ------
1029            // Used by the interpreter
1030            // Used to allocate variables
1031            // Witness builder related
1032            witness,
1033            // ------
1034            // Inputs
1035            z0: z0.clone(),
1036            zi: z0,
1037        }
1038    }
1039
1040    /// Reset the environment to build the next iteration
1041    pub fn reset_for_next_iteration(&mut self) {
1042        // Rest the state for the next row
1043        self.current_row = 0;
1044        self.state = core::array::from_fn(|_| BigInt::from(0_usize));
1045        self.idx_var = 0;
1046        self.current_instruction = VERIFIER_STARTING_INSTRUCTION;
1047        self.idx_values_to_absorb = 0;
1048    }
1049
1050    /// The blinder used to commit, to avoid committing to the zero polynomial
1051    /// and accumulated in the IVC.
1052    ///
1053    /// It is part of the instance, and it is accumulated in the IVC.
1054    pub fn accumulate_commitment_blinder(&mut self) {
1055        // TODO
1056    }
1057
1058    /// Commit to the program state and updating the environment with the
1059    /// result.
1060    ///
1061    /// This method is supposed to be called after a new iteration of the
1062    /// program has been executed.
1063    pub fn commit_state(&mut self) {
1064        if o1_utils::is_multiple_of(self.current_iteration, 2) {
1065            assert_eq!(
1066                self.current_row as u64,
1067                self.indexed_relation.domain_fp.d1.size,
1068                "The program has not been fully executed. Missing {} rows",
1069                self.indexed_relation.domain_fp.d1.size - self.current_row as u64,
1070            );
1071            // Use program_e1's commit_state method
1072            self.program_e1.commit_state(
1073                &self.indexed_relation.srs_e1,
1074                self.indexed_relation.domain_fp,
1075                &self.witness,
1076            )
1077        } else {
1078            assert_eq!(
1079                self.current_row as u64,
1080                self.indexed_relation.domain_fq.d1.size,
1081                "The program has not been fully executed. Missing {} rows",
1082                self.indexed_relation.domain_fq.d1.size - self.current_row as u64,
1083            );
1084            // Use program_e2's commit_state method
1085            self.program_e2.commit_state(
1086                &self.indexed_relation.srs_e2,
1087                self.indexed_relation.domain_fq,
1088                &self.witness,
1089            )
1090        }
1091    }
1092
1093    /// Absorb the last committed program state in the correct sponge.
1094    ///
1095    /// For a description of the messages to be given to the sponge, including
1096    /// the expected instantiation, refer to the section "Message Passing" in
1097    /// [crate::interpreter].
1098    pub fn absorb_state(&mut self) {
1099        let state = if o1_utils::is_multiple_of(self.current_iteration, 2) {
1100            // Use program_e1's absorb_state method
1101            let state = self
1102                .program_e1
1103                .absorb_state(self.last_program_digest_after_execution.clone());
1104            state.try_into().unwrap()
1105        } else {
1106            // Use program_e2's absorb_state method
1107            let state = self
1108                .program_e2
1109                .absorb_state(self.last_program_digest_after_execution.clone());
1110            state.try_into().unwrap()
1111        };
1112
1113        self.prover_sponge_state = state;
1114    }
1115
1116    /// Compute the output of the application on the previous output
1117    // TODO: we should compute the hash of the previous commitments, only on
1118    // CPU?
1119    pub fn compute_output(&mut self) {
1120        self.zi = BigInt::from(42_usize)
1121    }
1122
1123    pub fn fetch_instruction(&self) -> Instruction {
1124        self.current_instruction
1125    }
1126
1127    /// Simulate an interaction with the verifier by requesting to coin a
1128    /// challenge from the current prover sponge state.
1129    ///
1130    /// This method supposes that all the messages have been sent to the
1131    /// verifier previously, and the attribute [self.prover_sponge_state] has
1132    /// been updated accordingly by absorbing all the messages correctly.
1133    ///
1134    /// The side-effect of this method will be to run a permutation on the
1135    /// sponge state _after_ coining the challenge.
1136    /// There is an hypothesis on the sponge state that the inner permutation
1137    /// has been correctly executed if the absorbtion rate had been reached at
1138    /// the last absorbtion.
1139    ///
1140    /// The challenge will be added to the [self.challenges] attribute at the
1141    /// position given by the challenge `chal`.
1142    ///
1143    /// Internally, the method is implemented by simply loading the prover
1144    /// sponge state, and squeezing a challenge from it, relying on the
1145    /// implementation of the sponge. Usually, the challenge would be the first
1146    /// N bits of the first element, but it is left as an implementation detail
1147    /// of the sponge given by the curve.
1148    pub fn coin_challenge(&mut self, chal: ChallengeTerm) {
1149        let sponge_state_vec: Vec<BigInt> = self.prover_sponge_state.to_vec();
1150
1151        let (verifier_answer, new_state) = if o1_utils::is_multiple_of(self.current_iteration, 2) {
1152            self.program_e1.coin_challenge(sponge_state_vec)
1153        } else {
1154            self.program_e2.coin_challenge(sponge_state_vec)
1155        };
1156
1157        self.challenges[chal] = verifier_answer;
1158        self.prover_sponge_state = new_state.try_into().unwrap();
1159    }
1160
1161    /// Accumulate the program state (or in other words,
1162    /// the witness), by adding the last computed program state into the
1163    /// program state accumulator.
1164    ///
1165    /// This method is supposed to be called after the program state has been
1166    /// committed (by calling [self.commit_state]) and absorbed (by calling
1167    /// [self.absorb_state]). The "relation randomiser" must also have been
1168    /// coined and saved in the environment before, by calling
1169    /// [self.coin_challenge].
1170    ///
1171    /// The program state is accumulated into a different accumulator, depending
1172    /// on the curve currently being used.
1173    ///
1174    /// This is part of the work the prover of the accumulation/folding scheme.
1175    ///
1176    /// This must translate the following equation:
1177    /// ```text
1178    /// acc_(p, n + 1) = acc_(p, n) * chal w
1179    ///               OR
1180    /// acc_(q, n + 1) = acc_(q, n) * chal w
1181    /// ```
1182    /// where acc and w are vectors of the same size.
1183    pub fn accumulate_program_state(&mut self) {
1184        let chal = self.challenges[ChallengeTerm::RelationCombiner].clone();
1185
1186        if o1_utils::is_multiple_of(self.current_iteration, 2) {
1187            self.program_e1
1188                .accumulate_program_state(chal, &self.witness);
1189        } else {
1190            self.program_e2
1191                .accumulate_program_state(chal, &self.witness);
1192        }
1193    }
1194
1195    /// Accumulate the committed state by adding the last committed state into
1196    /// the committed state accumulator.
1197    ///
1198    /// The commitments are accumulated into a different accumulator, depending
1199    /// on the curve currently being used.
1200    ///
1201    /// This is part of the work the prover of the accumulation/folding scheme.
1202    ///
1203    /// This must translate the following equation:
1204    /// ```text
1205    /// C_(p, n + 1) = C_(p, n) + chal * comm
1206    ///               OR
1207    /// C_(q, n + 1) = C_(q, n) + chal * comm
1208    /// ```
1209    ///
1210    /// Note that the committed program state is encoded in
1211    /// [crate::NUMBER_OF_COLUMNS] values, therefore we must iterate over all
1212    /// the columns to accumulate the committed state.
1213    pub fn accumulate_committed_state(&mut self) {
1214        let chal = self.challenges[ChallengeTerm::RelationCombiner].clone();
1215
1216        if o1_utils::is_multiple_of(self.current_iteration, 2) {
1217            self.program_e2.accumulate_committed_state(chal);
1218        } else {
1219            self.program_e1.accumulate_committed_state(chal);
1220        }
1221    }
1222}
arrabbiata/witness.rs

arrabbiata/
witness.rs
