feat(Recursion): evaluate constraints in a single expression (#592)

core/src/stark/folder.rs

@@ -125,11 +125,17 @@ impl<'a, SC: StarkGenericConfig> AirBuilderWithPublicValues for ProverConstraint
     }
 }
 
-pub type VerifierConstraintFolder<'a, SC> =
-    GenericVerifierConstraintFolder<'a, Val<SC>, Challenge<SC>, Challenge<SC>, Challenge<SC>>;
+pub type VerifierConstraintFolder<'a, SC> = GenericVerifierConstraintFolder<
+    'a,
+    Val<SC>,
+    Challenge<SC>,
+    Val<SC>,
+    Challenge<SC>,
+    Challenge<SC>,
+>;
 
 /// A folder for verifier constraints.
-pub struct GenericVerifierConstraintFolder<'a, F, EF, Var, Expr> {
+pub struct GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr> {
     pub preprocessed: VerticalPair<RowMajorMatrixView<'a, Var>, RowMajorMatrixView<'a, Var>>,
     pub main: VerticalPair<RowMajorMatrixView<'a, Var>, RowMajorMatrixView<'a, Var>>,
     pub perm: VerticalPair<RowMajorMatrixView<'a, Var>, RowMajorMatrixView<'a, Var>>,
@@ -140,11 +146,12 @@ pub struct GenericVerifierConstraintFolder<'a, F, EF, Var, Expr> {
     pub is_transition: Var,
     pub alpha: Var,
     pub accumulator: Expr,
-    pub public_values: &'a [F],
+    pub public_values: &'a [PubVar],
     pub _marker: PhantomData<(F, EF)>,
 }
 
-impl<'a, F, EF, Var, Expr> AirBuilder for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
+impl<'a, F, EF, PubVar, Var, Expr> AirBuilder
+    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
 where
     F: Field,
     EF: ExtensionField<F>,
@@ -170,6 +177,7 @@ where
         + Mul<Expr, Output = Expr>
         + Send
         + Sync,
+    PubVar: Into<Expr> + Copy,
 {
     type F = F;
     type Expr = Expr;
@@ -203,8 +211,8 @@ where
     }
 }
 
-impl<'a, F, EF, Var, Expr> ExtensionBuilder
-    for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
+impl<'a, F, EF, PubVar, Var, Expr> ExtensionBuilder
+    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
 where
     F: Field,
     EF: ExtensionField<F>,
@@ -230,6 +238,7 @@ where
         + Mul<Expr, Output = Expr>
         + Send
         + Sync,
+    PubVar: Into<Expr> + Copy,
 {
     type EF = EF;
     type ExprEF = Expr;
@@ -243,8 +252,8 @@ where
     }
 }
 
-impl<'a, F, EF, Var, Expr> PermutationAirBuilder
-    for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
+impl<'a, F, EF, PubVar, Var, Expr> PermutationAirBuilder
+    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
 where
     F: Field,
     EF: ExtensionField<F>,
@@ -270,6 +279,7 @@ where
         + Mul<Expr, Output = Expr>
         + Send
         + Sync,
+    PubVar: Into<Expr> + Copy,
 {
     type MP = VerticalPair<RowMajorMatrixView<'a, Var>, RowMajorMatrixView<'a, Var>>;
     type RandomVar = Var;
@@ -283,8 +293,8 @@ where
     }
 }
 
-impl<'a, F, EF, Var, Expr> MultiTableAirBuilder
-    for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
+impl<'a, F, EF, PubVar, Var, Expr> MultiTableAirBuilder
+    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
 where
     F: Field,
     EF: ExtensionField<F>,
@@ -310,6 +320,7 @@ where
         + Mul<Expr, Output = Expr>
         + Send
         + Sync,
+    PubVar: Into<Expr> + Copy,
 {
     type Sum = Var;
 
@@ -318,7 +329,8 @@ where
     }
 }
 
-impl<'a, F, EF, Var, Expr> PairBuilder for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
+impl<'a, F, EF, PubVar, Var, Expr> PairBuilder
+    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
 where
     F: Field,
     EF: ExtensionField<F>,
@@ -344,14 +356,15 @@ where
         + Mul<Expr, Output = Expr>
         + Send
         + Sync,
+    PubVar: Into<Expr> + Copy,
 {
     fn preprocessed(&self) -> Self::M {
         self.preprocessed
     }
 }
 
-impl<'a, F, EF, Var, Expr> EmptyMessageBuilder
-    for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
+impl<'a, F, EF, PubVar, Var, Expr> EmptyMessageBuilder
+    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
 where
     F: Field,
     EF: ExtensionField<F>,
@@ -377,11 +390,12 @@ where
         + Mul<Expr, Output = Expr>
         + Send
         + Sync,
+    PubVar: Into<Expr> + Copy,
 {
 }
 
-impl<'a, F, EF, Var, Expr> AirBuilderWithPublicValues
-    for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
+impl<'a, F, EF, PubVar, Var, Expr> AirBuilderWithPublicValues
+    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
 where
     F: Field,
     EF: ExtensionField<F>,
@@ -407,8 +421,9 @@ where
         + Mul<Expr, Output = Expr>
         + Send
         + Sync,
+    PubVar: Into<Expr> + Copy,
 {
-    type PublicVar = Self::F;
+    type PublicVar = PubVar;
 
     fn public_values(&self) -> &[Self::PublicVar] {
         self.public_values

recursion/circuit/src/constraints.rs

@@ -13,7 +13,8 @@ use sp1_recursion_compiler::ir::Felt;
 use sp1_recursion_compiler::ir::{Builder, Config, Ext};
 use sp1_recursion_compiler::prelude::SymbolicExt;
 use sp1_recursion_program::commit::PolynomialSpaceVariable;
-use sp1_recursion_program::folder::RecursiveVerifierConstraintFolder;
+
+use sp1_recursion_program::stark::RecursiveVerifierConstraintFolder;
 
 use crate::domain::TwoAdicMultiplicativeCosetVariable;
 use crate::stark::StarkVerifierCircuit;
@@ -57,15 +58,12 @@ where
             next: unflatten(&opening.permutation.next),
         };
 
-        let zero: Ext<SC::Val, SC::Challenge> = builder.eval(SC::Val::zero());
-
         let mut folder_pv = Vec::new();
         for i in 0..PROOF_MAX_NUM_PVS {
             folder_pv.push(builder.get(&public_values, i));
         }
 
-        let mut folder = RecursiveVerifierConstraintFolder {
-            builder,
+        let mut folder = RecursiveVerifierConstraintFolder::<C> {
             preprocessed: opening.preprocessed.view(),
             main: opening.main.view(),
             perm: perm_opening.view(),
@@ -76,11 +74,12 @@ where
             is_last_row: selectors.is_last_row,
             is_transition: selectors.is_transition,
             alpha,
-            accumulator: zero,
+            accumulator: SymbolicExt::zero(),
+            _marker: std::marker::PhantomData,
         };
 
         chip.eval(&mut folder);
-        folder.accumulator
+        builder.eval(folder.accumulator)
     }
 
     fn recompute_quotient(

recursion/circuit/src/stark.rs

@@ -20,7 +20,7 @@ use sp1_recursion_compiler::prelude::SymbolicVar;
 use sp1_recursion_core::stark::config::{outer_fri_config, BabyBearPoseidon2Outer};
 use sp1_recursion_core::stark::RecursionAir;
 use sp1_recursion_program::commit::PolynomialSpaceVariable;
-use sp1_recursion_program::folder::RecursiveVerifierConstraintFolder;
+use sp1_recursion_program::stark::RecursiveVerifierConstraintFolder;
 
 use crate::domain::{new_coset, TwoAdicMultiplicativeCosetVariable};
 use crate::types::TwoAdicPcsMatsVariable;

recursion/compiler/src/asm/code.rs

@@ -46,6 +46,10 @@ impl<F: PrimeField32, EF: ExtensionField<F>> AssemblyCode<F, EF> {
         Self { blocks, labels }
     }
 
+    pub fn size(&self) -> usize {
+        self.blocks.iter().map(|block| block.0.len()).sum()
+    }
+
     /// Convert the assembly code to a program.
     pub fn machine_code(self) -> RecursionProgram<F> {
         let blocks = self.blocks;

recursion/compiler/src/asm/compiler.rs

@@ -596,6 +596,7 @@ impl<F: PrimeField32 + TwoAdicField, EF: ExtensionField<F> + TwoAdicField> AsmCo
 
     pub fn compile(self) -> RecursionProgram<F> {
         let code = self.code();
+        tracing::info!("Program size: {}", code.size());
         code.machine_code()
     }
 

recursion/program/src/constraints.rs

@@ -14,8 +14,8 @@ use sp1_recursion_compiler::prelude::ExtConst;
 use sp1_recursion_compiler::prelude::{Builder, Ext, SymbolicExt};
 
 use crate::commit::PolynomialSpaceVariable;
-use crate::folder::RecursiveVerifierConstraintFolder;
 use crate::fri::TwoAdicMultiplicativeCosetVariable;
+use crate::stark::RecursiveVerifierConstraintFolder;
 use crate::stark::StarkVerifier;
 use crate::types::ChipOpenedValuesVariable;
 use crate::types::ChipOpening;
@@ -55,15 +55,14 @@ where
             next: unflatten(&opening.permutation.next),
         };
 
-        let zero: Ext<SC::Val, SC::Challenge> = builder.eval(SC::Val::zero());
+        // let zero: Ext<SC::Val, SC::Challenge> = builder.eval(SC::Val::zero());
 
         let mut folder_pv = Vec::new();
         for i in 0..PROOF_MAX_NUM_PVS {
             folder_pv.push(builder.get(&public_values, i));
         }
 
-        let mut folder = RecursiveVerifierConstraintFolder {
-            builder,
+        let mut folder = RecursiveVerifierConstraintFolder::<C> {
             preprocessed: opening.preprocessed.view(),
             main: opening.main.view(),
             perm: perm_opening.view(),
@@ -74,11 +73,12 @@ where
             is_last_row: selectors.is_last_row,
             is_transition: selectors.is_transition,
             alpha,
-            accumulator: zero,
+            accumulator: SymbolicExt::zero(),
+            _marker: std::marker::PhantomData,
         };
 
         chip.eval(&mut folder);
-        folder.accumulator
+        builder.eval(folder.accumulator)
     }
 
     fn recompute_quotient(

recursion/program/src/lib.rs

@@ -6,7 +6,6 @@
 pub mod challenger;
 pub mod commit;
 pub mod constraints;
-pub mod folder;
 pub mod fri;
 pub mod hints;
 pub mod reduce;