Merge pull request #2652 from o1-labs/o1vm/quotient-polynomial

o1vm/pickles: introduce the computation of the quotient polynomial

o1vm/Cargo.toml

@@ -60,4 +60,5 @@ rand.workspace = true
 libc.workspace = true
 rayon.workspace = true
 sha3.workspace = true
-itertools.workspace = true
+itertools.workspace = true
+thiserror.workspace = true

o1vm/src/pickles/column_env.rs

@@ -71,10 +71,10 @@ impl<'a, F: FftField> TColumnEnvironment<'a, F, BerkeleyChallengeTerm, BerkeleyC
 
     fn get_domain(&self, d: Domain) -> Radix2EvaluationDomain<F> {
         match d {
-            Domain::D1 => self.domain.d1,
-            Domain::D2 => self.domain.d2,
-            Domain::D4 => self.domain.d4,
             Domain::D8 => self.domain.d8,
+            Domain::D1 | Domain::D2 | Domain::D4 => {
+                panic!("Not supposed to be in MIPS. All columns are evaluated on d8")
+            }
         }
     }
 

o1vm/src/pickles/main.rs

@@ -126,13 +126,15 @@ pub fn main() -> ExitCode {
             // FIXME
             let start_iteration = Instant::now();
             debug!("Limit of {DOMAIN_SIZE} reached. We make a proof, verify it (for testing) and start with a new branch new chunk");
-            let _proof: Proof<Vesta> =
+            let _proof: Result<Proof<Vesta>, prover::ProverError> =
                 prover::prove::<
                     Vesta,
                     DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
                     DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
                     _,
                 >(domain_fp, &srs, curr_proof_inputs, &constraints, &mut rng);
+            // FIXME: check that the proof is correct. This is for testing purposes.
+            // Leaving like this for now.
             debug!(
                 "Proof generated in {elapsed} μs",
                 elapsed = start_iteration.elapsed().as_micros()

o1vm/src/pickles/prover.rs

@@ -24,6 +24,14 @@ use super::{
     proof::{Proof, ProofInputs, WitnessColumns},
 };
 use crate::E;
+use thiserror::Error;
+
+/// Errors that can arise when creating a proof
+#[derive(Error, Debug, Clone)]
+pub enum ProverError {
+    #[error("the provided constraint has degree {0} > allowed {1}; expr: {2}")]
+    ConstraintDegreeTooHigh(u64, u64, String),
+}
 
 /// Make a PlonKish proof for the given circuit. As inputs, we get the execution
 /// trace consisting of evaluations of polynomials over a certain domain
@@ -47,9 +55,9 @@ pub fn prove<
     domain: EvaluationDomains<G::ScalarField>,
     srs: &SRS<G>,
     inputs: ProofInputs<G>,
-    _constraints: &[E<G::ScalarField>],
+    constraints: &[E<G::ScalarField>],
     rng: &mut RNG,
-) -> Proof<G>
+) -> Result<Proof<G>, ProverError>
 where
     <G as AffineRepr>::BaseField: PrimeField,
     RNG: RngCore + CryptoRng,
@@ -153,7 +161,7 @@ where
     let alpha: G::ScalarField = fq_sponge.challenge();
 
     let zk_rows = 0;
-    let _column_env: ColumnEnvironment<'_, G::ScalarField> = {
+    let column_env: ColumnEnvironment<'_, G::ScalarField> = {
         // FIXME: use a proper Challenge structure
         let challenges = BerkeleyChallenges {
             alpha,
@@ -176,7 +184,48 @@ where
         }
     };
 
-    // FIXME: add quotient polynomial
+    let quotient_poly: DensePolynomial<G::ScalarField> = {
+        // Compute ∑ α^i constraint_i as an expression
+        let combined_expr =
+            E::combine_constraints(0..(constraints.len() as u32), (constraints).to_vec());
+
+        // We want to compute the quotient polynomial, i.e.
+        // t(X) = (∑ α^i constraint_i(X)) / Z_H(X).
+        // The sum of the expressions is called the "constraint polynomial".
+        // We will use the evaluations points of the individual witness
+        // columns.
+        // Note that as the constraints might be of higher degree than N, the
+        // size of the set H we want the constraints to be verified on, we must
+        // have more than N evaluations points for each columns. This is handled
+        // in the ColumnEnvironment structure.
+        // Reminder: to compute P(X) = P_{1}(X) * P_{2}(X), from the evaluations
+        // of P_{1} and P_{2}, with deg(P_{1}) = deg(P_{2}(X)) = N, we must have
+        // 2N evaluation points to compute P as deg(P(X)) <= 2N.
+        let expr_evaluation: Evaluations<G::ScalarField, D<G::ScalarField>> =
+            combined_expr.evaluations(&column_env);
+
+        // And we interpolate using the evaluations
+        let expr_evaluation_interpolated = expr_evaluation.interpolate();
+
+        let fail_final_q_division = || {
+            panic!("Division by vanishing poly must not fail at this point, we checked it before")
+        };
+        // We compute the polynomial t(X) by dividing the constraints polynomial
+        // by the vanishing polynomial, i.e. Z_H(X).
+        let (quotient, res) = expr_evaluation_interpolated
+            .divide_by_vanishing_poly(domain.d1)
+            .unwrap_or_else(fail_final_q_division);
+        // As the constraints must be verified on H, the rest of the division
+        // must be equal to 0 as the constraints polynomial and Z_H(X) are both
+        // equal on H.
+        if !res.is_zero() {
+            fail_final_q_division();
+        }
+
+        quotient
+    };
+
+    let _t_comm = srs.commit_non_hiding(&quotient_poly, 7);
 
     ////////////////////////////////////////////////////////////////////////////
     // Round 3: Evaluations at ζ and ζω
@@ -272,10 +321,10 @@ where
         rng,
     );
 
-    Proof {
+    Ok(Proof {
         commitments,
         zeta_evaluations,
         zeta_omega_evaluations,
         opening_proof,
-    }
+    })
 }