From 648eb0bb6eb9b98214627f2c061dee967480da93 Mon Sep 17 00:00:00 2001 From: porcuquine <1746729+porcuquine@users.noreply.github.com> Date: Fri, 8 Apr 2022 06:30:52 -0700 Subject: [PATCH] Fix CS::one() bug in solver. (#24) * Test and fix solver CS::one() bug. * Remove unused linear-combination evaluations. * rustfmt * Clippy. Co-authored-by: porcuquine --- src/bellperson/r1cs.rs | 2 +- src/bellperson/solver.rs | 54 +++++----------------------- tests/num.rs | 77 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 87 insertions(+), 46 deletions(-) create mode 100644 tests/num.rs diff --git a/src/bellperson/r1cs.rs b/src/bellperson/r1cs.rs index eabf04b..afed62f 100644 --- a/src/bellperson/r1cs.rs +++ b/src/bellperson/r1cs.rs @@ -42,7 +42,7 @@ where gens: &R1CSGens, ) -> Result<(R1CSInstance, R1CSWitness), NovaError> { let W = R1CSWitness::::new(shape, &self.aux_assignment)?; - let X = &self.input_assignment; + let X = &self.input_assignment[1..]; let comm_W = W.commit(gens); diff --git a/src/bellperson/solver.rs b/src/bellperson/solver.rs index d1899d0..39aca5e 100644 --- a/src/bellperson/solver.rs +++ b/src/bellperson/solver.rs @@ -1,6 +1,6 @@ //! Support for generating R1CS witness using bellperson. -use crate::traits::Group; +use crate::traits::{Group, PrimeField as PF}; use ff::PrimeField; use bellperson::{ @@ -91,14 +91,18 @@ where type Root = Self; fn new() -> Self { + let input_assignment = vec![G::Scalar::one()]; + let mut d = DensityTracker::new(); + d.add_element(); + Self { a_aux_density: DensityTracker::new(), - b_input_density: DensityTracker::new(), + b_input_density: d, b_aux_density: DensityTracker::new(), a: vec![], b: vec![], c: vec![], - input_assignment: vec![], + input_assignment, aux_assignment: vec![], } } @@ -128,7 +132,7 @@ where Ok(Variable(Index::Input(self.input_assignment.len() - 1))) } - fn enforce(&mut self, _: A, a: LA, b: LB, c: LC) + fn enforce(&mut self, _: A, _a: LA, _b: LB, _c: LC) where A: FnOnce() -> AR, AR: Into, @@ -136,47 +140,7 @@ where LB: FnOnce(LinearCombination) -> LinearCombination, LC: FnOnce(LinearCombination) -> LinearCombination, { - let a = a(LinearCombination::zero()); - let b = b(LinearCombination::zero()); - let c = c(LinearCombination::zero()); - - let input_assignment = &self.input_assignment; - let aux_assignment = &self.aux_assignment; - let a_aux_density = &mut self.a_aux_density; - let b_input_density = &mut self.b_input_density; - let b_aux_density = &mut self.b_aux_density; - - let a_res = a.eval( - // Inputs have full density in the A query - // because there are constraints of the - // form x * 0 = 0 for each input. - None, - Some(a_aux_density), - input_assignment, - aux_assignment, - ); - - let b_res = b.eval( - Some(b_input_density), - Some(b_aux_density), - input_assignment, - aux_assignment, - ); - - let c_res = c.eval( - // There is no C polynomial query, - // though there is an (beta)A + (alpha)B + C - // query for all aux variables. - // However, that query has full density. - None, - None, - input_assignment, - aux_assignment, - ); - - self.a.push(a_res); - self.b.push(b_res); - self.c.push(c_res); + // Do nothing: we don't care about linear-combination evaluations in this context. } fn push_namespace(&mut self, _: N) diff --git a/tests/num.rs b/tests/num.rs new file mode 100644 index 0000000..a0f5b5a --- /dev/null +++ b/tests/num.rs @@ -0,0 +1,77 @@ +use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; +use ff::PrimeField; +use nova_snark::bellperson::{ + r1cs::{NovaShape, NovaWitness}, + shape_cs::ShapeCS, + solver::SatisfyingAssignment, +}; + +fn synthesize_use_cs_one>( + cs: &mut CS, +) -> Result<(), SynthesisError> { + let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?; + let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?; + cs.enforce( + || "check a = b", + |lc| lc + a.get_variable() - b.get_variable(), + |lc| lc + CS::one(), + |lc| lc, + ); + let _ = a.inputize(cs.namespace(|| "a is input")); + let _ = b.inputize(cs.namespace(|| "b is input")); + Ok(()) +} + +fn synthesize_use_cs_one_after_inputize>( + cs: &mut CS, +) -> Result<(), SynthesisError> { + let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?; + let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?; + let _ = a.inputize(cs.namespace(|| "a is input")); + cs.enforce( + || "check a = b", + |lc| lc + a.get_variable() - b.get_variable(), + |lc| lc + CS::one(), + |lc| lc, + ); + let _ = b.inputize(cs.namespace(|| "b is input")); + Ok(()) +} + +#[test] +fn test_use_cs_one() { + type G = pasta_curves::pallas::Point; + + //First create the shape + let mut cs: ShapeCS = ShapeCS::new(); + let _ = synthesize_use_cs_one(&mut cs); + let shape = cs.r1cs_shape(); + let gens = cs.r1cs_gens(); + + //Now get the assignment + let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); + let _ = synthesize_use_cs_one(&mut cs); + let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap(); + + //Make sure that this is satisfiable + assert!(shape.is_sat(&gens, &inst, &witness).is_ok()); +} + +#[test] +fn test_use_cs_one_after_inputize() { + type G = pasta_curves::pallas::Point; + + //First create the shape + let mut cs: ShapeCS = ShapeCS::new(); + let _ = synthesize_use_cs_one_after_inputize(&mut cs); + let shape = cs.r1cs_shape(); + let gens = cs.r1cs_gens(); + + //Now get the assignment + let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); + let _ = synthesize_use_cs_one_after_inputize(&mut cs); + let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap(); + + //Make sure that this is satisfiable + assert!(shape.is_sat(&gens, &inst, &witness).is_ok()); +}