diff --git a/src/frontend/constraint_system.rs b/src/frontend/constraint_system.rs index f8030f3a..47f2fd16 100644 --- a/src/frontend/constraint_system.rs +++ b/src/frontend/constraint_system.rs @@ -69,6 +69,13 @@ pub trait ConstraintSystem: 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> ConstraintSystem CS::one() } + fn zero() -> Variable { + CS::zero() + } + fn alloc(&mut self, annotation: A, f: F) -> Result where F: FnOnce() -> Result, @@ -332,6 +343,10 @@ impl> ConstraintSystem CS::one() } + fn zero() -> Variable { + CS::zero() + } + fn alloc(&mut self, annotation: A, f: F) -> Result where F: FnOnce() -> Result, diff --git a/src/frontend/gadgets/multieq.rs b/src/frontend/gadgets/multieq.rs index 3c7e4875..eb73f7f8 100644 --- a/src/frontend/gadgets/multieq.rs +++ b/src/frontend/gadgets/multieq.rs @@ -81,6 +81,10 @@ impl> ConstraintSystem CS::one() } + fn zero() -> Variable { + CS::zero() + } + fn alloc(&mut self, annotation: A, f: F) -> Result where F: FnOnce() -> Result, diff --git a/src/frontend/gadgets/num.rs b/src/frontend/gadgets/num.rs index 3641b3a9..9c1e7851 100644 --- a/src/frontend/gadgets/num.rs +++ b/src/frontend/gadgets/num.rs @@ -47,6 +47,15 @@ impl AllocatedNum { } } + /// Returns an `AllocatedNum` wrapping the built-in `CS::zero()` variable. + /// Costs zero constraints since it uses the input-1 wire directly. + pub fn zero>() -> Self { + AllocatedNum { + value: Some(Scalar::ZERO), + variable: CS::zero(), + } + } + /// Allocate a `Variable(Aux)` in a `ConstraintSystem`. pub fn alloc(mut cs: CS, value: F) -> Result where diff --git a/src/frontend/r1cs.rs b/src/frontend/r1cs.rs index 1a1a24d9..710d31fb 100644 --- a/src/frontend/r1cs.rs +++ b/src/frontend/r1cs.rs @@ -32,7 +32,7 @@ impl NovaWitness for SatisfyingAssignment { ck: &CommitmentKey, ) -> Result<(R1CSInstance, R1CSWitness), NovaError> { let W = R1CSWitness::::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) } } }; diff --git a/src/frontend/shape_cs.rs b/src/frontend/shape_cs.rs index 05a4e996..c0a6e995 100644 --- a/src/frontend/shape_cs.rs +++ b/src/frontend/shape_cs.rs @@ -47,7 +47,7 @@ impl Default for ShapeCS { fn default() -> Self { ShapeCS { constraints: vec![], - inputs: 1, + inputs: 2, aux: 0, } } diff --git a/src/frontend/test_shape_cs.rs b/src/frontend/test_shape_cs.rs index dfa2e419..498c6f49 100644 --- a/src/frontend/test_shape_cs.rs +++ b/src/frontend/test_shape_cs.rs @@ -220,11 +220,12 @@ impl Default for TestShapeCS { fn default() -> Self { let mut map = HashMap::new(); map.insert("ONE".into(), NamedObject::Var(TestShapeCS::::one())); + map.insert("ZERO".into(), NamedObject::Var(TestShapeCS::::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![], } } diff --git a/src/frontend/util_cs/test_cs.rs b/src/frontend/util_cs/test_cs.rs index cd8567c0..35d2c0f8 100644 --- a/src/frontend/util_cs/test_cs.rs +++ b/src/frontend/util_cs/test_cs.rs @@ -73,12 +73,13 @@ impl Default for TestConstraintSystem { 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![], } } diff --git a/src/frontend/util_cs/witness_cs.rs b/src/frontend/util_cs/witness_cs.rs index 22db16f3..23893451 100644 --- a/src/frontend/util_cs/witness_cs.rs +++ b/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::::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::::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 + } +} diff --git a/src/gadgets/ecc.rs b/src/gadgets/ecc.rs index a8a264f8..44c23266 100644 --- a/src/gadgets/ecc.rs +++ b/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>(mut cs: CS) -> Result { - let zero = alloc_zero(cs.namespace(|| "zero")); + pub fn default>(_cs: CS) -> Result { + let zero = AllocatedNum::zero::(); let one = AllocatedNum::one::(); 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::(); let x = conditionally_select2( cs.namespace(|| "select x"), &zero, diff --git a/src/gadgets/utils.rs b/src/gadgets/utils.rs index be092dc6..22d45e4d 100644 --- a/src/gadgets/utils.rs +++ b/src/gadgets/utils.rs @@ -41,18 +41,6 @@ where Ok(num) } -/// Allocate a variable that is set to zero -pub fn alloc_zero>(mut cs: CS) -> AllocatedNum { - 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( mut cs: CS, diff --git a/src/neutron/circuit/mod.rs b/src/neutron/circuit/mod.rs index be4acd6b..f6c0625c 100644 --- a/src/neutron/circuit/mod.rs +++ b/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> 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::(); 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::(&expect!["5493"]); - test_recursive_circuit_with::(&expect!["5773"]); - test_recursive_circuit_with::(&expect!["6238"]); + test_recursive_circuit_with::(&expect!["5491"]); + test_recursive_circuit_with::(&expect!["5771"]); + test_recursive_circuit_with::(&expect!["6236"]); } } diff --git a/src/neutron/circuit/relation.rs b/src/neutron/circuit/relation.rs index ab36555c..38435f4e 100644 --- a/src/neutron/circuit/relation.rs +++ b/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 AllocatedFoldedInstance { 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::(); let u = T.clone(); diff --git a/src/neutron/mod.rs b/src/neutron/mod.rs index 457f81e8..e1220d0e 100644 --- a/src/neutron/mod.rs +++ b/src/neutron/mod.rs @@ -544,17 +544,17 @@ mod tests { fn test_pp_digest() { test_pp_digest_with::( &TrivialCircuit::<_>::default(), - &expect!["4d22b1021985b02532b1cc83ab566d503d8db8cf7de1acac525d39e3c2508e03"], + &expect!["84ce92990218d2086fa3483c4722bf6b8c1b22fff91f16506d540264b5fda502"], ); test_pp_digest_with::( &TrivialCircuit::<_>::default(), - &expect!["fdea1f44a4d102141c6f31efa72c04606c5e6d3ec9a6b37208238152717a4c03"], + &expect!["79cf01e1622a066ca791bbd14dea25109a682bb1e2cd264d1190bbbc65d7eb03"], ); test_pp_digest_with::( &TrivialCircuit::<_>::default(), - &expect!["bdcf8157e37b5d99c5c7168774e16ec11a24594833b078ebe6312e83fdfda600"], + &expect!["d21c7710497172b529dd361fd869bc212f85a842e04ac93f243039612f06ee03"], ); } diff --git a/src/neutron/nifs.rs b/src/neutron/nifs.rs index 03e0de6d..d2f3504d 100644 --- a/src/neutron/nifs.rs +++ b/src/neutron/nifs.rs @@ -235,11 +235,16 @@ impl NIFS { 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::>(), num_cons, - num_vars + 1 + num_io, + num_vars + 2 + num_io, ); let B = A.clone(); let C = A.clone(); diff --git a/src/neutron/relation.rs b/src/neutron/relation.rs index 0bce2abe..4ee6e730 100644 --- a/src/neutron/relation.rs +++ b/src/neutron/relation.rs @@ -75,7 +75,7 @@ impl Structure { W: &FoldedWitness, ) -> 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 diff --git a/src/nova/circuit/mod.rs b/src/nova/circuit/mod.rs index 7b8b608c..3a5aba1f 100644 --- a/src/nova/circuit/mod.rs +++ b/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> 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::(); 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::(9830, 10361); - test_recursive_circuit_with::(9998, 10550); - test_recursive_circuit_with::(10277, 10973); + test_recursive_circuit_with::(9822, 10353); + test_recursive_circuit_with::(9990, 10542); + test_recursive_circuit_with::(10269, 10965); } } diff --git a/src/nova/circuit/r1cs.rs b/src/nova/circuit/r1cs.rs index b8b3ed8b..4a4892e4 100644 --- a/src/nova/circuit/r1cs.rs +++ b/src/nova/circuit/r1cs.rs @@ -9,8 +9,8 @@ use crate::{ util::{f_to_nat, Num}, }, utils::{ - alloc_bignat_constant, alloc_scalar_as_base, alloc_zero, conditionally_select, - conditionally_select2, conditionally_select_bignat, le_bits_to_num, + alloc_bignat_constant, alloc_scalar_as_base, conditionally_select, conditionally_select2, + conditionally_select_bignat, le_bits_to_num, }, }, r1cs::{R1CSInstance, RelaxedR1CSInstance}, @@ -55,7 +55,7 @@ impl AllocatedR1CSInstance { // so we can use it as a canonical representation for infinity. let (_, b, _, _) = E::GE::group_params(); if b != E::Base::ZERO { - let zero = alloc_zero(cs.namespace(|| "zero for absorb")); + let zero = AllocatedNum::zero::(); let x = conditionally_select2( cs.namespace(|| "select x"), &zero, @@ -205,7 +205,7 @@ impl AllocatedRelaxedR1CSInstance { // so we can use it as a canonical representation for infinity. let (_, b, _, _) = E::GE::group_params(); if b != E::Base::ZERO { - let zero = alloc_zero(cs.namespace(|| "zero for absorb")); + let zero = AllocatedNum::zero::(); // Absorb W let w_x = conditionally_select2( cs.namespace(|| "select W.x"), @@ -300,7 +300,7 @@ impl AllocatedRelaxedR1CSInstance { // When B != 0, use (0,0) for infinity let (_, b, _, _) = E::GE::group_params(); if b != E::Base::ZERO { - let zero = alloc_zero(cs.namespace(|| "zero for T absorb")); + let zero = AllocatedNum::zero::(); let t_x = conditionally_select2(cs.namespace(|| "select T.x"), &zero, &T.x, &T.is_infinity)?; let t_y = conditionally_select2(cs.namespace(|| "select T.y"), &zero, &T.y, &T.is_infinity)?; ro.absorb(&t_x); diff --git a/src/nova/mod.rs b/src/nova/mod.rs index 5d620828..bed8f6d1 100644 --- a/src/nova/mod.rs +++ b/src/nova/mod.rs @@ -1125,17 +1125,17 @@ mod tests { fn test_pp_digest() { test_pp_digest_with::( &TrivialCircuit::<_>::default(), - &expect!["5554dcef9f66efdf2477d0ada1f553f0e7edd9191391156edfca338cb270aa02"], + &expect!["38f70d85e696589d80905c20c8e7736d2f348d3361465cdf1de033bba7a54001"], ); test_pp_digest_with::( &TrivialCircuit::<_>::default(), - &expect!["a5ad54e26a84517739bde0fd1e56f10aa1f8321bfee234c347af0fb9b14bfb00"], + &expect!["71484b443e98587c2c2cc2938caf2d677eca117f179f24eb5d7f51cf271fe600"], ); test_pp_digest_with::( &TrivialCircuit::<_>::default(), - &expect!["b403daf596511f975656f8621269c1e885b60863aebd7a095000b599f6ed2802"], + &expect!["393f15fdeabf1cff656421f5e914ff3909f1d16f06aa24c57a8fd8723de66803"], ); } diff --git a/src/nova/nifs.rs b/src/nova/nifs.rs index bafc0602..b4b36439 100644 --- a/src/nova/nifs.rs +++ b/src/nova/nifs.rs @@ -446,29 +446,29 @@ mod tests { // `(Z2 + 5) * 1 - I1 = 0` // Relaxed R1CS is a set of three sparse matrices (A B C), where there is a row for every - // constraint and a column for every entry in z = (vars, u, inputs) + // constraint and a column for every entry in z = (vars, u, 0, inputs) // An R1CS instance is satisfiable iff: - // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, inputs) + // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, 0, inputs) let mut A: Vec<(usize, usize, E::Scalar)> = Vec::new(); let mut B: Vec<(usize, usize, E::Scalar)> = Vec::new(); let mut C: Vec<(usize, usize, E::Scalar)> = Vec::new(); // constraint 0 entries in (A,B,C) // `I0 * I0 - Z0 = 0` - A.push((0, num_vars + 1, one)); - B.push((0, num_vars + 1, one)); + A.push((0, num_vars + 2, one)); + B.push((0, num_vars + 2, one)); C.push((0, 0, one)); // constraint 1 entries in (A,B,C) // `Z0 * I0 - Z1 = 0` A.push((1, 0, one)); - B.push((1, num_vars + 1, one)); + B.push((1, num_vars + 2, one)); C.push((1, 1, one)); // constraint 2 entries in (A,B,C) // `(Z1 + I0) * 1 - Z2 = 0` A.push((2, 1, one)); - A.push((2, num_vars + 1, one)); + A.push((2, num_vars + 2, one)); B.push((2, num_vars, one)); C.push((2, 2, one)); @@ -477,20 +477,20 @@ mod tests { A.push((3, 2, one)); A.push((3, num_vars, one + one + one + one + one)); B.push((3, num_vars, one)); - C.push((3, num_vars + 2, one)); + C.push((3, num_vars + 3, one)); (num_cons, num_vars, num_io, A, B, C) }; // create a shape object let rows = num_cons; - let num_inputs = num_io + 1; + let num_inputs = num_io + 2; let cols = num_vars + num_inputs; let S = { let res = R1CSShape::new( num_cons, num_vars, - num_inputs - 1, + num_inputs - 2, SparseMatrix::new(&A, rows, cols), SparseMatrix::new(&B, rows, cols), SparseMatrix::new(&C, rows, cols), @@ -582,29 +582,29 @@ mod tests { // `(Z2 + 5) * 1 - I1 = 0` // Relaxed R1CS is a set of three sparse matrices (A B C), where there is a row for every - // constraint and a column for every entry in z = (vars, u, inputs) + // constraint and a column for every entry in z = (vars, u, 0, inputs) // An R1CS instance is satisfiable iff: - // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, inputs) + // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, 0, inputs) let mut A: Vec<(usize, usize, E::Scalar)> = Vec::new(); let mut B: Vec<(usize, usize, E::Scalar)> = Vec::new(); let mut C: Vec<(usize, usize, E::Scalar)> = Vec::new(); // constraint 0 entries in (A,B,C) // `I0 * I0 - Z0 = 0` - A.push((0, num_vars + 1, one)); - B.push((0, num_vars + 1, one)); + A.push((0, num_vars + 2, one)); + B.push((0, num_vars + 2, one)); C.push((0, 0, one)); // constraint 1 entries in (A,B,C) // `Z0 * I0 - Z1 = 0` A.push((1, 0, one)); - B.push((1, num_vars + 1, one)); + B.push((1, num_vars + 2, one)); C.push((1, 1, one)); // constraint 2 entries in (A,B,C) // `(Z1 + I0) * 1 - Z2 = 0` A.push((2, 1, one)); - A.push((2, num_vars + 1, one)); + A.push((2, num_vars + 2, one)); B.push((2, num_vars, one)); C.push((2, 2, one)); @@ -613,20 +613,20 @@ mod tests { A.push((3, 2, one)); A.push((3, num_vars, one + one + one + one + one)); B.push((3, num_vars, one)); - C.push((3, num_vars + 2, one)); + C.push((3, num_vars + 3, one)); (num_cons, num_vars, num_io, A, B, C) }; // create a shape object let rows = num_cons; - let num_inputs = num_io + 1; + let num_inputs = num_io + 2; let cols = num_vars + num_inputs; let S = { let res = R1CSShape::new( num_cons, num_vars, - num_inputs - 1, + num_inputs - 2, SparseMatrix::new(&A, rows, cols), SparseMatrix::new(&B, rows, cols), SparseMatrix::new(&C, rows, cols), diff --git a/src/r1cs/mod.rs b/src/r1cs/mod.rs index 0e8a90f5..ac4ff220 100644 --- a/src/r1cs/mod.rs +++ b/src/r1cs/mod.rs @@ -156,7 +156,7 @@ impl R1CSShape { -> Result, NovaError> { M.iter() .map(|(row, col, _val)| { - if row >= num_cons || col > num_io + num_vars { + if row >= num_cons || col > num_io + num_vars + 1 { Err(NovaError::InvalidIndex) } else { Ok(()) @@ -367,12 +367,12 @@ impl R1CSShape { } // Checks regularity conditions on the R1CSShape, required in Spartan-class SNARKs - // Returns false if num_cons or num_vars are not powers of two, or if num_io > num_vars + // Returns false if num_cons or num_vars are not powers of two, or if num_io+2 > num_vars #[inline] pub(crate) fn is_regular_shape(&self) -> bool { let cons_valid = self.num_cons.next_power_of_two() == self.num_cons; let vars_valid = self.num_vars.next_power_of_two() == self.num_vars; - let io_lt_vars = self.num_io < self.num_vars; + let io_lt_vars = self.num_io + 1 < self.num_vars; cons_valid && vars_valid && io_lt_vars } @@ -381,7 +381,7 @@ impl R1CSShape { &self, z: &[E::Scalar], ) -> Result<(Vec, Vec, Vec), NovaError> { - if z.len() != self.num_io + self.num_vars + 1 { + if z.len() != self.num_io + self.num_vars + 2 { return Err(NovaError::InvalidWitnessLength); } @@ -416,7 +416,7 @@ impl R1CSShape { ), NovaError, > { - if z1.len() != self.num_io + self.num_vars + 1 || z2.len() != self.num_io + self.num_vars + 1 { + if z1.len() != self.num_io + self.num_vars + 2 || z2.len() != self.num_io + self.num_vars + 2 { return Err(NovaError::InvalidWitnessLength); } @@ -456,7 +456,7 @@ impl R1CSShape { // verify if Az * Bz = u*Cz + E let res_eq = { - 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.multiply_vec(&z)?; assert_eq!(Az.len(), self.num_cons); assert_eq!(Bz.len(), self.num_cons); @@ -501,7 +501,12 @@ impl R1CSShape { // verify if Az * Bz = u*Cz let res_eq = { - let z = [W.W.clone(), vec![E::Scalar::ONE], U.X.clone()].concat(); + let z = [ + W.W.clone(), + vec![E::Scalar::ONE, E::Scalar::ZERO], + U.X.clone(), + ] + .concat(); let (Az, Bz, Cz) = self.multiply_vec(&z)?; assert_eq!(Az.len(), self.num_cons); assert_eq!(Bz.len(), self.num_cons); @@ -541,7 +546,7 @@ impl R1CSShape { ) -> Result<(Vec, Commitment), NovaError> { // The following code uses the optimization suggested in // Section 5.2 of [Mova](https://eprint.iacr.org/2024/1220.pdf) - let z_len = W1.W.len() + 1 + U1.X.len(); + let z_len = W1.W.len() + 2 + U1.X.len(); let Z = if z_len <= PARALLEL_THRESHOLD { let mut z = Vec::with_capacity(z_len); W1.W @@ -549,14 +554,20 @@ impl R1CSShape { .zip(W2.W.iter()) .for_each(|(w1, w2)| z.push(*w1 + *w2)); z.push(U1.u + E::Scalar::ONE); + z.push(E::Scalar::ZERO); U1.X .iter() .zip(U2.X.iter()) .for_each(|(x1, x2)| z.push(*x1 + *x2)); z } else { - let Z1 = [W1.W.clone(), vec![U1.u], U1.X.clone()].concat(); - let Z2 = [W2.W.clone(), vec![E::Scalar::ONE], U2.X.clone()].concat(); + let Z1 = [W1.W.clone(), vec![U1.u, E::Scalar::ZERO], U1.X.clone()].concat(); + let Z2 = [ + W2.W.clone(), + vec![E::Scalar::ONE, E::Scalar::ZERO], + U2.X.clone(), + ] + .concat(); Z1.into_par_iter() .zip(Z2.into_par_iter()) .map(|(z1, z2)| z1 + z2) @@ -590,8 +601,8 @@ impl R1CSShape { W2: &RelaxedR1CSWitness, r_T: &E::Scalar, ) -> Result<(Vec, Commitment), NovaError> { - let Z1 = [W1.W.clone(), vec![U1.u], U1.X.clone()].concat(); - let Z2 = [W2.W.clone(), vec![U2.u], U2.X.clone()].concat(); + let Z1 = [W1.W.clone(), vec![U1.u, E::Scalar::ZERO], U1.X.clone()].concat(); + let Z2 = [W2.W.clone(), vec![U2.u, E::Scalar::ZERO], U2.X.clone()].concat(); // The following code uses the optimization suggested in // Section 5.2 of [Mova](https://eprint.iacr.org/2024/1220.pdf) @@ -696,7 +707,7 @@ impl R1CSShape { return self.clone(); } - let num_vars_padded = max(self.num_vars, self.num_io + 1).next_power_of_two(); + let num_vars_padded = max(self.num_vars, self.num_io + 2).next_power_of_two(); let num_cons_padded = self.num_cons.next_power_of_two(); let apply_pad = |mut M: SparseMatrix| -> SparseMatrix { @@ -742,12 +753,15 @@ impl R1CSShape { &self, ck: &CommitmentKey, ) -> Result<(RelaxedR1CSInstance, RelaxedR1CSWitness), NovaError> { - // sample Z = (W, u, X) - let Z = (0..self.num_vars + self.num_io + 1) + // sample Z = (W, u, 0, X) + let mut Z = (0..self.num_vars + self.num_io + 2) .into_par_iter() .map(|_| E::Scalar::random(&mut OsRng)) .collect::>(); + // Force the zero-wire position to be zero + Z[self.num_vars + 1] = E::Scalar::ZERO; + let r_W = E::Scalar::random(&mut OsRng); let r_E = E::Scalar::random(&mut OsRng); @@ -774,7 +788,7 @@ impl R1CSShape { comm_W, comm_E, u, - X: Z[self.num_vars + 1..].to_vec(), + X: Z[self.num_vars + 2..].to_vec(), }, RelaxedR1CSWitness { W: Z[..self.num_vars].to_vec(), @@ -1305,29 +1319,29 @@ mod tests { // `(Z2 + 5) * 1 - I1 = 0` // Relaxed R1CS is a set of three sparse matrices (A B C), where there is a row for every - // constraint and a column for every entry in z = (vars, u, inputs) + // constraint and a column for every entry in z = (vars, u, 0, inputs) // An R1CS instance is satisfiable iff: - // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, inputs) + // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, 0, inputs) let mut A: Vec<(usize, usize, E::Scalar)> = Vec::new(); let mut B: Vec<(usize, usize, E::Scalar)> = Vec::new(); let mut C: Vec<(usize, usize, E::Scalar)> = Vec::new(); // constraint 0 entries in (A,B,C) // `I0 * I0 - Z0 = 0` - A.push((0, num_vars + 1, one)); - B.push((0, num_vars + 1, one)); + A.push((0, num_vars + 2, one)); + B.push((0, num_vars + 2, one)); C.push((0, 0, one)); // constraint 1 entries in (A,B,C) // `Z0 * I0 - Z1 = 0` A.push((1, 0, one)); - B.push((1, num_vars + 1, one)); + B.push((1, num_vars + 2, one)); C.push((1, 1, one)); // constraint 2 entries in (A,B,C) // `(Z1 + I0) * 1 - Z2 = 0` A.push((2, 1, one)); - A.push((2, num_vars + 1, one)); + A.push((2, num_vars + 2, one)); B.push((2, num_vars, one)); C.push((2, 2, one)); @@ -1336,14 +1350,14 @@ mod tests { A.push((3, 2, one)); A.push((3, num_vars, one + one + one + one + one)); B.push((3, num_vars, one)); - C.push((3, num_vars + 2, one)); + C.push((3, num_vars + 3, one)); (num_cons, num_vars, num_io, A, B, C) }; // create a shape object let rows = num_cons; - let cols = num_vars + num_io + 1; + let cols = num_vars + num_io + 2; let res = R1CSShape::new( num_cons, @@ -1420,9 +1434,9 @@ mod tests { fn test_multiply_vec_pair_with() { // tiny_r1cs(4) has num_cons=4, num_vars=4, num_io=2 - // z has length num_vars + 1 + num_io = 7 + // z has length num_vars + 2 + num_io = 8 let S = tiny_r1cs::(4); - let z_len = S.num_vars + 1 + S.num_io; + let z_len = S.num_vars + 2 + S.num_io; let z1: Vec = (1..=z_len as u64).map(E::Scalar::from).collect(); let z2: Vec = (10..10 + z_len as u64).map(E::Scalar::from).collect(); diff --git a/src/spartan/ppsnark.rs b/src/spartan/ppsnark.rs index d38f9331..0c80033b 100644 --- a/src/spartan/ppsnark.rs +++ b/src/spartan/ppsnark.rs @@ -1073,7 +1073,7 @@ impl> RelaxedR1CSSNARKTrait for Relax transcript.absorb(b"U", U); // compute the full satisfying assignment by concatenating W.W, U.u, and U.X - 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(); // compute Az, Bz, Cz let (Az, Bz, Cz) = S.multiply_vec(&z)?; @@ -1539,7 +1539,7 @@ impl> RelaxedR1CSSNARKTrait for Relax let eval_X = { // public IO is (u, X) - let X = vec![U.u] + let X = vec![U.u, E::Scalar::ZERO] .into_iter() .chain(U.X.iter().cloned()) .collect::>(); diff --git a/src/spartan/snark.rs b/src/spartan/snark.rs index 4c6148d3..e4482a46 100644 --- a/src/spartan/snark.rs +++ b/src/spartan/snark.rs @@ -130,7 +130,7 @@ impl> RelaxedR1CSSNARKTrait for Relax transcript.absorb(b"U", U); // compute the full satisfying assignment by concatenating W.W, U.u, and U.X - let mut z = [W.W.clone(), vec![U.u], U.X.clone()].concat(); + let mut z = [W.W.clone(), vec![U.u, E::Scalar::ZERO], U.X.clone()].concat(); let (num_rounds_x, num_rounds_y) = ( usize::try_from(S.num_cons.ilog2()).unwrap(), @@ -310,7 +310,7 @@ impl> RelaxedR1CSSNARKTrait for Relax let eval_Z = { let eval_X = { // public IO is (u, X) - let X = vec![U.u] + let X = vec![U.u, E::Scalar::ZERO] .into_iter() .chain(U.X.iter().cloned()) .collect::>();