chore: test blackbox binary op instructions

acvm-repo/acir/src/circuit/mod.rs

@@ -377,18 +377,21 @@ mod tests {
             output: Witness(3),
         })
     }
+
     fn range_opcode<F: AcirField>() -> Opcode<F> {
         Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
             input: FunctionInput::witness(Witness(1), 8),
         })
     }
+
     fn keccakf1600_opcode<F: AcirField>() -> Opcode<F> {
         let inputs: Box<[FunctionInput<F>; 25]> =
             Box::new(std::array::from_fn(|i| FunctionInput::witness(Witness(i as u32 + 1), 8)));
         let outputs: Box<[Witness; 25]> = Box::new(std::array::from_fn(|i| Witness(i as u32 + 26)));
 
         Opcode::BlackBoxFuncCall(BlackBoxFuncCall::Keccakf1600 { inputs, outputs })
     }
+
     fn schnorr_verify_opcode<F: AcirField>() -> Opcode<F> {
         let public_key_x = FunctionInput::witness(Witness(1), FieldElement::max_num_bits());
         let public_key_y = FunctionInput::witness(Witness(2), FieldElement::max_num_bits());

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

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])

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<FieldElement>,
+        Option<FieldElement>,
+    ) -> BlackBoxFuncCall<FieldElement>,
+    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<FieldElement>,
+) -> FunctionInput<FieldElement> {
+    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<FieldElement>, y: Option<FieldElement>) -> BlackBoxFuncCall<FieldElement> {
+    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<FieldElement>, y: Option<FieldElement>) -> BlackBoxFuncCall<FieldElement> {
+    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<FieldElement>, Option<FieldElement>) -> BlackBoxFuncCall<FieldElement>,
+    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<FieldElement>, Option<FieldElement>) -> BlackBoxFuncCall<FieldElement>,
+    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<FieldElement>, Option<FieldElement>) -> BlackBoxFuncCall<FieldElement>,
+    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<FieldElement>, Option<FieldElement>) -> BlackBoxFuncCall<FieldElement>,
+    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::<u128>(), "[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);
+    }
+}