Skip to content

Commit

Permalink
fix: prop_test_is_less_than_safe (#58)
Browse files Browse the repository at this point in the history
This test doesn't run any prover so the input must satisfy range check
assumption. More serious coverage is provided by
`prop_test_neg_is_less_than_safe`
  • Loading branch information
jonathanpwang authored May 23, 2023
1 parent bebfb39 commit 71cfc51
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 11 deletions.
7 changes: 4 additions & 3 deletions halo2-base/src/gates/tests/pos_prop_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -261,18 +261,19 @@ proptest! {
// Range Check Property Tests

#[test]
fn prop_test_is_less_than(a in rand_witness().prop_filter("not zero", |&x| *x.value() != Fr::zero()),
b in any::<u64>().prop_filter("not zero", |&x| x != 0),
fn prop_test_is_less_than(a in rand_witness(), b in any::<u64>().prop_filter("not zero", |&x| x != 0),
lookup_bits in 4..=16_usize) {
let bits = std::cmp::max(fe_to_biguint(a.value()).bits() as usize, bit_length(b));
let ground_truth = is_less_than_ground_truth((*a.value(), Fr::from(b)));
let result = range_gate_tests::test_is_less_than(([a, Witness(Fr::from(b))], bit_length(b), lookup_bits));
let result = range_gate_tests::test_is_less_than(([a, Witness(Fr::from(b))], bits, lookup_bits));
prop_assert_eq!(result, ground_truth);
}

#[test]
fn prop_test_is_less_than_safe(a in rand_fr().prop_filter("not zero", |&x| x != Fr::zero()),
b in any::<u64>().prop_filter("not zero", |&x| x != 0),
lookup_bits in 4..=16_usize) {
prop_assume!(fe_to_biguint(&a).bits() as usize <= bit_length(b));
let ground_truth = is_less_than_ground_truth((a, Fr::from(b)));
let result = range_gate_tests::test_is_less_than_safe((a, b, lookup_bits));
prop_assert_eq!(result, ground_truth);
Expand Down
18 changes: 10 additions & 8 deletions halo2-base/src/gates/tests/range_gate_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -86,22 +86,24 @@ pub fn test_check_big_less_than_safe<F: ScalarField + BigPrimeField>(
}

#[test_case(([0, 1].map(Fr::from).map(Witness), 3, 12) => Fr::from(1) ; "is_less_than() pos")]
pub fn test_is_less_than<F: ScalarField>(inputs: ([QuantumCell<F>; 2], usize, usize)) -> F {
pub fn test_is_less_than<F: ScalarField>(
(inputs, bits, lookup_bits): ([QuantumCell<F>; 2], usize, usize),
) -> F {
let mut builder = GateThreadBuilder::mock();
let ctx = builder.main(0);
let chip = RangeChip::default(inputs.2);
let a = chip.is_less_than(ctx, inputs.0[0], inputs.0[1], inputs.1);
let chip = RangeChip::default(lookup_bits);
let a = chip.is_less_than(ctx, inputs[0], inputs[1], bits);
*a.value()
}

#[test_case((Fr::zero(), 3, 3) => Fr::from(1) ; "is_less_than_safe() pos")]
pub fn test_is_less_than_safe<F: ScalarField>(inputs: (F, u64, usize)) -> F {
pub fn test_is_less_than_safe<F: ScalarField>((a, b, lookup_bits): (F, u64, usize)) -> F {
let mut builder = GateThreadBuilder::mock();
let ctx = builder.main(0);
let chip = RangeChip::default(inputs.2);
let a = ctx.assign_witnesses([inputs.0])[0];
let b = chip.is_less_than_safe(ctx, a, inputs.1);
*b.value()
let chip = RangeChip::default(lookup_bits);
let a = ctx.load_witness(a);
let lt = chip.is_less_than_safe(ctx, a, b);
*lt.value()
}

#[test_case((biguint_to_fe(&BigUint::from(2u64).pow(239)), BigUint::from(2u64).pow(240) - 1usize, 8) => Fr::from(1) ; "is_big_less_than_safe() pos")]
Expand Down

0 comments on commit 71cfc51

Please sign in to comment.