feat: add built-in zero wire (Aux(0)) to constraint system

src/frontend/constraint_system.rs

@@ -69,6 +69,16 @@ pub trait ConstraintSystem<Scalar: PrimeField>: Sized + Send {
     Variable::new_unchecked(Index::Input(0))
   }
 
+  /// Return the "zero" auxiliary variable.
+  ///
+  /// # Implementor invariants
+  ///
+  /// * `Aux(0)` **must** be reserved at construction time and **must not** be
+  ///   returned by [`alloc`](ConstraintSystem::alloc).
+  /// * A constraint `0 * 0 = Aux(0)` (i.e. `Aux(0) == 0`) **must** be added
+  ///   by the constructor so the variable is properly enforced.
+  fn zero() -> Variable;
+
   /// Allocate a private variable in the constraint system. The provided function is used to
   /// determine the assignment of the variable. The given `annotation` function is invoked
   /// in testing contexts in order to derive a unique name for this variable in the current
@@ -244,6 +254,10 @@ impl<Scalar: PrimeField, CS: ConstraintSystem<Scalar>> ConstraintSystem<Scalar>
     CS::one()
   }
 
+  fn zero() -> Variable {
+    CS::zero()
+  }
+
   fn alloc<F, A, AR>(&mut self, annotation: A, f: F) -> Result<Variable, SynthesisError>
   where
     F: FnOnce() -> Result<Scalar, SynthesisError>,
@@ -332,6 +346,10 @@ impl<Scalar: PrimeField, CS: ConstraintSystem<Scalar>> ConstraintSystem<Scalar>
     CS::one()
   }
 
+  fn zero() -> Variable {
+    CS::zero()
+  }
+
   fn alloc<F, A, AR>(&mut self, annotation: A, f: F) -> Result<Variable, SynthesisError>
   where
     F: FnOnce() -> Result<Scalar, SynthesisError>,

src/frontend/gadgets/multieq.rs

@@ -81,6 +81,10 @@ impl<Scalar: PrimeField, CS: ConstraintSystem<Scalar>> ConstraintSystem<Scalar>
     CS::one()
   }
 
+  fn zero() -> Variable {
+    CS::zero()
+  }
+
   fn alloc<F, A, AR>(&mut self, annotation: A, f: F) -> Result<Variable, SynthesisError>
   where
     F: FnOnce() -> Result<Scalar, SynthesisError>,

src/frontend/gadgets/num.rs

@@ -47,6 +47,15 @@ impl<Scalar: PrimeField> AllocatedNum<Scalar> {
     }
   }
 
+  /// Returns an `AllocatedNum` wrapping the built-in `CS::zero()` variable.
+  /// Costs zero constraints since Aux(0) is pre-constrained to zero by the CS.
+  pub fn zero<CS: ConstraintSystem<Scalar>>() -> Self {
+    AllocatedNum {
+      value: Some(Scalar::ZERO),
+      variable: CS::zero(),
+    }
+  }
+
   /// Allocate a `Variable(Aux)` in a `ConstraintSystem`.
   pub fn alloc<CS, F>(mut cs: CS, value: F) -> Result<Self, SynthesisError>
   where
@@ -585,11 +594,14 @@ mod tests {
   fn test_allocated_num_one() {
     let mut cs = TestConstraintSystem::<Fr>::new();
 
+    // TestConstraintSystem starts with 1 constraint (the built-in zero enforcement)
+    let base_constraints = cs.num_constraints();
+
     // AllocatedNum::one() should add zero constraints
     let one = AllocatedNum::<Fr>::one::<TestConstraintSystem<Fr>>();
     assert_eq!(one.get_value(), Some(Fr::ONE));
     assert_eq!(one.get_variable(), TestConstraintSystem::<Fr>::one());
-    assert_eq!(cs.num_constraints(), 0);
+    assert_eq!(cs.num_constraints(), base_constraints);
 
     // Compare: the old alloc + enforce pattern adds 1 constraint
     let one_old = AllocatedNum::alloc_infallible(cs.namespace(|| "alloc"), || Fr::ONE);
@@ -599,6 +611,18 @@ mod tests {
       |lc| lc + TestConstraintSystem::<Fr>::one(),
       |lc| lc + one_old.get_variable(),
     );
-    assert_eq!(cs.num_constraints(), 1);
+    assert_eq!(cs.num_constraints(), base_constraints + 1);
+  }
+
+  #[test]
+  fn test_allocated_num_zero() {
+    let cs = TestConstraintSystem::<Fr>::new();
+    let base_constraints = cs.num_constraints();
+
+    // AllocatedNum::zero() should add zero constraints
+    let zero = AllocatedNum::<Fr>::zero::<TestConstraintSystem<Fr>>();
+    assert_eq!(zero.get_value(), Some(Fr::ZERO));
+    assert_eq!(zero.get_variable(), TestConstraintSystem::<Fr>::zero());
+    assert_eq!(cs.num_constraints(), base_constraints);
   }
 }

src/frontend/shape_cs.rs

@@ -45,17 +45,26 @@ impl<E: Engine> ShapeCS<E> {
 
 impl<E: Engine> Default for ShapeCS<E> {
   fn default() -> Self {
+    let zero_var = Variable::new_unchecked(Index::Aux(0));
+    // Enforce Aux(0) = 0: the constraint 0 * 0 = Aux(0)
+    let a = LinearCombination::<<E as Engine>::Scalar>::zero();
+    let b = LinearCombination::<<E as Engine>::Scalar>::zero();
+    let c = LinearCombination::<<E as Engine>::Scalar>::zero() + zero_var;
     ShapeCS {
-      constraints: vec![],
+      constraints: vec![(a, b, c)],
       inputs: 1,
-      aux: 0,
+      aux: 1, // Aux(0) reserved for zero
     }
   }
 }
 
 impl<E: Engine> ConstraintSystem<E::Scalar> for ShapeCS<E> {
   type Root = Self;
 
+  fn zero() -> Variable {
+    Variable::new_unchecked(Index::Aux(0))
+  }
+
   fn alloc<F, A, AR>(&mut self, _annotation: A, _f: F) -> Result<Variable, SynthesisError>
   where
     F: FnOnce() -> Result<E::Scalar, SynthesisError>,

src/frontend/test_shape_cs.rs

@@ -220,12 +220,17 @@ impl<E: Engine> Default for TestShapeCS<E> {
   fn default() -> Self {
     let mut map = HashMap::new();
     map.insert("ONE".into(), NamedObject::Var(TestShapeCS::<E>::one()));
+    map.insert("ZERO".into(), NamedObject::Var(TestShapeCS::<E>::zero()));
+    let zero_var = Variable::new_unchecked(Index::Aux(0));
+    let a = LinearCombination::<<E as Engine>::Scalar>::zero();
+    let b = LinearCombination::<<E as Engine>::Scalar>::zero();
+    let c = LinearCombination::<<E as Engine>::Scalar>::zero() + zero_var;
     TestShapeCS {
       named_objects: map,
       current_namespace: vec![],
-      constraints: vec![],
+      constraints: vec![(a, b, c, "ZERO".into())],
       inputs: vec![String::from("ONE")],
-      aux: vec![],
+      aux: vec![String::from("ZERO")],
     }
   }
 }
@@ -236,6 +241,10 @@ where
 {
   type Root = Self;
 
+  fn zero() -> Variable {
+    Variable::new_unchecked(Index::Aux(0))
+  }
+
   fn alloc<F, A, AR>(&mut self, annotation: A, _f: F) -> Result<Variable, SynthesisError>
   where
     F: FnOnce() -> Result<E::Scalar, SynthesisError>,

src/frontend/util_cs/test_cs.rs

@@ -73,13 +73,19 @@ impl<Scalar: PrimeField> Default for TestConstraintSystem<Scalar> {
   fn default() -> Self {
     let mut map = HashMap::new();
     map.insert("ONE".into(), NamedObject::Var);
+    map.insert("ZERO".into(), NamedObject::Var);
+
+    let zero_var = Variable::new_unchecked(Index::Aux(0));
+    let a = LinearCombination::<Scalar>::zero();
+    let b = LinearCombination::<Scalar>::zero();
+    let c = LinearCombination::<Scalar>::zero() + zero_var;
 
     TestConstraintSystem {
       named_objects: map,
       current_namespace: vec![],
-      constraints: vec![],
+      constraints: vec![(a, b, c, "ZERO".into())],
       inputs: vec![(Scalar::ONE, "ONE".into())],
-      aux: vec![],
+      aux: vec![(Scalar::ZERO, "ZERO".into())],
     }
   }
 }
@@ -153,6 +159,10 @@ fn compute_path(ns: &[String], this: &str) -> String {
 impl<Scalar: PrimeField> ConstraintSystem<Scalar> for TestConstraintSystem<Scalar> {
   type Root = Self;
 
+  fn zero() -> Variable {
+    Variable::new_unchecked(Index::Aux(0))
+  }
+
   fn alloc<F, A, AR>(&mut self, annotation: A, f: F) -> Result<Variable, SynthesisError>
   where
     F: FnOnce() -> Result<Scalar, SynthesisError>,

src/frontend/util_cs/witness_cs.rs

@@ -51,9 +51,11 @@ where
   pub fn with_capacity(aux_capacity: usize, input_capacity: usize) -> Self {
     let mut input_assignment = Vec::with_capacity(input_capacity + 1);
     input_assignment.push(Scalar::ONE);
+    let mut aux_assignment = Vec::with_capacity(aux_capacity + 1);
+    aux_assignment.push(Scalar::ZERO);
     Self {
       input_assignment,
-      aux_assignment: Vec::with_capacity(aux_capacity),
+      aux_assignment,
     }
   }
 
@@ -62,6 +64,7 @@ where
     self.input_assignment.clear();
     self.input_assignment.push(Scalar::ONE);
     self.aux_assignment.clear();
+    self.aux_assignment.push(Scalar::ZERO);
   }
 
   /// Get input assignment
@@ -81,12 +84,17 @@ where
 {
   type Root = Self;
 
+  fn zero() -> Variable {
+    Variable::new_unchecked(Index::Aux(0))
+  }
+
   fn new() -> Self {
     let input_assignment = vec![Scalar::ONE];
+    let aux_assignment = vec![Scalar::ZERO];
 
     Self {
       input_assignment,
-      aux_assignment: vec![],
+      aux_assignment,
     }
   }
 
@@ -147,9 +155,10 @@ where
 
   fn extend(&mut self, other: &Self) {
     self.input_assignment
-            // Skip first input, which must have been a temporarily allocated one variable.
+            // Skip built-in Input(0) = ONE, which is always the first input.
             .extend(&other.input_assignment[1..]);
-    self.aux_assignment.extend(&other.aux_assignment);
+    // Skip built-in Aux(0) = ZERO, which is always the first aux.
+    self.aux_assignment.extend(&other.aux_assignment[1..]);
   }
 
   ////////////////////////////////////////////////////////////////////////////////

src/gadgets/ecc.rs

@@ -8,7 +8,7 @@ use crate::{
   gadgets::{
     nonnative::{bignat::BigNat, util::f_to_nat},
     utils::{
-      alloc_bignat_constant, alloc_constant, alloc_num_equals, alloc_zero, conditionally_select,
+      alloc_bignat_constant, alloc_constant, alloc_num_equals, conditionally_select,
       conditionally_select2, conditionally_select_bignat, select_num_or_one, select_num_or_zero,
       select_num_or_zero2, select_one_or_diff2, select_one_or_num2, select_zero_or_num2,
     },
@@ -109,8 +109,8 @@ where
   }
 
   /// Allocates a default point on the curve, set to the identity point.
-  pub fn default<CS: ConstraintSystem<E::Base>>(mut cs: CS) -> Result<Self, SynthesisError> {
-    let zero = alloc_zero(cs.namespace(|| "zero"));
+  pub fn default<CS: ConstraintSystem<E::Base>>(_cs: CS) -> Result<Self, SynthesisError> {
+    let zero = AllocatedNum::zero::<CS>();
     let one = AllocatedNum::one::<CS>();
 
     Ok(AllocatedPoint {
@@ -607,7 +607,7 @@ where
   ) -> Result<(), SynthesisError> {
     let (_, b, _, _) = E::GE::group_params();
     if b != E::Base::ZERO {
-      let zero = alloc_zero(cs.namespace(|| "zero for absorb"));
+      let zero = AllocatedNum::zero::<CS>();
       let x = conditionally_select2(
         cs.namespace(|| "select x"),
         &zero,

src/gadgets/utils.rs

@@ -41,18 +41,6 @@ where
   Ok(num)
 }
 
-/// Allocate a variable that is set to zero
-pub fn alloc_zero<F: PrimeField, CS: ConstraintSystem<F>>(mut cs: CS) -> AllocatedNum<F> {
-  let zero = AllocatedNum::alloc_infallible(cs.namespace(|| "alloc"), || F::ZERO);
-  cs.enforce(
-    || "check zero is valid",
-    |lc| lc,
-    |lc| lc,
-    |lc| lc + zero.get_variable(),
-  );
-  zero
-}
-
 /// Allocate a scalar as a base. Only to be used is the scalar fits in base!
 pub fn alloc_scalar_as_base<E, CS>(
   mut cs: CS,

src/neutron/circuit/mod.rs

@@ -11,7 +11,7 @@ use crate::{
   },
   gadgets::{
     ecc::AllocatedNonnativePoint,
-    utils::{alloc_num_equals, alloc_zero, conditionally_select_vec, le_bits_to_num},
+    utils::{alloc_num_equals, conditionally_select_vec, le_bits_to_num},
   },
   neutron::{nifs::NIFS, relation::FoldedInstance},
   r1cs::R1CSInstance,
@@ -283,7 +283,7 @@ impl<E: Engine, SC: StepCircuit<E::Scalar>> NeutronAugmentedCircuit<'_, E, SC> {
       self.alloc_witness(cs.namespace(|| "allocate the circuit witness"), arity)?;
 
     // Compute variable indicating if this is the base case
-    let zero = alloc_zero(cs.namespace(|| "zero"));
+    let zero = AllocatedNum::zero::<CS>();
     let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?;
 
     // synthesize base case
@@ -436,8 +436,8 @@ mod tests {
 
   #[test]
   fn test_neutron_recursive_circuit_pasta() {
-    test_recursive_circuit_with::<PallasEngine, VestaEngine>(&expect!["5493"]);
-    test_recursive_circuit_with::<Bn256EngineKZG, GrumpkinEngine>(&expect!["5773"]);
-    test_recursive_circuit_with::<Secp256k1Engine, Secq256k1Engine>(&expect!["6238"]);
+    test_recursive_circuit_with::<PallasEngine, VestaEngine>(&expect!["5492"]);
+    test_recursive_circuit_with::<Bn256EngineKZG, GrumpkinEngine>(&expect!["5772"]);
+    test_recursive_circuit_with::<Secp256k1Engine, Secq256k1Engine>(&expect!["6237"]);
   }
 }

src/neutron/circuit/relation.rs

@@ -1,10 +1,7 @@
 //! This module implements various gadgets necessary for folding R1CS types with NeutronNova folding scheme.
 use crate::{
   frontend::{num::AllocatedNum, Boolean, ConstraintSystem, SynthesisError},
-  gadgets::{
-    ecc::AllocatedNonnativePoint,
-    utils::{alloc_zero, conditionally_select},
-  },
+  gadgets::{ecc::AllocatedNonnativePoint, utils::conditionally_select},
   neutron::{circuit::r1cs::AllocatedNonnativeR1CSInstance, relation::FoldedInstance},
   traits::{commitment::CommitmentTrait, Engine, ROCircuitTrait},
 };
@@ -71,7 +68,7 @@ impl<E: Engine> AllocatedFoldedInstance<E> {
     let comm_E = comm_W.clone();
 
     // Allocate T = 0. Similar to X0 and X1, we do not need to check that T is well-formed
-    let T = alloc_zero(cs.namespace(|| "allocate T"));
+    let T = AllocatedNum::zero::<CS>();
 
     let u = T.clone();
 

src/neutron/mod.rs

@@ -544,17 +544,17 @@ mod tests {
   fn test_pp_digest() {
     test_pp_digest_with::<PallasEngine, VestaEngine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["4d22b1021985b02532b1cc83ab566d503d8db8cf7de1acac525d39e3c2508e03"],
+      &expect!["750b49c7d61647ff4805affb81358ed9fc7ba107fd2395ee252350d9039ba203"],
     );
 
     test_pp_digest_with::<Bn256EngineIPA, GrumpkinEngine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["fdea1f44a4d102141c6f31efa72c04606c5e6d3ec9a6b37208238152717a4c03"],
+      &expect!["816fb0f716c65cf700e357f9dcf5a7238933b16af89ab428d63f5c976438f700"],
     );
 
     test_pp_digest_with::<Secp256k1Engine, Secq256k1Engine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["bdcf8157e37b5d99c5c7168774e16ec11a24594833b078ebe6312e83fdfda600"],
+      &expect!["e9ece80b99b3a82b1c1a29bce4f1148186888754ef9f74b96f6244578cb2e902"],
     );
   }
 

src/nova/circuit/mod.rs

@@ -11,9 +11,7 @@ use crate::{
   },
   gadgets::{
     ecc::AllocatedPoint,
-    utils::{
-      alloc_num_equals, alloc_scalar_as_base, alloc_zero, conditionally_select_vec, le_bits_to_num,
-    },
+    utils::{alloc_num_equals, alloc_scalar_as_base, conditionally_select_vec, le_bits_to_num},
   },
   r1cs::{R1CSInstance, RelaxedR1CSInstance},
   traits::{
@@ -254,7 +252,7 @@ impl<E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'_, E, SC> {
       self.alloc_witness(cs.namespace(|| "allocate the circuit witness"), arity)?;
 
     // Compute variable indicating if this is the base case
-    let zero = alloc_zero(cs.namespace(|| "zero"));
+    let zero = AllocatedNum::zero::<CS>();
     let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?;
 
     // compute hash of the non-deterministic inputs
@@ -451,8 +449,8 @@ mod tests {
 
   #[test]
   fn test_recursive_circuit() {
-    test_recursive_circuit_with::<PallasEngine, VestaEngine>(9830, 10361);
-    test_recursive_circuit_with::<Bn256EngineKZG, GrumpkinEngine>(9998, 10550);
-    test_recursive_circuit_with::<Secp256k1Engine, Secq256k1Engine>(10277, 10973);
+    test_recursive_circuit_with::<PallasEngine, VestaEngine>(9823, 10354);
+    test_recursive_circuit_with::<Bn256EngineKZG, GrumpkinEngine>(9991, 10543);
+    test_recursive_circuit_with::<Secp256k1Engine, Secq256k1Engine>(10270, 10966);
   }
 }