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

src/frontend/constraint_system.rs

@@ -69,6 +69,11 @@ pub trait ConstraintSystem<Scalar: PrimeField>: Sized + Send {
     Variable::new_unchecked(Index::Input(0))
   }
 
+  /// Return the "zero" auxiliary variable (Aux(0), enforced to equal zero)
+  fn zero() -> Variable {
+    Variable::new_unchecked(Index::Aux(0))
+  }
+
   /// 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 +249,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 +341,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,6 @@ 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);
   }
 }

src/frontend/shape_cs.rs

@@ -45,10 +45,15 @@ 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
     }
   }
 }

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")],
     }
   }
 }

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())],
     }
   }
 }

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
@@ -83,10 +86,11 @@ where
 
   fn new() -> Self {
     let input_assignment = vec![Scalar::ONE];
+    let aux_assignment = vec![Scalar::ZERO];
 
     Self {
       input_assignment,
-      aux_assignment: vec![],
+      aux_assignment,
     }
   }
 
@@ -149,7 +153,8 @@ where
     self.input_assignment
             // Skip first input, which must have been a temporarily allocated one variable.
             .extend(&other.input_assignment[1..]);
-    self.aux_assignment.extend(&other.aux_assignment);
+    // Skip first aux, which must have been a temporarily allocated zero variable.
+    self.aux_assignment.extend(&other.aux_assignment[1..]);
   }
 
   ////////////////////////////////////////////////////////////////////////////////

src/gadgets/utils.rs

@@ -41,16 +41,10 @@ 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 variable that is set to zero.
+/// Uses the built-in CS::zero() wire (Aux(0)), so this is free (no extra constraints).
+pub fn alloc_zero<F: PrimeField, CS: ConstraintSystem<F>>(_cs: CS) -> AllocatedNum<F> {
+  AllocatedNum::zero::<CS>()
 }
 
 /// Allocate a scalar as a base. Only to be used is the scalar fits in base!

src/nova/circuit/mod.rs

@@ -451,8 +451,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);
   }
 }

src/nova/mod.rs

@@ -1125,17 +1125,17 @@ mod tests {
   fn test_pp_digest() {
     test_pp_digest_with::<PallasEngine, VestaEngine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["5554dcef9f66efdf2477d0ada1f553f0e7edd9191391156edfca338cb270aa02"],
+      &expect!["79427ff4955e7cf8112f37965e3922ef166cb650f93578db5c65b045d0a71300"],
     );
 
     test_pp_digest_with::<Bn256EngineIPA, GrumpkinEngine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["a5ad54e26a84517739bde0fd1e56f10aa1f8321bfee234c347af0fb9b14bfb00"],
+      &expect!["a091b0952ea6c6b7247d3de59dac55c39236e4eec78519608a9572370d88e600"],
     );
 
     test_pp_digest_with::<Secp256k1Engine, Secq256k1Engine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["b403daf596511f975656f8621269c1e885b60863aebd7a095000b599f6ed2802"],
+      &expect!["45c048e2413bafd2433432357aa88f343ee9106827f5dced2718c5b95f3c8601"],
     );
   }