feat: structural zero wire in R1CS layout (z = [w, 1, 0, x])

src/frontend/constraint_system.rs

@@ -69,6 +69,13 @@ pub trait ConstraintSystem<Scalar: PrimeField>: Sized + Send {
     Variable::new_unchecked(Index::Input(0))
   }
 
+  /// Return the "zero" input variable.
+  /// This is a structural part of the R1CS vector `z = [w, 1, 0, x]`,
+  /// requiring no auxiliary variable or enforcement constraint.
+  fn zero() -> Variable {
+    Variable::new_unchecked(Index::Input(1))
+  }
+
   /// 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 +251,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 +343,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 it uses the input-1 wire directly.
+  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

src/frontend/r1cs.rs

@@ -32,7 +32,7 @@ impl<E: Engine> NovaWitness<E> for SatisfyingAssignment<E> {
     ck: &CommitmentKey<E>,
   ) -> Result<(R1CSInstance<E>, R1CSWitness<E>), NovaError> {
     let W = R1CSWitness::<E>::new(shape, self.aux_assignment())?;
-    let X = &self.input_assignment()[1..];
+    let X = &self.input_assignment()[2..];
 
     let comm_W = W.commit(ck);
 
@@ -74,8 +74,8 @@ macro_rules! impl_nova_shape {
         B.cols = num_vars + num_inputs;
         C.cols = num_vars + num_inputs;
 
-        // Don't count One as an input for shape's purposes.
-        R1CSShape::new(num_constraints, num_vars, num_inputs - 1, A, B, C)
+        // Don't count One and Zero as inputs for shape's purposes.
+        R1CSShape::new(num_constraints, num_vars, num_inputs - 2, A, B, C)
       }
     }
   };

src/frontend/shape_cs.rs

@@ -47,7 +47,7 @@ impl<E: Engine> Default for ShapeCS<E> {
   fn default() -> Self {
     ShapeCS {
       constraints: vec![],
-      inputs: 1,
+      inputs: 2,
       aux: 0,
     }
   }

src/frontend/test_shape_cs.rs

@@ -220,11 +220,12 @@ 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()));
     TestShapeCS {
       named_objects: map,
       current_namespace: vec![],
       constraints: vec![],
-      inputs: vec![String::from("ONE")],
+      inputs: vec![String::from("ONE"), String::from("ZERO")],
       aux: vec![],
     }
   }

src/frontend/util_cs/test_cs.rs

@@ -73,12 +73,13 @@ 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);
 
     TestConstraintSystem {
       named_objects: map,
       current_namespace: vec![],
       constraints: vec![],
-      inputs: vec![(Scalar::ONE, "ONE".into())],
+      inputs: vec![(Scalar::ONE, "ONE".into()), (Scalar::ZERO, "ZERO".into())],
       aux: vec![],
     }
   }

src/frontend/util_cs/witness_cs.rs

@@ -49,8 +49,9 @@ where
 {
   /// Create a new WitnessCS with pre-allocated capacity for aux and input variables.
   pub fn with_capacity(aux_capacity: usize, input_capacity: usize) -> Self {
-    let mut input_assignment = Vec::with_capacity(input_capacity + 1);
+    let mut input_assignment = Vec::with_capacity(input_capacity + 2);
     input_assignment.push(Scalar::ONE);
+    input_assignment.push(Scalar::ZERO);
     Self {
       input_assignment,
       aux_assignment: Vec::with_capacity(aux_capacity),
@@ -61,6 +62,7 @@ where
   pub fn clear(&mut self) {
     self.input_assignment.clear();
     self.input_assignment.push(Scalar::ONE);
+    self.input_assignment.push(Scalar::ZERO);
     self.aux_assignment.clear();
   }
 
@@ -82,7 +84,7 @@ where
   type Root = Self;
 
   fn new() -> Self {
-    let input_assignment = vec![Scalar::ONE];
+    let input_assignment = vec![Scalar::ONE, Scalar::ZERO];
 
     Self {
       input_assignment,
@@ -147,8 +149,8 @@ where
 
   fn extend(&mut self, other: &Self) {
     self.input_assignment
-            // Skip first input, which must have been a temporarily allocated one variable.
-            .extend(&other.input_assignment[1..]);
+            // Skip built-in Input(0) = ONE and Input(1) = ZERO.
+            .extend(&other.input_assignment[2..]);
     self.aux_assignment.extend(&other.aux_assignment);
   }
 
@@ -190,3 +192,37 @@ where
     &self.aux_assignment
   }
 }
+
+#[cfg(test)]
+mod tests {
+  use super::*;
+  use crate::frontend::ConstraintSystem;
+  use ff::Field;
+  use halo2curves::pasta::Fq as Scalar;
+
+  #[test]
+  fn test_extend_skips_builtin_inputs() {
+    // `other` has the 2 built-in inputs (ONE, ZERO) plus one user input
+    let mut other = WitnessCS::<Scalar>::new();
+    other
+      .alloc_input(|| "user_input", || Ok(Scalar::from(42u64)))
+      .unwrap();
+    assert_eq!(other.input_assignment.len(), 3); // ONE, ZERO, user
+
+    // `self` starts with just the 2 built-in inputs
+    let mut base = WitnessCS::<Scalar>::new();
+    assert_eq!(base.input_assignment.len(), 2); // ONE, ZERO
+
+    base.extend(&other);
+
+    // Only the user input should be copied, not the built-in ONE or ZERO
+    assert_eq!(
+      base.input_assignment.len(),
+      3,
+      "extend should copy only user inputs, not built-in ONE/ZERO"
+    );
+    assert_eq!(base.input_assignment[0], Scalar::ONE); // ONE
+    assert_eq!(base.input_assignment[1], Scalar::ZERO); // ZERO
+    assert_eq!(base.input_assignment[2], Scalar::from(42u64)); // user input
+  }
+}

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!["5491"]);
+    test_recursive_circuit_with::<Bn256EngineKZG, GrumpkinEngine>(&expect!["5771"]);
+    test_recursive_circuit_with::<Secp256k1Engine, Secq256k1Engine>(&expect!["6236"]);
   }
 }

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!["84ce92990218d2086fa3483c4722bf6b8c1b22fff91f16506d540264b5fda502"],
     );
 
     test_pp_digest_with::<Bn256EngineIPA, GrumpkinEngine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["fdea1f44a4d102141c6f31efa72c04606c5e6d3ec9a6b37208238152717a4c03"],
+      &expect!["79cf01e1622a066ca791bbd14dea25109a682bb1e2cd264d1190bbbc65d7eb03"],
     );
 
     test_pp_digest_with::<Secp256k1Engine, Secq256k1Engine, _>(
       &TrivialCircuit::<_>::default(),
-      &expect!["bdcf8157e37b5d99c5c7168774e16ec11a24594833b078ebe6312e83fdfda600"],
+      &expect!["d21c7710497172b529dd361fd869bc212f85a842e04ac93f243039612f06ee03"],
     );
   }
 

src/neutron/nifs.rs

@@ -235,11 +235,16 @@ impl<E: Engine> NIFS<E> {
 
     let (res1, res2) = rayon::join(
       || {
-        let z1 = [W1.W.clone(), vec![U1.u], U1.X.clone()].concat();
+        let z1 = [W1.W.clone(), vec![U1.u, E::Scalar::ZERO], U1.X.clone()].concat();
         S.S.multiply_vec(&z1)
       },
       || {
-        let z2 = [W2.W.clone(), vec![E::Scalar::ONE], U2.X.clone()].concat();
+        let z2 = [
+          W2.W.clone(),
+          vec![E::Scalar::ONE, E::Scalar::ZERO],
+          U2.X.clone(),
+        ]
+        .concat();
         S.S.multiply_vec(&z2)
       },
     );
@@ -550,7 +555,7 @@ mod benchmarks {
         .map(|i| (i, i, E::Scalar::ONE))
         .collect::<Vec<_>>(),
       num_cons,
-      num_vars + 1 + num_io,
+      num_vars + 2 + num_io,
     );
     let B = A.clone();
     let C = A.clone();

src/neutron/relation.rs

@@ -75,7 +75,7 @@ impl<E: Engine> Structure<E> {
     W: &FoldedWitness<E>,
   ) -> Result<(), NovaError> {
     // check if the witness is satisfying
-    let z = [W.W.clone(), vec![U.u], U.X.clone()].concat();
+    let z = [W.W.clone(), vec![U.u, E::Scalar::ZERO], U.X.clone()].concat();
     let (Az, Bz, Cz) = self.S.multiply_vec(&z)?;
 
     // full_E is the outer product of E1 and E2

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>(9822, 10353);
+    test_recursive_circuit_with::<Bn256EngineKZG, GrumpkinEngine>(9990, 10542);
+    test_recursive_circuit_with::<Secp256k1Engine, Secq256k1Engine>(10269, 10965);
   }
 }