Merge pull request #3073 from o1-labs/dw/use-selectors-in-setup

Arrabbiata: move selectors into setup

Author: dannywillems

arrabbiata/src/column.rs

@@ -1,4 +1,4 @@
-use crate::challenge::ChallengeTerm;
+use crate::{challenge::ChallengeTerm, interpreter::Instruction};
 use kimchi::circuits::expr::{CacheId, ConstantExpr, Expr, FormattedOutput};
 use std::collections::HashMap;
 use strum_macros::{EnumCount as EnumCountMacro, EnumIter};
@@ -14,6 +14,16 @@ use crate::NUMBER_OF_COLUMNS;
 // depend on runtime values (e.g. in a zero-knowledge virtual machine).
 #[derive(Debug, Clone, Copy, PartialEq, EnumCountMacro, EnumIter, Eq, Hash)]
 pub enum Gadget {
+    /// A dummy gadget, doing nothing. Use for padding.
+    NoOp,
+
+    /// The gadget defining the app.
+    ///
+    /// For now, the application is considered to be a one-line computation.
+    /// However, we want to see the application as a collection of reusable
+    /// gadgets.
+    ///
+    /// See `<https://github.com/o1-labs/proof-systems/issues/3074>`
     App,
     // Elliptic curve related gadgets
     EllipticCurveAddition,
@@ -41,6 +51,21 @@ pub enum Gadget {
     PoseidonSpongeAbsorb,
 }
 
+/// Convert an instruction into the corresponding gadget.
+impl From<Instruction> for Gadget {
+    fn from(val: Instruction) -> Gadget {
+        match val {
+            Instruction::NoOp => Gadget::NoOp,
+            Instruction::PoseidonFullRound(starting_round) => {
+                Gadget::PoseidonFullRound(starting_round)
+            }
+            Instruction::PoseidonSpongeAbsorb => Gadget::PoseidonSpongeAbsorb,
+            Instruction::EllipticCurveScaling(_i_comm, _s) => Gadget::EllipticCurveScaling,
+            Instruction::EllipticCurveAddition(_i) => Gadget::EllipticCurveAddition,
+        }
+    }
+}
+
 #[derive(Debug, Clone, Copy, PartialEq)]
 pub enum Column {
     Selector(Gadget),
@@ -74,11 +99,15 @@ pub type E<Fp> = Expr<ConstantExpr<Fp, ChallengeTerm>, Column>;
 impl From<Gadget> for usize {
     fn from(val: Gadget) -> usize {
         match val {
-            Gadget::App => 0,
-            Gadget::EllipticCurveAddition => 1,
-            Gadget::EllipticCurveScaling => 2,
-            Gadget::PoseidonSpongeAbsorb => 3,
-            Gadget::PoseidonFullRound(starting_round) => 4 + starting_round / 5,
+            Gadget::NoOp => 0,
+            Gadget::App => 1,
+            Gadget::EllipticCurveAddition => 2,
+            Gadget::EllipticCurveScaling => 3,
+            Gadget::PoseidonSpongeAbsorb => 4,
+            Gadget::PoseidonFullRound(starting_round) => {
+                assert_eq!(starting_round % 5, 0);
+                5 + starting_round / 5
+            }
         }
     }
 }
@@ -88,6 +117,7 @@ impl FormattedOutput for Column {
     fn latex(&self, _cache: &mut HashMap<CacheId, Self>) -> String {
         match self {
             Column::Selector(sel) => match sel {
+                Gadget::NoOp => "q_noop".to_string(),
                 Gadget::App => "q_app".to_string(),
                 Gadget::EllipticCurveAddition => "q_ec_add".to_string(),
                 Gadget::EllipticCurveScaling => "q_ec_mul".to_string(),
@@ -104,6 +134,7 @@ impl FormattedOutput for Column {
     fn text(&self, _cache: &mut HashMap<CacheId, Self>) -> String {
         match self {
             Column::Selector(sel) => match sel {
+                Gadget::NoOp => "q_noop".to_string(),
                 Gadget::App => "q_app".to_string(),
                 Gadget::EllipticCurveAddition => "q_ec_add".to_string(),
                 Gadget::EllipticCurveScaling => "q_ec_mul".to_string(),

arrabbiata/src/constraint.rs

@@ -28,7 +28,6 @@ where
     pub idx_var: usize,
     pub idx_var_next_row: usize,
     pub constraints: Vec<E<C::ScalarField>>,
-    pub activated_gadget: Option<Gadget>,
 }
 
 impl<C: ArrabbiataCurve> Env<C>
@@ -48,7 +47,6 @@ where
             idx_var: 0,
             idx_var_next_row: 0,
             constraints: Vec::new(),
-            activated_gadget: None,
         }
     }
 }
@@ -100,10 +98,6 @@ where
         res
     }
 
-    fn activate_gadget(&mut self, gadget: Gadget) {
-        self.activated_gadget = Some(gadget);
-    }
-
     fn add_constraint(&mut self, constraint: Self::Variable) {
         let degree = constraint.degree(1, 0);
         debug!("Adding constraint of degree {degree}: {:}", constraint);
@@ -151,7 +145,6 @@ where
         self.idx_var = 0;
         self.idx_var_next_row = 0;
         self.constraints.clear();
-        self.activated_gadget = None;
     }
 
     fn coin_folding_combiner(&mut self, pos: Self::Position) -> Self::Variable {

arrabbiata/src/column_env.rs arrabbiata/src/decider/column_env.rs

@@ -0,0 +1,4 @@
+pub mod column_env;
+pub mod proof;
+pub mod prover;
+pub mod verifier;

arrabbiata/src/decider/mod.rs

@@ -1,6 +1,6 @@
 //! A prover for the folding/accumulation scheme
 
-use crate::{curve::ArrabbiataCurve, proof::Proof};
+use crate::{curve::ArrabbiataCurve, decider::proof::Proof};
 use ark_ff::PrimeField;
 
 use crate::witness::Env;

arrabbiata/src/proof.rs arrabbiata/src/decider/proof.rs

@@ -570,9 +570,7 @@
 //!                       +-----------------------------+
 //! ```
 
-use crate::{
-    column::Gadget, curve::PlonkSpongeConstants, MAXIMUM_FIELD_SIZE_IN_BITS, NUMBER_OF_COLUMNS,
-};
+use crate::{curve::PlonkSpongeConstants, MAXIMUM_FIELD_SIZE_IN_BITS, NUMBER_OF_COLUMNS};
 use ark_ff::{One, Zero};
 use log::debug;
 use mina_poseidon::constants::SpongeConstants;
@@ -621,6 +619,11 @@ pub enum Instruction {
     NoOp,
 }
 
+/// 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 VERIFIER_STARTING_INSTRUCTION: Instruction = Instruction::PoseidonSpongeAbsorb;
+
 /// Define the side of the temporary accumulator.
 /// When computing G1 + G2, the interpreter will load G1 and after that G2.
 /// This enum is used to decide which side fetching into the cells.
@@ -662,9 +665,6 @@ pub trait InterpreterEnv {
     /// Set the value of the variable at the given position for the current row
     fn write_column(&mut self, col: Self::Position, v: Self::Variable) -> Self::Variable;
 
-    /// Activate the gadget for the row.
-    fn activate_gadget(&mut self, gadget: Gadget);
-
     /// Build the constant zero
     fn zero(&self) -> Self::Variable;
 
@@ -874,7 +874,6 @@ pub fn run_ivc<E: InterpreterEnv>(env: &mut E, instr: Instruction) {
             assert!(processing_bit < MAXIMUM_FIELD_SIZE_IN_BITS, "Invalid bit index. The fields are maximum on {MAXIMUM_FIELD_SIZE_IN_BITS} bits, therefore we cannot process the bit {processing_bit}");
             assert!(i_comm < NUMBER_OF_COLUMNS, "Invalid index. We do only support the scaling of the commitments to the columns, for now. We must additionally support the scaling of cross-terms and error terms");
             debug!("Processing scaling of commitment {i_comm}, bit {processing_bit}");
-            env.activate_gadget(Gadget::EllipticCurveScaling);
             // When processing the first bit, we must load the scalar, and it
             // comes from previous computation.
             // The two first columns are supposed to be used for the output.
@@ -1018,7 +1017,6 @@ pub fn run_ivc<E: InterpreterEnv>(env: &mut E, instr: Instruction) {
             };
         }
         Instruction::EllipticCurveAddition(i_comm) => {
-            env.activate_gadget(Gadget::EllipticCurveAddition);
             assert!(i_comm < NUMBER_OF_COLUMNS, "Invalid index. We do only support the addition of the commitments to the columns, for now. We must additionally support the scaling of cross-terms and error terms");
             let (x1, y1) = {
                 let x1 = env.allocate();
@@ -1075,8 +1073,6 @@ pub fn run_ivc<E: InterpreterEnv>(env: &mut E, instr: Instruction) {
                 starting_round + 5
             );
 
-            env.activate_gadget(Gadget::PoseidonFullRound(starting_round));
-
             let round_input_positions: Vec<E::Position> = (0..PlonkSpongeConstants::SPONGE_WIDTH)
                 .map(|_i| env.allocate())
                 .collect();
@@ -1146,8 +1142,6 @@ pub fn run_ivc<E: InterpreterEnv>(env: &mut E, instr: Instruction) {
             });
         }
         Instruction::PoseidonSpongeAbsorb => {
-            env.activate_gadget(Gadget::PoseidonSpongeAbsorb);
-
             let round_input_positions: Vec<E::Position> = (0..PlonkSpongeConstants::SPONGE_WIDTH
                 - 1)
                 .map(|_i| env.allocate())
@@ -1186,3 +1180,50 @@ pub fn run_ivc<E: InterpreterEnv>(env: &mut E, instr: Instruction) {
     // Compute the hash of the public input
     // FIXME: add the verification key. We should have a hash of it.
 }
+
+/// Describe the control-flow for the verifier circuit.
+pub fn fetch_next_instruction(current_instruction: Instruction) -> Instruction {
+    match current_instruction {
+        Instruction::PoseidonFullRound(i) => {
+            if i < PlonkSpongeConstants::PERM_ROUNDS_FULL - 5 {
+                Instruction::PoseidonFullRound(i + 5)
+            } else {
+                // FIXME: for now, we continue absorbing because the current
+                // code, while fetching the values to absorb, raises an
+                // exception when we absorbed everythimg, and the main file
+                // handles the halt by filling as many rows as expected (see
+                // [VERIFIER_CIRCUIT_SIZE]).
+                Instruction::PoseidonSpongeAbsorb
+            }
+        }
+        Instruction::PoseidonSpongeAbsorb => {
+            // Whenever we absorbed a value, we run the permutation.
+            Instruction::PoseidonFullRound(0)
+        }
+        Instruction::EllipticCurveScaling(i_comm, bit) => {
+            // TODO: we still need to substract (or not?) the blinder.
+            // Maybe we can avoid this by aggregating them.
+            // TODO: we also need to aggregate the cross-terms.
+            // Therefore i_comm must also take into the account the number
+            // of cross-terms.
+            assert!(i_comm < NUMBER_OF_COLUMNS, "Maximum number of columns reached ({NUMBER_OF_COLUMNS}), increase the number of columns");
+            assert!(bit < MAXIMUM_FIELD_SIZE_IN_BITS, "Maximum number of bits reached ({MAXIMUM_FIELD_SIZE_IN_BITS}), increase the number of bits");
+            if bit < MAXIMUM_FIELD_SIZE_IN_BITS - 1 {
+                Instruction::EllipticCurveScaling(i_comm, bit + 1)
+            } else if i_comm < NUMBER_OF_COLUMNS - 1 {
+                Instruction::EllipticCurveScaling(i_comm + 1, 0)
+            } else {
+                // We have computed all the bits for all the columns
+                Instruction::NoOp
+            }
+        }
+        Instruction::EllipticCurveAddition(i_comm) => {
+            if i_comm < NUMBER_OF_COLUMNS - 1 {
+                Instruction::EllipticCurveAddition(i_comm + 1)
+            } else {
+                Instruction::NoOp
+            }
+        }
+        Instruction::NoOp => Instruction::NoOp,
+    }
+}

arrabbiata/src/prover.rs arrabbiata/src/decider/prover.rs

@@ -5,26 +5,25 @@ use strum::EnumCount as _;
 pub mod challenge;
 pub mod cli;
 pub mod column;
-pub mod column_env;
 pub mod constraint;
 pub mod curve;
+
+/// The final decider, i.e. the SNARK used on the accumulation scheme.
+pub mod decider;
+
 pub mod interpreter;
 pub mod logup;
 pub mod poseidon_3_60_0_5_5_fp;
 pub mod poseidon_3_60_0_5_5_fq;
-pub mod proof;
-pub mod prover;
 pub mod setup;
-pub mod verifier;
 pub mod witness;
 
 /// The maximum degree of the polynomial that can be represented by the
 /// polynomial-time function the library supports.
 pub const MAX_DEGREE: usize = 5;
 
 /// The minimum SRS size required to use Nova, in base 2.
-/// Requiring at least 2^16 to perform 16bits range checks.
-pub const MIN_SRS_LOG2_SIZE: usize = 16;
+pub const MIN_SRS_LOG2_SIZE: usize = 8;
 
 /// The maximum number of columns that can be used in the circuit.
 pub const NUMBER_OF_COLUMNS: usize = 15;
@@ -58,8 +57,8 @@ pub const MAXIMUM_FIELD_SIZE_IN_BITS: u64 = 255;
 /// verifier circuit.
 pub const NUMBER_OF_VALUES_TO_ABSORB_PUBLIC_IO: usize = NUMBER_OF_COLUMNS * 2;
 
-/// The number of selectors used in the circuit.
-pub const NUMBER_OF_SELECTORS: usize =
+/// The number of gadgets supported by the program
+pub const NUMBER_OF_GADGETS: usize =
     column::Gadget::COUNT + (PlonkSpongeConstants::PERM_ROUNDS_FULL / 5);
 
 /// The arity of the multivariate polynomials describing the constraints.

arrabbiata/src/verifier.rs arrabbiata/src/decider/verifier.rs

@@ -36,20 +36,19 @@ pub fn execute(args: cli::ExecuteArgs) {
     // FIXME: correctly setup
     let indexed_relation = IndexedRelation::new(srs_log2_size);
 
-    let domain_size = 1 << srs_log2_size;
-
     let mut env = witness::Env::<Fp, Fq, Vesta, Pallas>::new(BigInt::from(1u64), indexed_relation);
 
-    let n_iteration_per_fold = domain_size - VERIFIER_CIRCUIT_SIZE;
-
     while env.current_iteration < n_iteration {
         let start_iteration = Instant::now();
 
         info!("Run iteration: {}/{}", env.current_iteration, n_iteration);
 
         // Build the application circuit
-        info!("Running {n_iteration_per_fold} iterations of the application circuit");
-        for _i in 0..n_iteration_per_fold {
+        info!(
+            "Running {} iterations of the application circuit",
+            env.indexed_relation.app_size
+        );
+        for _i in 0..env.indexed_relation.app_size {
             interpreter::run_app(&mut env);
             env.reset();
         }
@@ -63,13 +62,15 @@ pub fn execute(args: cli::ExecuteArgs) {
         // Poseidon hash, and we write on the next row. We don't want to execute
         // a new instruction for the verifier circuit here.
         for i in 0..VERIFIER_CIRCUIT_SIZE - 1 {
-            let instr = env.fetch_instruction();
+            let current_instr = env.fetch_instruction();
             debug!(
                 "Running verifier row {} (instruction = {:?}, witness row = {})",
-                i, instr, env.current_row
+                i,
+                current_instr.clone(),
+                env.current_row
             );
-            interpreter::run_ivc(&mut env, instr);
-            env.current_instruction = env.fetch_next_instruction();
+            interpreter::run_ivc(&mut env, current_instr);
+            env.current_instruction = interpreter::fetch_next_instruction(current_instr);
             env.reset();
         }
         // FIXME: additional row for the Poseidon hash