Merge pull request #3075 from o1-labs/arrabbiata/use-program-structure-in-env

Arrabbiata: introduce the structure Program

Author: dannywillems

arrabbiata/src/witness.rs

@@ -1,13 +1,13 @@
 use ark_ec::CurveConfig;
 use ark_ff::PrimeField;
 use ark_poly::Evaluations;
-use kimchi::circuits::gate::CurrOrNext;
+use kimchi::circuits::{domains::EvaluationDomains, gate::CurrOrNext};
 use log::debug;
 use mina_poseidon::constants::SpongeConstants;
 use num_bigint::{BigInt, BigUint};
 use num_integer::Integer;
 use o1_utils::field_helpers::FieldHelpers;
-use poly_commitment::{commitment::CommitmentCurve, PolyComm, SRS as _};
+use poly_commitment::{commitment::CommitmentCurve, ipa::SRS, PolyComm, SRS as _};
 use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
 
 use crate::{
@@ -18,6 +18,242 @@ use crate::{
     setup, NUMBER_OF_COLUMNS, NUMBER_OF_VALUES_TO_ABSORB_PUBLIC_IO,
 };
 
+/// A running program that the (folding) interpreter has access to.
+pub struct Program<
+    Fp: PrimeField,
+    Fq: PrimeField,
+    E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>,
+> where
+    E1::BaseField: PrimeField,
+    <<E1 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
+{
+    /// Commitments to the accumulated program state.
+    ///
+    /// In Nova language, this is the commitment to the witness accumulator.
+    pub accumulated_committed_state: Vec<PolyComm<E1>>,
+
+    /// Commitments to the previous program states.
+    ///
+    /// In Nova language, this is the commitment to the previous witness.
+    pub previous_committed_state: Vec<PolyComm<E1>>,
+
+    /// Accumulated witness for the program state.
+    ///
+    /// In Nova language, this is the accumulated witness W.
+    ///
+    /// The size of the outer vector must be equal to the number of columns in
+    /// the circuit.
+    /// The size of the inner vector must be equal to the number of rows in
+    /// the circuit.
+    pub accumulated_program_state: Vec<Vec<E1::ScalarField>>,
+
+    /// List of the accumulated challenges over time.
+    pub accumulated_challenges: Challenges<BigInt>,
+
+    /// Challenges during the last computation.
+    /// This field is useful to keep track of the challenges that must be
+    /// verified in circuit.
+    pub previous_challenges: Challenges<BigInt>,
+}
+
+impl<Fp: PrimeField, Fq: PrimeField, E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>>
+    Program<Fp, Fq, E1>
+where
+    E1::BaseField: PrimeField,
+    <<E1 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
+{
+    pub fn new(srs_size: usize, blinder: E1) -> Self {
+        // Default set to the blinders. Using double to make the EC scaling happy.
+        let previous_committed_state: Vec<PolyComm<E1>> = (0..NUMBER_OF_COLUMNS)
+            .map(|_| PolyComm::new(vec![(blinder + blinder).into()]))
+            .collect();
+
+        // FIXME: zero will not work.
+        let accumulated_committed_state: Vec<PolyComm<E1>> = (0..NUMBER_OF_COLUMNS)
+            .map(|_| PolyComm::new(vec![blinder]))
+            .collect();
+
+        let mut accumulated_program_state: Vec<Vec<E1::ScalarField>> =
+            Vec::with_capacity(NUMBER_OF_COLUMNS);
+        {
+            let mut vec: Vec<E1::ScalarField> = Vec::with_capacity(srs_size);
+            (0..srs_size).for_each(|_| vec.push(E1::ScalarField::zero()));
+            (0..NUMBER_OF_COLUMNS).for_each(|_| accumulated_program_state.push(vec.clone()));
+        };
+
+        let accumulated_challenges: Challenges<BigInt> = Challenges::default();
+
+        let previous_challenges: Challenges<BigInt> = Challenges::default();
+
+        Self {
+            accumulated_committed_state,
+            previous_committed_state,
+            accumulated_program_state,
+            accumulated_challenges,
+            previous_challenges,
+        }
+    }
+
+    /// Commit to the program state and updating the environment with the
+    /// result.
+    ///
+    /// This method is supposed to be called after a new iteration of the
+    /// program has been executed.
+    pub fn commit_state(
+        &mut self,
+        srs: &SRS<E1>,
+        domain: EvaluationDomains<E1::ScalarField>,
+        witness: Vec<Vec<BigInt>>,
+    ) {
+        let comms: Vec<PolyComm<E1>> = witness
+            .par_iter()
+            .map(|evals| {
+                let evals: Vec<E1::ScalarField> = evals
+                    .par_iter()
+                    .map(|x| E1::ScalarField::from_biguint(&x.to_biguint().unwrap()).unwrap())
+                    .collect();
+                let evals = Evaluations::from_vec_and_domain(evals.to_vec(), domain.d1);
+                srs.commit_evaluations_non_hiding(domain.d1, &evals)
+            })
+            .collect();
+        self.previous_committed_state = comms
+    }
+
+    /// Absorb the last committed program state in the correct sponge.
+    ///
+    /// For a description of the messages to be given to the sponge, including
+    /// the expected instantiation, refer to the section "Message Passing" in
+    /// [crate::interpreter].
+    pub fn absorb_state(&mut self, digest: BigInt) -> Vec<BigInt> {
+        let mut sponge = E1::create_new_sponge();
+        let previous_state: E1::BaseField =
+            E1::BaseField::from_biguint(&digest.to_biguint().unwrap()).unwrap();
+        E1::absorb_fq(&mut sponge, previous_state);
+        self.previous_committed_state
+            .iter()
+            .for_each(|comm| E1::absorb_curve_points(&mut sponge, &comm.chunks));
+        let state: Vec<BigInt> = sponge
+            .sponge
+            .state
+            .iter()
+            .map(|x| x.to_biguint().into())
+            .collect();
+        state
+    }
+
+    /// Simulate an interaction with the verifier by requesting to coin a
+    /// challenge from the current prover sponge state.
+    ///
+    /// This method supposes that all the messages have been sent to the
+    /// verifier previously, and the attribute [self.prover_sponge_state] has
+    /// been updated accordingly by absorbing all the messages correctly.
+    ///
+    /// The side-effect of this method will be to run a permutation on the
+    /// sponge state _after_ coining the challenge.
+    /// There is an hypothesis on the sponge state that the inner permutation
+    /// has been correctly executed if the absorbtion rate had been reached at
+    /// the last absorbtion.
+    ///
+    /// The challenge will be added to the [self.challenges] attribute at the
+    /// position given by the challenge `chal`.
+    ///
+    /// Internally, the method is implemented by simply loading the prover
+    /// sponge state, and squeezing a challenge from it, relying on the
+    /// implementation of the sponge. Usually, the challenge would be the first
+    /// N bits of the first element, but it is left as an implementation detail
+    /// of the sponge given by the curve.
+    pub fn coin_challenge(&self, sponge_state: Vec<BigInt>) -> (BigInt, Vec<BigInt>) {
+        let mut sponge = E1::create_new_sponge();
+        sponge_state.iter().for_each(|x| {
+            E1::absorb_fq(
+                &mut sponge,
+                E1::BaseField::from_biguint(&x.to_biguint().unwrap()).unwrap(),
+            )
+        });
+        let verifier_answer = E1::squeeze_challenge(&mut sponge).to_biguint().into();
+        sponge.sponge.poseidon_block_cipher();
+        let state: Vec<BigInt> = sponge
+            .sponge
+            .state
+            .iter()
+            .map(|x| x.to_biguint().into())
+            .collect();
+        (verifier_answer, state)
+    }
+
+    /// Accumulate the program state (or in other words,
+    /// the witness), by adding the last computed program state into the
+    /// program state accumulator.
+    ///
+    /// This method is supposed to be called after the program state has been
+    /// committed (by calling [self.commit_state]) and absorbed (by calling
+    /// [self.absorb_state]). The "relation randomiser" must also have been
+    /// coined and saved in the environment before, by calling
+    /// [self.coin_challenge].
+    ///
+    /// The program state is accumulated into a different accumulator, depending
+    /// on the curve currently being used.
+    ///
+    /// This is part of the work the prover of the accumulation/folding scheme.
+    ///
+    /// This must translate the following equation:
+    /// ```text
+    /// acc_(p, n + 1) = acc_(p, n) * chal w
+    ///               OR
+    /// acc_(q, n + 1) = acc_(q, n) * chal w
+    /// ```
+    /// where acc and w are vectors of the same size.
+    pub fn accumulate_program_state(&mut self, chal: BigInt, witness: Vec<Vec<BigInt>>) {
+        let modulus: BigInt = E1::ScalarField::modulus_biguint().into();
+        self.accumulated_program_state = self
+            .accumulated_program_state
+            .iter()
+            .zip(witness.iter()) // This iterate over the columns
+            .map(|(evals_accumulator, evals_witness)| {
+                evals_accumulator
+                    .iter()
+                    .zip(evals_witness.iter()) // This iterate over the rows
+                    .map(|(acc, w)| {
+                        let rhs: BigInt = (chal.clone() * w).mod_floor(&modulus);
+                        let rhs: BigUint = rhs.to_biguint().unwrap();
+                        let res = E1::ScalarField::from_biguint(&rhs).unwrap();
+                        *acc + res
+                    })
+                    .collect()
+            })
+            .collect();
+    }
+
+    /// Accumulate the committed state by adding the last committed state into
+    /// the committed state accumulator.
+    ///
+    /// The commitments are accumulated into a different accumulator, depending
+    /// on the curve currently being used.
+    ///
+    /// This is part of the work the prover of the accumulation/folding scheme.
+    ///
+    /// This must translate the following equation:
+    /// ```text
+    /// C_(p, n + 1) = C_(p, n) + chal * comm
+    ///               OR
+    /// C_(q, n + 1) = C_(q, n) + chal * comm
+    /// ```
+    ///
+    /// Note that the committed program state is encoded in
+    /// [crate::NUMBER_OF_COLUMNS] values, therefore we must iterate over all
+    /// the columns to accumulate the committed state.
+    pub fn accumulate_committed_state(&mut self, chal: BigInt) {
+        let chal: BigUint = chal.to_biguint().unwrap();
+        let chal: E1::ScalarField = E1::ScalarField::from_biguint(&chal).unwrap();
+        self.accumulated_committed_state = self
+            .accumulated_committed_state
+            .iter()
+            .zip(self.previous_committed_state.iter())
+            .map(|(l, r)| l + &r.scale(chal))
+            .collect();
+    }
+}
+
 /// An environment is used to contain the state of a long "running program".
 ///
 /// The running program is composed of two parts: one user application and one
@@ -214,11 +450,6 @@ pub struct Env<
     // ---------------
 }
 
-// The condition on the parameters for E1 and E2 is to get the coefficients and
-// convert them into biguint.
-// The condition SWModelParameters is to get the parameters of the curve as
-// biguint to use them to compute the slope in the elliptic curve addition
-// algorithm.
 impl<
         Fp: PrimeField,
         Fq: PrimeField,