-
Notifications
You must be signed in to change notification settings - Fork 307
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into 12-09-chore_removing_noir_bug_workaround
- Loading branch information
Showing
325 changed files
with
7,959 additions
and
4,522 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
51 changes: 0 additions & 51 deletions
51
barretenberg/acir_tests/regenerate_verify_honk_proof_inputs.sh
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
1 change: 1 addition & 0 deletions
1
barretenberg/cpp/src/barretenberg/acir_formal_proofs/CMakeLists.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| barretenberg_module(acir_formal_proofs dsl circuit_checker smt_verification common) |
47 changes: 47 additions & 0 deletions
47
barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,47 @@ | ||
| # Formal Verification of ACIR Instructions | ||
|
|
||
| This module provides formal verification capabilities for ACIR (Arithmetic Circuit Intermediate Representation) instructions generated from Noir SSA code. | ||
|
|
||
| ## Overview | ||
|
|
||
| The verifier uses SMT (Satisfiability Modulo Theories) solving to formally verify the correctness of ACIR instructions. It supports verification of: | ||
|
|
||
| - Arithmetic operations (add, subtract, multiply, divide) | ||
| - Bitwise operations (AND, OR, XOR, NOT) | ||
| - Shifts (left shift, right shift) | ||
| - Comparisons (equality, less than, greater than) | ||
| - Field arithmetic | ||
|
|
||
| ## Tests | ||
|
|
||
| ⚠️ **WARNING**: Do not run these tests on a local machine without sufficient memory (>32GB RAM). The tests can consume large amounts of memory and CPU resources. Some tests like integer division can run for multiple days. It is recommended to run these tests in a controlled environment with adequate resources. | ||
|
|
||
| ### 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. |
70 changes: 70 additions & 0 deletions
70
barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,70 @@ | ||
| #include "acir_loader.hpp" | ||
| #include "barretenberg/dsl/acir_format/acir_format.hpp" | ||
| #include "barretenberg/dsl/acir_format/acir_to_constraint_buf.hpp" | ||
| #include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" | ||
| #include "barretenberg/smt_verification/terms/term.hpp" | ||
| #include "msgpack/v3/sbuffer_decl.hpp" | ||
| #include <fstream> | ||
| #include <string> | ||
| #include <vector> | ||
|
|
||
| std::vector<uint8_t> readFile(std::string filename) | ||
| { | ||
| std::ifstream file(filename, std::ios::binary); | ||
| file.unsetf(std::ios::skipws); | ||
|
|
||
| std::streampos fileSize; | ||
|
|
||
| file.seekg(0, std::ios::end); | ||
| fileSize = file.tellg(); | ||
| file.seekg(0, std::ios::beg); | ||
|
|
||
| std::vector<uint8_t> vec; | ||
|
|
||
| vec.insert(vec.begin(), std::istream_iterator<uint8_t>(file), std::istream_iterator<uint8_t>()); | ||
| file.close(); | ||
| return vec; | ||
| } | ||
|
|
||
| AcirToSmtLoader::AcirToSmtLoader(std::string filename) | ||
| { | ||
| this->acir_program_buf = readFile(filename); | ||
| this->instruction_name = filename; | ||
| this->constraint_system = acir_format::program_buf_to_acir_format(this->acir_program_buf, false).at(0); | ||
| this->circuit_buf = this->get_circuit_builder().export_circuit(); | ||
| } | ||
|
|
||
| bb::UltraCircuitBuilder AcirToSmtLoader::get_circuit_builder() | ||
| { | ||
| bb::UltraCircuitBuilder builder = acir_format::create_circuit(this->constraint_system, false); | ||
| builder.set_variable_name(0, "a"); | ||
| builder.set_variable_name(1, "b"); | ||
| builder.set_variable_name(2, "c"); | ||
| return builder; | ||
| } | ||
|
|
||
| smt_solver::Solver AcirToSmtLoader::get_smt_solver() | ||
| { | ||
| smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(this->circuit_buf); | ||
| // In circuits generated by the shift left (shl) opcode, there is a variable with bit length 197. | ||
| // This is likely because the shl operation internally calls truncate opcode to handle overflow | ||
| return smt_solver::Solver(circuit_info.modulus, smt_circuit::default_solver_config, 16, 240); | ||
| } | ||
|
|
||
| smt_circuit::UltraCircuit AcirToSmtLoader::get_bitvec_smt_circuit(smt_solver::Solver* solver) | ||
| { | ||
| smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(this->circuit_buf); | ||
| return smt_circuit::UltraCircuit(circuit_info, solver, smt_terms::TermType::BVTerm); | ||
| } | ||
|
|
||
| smt_circuit::UltraCircuit AcirToSmtLoader::get_field_smt_circuit(smt_solver::Solver* solver) | ||
| { | ||
| smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(this->circuit_buf); | ||
| return smt_circuit::UltraCircuit(circuit_info, solver, smt_terms::TermType::FFTerm); | ||
| } | ||
|
|
||
| smt_circuit::UltraCircuit AcirToSmtLoader::get_integer_smt_circuit(smt_solver::Solver* solver) | ||
| { | ||
| smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(this->circuit_buf); | ||
| return smt_circuit::UltraCircuit(circuit_info, solver, smt_terms::TermType::ITerm); | ||
| } |
Oops, something went wrong.