feat: verify constraints (#409)

core/src/air/extension.rs

@@ -1,4 +1,7 @@
-use p3_field::AbstractField;
+use p3_field::{
+    extension::{BinomialExtensionField, BinomiallyExtendable},
+    AbstractExtensionField, AbstractField,
+};
 use sp1_derive::AlignedBorrow;
 use std::ops::{Add, Mul, Neg, Sub};
 
@@ -8,6 +11,17 @@ const DEGREE: usize = 4;
 #[repr(C)]
 pub struct BinomialExtension<T>(pub [T; DEGREE]);
 
+impl<T> BinomialExtension<T> {
+    pub fn from_base(b: T) -> Self
+    where
+        T: AbstractField,
+    {
+        let mut arr: [T; DEGREE] = core::array::from_fn(|_| T::zero());
+        arr[0] = b;
+        Self(arr)
+    }
+}
+
 impl<T: Add<Output = T> + Clone> Add for BinomialExtension<T> {
     type Output = Self;
 
@@ -62,3 +76,33 @@ impl<T: AbstractField + Copy> Neg for BinomialExtension<T> {
         Self([-self.0[0], -self.0[1], -self.0[2], -self.0[3]])
     }
 }
+
+impl<AF> From<BinomialExtensionField<AF, DEGREE>> for BinomialExtension<AF>
+where
+    AF: AbstractField + Copy,
+    AF::F: BinomiallyExtendable<DEGREE>,
+{
+    fn from(value: BinomialExtensionField<AF, DEGREE>) -> Self {
+        let arr: [AF; DEGREE] = value.as_base_slice().try_into().unwrap();
+        Self(arr)
+    }
+}
+
+impl<AF> From<BinomialExtension<AF>> for BinomialExtensionField<AF, DEGREE>
+where
+    AF: AbstractField + Copy,
+    AF::F: BinomiallyExtendable<DEGREE>,
+{
+    fn from(value: BinomialExtension<AF>) -> Self {
+        BinomialExtensionField::from_base_slice(&value.0)
+    }
+}
+
+impl<T> IntoIterator for BinomialExtension<T> {
+    type Item = T;
+    type IntoIter = core::array::IntoIter<T, DEGREE>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.0.into_iter()
+    }
+}

core/src/stark/verifier.rs

@@ -5,6 +5,7 @@ use itertools::Itertools;
 use p3_air::Air;
 use p3_challenger::CanObserve;
 use p3_challenger::FieldChallenger;
+use p3_commit::LagrangeSelectors;
 use p3_commit::Pcs;
 use p3_commit::PolynomialSpace;
 use p3_field::AbstractExtensionField;
@@ -197,38 +198,31 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
     where
         A: for<'a> Air<VerifierConstraintFolder<'a, SC>>,
     {
-        use p3_field::Field;
         let sels = trace_domain.selectors_at_point(zeta);
 
-        let zps = qc_domains
-            .iter()
-            .enumerate()
-            .map(|(i, domain)| {
-                qc_domains
-                    .iter()
-                    .enumerate()
-                    .filter(|(j, _)| *j != i)
-                    .map(|(_, other_domain)| {
-                        other_domain.zp_at_point(zeta)
-                            * other_domain.zp_at_point(domain.first_point()).inverse()
-                    })
-                    .product::<SC::Challenge>()
-            })
-            .collect_vec();
+        let quotient = Self::recompute_quotient(&opening, &qc_domains, zeta);
+        let folded_constraints =
+            Self::eval_constraints(chip, &opening, &sels, alpha, permutation_challenges);
 
-        let quotient = opening
-            .quotient
-            .iter()
-            .enumerate()
-            .map(|(ch_i, ch)| {
-                assert_eq!(ch.len(), SC::Challenge::D);
-                ch.iter()
-                    .enumerate()
-                    .map(|(e_i, &c)| zps[ch_i] * SC::Challenge::monomial(e_i) * c)
-                    .sum::<SC::Challenge>()
-            })
-            .sum::<SC::Challenge>();
+        // Check that the constraints match the quotient, i.e.
+        //     folded_constraints(zeta) / Z_H(zeta) = quotient(zeta)
+        match folded_constraints * sels.inv_zeroifier == quotient {
+            true => Ok(()),
+            false => Err(OodEvaluationMismatch),
+        }
+    }
 
+    #[cfg(feature = "perf")]
+    pub fn eval_constraints(
+        chip: &MachineChip<SC, A>,
+        opening: &ChipOpenedValues<SC::Challenge>,
+        selectors: &LagrangeSelectors<SC::Challenge>,
+        alpha: SC::Challenge,
+        permutation_challenges: &[SC::Challenge],
+    ) -> SC::Challenge
+    where
+        A: for<'a> Air<VerifierConstraintFolder<'a, SC>>,
+    {
         // Reconstruct the prmutation opening values as extention elements.
         let unflatten = |v: &[SC::Challenge]| {
             v.chunks_exact(SC::Challenge::D)
@@ -253,23 +247,54 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
             perm: perm_opening.view(),
             perm_challenges: permutation_challenges,
             cumulative_sum: opening.cumulative_sum,
-            is_first_row: sels.is_first_row,
-            is_last_row: sels.is_last_row,
-            is_transition: sels.is_transition,
+            is_first_row: selectors.is_first_row,
+            is_last_row: selectors.is_last_row,
+            is_transition: selectors.is_transition,
             alpha,
             accumulator: SC::Challenge::zero(),
             _marker: PhantomData,
         };
         chip.eval(&mut folder);
 
-        let folded_constraints = folder.accumulator;
+        folder.accumulator
+    }
 
-        // Check that the constraints match the quotient, i.e.
-        //     folded_constraints(zeta) / Z_H(zeta) = quotient(zeta)
-        match folded_constraints * sels.inv_zeroifier == quotient {
-            true => Ok(()),
-            false => Err(OodEvaluationMismatch),
-        }
+    #[cfg(feature = "perf")]
+    pub fn recompute_quotient(
+        opening: &ChipOpenedValues<SC::Challenge>,
+        qc_domains: &[Domain<SC>],
+        zeta: SC::Challenge,
+    ) -> SC::Challenge {
+        use p3_field::Field;
+
+        let zps = qc_domains
+            .iter()
+            .enumerate()
+            .map(|(i, domain)| {
+                qc_domains
+                    .iter()
+                    .enumerate()
+                    .filter(|(j, _)| *j != i)
+                    .map(|(_, other_domain)| {
+                        other_domain.zp_at_point(zeta)
+                            * other_domain.zp_at_point(domain.first_point()).inverse()
+                    })
+                    .product::<SC::Challenge>()
+            })
+            .collect_vec();
+
+        opening
+            .quotient
+            .iter()
+            .enumerate()
+            .map(|(ch_i, ch)| {
+                assert_eq!(ch.len(), SC::Challenge::D);
+                ch.iter()
+                    .enumerate()
+                    .map(|(e_i, &c)| zps[ch_i] * SC::Challenge::monomial(e_i) * c)
+                    .sum::<SC::Challenge>()
+            })
+            .sum::<SC::Challenge>()
     }
 }
 

recursion/compiler/Cargo.toml

@@ -19,4 +19,5 @@ serde = { version = "1.0.197", features = ["derive"] }
 
 [dev-dependencies]
 p3-baby-bear = { workspace = true }
+p3-challenger = { workspace = true }
 rand = "0.8.4"

recursion/compiler/examples/fibonacci.rs

@@ -48,7 +48,21 @@ fn main() {
     println!("{}", code);
 
     let program = code.machine_code();
+    println!("Program size = {}", program.instructions.len());
 
     let mut runtime = Runtime::<F, EF>::new(&program);
     runtime.run();
+
+    // let config = SC::new();
+    // let machine = RecursionAir::machine(config);
+    // let (pk, vk) = machine.setup(&program);
+    // let mut challenger = machine.config().challenger();
+
+    // let start = Instant::now();
+    // let proof = machine.prove::<LocalProver<_, _>>(&pk, runtime.record, &mut challenger);
+    // let duration = start.elapsed().as_secs();
+
+    // let mut challenger = machine.config().challenger();
+    // machine.verify(&vk, &proof, &mut challenger).unwrap();
+    // println!("proving duration = {}", duration);
 }