M Cargo.toml → Cargo.toml

@@ -48,6 +48,7 @@ hex = "0.4.3"
 pprof = { version = "0.11" }
 cfg-if = "1.0.0"
 sha2 = "0.10.7"
+proptest = "1.2.0"
 
 [[bench]]
 name = "recursive-snark"

M src/gadgets/nonnative/bignat.rs → src/gadgets/nonnative/bignat.rs

@@ -783,7 +783,9 @@
 #[cfg(test)]
 mod tests {
   use super::*;
-  use bellperson::Circuit;
+  use bellperson::{gadgets::test::TestConstraintSystem, Circuit};
+  use pasta_curves::pallas::Scalar;
+  use proptest::prelude::*;
 
   pub struct PolynomialMultiplier<Scalar: PrimeField> {
     pub a: Vec<Scalar>,
@@ -816,6 +818,81 @@ values: Some(self.b),
       };
       let _prod = a.alloc_product(cs.namespace(|| "product"), &b)?;
       Ok(())
+    }
+  }
+
+  #[test]
+  fn test_polynomial_multiplier_circuit() {
+    let mut cs = TestConstraintSystem::<pasta_curves::pallas::Scalar>::new();
+
+    let circuit = PolynomialMultiplier {
+      a: [1, 1, 1].iter().map(|i| Scalar::from_u128(*i)).collect(),
+      b: [1, 1].iter().map(|i| Scalar::from_u128(*i)).collect(),
+    };
+
+    circuit.synthesize(&mut cs).expect("synthesis failed");
+
+    if let Some(token) = cs.which_is_unsatisfied() {
+      eprintln!("Error: {} is unsatisfied", token);
+    }
+  }
+
+  #[derive(Debug)]
+  pub struct BigNatBitDecompInputs {
+    pub n: BigInt,
+  }
+
+  pub struct BigNatBitDecompParams {
+    pub limb_width: usize,
+    pub n_limbs: usize,
+  }
+
+  pub struct BigNatBitDecomp {
+    inputs: Option<BigNatBitDecompInputs>,
+    params: BigNatBitDecompParams,
+  }
+
+  impl<Scalar: PrimeField> Circuit<Scalar> for BigNatBitDecomp {
+    fn synthesize<CS: ConstraintSystem<Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
+      let n = BigNat::alloc_from_nat(
+        cs.namespace(|| "n"),
+        || Ok(self.inputs.grab()?.n.clone()),
+        self.params.limb_width,
+        self.params.n_limbs,
+      )?;
+      n.decompose(cs.namespace(|| "decomp"))?;
+      Ok(())
+    }
+  }
+
+  proptest! {
+
+    #![proptest_config(ProptestConfig {
+      cases: 10, // this test is costlier as max n gets larger
+      .. ProptestConfig::default()
+    })]
+    #[test]
+    fn test_big_nat_can_decompose(n in any::<u16>(), limb_width in 40u8..200) {
+        let n = n as usize;
+
+        let n_limbs = if n == 0 {
+            1
+        } else {
+            (n - 1) / limb_width as usize + 1
+        };
+
+        let circuit = BigNatBitDecomp {
+           inputs: Some(BigNatBitDecompInputs {
+                n: BigInt::from(n),
+            }),
+            params: BigNatBitDecompParams {
+                limb_width: limb_width as usize,
+                n_limbs,
+            },
+        };
+        let mut cs = TestConstraintSystem::<pasta_curves::pallas::Scalar>::new();
+        circuit.synthesize(&mut cs).expect("synthesis failed");
+        prop_assert!(cs.is_satisfied());
     }
   }
 }