diff --git a/Cargo.lock b/Cargo.lock index f6011b705e5..bd70c8fef2c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -48,6 +48,7 @@ dependencies = [ "brillig_vm", "indexmap 1.9.3", "num-bigint", + "proptest", "serde", "thiserror", "tracing", diff --git a/acvm-repo/acir/src/circuit/mod.rs b/acvm-repo/acir/src/circuit/mod.rs index 5d749e709b3..00d0933a3aa 100644 --- a/acvm-repo/acir/src/circuit/mod.rs +++ b/acvm-repo/acir/src/circuit/mod.rs @@ -377,11 +377,13 @@ mod tests { output: Witness(3), }) } + fn range_opcode() -> Opcode { Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE { input: FunctionInput::witness(Witness(1), 8), }) } + fn keccakf1600_opcode() -> Opcode { let inputs: Box<[FunctionInput; 25]> = Box::new(std::array::from_fn(|i| FunctionInput::witness(Witness(i as u32 + 1), 8))); @@ -389,6 +391,7 @@ mod tests { Opcode::BlackBoxFuncCall(BlackBoxFuncCall::Keccakf1600 { inputs, outputs }) } + fn schnorr_verify_opcode() -> Opcode { let public_key_x = FunctionInput::witness(Witness(1), FieldElement::max_num_bits()); let public_key_y = FunctionInput::witness(Witness(2), FieldElement::max_num_bits()); diff --git a/acvm-repo/acvm/Cargo.toml b/acvm-repo/acvm/Cargo.toml index 5b6397a1011..4cda53de241 100644 --- a/acvm-repo/acvm/Cargo.toml +++ b/acvm-repo/acvm/Cargo.toml @@ -38,3 +38,4 @@ bls12_381 = [ [dev-dependencies] ark-bls12-381 = { version = "^0.4.0", default-features = false, features = ["curve"] } +proptest.workspace = true diff --git a/acvm-repo/acvm/tests/solver.proptest-regressions b/acvm-repo/acvm/tests/solver.proptest-regressions new file mode 100644 index 00000000000..35627c1fbae --- /dev/null +++ b/acvm-repo/acvm/tests/solver.proptest-regressions @@ -0,0 +1,13 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc e4dd0e141df173f5dfdfb186bba4154247ec284b71d8f294fa3282da953a0e92 # shrinks to x = 0, y = 1 +cc 419ed6fdf1bf1f2513889c42ec86c665c9d0500ceb075cbbd07f72444dbd78c6 # shrinks to x = 266672725 +cc 0810fc9e126b56cf0a0ddb25e0dc498fa3b2f1980951550403479fc01c209833 # shrinks to modulus = [71, 253, 124, 216, 22, 140, 32, 60, 141, 202, 113, 104, 145, 106, 129, 151, 93, 88, 129, 129, 182, 69, 80, 184, 41, 160, 49, 225, 114, 78, 100, 48], zero_or_ones_constant = false, use_constant = false +cc 735ee9beb1a1dbb82ded6f30e544d7dfde149957e5d45a8c96fc65a690b6b71c # shrinks to (xs, modulus) = ([(0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (49, false)], [71, 253, 124, 216, 22, 140, 32, 60, 141, 202, 113, 104, 145, 106, 129, 151, 93, 88, 129, 129, 182, 69, 80, 184, 41, 160, 49, 225, 114, 78, 100, 48]) +cc ca81bc11114a2a2b34021f44ecc1e10cb018e35021ef4d728e07a6791dad38d6 # shrinks to (xs, modulus) = ([(0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (49, false)], [71, 253, 124, 216, 22, 140, 32, 60, 141, 202, 113, 104, 145, 106, 129, 151, 93, 88, 129, 129, 182, 69, 80, 184, 41, 160, 49, 225, 114, 78, 100, 48]) +cc 6c1d571a0111e6b4c244dc16da122ebab361e77b71db7770d638076ab21a717b # shrinks to (xs, modulus) = ([(0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (49, false)], [71, 253, 124, 216, 22, 140, 32, 60, 141, 202, 113, 104, 145, 106, 129, 151, 93, 88, 129, 129, 182, 69, 80, 184, 41, 160, 49, 225, 114, 78, 100, 48]) +cc ccb7061ab6b85e2554d00bf03d74204977ed7a4109d7e2d5c6b5aaa2179cfaf9 # shrinks to (xs, modulus) = ([(0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (0, false), (49, false)], [71, 253, 124, 216, 22, 140, 32, 60, 141, 202, 113, 104, 145, 106, 129, 151, 93, 88, 129, 129, 182, 69, 80, 184, 41, 160, 49, 225, 114, 78, 100, 48]) diff --git a/acvm-repo/acvm/tests/solver.rs b/acvm-repo/acvm/tests/solver.rs index e55dbb73ae1..279b0444609 100644 --- a/acvm-repo/acvm/tests/solver.rs +++ b/acvm-repo/acvm/tests/solver.rs @@ -5,7 +5,7 @@ use acir::{ brillig::{BinaryFieldOp, HeapArray, MemoryAddress, Opcode as BrilligOpcode, ValueOrArray}, circuit::{ brillig::{BrilligBytecode, BrilligInputs, BrilligOutputs}, - opcodes::{BlockId, BlockType, MemOp}, + opcodes::{BlackBoxFuncCall, BlockId, BlockType, FunctionInput, MemOp}, Opcode, OpcodeLocation, }, native_types::{Expression, Witness, WitnessMap}, @@ -16,6 +16,10 @@ use acvm::pwg::{ACVMStatus, ErrorLocation, ForeignCallWaitInfo, OpcodeResolution use acvm_blackbox_solver::StubbedBlackBoxSolver; use brillig_vm::brillig::HeapValueType; +use proptest::arbitrary::any; +use proptest::prelude::*; +use proptest::result::maybe_ok; + // Reenable these test cases once we move the brillig implementation of inversion down into the acvm stdlib. #[test] @@ -722,3 +726,187 @@ fn memory_operations() { assert_eq!(witness_map[&Witness(8)], FieldElement::from(6u128)); } + +// Solve the given BlackBoxFuncCall with witnesses: 1, 2 as x, y, resp. +#[cfg(test)] +fn solve_blackbox_func_call( + blackbox_func_call: impl Fn( + Option, + Option, + ) -> BlackBoxFuncCall, + x: (FieldElement, bool), // if false, use a Witness + y: (FieldElement, bool), // if false, use a Witness +) -> FieldElement { + let (x, x_constant) = x; + let (y, y_constant) = y; + + let initial_witness = WitnessMap::from(BTreeMap::from_iter([(Witness(1), x), (Witness(2), y)])); + + let mut lhs = None; + if x_constant { + lhs = Some(x); + } + + let mut rhs = None; + if y_constant { + rhs = Some(y); + } + + let op = Opcode::BlackBoxFuncCall(blackbox_func_call(lhs, rhs)); + let opcodes = vec![op]; + let unconstrained_functions = vec![]; + let mut acvm = + ACVM::new(&StubbedBlackBoxSolver, &opcodes, initial_witness, &unconstrained_functions, &[]); + let solver_status = acvm.solve(); + assert_eq!(solver_status, ACVMStatus::Solved); + let witness_map = acvm.finalize(); + + witness_map[&Witness(3)] +} + +fn function_input_from_option( + witness: Witness, + opt_constant: Option, +) -> FunctionInput { + opt_constant + .map(|constant| FunctionInput::constant(constant, FieldElement::max_num_bits())) + .unwrap_or(FunctionInput::witness(witness, FieldElement::max_num_bits())) +} + +fn and_op(x: Option, y: Option) -> BlackBoxFuncCall { + let lhs = function_input_from_option(Witness(1), x); + let rhs = function_input_from_option(Witness(2), y); + BlackBoxFuncCall::AND { lhs, rhs, output: Witness(3) } +} + +fn xor_op(x: Option, y: Option) -> BlackBoxFuncCall { + let lhs = function_input_from_option(Witness(1), x); + let rhs = function_input_from_option(Witness(2), y); + BlackBoxFuncCall::XOR { lhs, rhs, output: Witness(3) } +} + +fn prop_assert_commutative( + op: impl Fn(Option, Option) -> BlackBoxFuncCall, + x: (FieldElement, bool), + y: (FieldElement, bool), +) -> (FieldElement, FieldElement) { + (solve_blackbox_func_call(&op, x, y), solve_blackbox_func_call(&op, y, x)) +} + +fn prop_assert_associative( + op: impl Fn(Option, Option) -> BlackBoxFuncCall, + x: (FieldElement, bool), + y: (FieldElement, bool), + z: (FieldElement, bool), + use_constant_xy: bool, + use_constant_yz: bool, +) -> (FieldElement, FieldElement) { + let f_xy = (solve_blackbox_func_call(&op, x, y), use_constant_xy); + let f_f_xy_z = solve_blackbox_func_call(&op, f_xy, z); + + let f_yz = (solve_blackbox_func_call(&op, y, z), use_constant_yz); + let f_x_f_yz = solve_blackbox_func_call(&op, x, f_yz); + + (f_f_xy_z, f_x_f_yz) +} + +fn prop_assert_identity_l( + op: impl Fn(Option, Option) -> BlackBoxFuncCall, + op_identity: (FieldElement, bool), + x: (FieldElement, bool), +) -> (FieldElement, FieldElement) { + (solve_blackbox_func_call(op, op_identity, x), x.0) +} + +fn prop_assert_zero_l( + op: impl Fn(Option, Option) -> BlackBoxFuncCall, + op_zero: (FieldElement, bool), + x: (FieldElement, bool), +) -> (FieldElement, FieldElement) { + (solve_blackbox_func_call(op, op_zero, x), FieldElement::zero()) +} + +prop_compose! { + // Use both `u128` and hex proptest strategies + fn field_element() + (u128_or_hex in maybe_ok(any::(), "[0-9a-f]{64}"), + constant_input: bool) + -> (FieldElement, bool) + { + match u128_or_hex { + Ok(number) => (FieldElement::from(number), constant_input), + Err(hex) => (FieldElement::from_hex(&hex).expect("should accept any 32 byte hex string"), constant_input), + } + } +} + +fn field_element_ones() -> FieldElement { + let exponent: FieldElement = (253_u128).into(); + FieldElement::from(2u128).pow(&exponent) - FieldElement::one() +} + +proptest! { + + #[test] + fn and_commutative(x in field_element(), y in field_element()) { + let (lhs, rhs) = prop_assert_commutative(and_op, x, y); + prop_assert_eq!(lhs, rhs); + } + + #[test] + fn xor_commutative(x in field_element(), y in field_element()) { + let (lhs, rhs) = prop_assert_commutative(xor_op, x, y); + prop_assert_eq!(lhs, rhs); + } + + #[test] + fn and_associative(x in field_element(), y in field_element(), z in field_element(), use_constant_xy: bool, use_constant_yz: bool) { + let (lhs, rhs) = prop_assert_associative(and_op, x, y, z, use_constant_xy, use_constant_yz); + prop_assert_eq!(lhs, rhs); + } + + #[test] + // TODO(https://github.com/noir-lang/noir/issues/5638) + #[should_panic(expected = "assertion failed: `(left == right)`")] + fn xor_associative(x in field_element(), y in field_element(), z in field_element(), use_constant_xy: bool, use_constant_yz: bool) { + let (lhs, rhs) = prop_assert_associative(xor_op, x, y, z, use_constant_xy, use_constant_yz); + prop_assert_eq!(lhs, rhs); + } + + // test that AND(x, x) == x + #[test] + fn and_self_identity(x in field_element()) { + prop_assert_eq!(solve_blackbox_func_call(and_op, x, x), x.0); + } + + // test that XOR(x, x) == 0 + #[test] + fn xor_self_zero(x in field_element()) { + prop_assert_eq!(solve_blackbox_func_call(xor_op, x, x), FieldElement::zero()); + } + + #[test] + fn and_identity_l(x in field_element(), ones_constant: bool) { + let ones = (field_element_ones(), ones_constant); + let (lhs, rhs) = prop_assert_identity_l(and_op, ones, x); + if x <= ones { + prop_assert_eq!(lhs, rhs); + } else { + prop_assert!(lhs != rhs); + } + } + + #[test] + fn xor_identity_l(x in field_element(), zero_constant: bool) { + let zero = (FieldElement::zero(), zero_constant); + let (lhs, rhs) = prop_assert_identity_l(xor_op, zero, x); + prop_assert_eq!(lhs, rhs); + } + + #[test] + fn and_zero_l(x in field_element(), ones_constant: bool) { + let zero = (FieldElement::zero(), ones_constant); + let (lhs, rhs) = prop_assert_zero_l(and_op, zero, x); + prop_assert_eq!(lhs, rhs); + } +}