1use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
 2use ff::PrimeField;
 3use nova_snark::bellperson::{
 4  r1cs::{NovaShape, NovaWitness},
 5  shape_cs::ShapeCS,
 6  solver::SatisfyingAssignment,
 7};
 8
 9fn synthesize_use_cs_one<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
10  cs: &mut CS,
11) -> Result<(), SynthesisError> {
12  let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?;
13  let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?;
14  cs.enforce(
15    || "check a = b",
16    |lc| lc + a.get_variable() - b.get_variable(),
17    |lc| lc + CS::one(),
18    |lc| lc,
19  );
20  let _ = a.inputize(cs.namespace(|| "a is input"));
21  let _ = b.inputize(cs.namespace(|| "b is input"));
22  Ok(())
23}
24
25fn synthesize_use_cs_one_after_inputize<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
26  cs: &mut CS,
27) -> Result<(), SynthesisError> {
28  let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?;
29  let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?;
30  let _ = a.inputize(cs.namespace(|| "a is input"));
31  cs.enforce(
32    || "check a = b",
33    |lc| lc + a.get_variable() - b.get_variable(),
34    |lc| lc + CS::one(),
35    |lc| lc,
36  );
37  let _ = b.inputize(cs.namespace(|| "b is input"));
38  Ok(())
39}
40
41#[test]
42fn test_use_cs_one() {
43  type G = pasta_curves::pallas::Point;
44
45  //First create the shape
46  let mut cs: ShapeCS<G> = ShapeCS::new();
47  let _ = synthesize_use_cs_one(&mut cs);
48  let shape = cs.r1cs_shape();
49  let gens = cs.r1cs_gens();
50
51  //Now get the assignment
52  let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
53  let _ = synthesize_use_cs_one(&mut cs);
54  let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
55
56  //Make sure that this is satisfiable
57  assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
58}
59
60#[test]
61fn test_use_cs_one_after_inputize() {
62  type G = pasta_curves::pallas::Point;
63
64  //First create the shape
65  let mut cs: ShapeCS<G> = ShapeCS::new();
66  let _ = synthesize_use_cs_one_after_inputize(&mut cs);
67  let shape = cs.r1cs_shape();
68  let gens = cs.r1cs_gens();
69
70  //Now get the assignment
71  let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
72  let _ = synthesize_use_cs_one_after_inputize(&mut cs);
73  let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
74
75  //Make sure that this is satisfiable
76  assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
77}