Fix CS::one() bug in solver.

src/bellperson/r1cs.rs

@@ -42,7 +42,7 @@ where
     gens: &R1CSGens<G>,
   ) -> Result<(R1CSInstance<G>, R1CSWitness<G>), NovaError> {
     let W = R1CSWitness::<G>::new(shape, &self.aux_assignment)?;
-    let X = &self.input_assignment;
+    let X = &self.input_assignment[1..];
 
     let comm_W = W.commit(gens);
 

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,55 +132,15 @@ where
     Ok(Variable(Index::Input(self.input_assignment.len() - 1)))
   }
 
-  fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, a: LA, b: LB, c: LC)
+  fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, _a: LA, _b: LB, _c: LC)
   where
     A: FnOnce() -> AR,
     AR: Into<String>,
     LA: FnOnce(LinearCombination<G::Scalar>) -> LinearCombination<G::Scalar>,
     LB: FnOnce(LinearCombination<G::Scalar>) -> LinearCombination<G::Scalar>,
     LC: FnOnce(LinearCombination<G::Scalar>) -> LinearCombination<G::Scalar>,
   {
-    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<NR, N>(&mut self, _: N)

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<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
+  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<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
+  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<G> = 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<G> = 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<G> = 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<G> = 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());
+}