Skip to content

Commit

Permalink
Fix and cleanup tests (#59)
Browse files Browse the repository at this point in the history 
* fix: `prop_test_is_less_than_safe` (#58)

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`

* fix: safe_types should use utils::testing common fns
  • Loading branch information
@jonathanpwang
jonathanpwang authored May 23, 2023
1 parent cd10fc0 commit b80135b
Show file tree
Hide file tree
Showing 3 changed files with 147 additions and 130 deletions.
7 changes: 4 additions & 3 deletions halo2-base/src/gates/tests/pos_prop_tests.rs
View file
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
View file
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
252 changes: 133 additions & 119 deletions halo2-base/src/safe_types/tests.rs
View file
Original file line number Diff line number Diff line change
@@ -1,91 +1,46 @@
use crate::halo2_proofs::{
halo2curves::bn256::{Bn256, Fr, G1Affine},
plonk::{create_proof, verify_proof, Circuit, ProvingKey, VerifyingKey},
poly::commitment::ParamsProver,
poly::kzg::{
commitment::KZGCommitmentScheme, commitment::ParamsKZG, multiopen::ProverSHPLONK,
multiopen::VerifierSHPLONK, strategy::SingleStrategy,
},
transcript::{
Blake2bRead, Blake2bWrite, Challenge255, TranscriptReadBuffer, TranscriptWriterBuffer,
},
use crate::{
halo2_proofs::{halo2curves::bn256::Fr, poly::kzg::commitment::ParamsKZG},
utils::testing::{check_proof, gen_proof},
};

use super::*;
use crate::{
gates::{
builder::{RangeCircuitBuilder, GateThreadBuilder},
builder::{GateThreadBuilder, RangeCircuitBuilder},
RangeChip,
},
halo2_proofs::{
plonk::keygen_pk,
plonk::{keygen_vk, Assigned},
},
};
use rand::rngs::OsRng;
use itertools::Itertools;
use super::*;
use rand::rngs::OsRng;
use std::env;

/// helper function to generate a proof with real prover
pub fn gen_proof(
params: &ParamsKZG<Bn256>,
pk: &ProvingKey<G1Affine>,
circuit: impl Circuit<Fr>,
) -> Vec<u8> {
let mut transcript = Blake2bWrite::<_, _, Challenge255<_>>::init(vec![]);
create_proof::<
KZGCommitmentScheme<Bn256>,
ProverSHPLONK<'_, Bn256>,
Challenge255<_>,
_,
Blake2bWrite<Vec<u8>, G1Affine, _>,
_,
>(params, pk, &[circuit], &[&[]], OsRng, &mut transcript)
.expect("prover should not fail");
transcript.finalize()
}

/// helper function to verify a proof
pub fn check_proof(
params: &ParamsKZG<Bn256>,
vk: &VerifyingKey<G1Affine>,
proof: &[u8],
// soundness checks for `raw_bytes_to` function
fn test_raw_bytes_to_gen<const BYTES_PER_ELE: usize, const TOTAL_BITS: usize>(
k: u32,
raw_bytes: &[Fr],
outputs: &[Fr],
expect_satisfied: bool,
) {
let verifier_params = params.verifier_params();
let strategy = SingleStrategy::new(params);
let mut transcript = Blake2bRead::<_, _, Challenge255<_>>::init(proof);
let res = verify_proof::<
KZGCommitmentScheme<Bn256>,
VerifierSHPLONK<'_, Bn256>,
Challenge255<G1Affine>,
Blake2bRead<&[u8], G1Affine, Challenge255<G1Affine>>,
SingleStrategy<'_, Bn256>,
>(verifier_params, vk, strategy, &[&[]], &mut transcript);

if expect_satisfied {
assert!(res.is_ok());
} else {
assert!(res.is_err());
}
}

// soundness checks for `raw_bytes_to` function
fn test_raw_bytes_to_gen<const BYTES_PER_ELE: usize, const TOTAL_BITS: usize>(k: u32, raw_bytes: &[Fr], outputs: &[Fr], expect_satisfied: bool) {
// first create proving and verifying key
let mut builder = GateThreadBuilder::<Fr>::keygen();
let lookup_bits = 3;
env::set_var("LOOKUP_BITS", lookup_bits.to_string());
let range_chip = RangeChip::<Fr>::default(lookup_bits);
let safe_type_chip = SafeTypeChip::new(&range_chip);

let dummy_raw_bytes = builder.main(0).assign_witnesses((0..raw_bytes.len()).map(|_| Fr::zero()).collect::<Vec<_>>());
let dummy_raw_bytes = builder
.main(0)
.assign_witnesses((0..raw_bytes.len()).map(|_| Fr::zero()).collect::<Vec<_>>());

let safe_value = safe_type_chip.raw_bytes_to::<BYTES_PER_ELE, TOTAL_BITS>(
builder.main(0),
dummy_raw_bytes);
let safe_value =
safe_type_chip.raw_bytes_to::<BYTES_PER_ELE, TOTAL_BITS>(builder.main(0), dummy_raw_bytes);
// get the offsets of the safe value cells for later 'pranking'
let safe_value_offsets = safe_value.value().iter().map(|v| v.cell.unwrap().offset).collect::<Vec<_>>();
let safe_value_offsets =
safe_value.value().iter().map(|v| v.cell.unwrap().offset).collect::<Vec<_>>();
// set env vars
builder.config(k as usize, Some(9));
let circuit = RangeCircuitBuilder::keygen(builder);
Expand All @@ -101,11 +56,10 @@ fn test_raw_bytes_to_gen<const BYTES_PER_ELE: usize, const TOTAL_BITS: usize>(k:
let mut builder = GateThreadBuilder::<Fr>::prover();
let range_chip = RangeChip::<Fr>::default(lookup_bits);
let safe_type_chip = SafeTypeChip::new(&range_chip);

let assigned_raw_bytes = builder.main(0).assign_witnesses(inputs.to_vec());
safe_type_chip.raw_bytes_to::<BYTES_PER_ELE, TOTAL_BITS>(
builder.main(0),
assigned_raw_bytes);
safe_type_chip
.raw_bytes_to::<BYTES_PER_ELE, TOTAL_BITS>(builder.main(0), assigned_raw_bytes);
// prank the safe value cells
for (offset, witness) in safe_value_offsets.iter().zip_eq(outputs) {
builder.main(0).advice[*offset] = Assigned::<Fr>::Trivial(*witness);
Expand Down Expand Up @@ -134,37 +88,70 @@ fn test_raw_bytes_to_uint256() {
const TOTAL_BITS: usize = SafeUint256::<Fr>::TOTAL_BITS;
let k = 11;
// [0x0; 32] -> [0x0, 0x0]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(k, &[Fr::from(0); 32], &[Fr::from(0), Fr::from(0)], true);
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(1)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
&[Fr::from(1), Fr::from(0)], true);
k,
&[Fr::from(0); 32],
&[Fr::from(0), Fr::from(0)],
true,
);
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(1)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
&[Fr::from(1), Fr::from(0)],
true,
);
// [0x1, 0x2] + [0x0; 30] -> [0x201, 0x0]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 30].as_slice()].concat(),
&[Fr::from(0x201), Fr::from(0)], true);
k,
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 30].as_slice()].concat(),
&[Fr::from(0x201), Fr::from(0)],
true,
);
// [[0xff; 32] -> [2^248 - 1, 0xff]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[Fr::from(0xff); 32],
&[Fr::from_raw([0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffff]), Fr::from(0xff)], true);
k,
&[Fr::from(0xff); 32],
&[
Fr::from_raw([
0xffffffffffffffff,
0xffffffffffffffff,
0xffffffffffffffff,
0xffffffffffffff,
]),
Fr::from(0xff),
],
true,
);

// invalid raw_bytes, last bytes > 0xff
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(0); 31].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(),
&[Fr::from(0), Fr::from(0xff)], false);
k,
&[[Fr::from(0); 31].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(),
&[Fr::from(0), Fr::from(0xff)],
false,
);
// 0xff != 0xff00000000000000000000000000000000000000000000000000000000000000
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(0xff)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
&[Fr::from(0), Fr::from(0xff)], false);
k,
&[[Fr::from(0xff)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
&[Fr::from(0), Fr::from(0xff)],
false,
);
// outputs overflow
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[Fr::from(0xff); 32],
&[Fr::from_raw([0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffff]), Fr::from(0x1ff)], false);
k,
&[Fr::from(0xff); 32],
&[
Fr::from_raw([
0xffffffffffffffff,
0xffffffffffffffff,
0xffffffffffffffff,
0xffffffffffffff,
]),
Fr::from(0x1ff),
],
false,
);
}

#[test]
Expand All @@ -176,30 +163,40 @@ fn test_raw_bytes_to_uint64() {
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(k, &[Fr::from(0); 8], &[Fr::from(0)], true);
// [0x1, 0x2] + [0x0; 6] -> [0x201]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 6].as_slice()].concat(),
&[Fr::from(0x201)], true);
k,
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 6].as_slice()].concat(),
&[Fr::from(0x201)],
true,
);
// [[0xff; 8] -> [2^64-1]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[Fr::from(0xff); 8],
&[Fr::from(0xffffffffffffffff)], true);
k,
&[Fr::from(0xff); 8],
&[Fr::from(0xffffffffffffffff)],
true,
);

// invalid raw_bytes, last bytes > 0xff
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(0); 7].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(),
&[Fr::from(0xff00000000000000)], false);
k,
&[[Fr::from(0); 7].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(),
&[Fr::from(0xff00000000000000)],
false,
);
// 0xff != 0xff00000000000000000000000000000000000000000000000000000000000000
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(0xff)].as_slice(), [Fr::from(0); 7].as_slice()].concat(),
&[Fr::from(0xff00000000000000)], false);
k,
&[[Fr::from(0xff)].as_slice(), [Fr::from(0); 7].as_slice()].concat(),
&[Fr::from(0xff00000000000000)],
false,
);
// outputs overflow
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[Fr::from(0xff); 8],
&[Fr::from_raw([0xffffffffffffffff, 0x1, 0x0, 0x0])], false);
k,
&[Fr::from(0xff); 8],
&[Fr::from_raw([0xffffffffffffffff, 0x1, 0x0, 0x0])],
false,
);
}

#[test]
Expand All @@ -208,35 +205,52 @@ fn test_raw_bytes_to_bytes32() {
const TOTAL_BITS: usize = SafeBytes32::<Fr>::TOTAL_BITS;
let k = 10;
// [0x0; 32] -> [0x0; 32]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(k, &[Fr::from(0); 32], &[Fr::from(0); 32], true);
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(1)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
&[[Fr::from(1)].as_slice(), [Fr::from(0); 31].as_slice()].concat(), true);
k,
&[Fr::from(0); 32],
&[Fr::from(0); 32],
true,
);
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(1)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
&[[Fr::from(1)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
true,
);
// [0x1, 0x2] + [0x0; 30] -> [0x201, 0x0]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 30].as_slice()].concat(),
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 30].as_slice()].concat(), true);
k,
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 30].as_slice()].concat(),
&[[Fr::from(1), Fr::from(2)].as_slice(), [Fr::from(0); 30].as_slice()].concat(),
true,
);
// [[0xff; 32] -> [2^248 - 1, 0xff]
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[Fr::from(0xff); 32],
&[Fr::from(0xff); 32], true);
k,
&[Fr::from(0xff); 32],
&[Fr::from(0xff); 32],
true,
);

// invalid raw_bytes, last bytes > 0xff
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[[Fr::from(0); 31].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(),
&[[Fr::from(0); 31].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(), false);
&[[Fr::from(0); 31].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(),
&[[Fr::from(0); 31].as_slice(), [Fr::from(0x1ff)].as_slice()].concat(),
false,
);
// 0xff != 0xff00000000000000000000000000000000000000000000000000000000000000
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
k,
&[[Fr::from(0xff)].as_slice(), [Fr::from(0); 31].as_slice()].concat(),
&[[Fr::from(0); 31].as_slice(), [Fr::from(0xff)].as_slice()].concat(), false);
&[[Fr::from(0); 31].as_slice(), [Fr::from(0xff)].as_slice()].concat(),
false,
);
// outputs overflow
test_raw_bytes_to_gen::<BYTES_PER_ELE, TOTAL_BITS>(
k,
&[Fr::from(0xff); 32],
&[Fr::from(0x1ff); 32], false);
}
k,
&[Fr::from(0xff); 32],
&[Fr::from(0x1ff); 32],
false,
);
}

0 comments on commit b80135b

Please sign in to comment.