-Full decider checks

-Merge instance and advice

halo2_proofs/src/protostar/accumulator.rs

@@ -18,22 +18,20 @@ use crate::{
 use self::committed::Committed;
 
 use super::{
-    constraints::{paired::Paired, polynomial::PolynomialRef, Data},
+    constraints::{paired::Paired, polynomial::CommittedRef, Data},
     ProvingKey,
 };
 
-pub(super) mod advice;
 pub(super) mod committed;
 pub(super) mod compressed_verifier;
-pub(super) mod instance;
+pub(super) mod gate;
 pub(super) mod lookup;
 
 /// An `Accumulator` contains the entirety of the IOP transcript,
 /// including commitments and verifier challenges.
 #[derive(Debug, Clone, PartialEq)]
 pub struct Accumulator<C: CurveAffine> {
-    pub instance: instance::Transcript<C>,
-    pub advice: advice::Transcript<C>,
+    pub gate: gate::Transcript<C>,
     pub lookups: Vec<lookup::Transcript<C>>,
     pub beta: compressed_verifier::Transcript<C>,
 
@@ -68,8 +66,7 @@ impl<C: CurveAffine> Accumulator<C> {
     }
 
     fn merge(acc0: Self, acc1: Self, error_poly: Vec<C::Scalar>, alpha: C::Scalar) -> Self {
-        let instance = instance::Transcript::merge(alpha, acc0.instance, acc1.instance);
-        let advice = advice::Transcript::merge(alpha, acc0.advice, acc1.advice);
+        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))
             .collect();
@@ -88,8 +85,7 @@ impl<C: CurveAffine> Accumulator<C> {
         assert_eq!(error1, acc1.error);
 
         Self {
-            instance,
-            advice,
+            gate,
             lookups,
             beta,
             ys,
@@ -102,53 +98,73 @@ impl<C: CurveAffine> Accumulator<C> {
         pk: &ProvingKey<C>,
         acc: &Self,
     ) -> bool {
-        let committed_iter: Vec<&Committed<C>> = acc
-            .instance
-            .committed
-            .iter()
-            .chain(&acc.advice.committed)
-            .chain([&acc.beta.beta, &acc.beta.beta_shift].into_iter())
-            .chain(
-                acc.lookups
-                    .iter()
-                    .flat_map(|lookup| [&lookup.m, &lookup.g, &lookup.h].into_iter()),
-            )
-            .collect();
-
-        let committed_ok = committed_iter.iter().all(|c| c.decide(params));
-
-        let error_vec = Self::error_vector(pk, acc);
-
-        let error = error_vec
-            .iter()
-            .zip(acc.beta.beta.values.iter())
-            .fold(C::Scalar::ZERO, |acc, (e, b)| acc + (*e * b));
-
-        let error_ok = error == acc.error;
-
-        committed_ok && error_ok
+        // Check all Committed columns are correct (commit(values;bline) == commitment)
+        let committed_ok = {
+            let committed_iter: Vec<&Committed<C>> = acc
+                .gate
+                .instance
+                .iter()
+                .chain(&acc.gate.advice)
+                .chain([&acc.beta.beta, &acc.beta.error].into_iter())
+                .chain(
+                    acc.lookups
+                        .iter()
+                        .flat_map(|lookup| [&lookup.m, &lookup.g, &lookup.h].into_iter()),
+                )
+                .collect();
+            committed_iter.iter().all(|c| c.decide(params))
+        };
+
+        // Check Error term  (error == ∑ᵢ βᵢ * Gᵢ)
+        let error_ok = { acc.error == Self::error(&pk, &acc) };
+
+        // Check linear lookup constraint ∑ᵢ gᵢ == ∑ᵢ hᵢ
+        let lookups_ok = {
+            acc.lookups.iter().all(|lookup| {
+                let lhs: C::Scalar = lookup.g.values.iter().sum();
+                let rhs: C::Scalar = lookup.h.values.iter().sum();
+                lhs == rhs
+            })
+        };
+
+        // Check beta constraint eᵢ ≡ β ⋅ βᵢ − βᵢ₊₁, β₀ ≡ 1
+        let beta_ok = {
+            let beta_column = &acc.beta.beta.values;
+            let error_column = &acc.beta.error.values;
+
+            let beta = beta_column[1];
+
+            let powers_ok = (1..pk.num_rows)
+                .into_iter()
+                .all(|i| error_column[i - 1] == beta_column[i - 1] * beta - beta_column[i]);
+
+            let init_ok = beta_column[0] == C::Scalar::ONE;
+            powers_ok && init_ok
+        };
+
+        committed_ok && error_ok && lookups_ok && beta_ok
     }
 
-    pub fn error_vector(pk: &ProvingKey<C>, acc: &Self) -> Polynomial<C::Scalar, LagrangeCoeff> {
-        let lagrange_data = Data::<PolynomialRef<'_, C::Scalar, LagrangeCoeff>>::new(&pk, &acc);
+    pub fn error(pk: &ProvingKey<C>, acc: &Self) -> C::Scalar {
+        let lagrange_data = Data::<CommittedRef<'_, C>>::new(&pk, &acc);
 
-        let full_constraint = lagrange_data.full_constraint_no_beta(pk.cs.gates(), pk.cs.lookups());
+        let full_constraint = lagrange_data.full_constraint(pk.cs.gates(), pk.cs.lookups());
 
         let mut error = pk.domain.empty_lagrange();
         parallelize(&mut error, |value, start| {
             for (i, v) in value.iter_mut().enumerate() {
                 let row_idx = i + start;
                 *v = full_constraint.evaluate(
-                    &|c| c,
-                    &|challenge| *challenge.value,
-                    &|fixed| fixed.column[fixed.row_idx(row_idx, pk.num_rows)],
-                    &|witness| witness.column[witness.row_idx(row_idx, pk.num_rows)],
-                    &|e| -e,
+                    &|&c| c,
+                    &|&challenge| *challenge.value,
+                    &|&fixed| fixed.column.values[fixed.row_idx(row_idx, pk.num_rows)],
+                    &|&witness| witness.column.values[witness.row_idx(row_idx, pk.num_rows)],
+                    &|&e| -e,
                     &|a, b| a + b,
                     &|a, b| a * b,
                 );
             }
         });
-        error
+        error.into_iter().sum()
     }
 }

halo2_proofs/src/protostar/accumulator/committed.rs

@@ -1,3 +1,5 @@
+use std::ops::{Add, Mul};
+
 use ff::Field;
 use group::Curve;
 use halo2curves::CurveAffine;
@@ -12,38 +14,54 @@ use crate::{
     transcript::{EncodedChallenge, TranscriptWrite},
 };
 
+/// Represents a committed column sent that the verifier can query.
 #[derive(PartialEq, Debug, Clone)]
 pub struct Committed<C: CurveAffine> {
     pub values: Polynomial<C::Scalar, LagrangeCoeff>,
     pub commitment: C,
     pub blind: Blind<C::Scalar>,
 }
 
-impl<C: CurveAffine> Committed<C> {
-    pub(super) fn fold(alpha: C::Scalar, committed0: Self, committed1: Self) -> Self {
-        let values = {
-            let tmp = committed1.values - &committed0.values;
-            let tmp = tmp * alpha;
-            tmp + &committed0.values
-        };
-        let commitment = ((committed1.commitment - committed0.commitment) * alpha
-            + &committed0.commitment)
-            .to_affine();
-        let blind = (committed1.blind - committed0.blind) * alpha + committed0.blind;
+impl<C: CurveAffine> Add for Committed<C> {
+    type Output = Committed<C>;
+
+    fn add(self, rhs: Self) -> Self::Output {
         Self {
-            values,
-            commitment,
-            blind,
+            values: self.values + &rhs.values,
+            commitment: (self.commitment + rhs.commitment).to_affine(),
+            blind: self.blind + rhs.blind,
+        }
+    }
+}
+
+impl<C: CurveAffine> Mul<C::Scalar> for Committed<C> {
+    type Output = Committed<C>;
+
+    fn mul(self, rhs: C::Scalar) -> Self::Output {
+        Self {
+            values: self.values * rhs,
+            commitment: (self.commitment * rhs).to_affine(),
+            blind: self.blind * rhs,
         }
     }
+}
+
+impl<C: CurveAffine> Committed<C> {
+    /// Compute the linear combination (1−α)⋅ c₀ + α⋅c₁
+    pub(super) fn merge(alpha: C::Scalar, committed0: Self, committed1: Self) -> Self {
+        committed0 * (C::Scalar::ONE - alpha) + committed1 * alpha
+    }
 
+    /// Checks whether the commitment is valid with regards to the underlying column
     pub(super) fn decide<'params, P: Params<'params, C>>(&self, params: &P) -> bool {
         let commitment = params.commit_lagrange(&self.values, self.blind).to_affine();
         debug_assert_eq!(commitment, self.commitment);
         commitment == self.commitment
     }
 }
 
+/// Given a set of columns to be sent to the verifier, compute their commitments and write them to transcript.
+/// Commitments are blinded.
 pub fn batch_commit<
     'params,
     C: CurveAffine,
@@ -88,6 +106,8 @@ pub fn batch_commit<
         .collect()
 }
 
+/// Given a set of columns to be sent to the verifier, compute their commitments and write them to transcript.
+/// Commitments are transparent using a default blinding value.
 pub fn batch_commit_transparent<
     'params,
     C: CurveAffine,
@@ -130,6 +150,7 @@ pub fn batch_commit_transparent<
         .collect()
 }
 
+/// Compute a single blinded commitment and write it to the transcript
 pub fn commit<
     'params,
     C: CurveAffine,
@@ -154,6 +175,7 @@ pub fn commit<
     }
 }
 
+/// Compute a single transparent commitment and write it to the transcript
 pub fn commit_transparent<
     'params,
     C: CurveAffine,