comments

halo2_proofs/src/protostar/accumulator.rs

@@ -42,30 +42,72 @@ pub struct Accumulator<C: CurveAffine> {
 }
 
 impl<C: CurveAffine> Accumulator<C> {
+    /// Given two accumulators, run the folding reduction to produce a new accumulator.
+    /// If both input accumulators are correct, the output accumulator will be correct w.h.p. .
     pub fn fold<E: EncodedChallenge<C>, T: TranscriptWrite<C, E>>(
         pk: &ProvingKey<C>,
         acc0: Self,
         acc1: Self,
         transcript: &mut T,
     ) -> Self {
+        // Create a data structure containing pairs of committed columns, from which we can compute the constraints to be evaluated.
         let paired_data = Paired::<'_, C::Scalar>::new_data(pk, &acc0, &acc1);
 
+        // Get the full constraint polynomial for the gate and lookups
         let full_constraint = paired_data.full_constraint(pk.cs.gates(), pk.cs.lookups());
 
+        /*
+        Compute the error polynomial e(X) = ∑ᵢ βᵢ * Gᵢ(X)
+        NOTE: There are sevaral optimizations that can be performed at this point:
+        The i-th constraint Gᵢ is given by Gᵢ = ∑ⱼ yⱼ⋅ sⱼ,ᵢ⋅ Gⱼ,ᵢ, where
+          - yⱼ is a challenge for keeping all constraints linearly independent.
+          - sⱼ,ᵢ is a selector for the j-th constraint, which is 1 if the j-th constraint Gⱼ,ᵢ is active at row i,
+            and 0 otherwise.
+          - Gⱼ,ᵢ is the the j-th constraint, resulting from partially evaluating an expression Gⱼ in the the fixed
+            columns of row i.
+
+        - For each constraint Gⱼ, we can compute the polynomial eⱼ(X) = ∑ᵢ βᵢ⋅sⱼ,ᵢ⋅Gⱼ,ᵢ(X) indpendently of the other
+          constraints, and sum them at the end to obtain e(X) = ∑ⱼ yⱼ(X)⋅eⱼ(X).
+        - By checking the selectors, we can skip the evaluation of Gⱼ,ᵢ if it is not active at row i.
+        - The variables of the expression Gⱼ only need to be interpolated upto deg(Gⱼ)+1 rather than deg(e),
+          saving some unnecessary evaluations of Gⱼ.
+        - If a constraint G is linear (i.e. Gᵢ = L₀⋅(wᵢ−1) for checking that w₀ == 1, where L₀ is a fixed column)
+          then the error polynomial for this expression will always be 0, so we can skip the evaluation
+        */
         let error_poly = Paired::<'_, C::Scalar>::evaluate_compressed_polynomial(
             full_constraint,
             pk.usable_rows.clone(),
             pk.num_rows,
         );
+        // Sanity checks for ensuring the error polynomial is correct
+        {
+            let error0 = eval_polynomial(&error_poly, C::Scalar::ZERO);
+            let error1 = eval_polynomial(&error_poly, C::Scalar::ONE);
 
+            assert_eq!(error0, acc0.error);
+            assert_eq!(error1, acc1.error);
+        }
+
+        debug_assert_eq!(error_poly.len(), pk.max_folding_constraints_degree() + 1);
+
+        // Send the coefficients of the error polynomial to the verifier in the clear.
         for coef in &error_poly {
             let _ = transcript.write_scalar(*coef);
         }
+        /*
+        Note: The verifier will have to check that e(0) = acc0.error and e(1) = acc1.error.
+        We can instead send the quotient
+                e(X) - (1-t)e(0) - te(1)
+        e'(X) = ------------------------
+                         (1-t)t
+        and let the verifier compute
+        e(α) = (1-α)α⋅e'(α) + (1-α)⋅e₀ + α⋅e₁
+        */
+
+        // Sample ₀₁, a challenge for computing the interpolation of both accumulators.
         let alpha = *transcript.squeeze_challenge_scalar::<C::Scalar>();
-        Self::merge(acc0, acc1, error_poly, alpha)
-    }
+        let error = eval_polynomial(&error_poly, alpha);
 
-    fn merge(acc0: Self, acc1: Self, error_poly: Vec<C::Scalar>, alpha: C::Scalar) -> Self {
         let gate = gate::Transcript::merge(alpha, acc0.gate, acc1.gate);
         let lookups = zip(acc0.lookups.into_iter(), acc1.lookups.into_iter())
             .map(|(lookup0, lookup1)| lookup::Transcript::merge(alpha, lookup0, lookup1))
@@ -76,14 +118,6 @@ impl<C: CurveAffine> Accumulator<C> {
             .map(|(y0, y1)| y0 + alpha * (y1 - y0))
             .collect();
 
-        let error = eval_polynomial(&error_poly, alpha);
-
-        let error0 = eval_polynomial(&error_poly, C::Scalar::ZERO);
-        let error1 = eval_polynomial(&error_poly, C::Scalar::ONE);
-
-        assert_eq!(error0, acc0.error);
-        assert_eq!(error1, acc1.error);
-
         Self {
             gate,
             lookups,
@@ -93,6 +127,12 @@ impl<C: CurveAffine> Accumulator<C> {
         }
     }
 
+    /// Checks whether the accumulator is valid with regards to the proving key.
+    /// - Check all commitments are correct
+    /// - Check the error term is correct
+    /// - Verify the linear lookup constraints skipped during folding
+    /// - Check the correctness of the beta error vector
+    /// NOTE: Permutation and shuffle constraints are not verified here.
     pub fn decide<'params, P: Params<'params, C>>(
         params: &P,
         pk: &ProvingKey<C>,
@@ -145,6 +185,7 @@ impl<C: CurveAffine> Accumulator<C> {
         committed_ok && error_ok && lookups_ok && beta_ok
     }
 
+    /// Recompute the compressed error term e = ∑ᵢ βᵢ * Gᵢ
     pub fn error(pk: &ProvingKey<C>, acc: &Self) -> C::Scalar {
         let lagrange_data = Data::<CommittedRef<'_, C>>::new(&pk, &acc);
 
@@ -165,6 +206,6 @@ impl<C: CurveAffine> Accumulator<C> {
                 );
             }
         });
-        error.into_iter().sum()
+        error.iter().sum()
     }
 }

halo2_proofs/src/protostar/accumulator/compressed_verifier.rs

@@ -21,6 +21,8 @@ use halo2curves::CurveAffine;
 /// the Beta transcript allows all constraints to be batched into a single one.
 /// The verifer sends a random value beta, and the prover commits to the vector of powers of beta.
 /// The constraint to be checked becomes ∑ᵢ βᵢ ⋅ Gᵢ.
+/// We need to compute the committed error vector for checking the correctness of beta, but
+/// we can let the verifier compute it.
 #[derive(PartialEq, Debug, Clone)]
 pub struct Transcript<C: CurveAffine> {
     pub beta: Committed<C>,
@@ -51,6 +53,8 @@ impl<C: CurveAffine> Transcript<C> {
         // No need to blind since the contents are known by the verifier
         let committed = commit_transparent(params, beta_values, transcript);
 
+        // During the creation of an initial accumulator, the error is expecte to be zero
+        // It does not need to be committed since the verifier will set the commitment to the identity.
         let error = Committed {
             values: empty_lagrange(n as usize),
             commitment: C::identity(),
@@ -64,8 +68,10 @@ impl<C: CurveAffine> Transcript<C> {
     }
 
     pub(super) fn merge(alpha: C::Scalar, transcript0: Self, transcript1: Self) -> Self {
+        // Get the actual beta challenge from the vectors
         let beta0 = transcript0.beta.values[1];
         let beta1 = transcript1.beta.values[1];
+        // Compute the linear interpolation of both beta values
         let beta = Committed::merge(alpha, transcript0.beta.clone(), transcript1.beta.clone());
 
         // The error is given by e = r⋅a - b, where r is a challenge and a,b are vectors.

halo2_proofs/src/protostar/constraints.rs

@@ -16,6 +16,7 @@ pub(crate) mod expression;
 pub(crate) mod paired;
 pub(crate) mod polynomial;
 
+///
 pub struct Data<T: QueryType> {
     fixed: Vec<T::Fixed>,
     selectors: Vec<T::Fixed>,

halo2_proofs/src/protostar/constraints/expression.rs

@@ -36,22 +36,6 @@ impl<F, CV, FV, WV> Expression<F, CV, FV, WV> {
         }
     }
 
-    /// Applies `f` to all leaves
-    pub fn traverse(&self, f: &mut impl FnMut(&Self)) {
-        match self {
-            Self::Negated(e) => e.traverse(f),
-            Self::Sum(e1, e2) => {
-                e1.traverse(f);
-                e2.traverse(f);
-            }
-            Self::Product(e1, e2) => {
-                e1.traverse(f);
-                e2.traverse(f);
-            }
-            v => f(v),
-        }
-    }
-
     /// Evaluate the polynomial using the provided closures to perform the operations.
     pub fn evaluate<T>(
         &self,
@@ -155,13 +139,18 @@ pub struct ColumnQuery<T> {
 }
 
 impl<T> ColumnQuery<T> {
+    /// For a given row `idx` of a column with `num_rows` rows, return the row index of the rotated column.
     pub fn row_idx(&self, idx: usize, num_rows: usize) -> usize {
         let idx = self.rotation + idx as i32;
         idx.rem_euclid(num_rows as i32) as usize
     }
 }
 
 /// Reference to a challenge variable
+/// TODO: Circuit expressions containing powers of challenges will blow up the degree of the error polynomial.
+/// By substituting powers of a challenge with a symbolic variable, we can reduce the degree of the error polynomial.
+/// This requires the verifier to compute powers of the challenges it sends to the prover,
+/// and treat them as separate challenges during folding.
 #[derive(Clone, Copy, PartialEq)]
 pub struct ChallengeQuery<T> {
     pub value: T,

halo2_proofs/src/protostar/constraints/paired.rs

@@ -30,6 +30,9 @@ impl<'a, F: Field> QueryType for Paired<'a, F> {
 }
 
 impl<'a, F: Field> Paired<'a, F> {
+    /// Create a `Data` object from two accumulators, where each variable contains a pair of references to the
+    /// some column from two different accumulators. This allows us to create a QueriedExpression where the leaves
+    /// contain these two references.
     pub fn new_data<C>(
         pk: &'a ProvingKey<C>,
         acc0: &'a Accumulator<C>,
@@ -83,15 +86,42 @@ impl<'a, F: Field> Paired<'a, F> {
         }
     }
 
+    /// Given an expression G where the variables are the linear polynomials interpolating between
+    /// the challenges and witness columns from two accumulators,
+    /// return the polynomial e(X) = ∑ᵢ βᵢ(X) G(fᵢ, wᵢ(X), rᵢ(X)).
+    ///
+    /// The strategy for evaluating e(X) is as follows:
+    /// - Let D = {0,1,...,d} be the evaluation domain containing the first d + 1 integers, where d is the degree of e(X).
+    /// - For each row i, we evaluate the expression eᵢ(X) = βᵢ(X) G(fᵢ, wᵢ(X), rᵢ(X)) over D,
+    ///   and add it to the running sum for e(D) = ∑ᵢ eᵢ(D).
+    ///   - The input variables βᵢ(X), wᵢ(X), rᵢ(X) are linear polynomials of the form pᵢ(X) = (1−X)⋅pᵢ,₀ + X⋅pᵢ,₁,
+    ///     where pᵢ,₀ and pᵢ,₁ are values at the same position but from two different accumulators.
+    ///   - For each variable fᵢ, compute fᵢ(D) by setting
+    ///     - pᵢ(0) = pᵢ,₀
+    ///     - pᵢ(1) = pᵢ,₁
+    ///     - pᵢ(j) = pᵢ(j-1) + (pᵢ,₁ − pᵢ,₀) for j = 2, ..., d.
+    ///   - Since challenge variables are the same for each row, we compute the evaluations only once.
+    /// - Given the Expression for e(X), we evaluate it point-wise as eᵢ(j) = βᵢ(j) G(fᵢ, wᵢ(j), rᵢ(j)) for j in D.
+    ///
+    /// TODO: As an optimization, we can get away with evaluating the polynomial only at the points 2,...,d,
+    /// since e(0) and e(1) are the existing errors from both accumulators. If we let D' = D \ {0,1}, then we can compute
+    /// e(D') and reinsert the evaluations at 0 and 1 for the final result before the conversion to coefficients.
     pub fn evaluate_compressed_polynomial(
         expr: QueriedExpression<Self>,
         rows: Range<usize>,
         num_rows: usize,
     ) -> Vec<F> {
+        // Convert the expression into an indexed one, where all leaves are extracted into vectors,
+        // and replaced by the index in these vectors.
+        // This allows us to separate the evaluation of the variables from the evaluation of the expression,
+        // since the expression leaves will point to the indices in buffers where the evaluations are stored.
         let indexed = IndexedExpression::<Paired<'a, F>>::new(expr);
+        // Evaluate the polynomial at the points 0,1,...,d, where d is the degree of expr,
+        // since the polynomial e(X) has d+1 coefficients.
         let num_evals = indexed.expr.degree() + 1;
 
-        // Since challenges are the same for all rows, we only need to evaluate them once
+        // For two transcripts with respective challenge, c₀, c₁,
+        // compute the evaluations of the polynomial c(X) = (1−X)⋅c₀ + X⋅c₁
         let challenges: Vec<_> = indexed
             .challenges
             .iter()
@@ -104,10 +134,15 @@ impl<'a, F: Field> Paired<'a, F> {
             })
             .collect();
 
-        // Fixed and witness queries are different for each row, so we initialize them to 0
+        // For each variable of the expression, we allocate buffers for storing their evaluations at each row.
+        // - Fixed variables are considered as constants, so we only need to fetch the value from the proving key
+        //   and consider fᵢ(j) = fᵢ for all j
+        // - Witness variables are interpolated from the values at the two accumulators,
+        //   and the evaluations are stored in a buffer.
         let mut fixed = vec![F::ZERO; indexed.fixed.len()];
         let mut witness = vec![EvaluatedError::<F>::new(num_evals); indexed.witness.len()];
 
+        // Running sum for e(D) = ∑ᵢ eᵢ(D)
         let mut sum = EvaluatedError::<F>::new(num_evals);
 
         for row_index in rows {
@@ -125,8 +160,9 @@ impl<'a, F: Field> Paired<'a, F> {
                 witness.evaluate(eval0, eval1);
             }
 
-            // Evaluate the expression in the current row and
+            // Evaluate the expression in the current row and add it to e(D)
             for (eval_idx, eval) in sum.evals.iter_mut().enumerate() {
+                // For each `eval_idx` j = 0, 1, ..., d, evaluate the expression eᵢ(j) = βᵢ(j) G(fᵢ, wᵢ(j), rᵢ(j))
                 *eval += indexed.expr.evaluate(
                     &|&constant| constant,
                     &|&challenge_idx| challenges[challenge_idx].evals[eval_idx],
@@ -139,11 +175,12 @@ impl<'a, F: Field> Paired<'a, F> {
             }
         }
 
+        // Convert the evaluations into the coefficients of the polynomial
         sum.to_coefficients()
     }
 }
 
-///
+/// Represents a polynomial evaluated over the integers 0,1,...,d.
 #[derive(Clone)]
 pub struct EvaluatedError<F> {
     pub evals: Vec<F>,
@@ -158,28 +195,31 @@ impl<F: Field> AddAssign<&EvaluatedError<F>> for EvaluatedError<F> {
 }
 
 impl<F: Field> EvaluatedError<F> {
+    /// Create a set of `num_evals` evaluations of the zero polynomial
     pub fn new(num_evals: usize) -> Self {
         Self {
             evals: vec![F::ZERO; num_evals],
         }
     }
 
+    /// Returns the evaluations of the linear polynomial (1-X)eval0 + Xeval1.
     pub fn new_from_boolean_evals(eval0: F, eval1: F, num_evals: usize) -> Self {
         let mut result = Self::new(num_evals);
         result.evaluate(eval0, eval1);
         result
     }
 
+    /// Overwrites the current evaluations and replaces it with the evaluations of the linear polynomial (1-X)eval0 + Xeval1.
     pub fn evaluate(&mut self, eval0: F, eval1: F) {
-        self.evals[0] = eval0;
+        let mut curr = eval0;
         let diff = eval1 - eval0;
-        let mut prev = eval0;
-        for eval in self.evals.iter_mut().skip(1) {
-            *eval = prev + diff;
-            prev = *eval;
+        for eval in self.evals.iter_mut() {
+            *eval = curr;
+            curr += diff;
         }
     }
 
+    /// Convert the n evalations into the coefficients of the polynomial.
     pub fn to_coefficients(&self) -> Vec<F> {
         let points: Vec<_> = field_integers().take(self.evals.len()).collect();
         lagrange_interpolate(&points, &self.evals)