Skip to content

Commit cadc2b7

Browse files
defkitdefkit
authored
chore(docs): fix acir_formal_proofs docs (#16559)
Please read [contributing guidelines](CONTRIBUTING.md) and remove this line. For audit-related pull requests, please use the [audit PR template](?expand=1&template=audit.md).
2 parents 86b0722 + e99c45b commit cadc2b7

File tree

1 file changed

+24
-24
lines changed
  • barretenberg/cpp/src/barretenberg/acir_formal_proofs

1 file changed

+24
-24
lines changed

‎barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md‎

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#Formal Verification of ACIR Instructions
1+
# Formal Verification of ACIR Instructions
22

33
This module provides formal verification capabilities for ACIR (Arithmetic Circuit Intermediate Representation) instructions generated from Noir SSA code.
44

@@ -20,31 +20,31 @@ The verifier uses SMT (Satisfiability Modulo Theories) solving to formally verif
2020

2121
| Opcode | Lhs type/size | Rhs type/size | Time/seconds | Memory/GB | Success | SMT Term Type | Reason |
2222
| ----------- | ------------- | ------------- | ------------ | --------- | ------- | ---------------- | ------------------------------------------------------------------------------------------------------------- |
23-
| Binary::Add | Field | Field | 0.024 | - | ✓
24-
| TermType::FFTerm | | | Binary::Add | Unsigned_127 | Unsigned_127 | 2.8 | - | ✓
25-
| TermType::BVTerm | | | Binary::And | Unsigned_32 | Unsigned_32 | 6.7 | - | ✓
26-
| 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) |
27-
| Binary::Div | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | |
28-
| 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) |
29-
| 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) |
30-
| Binary::Eq | Field | Field | 19.2 | - | ✓ | TermType::FFTerm | |
31-
| Binary::Eq | Unsigned_127 | Unsigned_127 | 22.8 | - | ✓ | TermType::BVTerm | |
32-
| Binary::Lt | Unsigned_127 | Unsigned_127 | 56.7 | - | ✓ | TermType::BVTerm | |
33-
| Binary::Mod | Unsigned_127 | Unsigned_127 | - | 3.2 | ✗ | TermType::BVTerm | [Field and bitvector logic mixing](https://github.com/AztecProtocol/aztec-packages/issues/11722) |
34-
| Binary::Mul | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | |
35-
| Binary::Mul | Unsigned_127 | Unsigned_127 | 10.0 | - | ✓ | TermType::BVTerm | |
36-
| Binary::Or | Unsigned_32 | Unsigned_32 | 18.0 | - | ✓ | TermType::BVTerm | |
23+
| Binary::Add | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | - |
24+
| Binary::Add | Unsigned_127 | Unsigned_127 | 2.8 | - | ✓ | TermType::BVTerm | - |
25+
| Binary::And | Unsigned_32 | Unsigned_32 | 6.7 | - | ✓ | TermType::BVTerm | - |
26+
| 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) |
27+
| Binary::Div | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | - |
28+
| Binary::Div | Unsigned_126 | Unsigned_126 | >130 days | 20 | ✗ | TermType::BVTerm | Test takes too long |
29+
| Binary::Div | Signed_126 | Signed_126 | >130 days | 20 | ✗ | TermType::BVTerm | Test takes too long |
30+
| Binary::Eq | Field | Field | 19.2 | - | ✓ | TermType::FFTerm | - |
31+
| Binary::Eq | Unsigned_127 | Unsigned_127 | 22.8 | - | ✓ | TermType::BVTerm | - |
32+
| Binary::Lt | Unsigned_127 | Unsigned_127 | 56.7 | - | ✓ | TermType::BVTerm | - |
33+
| Binary::Mod | Unsigned_127 | Unsigned_127 | >130 days | 3.2 | ✗ | TermType::BVTerm | Test takes too long |
34+
| Binary::Mul | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | - |
35+
| Binary::Mul | Unsigned_127 | Unsigned_127 | 10.0 | - | ✓ | TermType::BVTerm | - |
36+
| Binary::Or | Unsigned_32 | Unsigned_32 | 18.0 | - | ✓ | TermType::BVTerm | - |
3737
| 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) |
38-
| Binary::Shl | Unsigned_64 | Unsigned_8 | 42331.61 | 63.2 | ✓ | TermType::BVTerm | |
39-
| Binary::Shl | Unsigned_32 | Unsigned_8 | 4574.0 | 30 | ✓ | TermType::BVTerm | |
40-
| Binary::Shr | Unsigned_64 | Unsigned_8 | 3927.88 | 10 | ✓ | TermType::BVTerm | |
41-
| Binary::Sub | Unsigned_127 | Unsigned_127 | 3.3 | - | ✓ | TermType::BVTerm | |
42-
| Binary::Xor | Unsigned_32 | Unsigned_32 | 14.7 | - | ✓ | TermType::BVTerm | |
38+
| Binary::Shl | Unsigned_64 | Unsigned_8 | 42331.61 | 63.2 | ✓ | TermType::BVTerm | - |
39+
| Binary::Shl | Unsigned_32 | Unsigned_8 | 4574.0 | 30 | ✓ | TermType::BVTerm | - |
40+
| Binary::Shr | Unsigned_64 | Unsigned_8 | 3927.88 | 10 | ✓ | TermType::BVTerm | - |
41+
| Binary::Sub | Unsigned_127 | Unsigned_127 | 3.3 | - | ✓ | TermType::BVTerm | - |
42+
| Binary::Xor | Unsigned_32 | Unsigned_32 | 14.7 | - | ✓ | TermType::BVTerm | - |
4343
| 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) |
44-
| Not | Unsigned_127 | - | 0.2 | - | ✓ | TermType::BVTerm | |
45-
| Cast | Field | Unsigned_64 | 0.05 | - | ✓ | TermType::FFTerm | |
46-
| Cast | Unsigned_64 | Unsigned_8 | 0.07 | - | ✓ | TermType::BVTerm | |
47-
| Cast | Unsigned_8 | Unsigned_64 | 0.6 | - | ✓ | TermType::BVTerm | |
44+
| Not | Unsigned_127 | - | 0.2 | - | ✓ | TermType::BVTerm | - |
45+
| Cast | Field | Unsigned_64 | 0.05 | - | ✓ | TermType::FFTerm | - |
46+
| Cast | Unsigned_64 | Unsigned_8 | 0.07 | - | ✓ | TermType::BVTerm | - |
47+
| Cast | Unsigned_8 | Unsigned_64 | 0.6 | - | ✓ | TermType::BVTerm | - |
4848

4949
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.
5050

0 commit comments

Comments
 (0)