Arrabbiata: clarify naming convention + absorb program state

arrabbiata/src/main.rs

@@ -106,7 +106,7 @@ pub fn main() {
         // env.next_commitments)
         // update next instance with current commitments
         // FIXME: Check twice the updated commitments
-        env.compute_and_update_previous_commitments();
+        env.commit_state();
 
         // FIXME:
         // Absorb all commitments in the sponge.

arrabbiata/src/witness.rs

@@ -19,18 +19,31 @@ use crate::{
     NUMBER_OF_VALUES_TO_ABSORB_PUBLIC_IO,
 };
 
-/// The first instruction in the IVC is the Poseidon permutation. It is used to
-/// start hashing the public input.
+/// The first instruction in the verifier circuit (often shortened in "IVC" in
+/// the crate) is the Poseidon permutation. It is used to start hashing the
+/// public input.
 pub const IVC_STARTING_INSTRUCTION: Instruction = Instruction::Poseidon(0);
 
-/// An environment that can be shared between IVC instances.
+/// An environment is used to contain the state of a long "running program".
 ///
-/// It contains all the accumulators that can be picked for a given fold
-/// instance k, including the sponges.
+/// The running program is composed of two parts: one user application and one
+/// verifier application. The verifier application is used to encode the
+/// correctness of previous program states computations.
+///
+/// The term "app(lication) state" will be used to refer to the state of the
+/// user application, and the term "IVC state" will be used to refer to the
+/// state of the verifier application. The term state will be used to refer to
+/// the state of the whole program.
+///
+/// The environment contains all the accumulators that can be picked for a given
+/// fold instance k, including the sponges.
 ///
 /// The environment is run over big integers to avoid performing
 /// reduction at all step. Instead the user implementing the interpreter can
 /// reduce in the corresponding field when they want.
+///
+/// The environment is generic over two curves (called E1 and E2) that are
+/// supposed to form a cycle.
 pub struct Env<
     Fp: PrimeField,
     Fq: PrimeField,
@@ -61,9 +74,9 @@ pub struct Env<
     // FIXME: use a blinded comm and also fold the blinder
     pub ivc_accumulator_e2: Vec<PolyComm<E2>>,
 
-    /// Commitments to the previous instances
-    pub previous_commitments_e1: Vec<PolyComm<E1>>,
-    pub previous_commitments_e2: Vec<PolyComm<E2>>,
+    /// Commitments to the previous program states.
+    pub previous_committed_state_e1: Vec<PolyComm<E1>>,
+    pub previous_committed_state_e2: Vec<PolyComm<E2>>,
     // ----------------
 
     // ----------------
@@ -498,7 +511,7 @@ where
                     if self.current_iteration % 2 == 0 {
                         match side {
                             Side::Left => {
-                                let pt = self.previous_commitments_e2[i_comm].get_first_chunk();
+                                let pt = self.previous_committed_state_e2[i_comm].get_first_chunk();
                                 // We suppose we never have a commitment equals to the
                                 // point at infinity
                                 let (pt_x, pt_y) = pt.to_coordinates().unwrap();
@@ -524,7 +537,7 @@ where
                     } else {
                         match side {
                             Side::Left => {
-                                let pt = self.previous_commitments_e1[i_comm].get_first_chunk();
+                                let pt = self.previous_committed_state_e1[i_comm].get_first_chunk();
                                 // We suppose we never have a commitment equals to the
                                 // point at infinity
                                 let (pt_x, pt_y) = pt.to_coordinates().unwrap();
@@ -568,11 +581,11 @@ where
                     }
                     Side::Right => {
                         if self.current_iteration % 2 == 0 {
-                            let pt = self.previous_commitments_e2[i_comm].get_first_chunk();
+                            let pt = self.previous_committed_state_e2[i_comm].get_first_chunk();
                             let (x, y) = pt.to_coordinates().unwrap();
                             (x.to_biguint().into(), y.to_biguint().into())
                         } else {
-                            let pt = self.previous_commitments_e1[i_comm].get_first_chunk();
+                            let pt = self.previous_committed_state_e1[i_comm].get_first_chunk();
                             let (x, y) = pt.to_coordinates().unwrap();
                             (x.to_biguint().into(), y.to_biguint().into())
                         }
@@ -822,10 +835,10 @@ impl<
         };
 
         // Default set to the blinders. Using double to make the EC scaling happy.
-        let previous_commitments_e1: Vec<PolyComm<E1>> = (0..NUMBER_OF_COLUMNS)
+        let previous_committed_state_e1: Vec<PolyComm<E1>> = (0..NUMBER_OF_COLUMNS)
             .map(|_| PolyComm::new(vec![(srs_e1.h + srs_e1.h).into()]))
             .collect();
-        let previous_commitments_e2: Vec<PolyComm<E2>> = (0..NUMBER_OF_COLUMNS)
+        let previous_committed_state_e2: Vec<PolyComm<E2>> = (0..NUMBER_OF_COLUMNS)
             .map(|_| PolyComm::new(vec![(srs_e2.h + srs_e2.h).into()]))
             .collect();
         // FIXME: zero will not work.
@@ -851,8 +864,8 @@ impl<
             // IVC only
             ivc_accumulator_e1,
             ivc_accumulator_e2,
-            previous_commitments_e1,
-            previous_commitments_e2,
+            previous_committed_state_e1,
+            previous_committed_state_e2,
             // ------
             // ------
             idx_var: 0,
@@ -909,11 +922,19 @@ impl<
         // TODO
     }
 
-    /// Compute the commitments to the current witness, and update the previous
-    /// instances.
-    // Might be worth renaming this function
-    pub fn compute_and_update_previous_commitments(&mut self) {
+    /// 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) {
         if self.current_iteration % 2 == 0 {
+            assert_eq!(
+                self.current_row as u64,
+                self.domain_fp.d1.size,
+                "The program has not been fully executed. Missing {} rows",
+                self.domain_fp.d1.size - self.current_row as u64,
+            );
             let comms: Vec<PolyComm<E1>> = self
                 .witness
                 .par_iter()
@@ -927,8 +948,14 @@ impl<
                         .commit_evaluations_non_hiding(self.domain_fp.d1, &evals)
                 })
                 .collect();
-            self.previous_commitments_e1 = comms
+            self.previous_committed_state_e1 = comms
         } else {
+            assert_eq!(
+                self.current_row as u64,
+                self.domain_fq.d1.size,
+                "The program has not been fully executed. Missing {} rows",
+                self.domain_fq.d1.size - self.current_row as u64,
+            );
             let comms: Vec<PolyComm<E2>> = self
                 .witness
                 .iter()
@@ -942,7 +969,7 @@ impl<
                         .commit_evaluations_non_hiding(self.domain_fq.d1, &evals)
                 })
                 .collect();
-            self.previous_commitments_e2 = comms
+            self.previous_committed_state_e2 = comms
         }
     }
 

arrabbiata/tests/witness.rs

@@ -79,7 +79,7 @@ fn test_unit_witness_elliptic_curve_addition() {
     assert_eq!(env.current_iteration, 0);
     let (exp_x3, exp_y3) = {
         let res: Pallas = (env.ivc_accumulator_e2[0].get_first_chunk()
-            + env.previous_commitments_e2[0].get_first_chunk())
+            + env.previous_committed_state_e2[0].get_first_chunk())
         .into();
         let (x3, y3) = res.to_coordinates().unwrap();
         (
@@ -99,7 +99,7 @@ fn test_unit_witness_elliptic_curve_addition() {
     assert_eq!(env.current_iteration, 1);
     let (exp_x3, exp_y3) = {
         let res: Vesta = (env.ivc_accumulator_e1[0].get_first_chunk()
-            + env.previous_commitments_e1[0].get_first_chunk())
+            + env.previous_committed_state_e1[0].get_first_chunk())
         .into();
         let (x3, y3) = res.to_coordinates().unwrap();
         (
@@ -119,7 +119,7 @@ fn test_unit_witness_elliptic_curve_addition() {
     assert_eq!(env.current_iteration, 2);
     let (exp_x3, exp_y3) = {
         let res: Pallas = (env.ivc_accumulator_e2[0].get_first_chunk()
-            + env.previous_commitments_e2[0].get_first_chunk())
+            + env.previous_committed_state_e2[0].get_first_chunk())
         .into();
         let (x3, y3) = res.to_coordinates().unwrap();
         (
@@ -188,7 +188,7 @@ where
         let x = Fq::rand(rng);
         Pallas::generator().mul_bigint(x.into_bigint()).into()
     };
-    env.previous_commitments_e2[0] = PolyComm::new(vec![p1]);
+    env.previous_committed_state_e2[0] = PolyComm::new(vec![p1]);
 
     // We only go up to the maximum bit field size.
     (0..MAXIMUM_FIELD_SIZE_IN_BITS).for_each(|bit_idx| {