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_alloc_bit<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
10  cs: &mut CS,
11) -> Result<(), SynthesisError> {
12  // get two bits as input and check that they are indeed bits
13  let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?;
14  let _ = a.inputize(cs.namespace(|| "a is input"));
15  cs.enforce(
16    || "check a is 0 or 1",
17    |lc| lc + CS::one() - a.get_variable(),
18    |lc| lc + a.get_variable(),
19    |lc| lc,
20  );
21  let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?;
22  let _ = b.inputize(cs.namespace(|| "b is input"));
23  cs.enforce(
24    || "check b is 0 or 1",
25    |lc| lc + CS::one() - b.get_variable(),
26    |lc| lc + b.get_variable(),
27    |lc| lc,
28  );
29  Ok(())
30}
31
32#[test]
33fn test_alloc_bit() {
34  type G = pasta_curves::pallas::Point;
35
36  // First create the shape
37  let mut cs: ShapeCS<G> = ShapeCS::new();
38  let _ = synthesize_alloc_bit(&mut cs);
39  let shape = cs.r1cs_shape();
40  let gens = cs.r1cs_gens();
41  println!("Mult mod constraint no: {}", cs.num_constraints());
42
43  // Now get the assignment
44  let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
45  let _ = synthesize_alloc_bit(&mut cs);
46  let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
47
48  // Make sure that this is satisfiable
49  assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
50}