Skip to content

Commit

Permalink
test: Tests for polynomial & bignat circuits (#205)
Browse files Browse the repository at this point in the history
- Used struct `PolynomialMultiplier` with a corresponding test
- Added `proptest` to dependencies for property-based testing
- Created property-based test to verify big number decomposition under various conditions
  • Loading branch information
huitseeker authored Jul 17, 2023
1 parent 82ca5fe commit 87499b3
Show file tree
Hide file tree
Showing 2 changed files with 79 additions and 1 deletion.
1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
79 changes: 78 additions & 1 deletion src/gadgets/nonnative/bignat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -783,7 +783,9 @@ impl<Scalar: PrimeField> Polynomial<Scalar> {
#[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>,
Expand Down Expand Up @@ -818,4 +820,79 @@ mod tests {
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());
}
}
}

0 comments on commit 87499b3

Please sign in to comment.