From 7afd8f95a137b7b1ea5c72a58f17e32e3c7f3eca Mon Sep 17 00:00:00 2001 From: jewelofchaos9 Date: Mon, 17 Feb 2025 11:31:41 +0000 Subject: [PATCH] final report --- .../barretenberg/acir_formal_proofs/README.md | 58 ++++++++++--------- 1 file changed, 31 insertions(+), 27 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md index 5dd3a5a29182..dfb743b9f163 100644 --- a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md @@ -18,30 +18,34 @@ The verifier uses SMT (Satisfiability Modulo Theories) solving to formally verif ### Results -| Opcode | Lhs type/size | Rhs type/size | Time/seconds | Memory/GB | Success | SMT Term Type | Reason | -| ----------- | ------------- | ------------- | ------------ | --------- | ------- | ---------------- | -------------------------- | -| Binary::Add | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | | -| Binary::Add | Unsigned_127 | Unsigned_127 | 2.8 | - | ✓ | TermType::BVTerm | | -| Binary::And | Unsigned_32 | Unsigned_32 | 6.7 | - | ✓ | TermType::BVTerm | | -| Binary::And | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | Probably bug in smt solver | -| Binary::Div | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | | -| Binary::Div | Unsigned_126 | Unsigned_126 | 402.7 | 3.5 | ✗ | TermType::BVTerm | Analysis in progress | -| Binary::Div | Signed_126 | Signed_126 | >17 days | 5.1 | ✗ | TermType::ITerm | Test takes too long | -| Binary::Eq | Field | Field | 19.2 | - | ✓ | TermType::FFTerm | | -| Binary::Eq | Unsigned_127 | Unsigned_127 | 22.8 | - | ✓ | TermType::BVTerm | | -| Binary::Lt | Unsigned_127 | Unsigned_127 | 56.7 | - | ✓ | TermType::BVTerm | | -| Binary::Mod | Unsigned_127 | Unsigned_127 | - | 3.2 | ✗ | TermType::BVTerm | Analysis in progress | -| Binary::Mul | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | | -| Binary::Mul | Unsigned_127 | Unsigned_127 | 10.0 | - | ✓ | TermType::BVTerm | | -| Binary::Or | Unsigned_32 | Unsigned_32 | 18.0 | - | ✓ | TermType::BVTerm | | -| Binary::Or | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | Probably bug in smt solver | -| Binary::Shl | Unsigned_64 | Unsigned_8 | 42331.61 | 63.2 | ✓ | TermType::BVTerm | | -| Binary::Shl | Unsigned_32 | Unsigned_8 | 4574.0 | 30 | ✓ | TermType::BVTerm | | -| Binary::Shr | Unsigned_64 | Unsigned_8 | 3927.88 | 10 | ✓ | TermType::BVTerm | | -| Binary::Sub | Unsigned_127 | Unsigned_127 | 3.3 | - | ✓ | TermType::BVTerm | | -| Binary::Xor | Unsigned_32 | Unsigned_32 | 14.7 | - | ✓ | TermType::BVTerm | | -| Binary::Xor | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | Probably bug in smt solver | -| Not | Unsigned_127 | - | 0.2 | - | ✓ | TermType::BVTerm | | - - -Each test attempts to find counterexamples that violate the expected behavior. A passing test indicates the operation is correctly implemented, while a failing test reveals potential issues. \ No newline at end of file +| Opcode | Lhs type/size | Rhs type/size | Time/seconds | Memory/GB | Success | SMT Term Type | Reason | +| ----------- | ------------- | ------------- | ------------ | --------- | ------- | ---------------- | ------------------------------------------------------------------------------------------------------------- | +| Binary::Add | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | | +| Binary::Add | Unsigned_127 | Unsigned_127 | 2.8 | - | ✓ | TermType::BVTerm | | +| Binary::And | Unsigned_32 | Unsigned_32 | 6.7 | - | ✓ | TermType::BVTerm | | +| Binary::And | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | [smt solver lookup doesnt support 2bits tables](https://github.com/AztecProtocol/aztec-packages/issues/11721) | +| Binary::Div | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | | +| Binary::Div | Unsigned_126 | Unsigned_126 | 402.7 | 3.5 | ✗ | TermType::BVTerm | [Field and bitvector logic mixing](https://github.com/AztecProtocol/aztec-packages/issues/11722) | +| Binary::Div | Signed_126 | Signed_126 | >17 days | 5.1 | ✗ | TermType::BVTerm | [Field and bitvector logic mixing](https://github.com/AztecProtocol/aztec-packages/issues/11722) | +| Binary::Eq | Field | Field | 19.2 | - | ✓ | TermType::FFTerm | | +| Binary::Eq | Unsigned_127 | Unsigned_127 | 22.8 | - | ✓ | TermType::BVTerm | | +| Binary::Lt | Unsigned_127 | Unsigned_127 | 56.7 | - | ✓ | TermType::BVTerm | | +| Binary::Mod | Unsigned_127 | Unsigned_127 | - | 3.2 | ✗ | TermType::BVTerm | [Field and bitvector logic mixing](https://github.com/AztecProtocol/aztec-packages/issues/11722) | +| Binary::Mul | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | | +| Binary::Mul | Unsigned_127 | Unsigned_127 | 10.0 | - | ✓ | TermType::BVTerm | | +| Binary::Or | Unsigned_32 | Unsigned_32 | 18.0 | - | ✓ | TermType::BVTerm | | +| Binary::Or | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | [smt solver lookup doesnt support 2bits tables](https://github.com/AztecProtocol/aztec-packages/issues/11721) | +| Binary::Shl | Unsigned_64 | Unsigned_8 | 42331.61 | 63.2 | ✓ | TermType::BVTerm | | +| Binary::Shl | Unsigned_32 | Unsigned_8 | 4574.0 | 30 | ✓ | TermType::BVTerm | | +| Binary::Shr | Unsigned_64 | Unsigned_8 | 3927.88 | 10 | ✓ | TermType::BVTerm | | +| Binary::Sub | Unsigned_127 | Unsigned_127 | 3.3 | - | ✓ | TermType::BVTerm | | +| Binary::Xor | Unsigned_32 | Unsigned_32 | 14.7 | - | ✓ | TermType::BVTerm | | +| Binary::Xor | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | [smt solver lookup doesnt support 2bits tables](https://github.com/AztecProtocol/aztec-packages/issues/11721) | +| Not | Unsigned_127 | - | 0.2 | - | ✓ | TermType::BVTerm | | + +Each test attempts to find counterexamples that violate the expected behavior. A passing test indicates the operation is correctly implemented, while a failing test reveals potential issues. + +### bugs found + +1. 3 bit overflow in AND/XOR/OR operations in barretenberg, fixed in [#11651](https://github.com/AztecProtocol/aztec-packages/commit/dddab22934b3abb798dbf204bccb68b557ee2193) +