diff --git a/barretenberg/cpp/src/CMakeLists.txt b/barretenberg/cpp/src/CMakeLists.txt index 1a9590e4d67..fd992566082 100644 --- a/barretenberg/cpp/src/CMakeLists.txt +++ b/barretenberg/cpp/src/CMakeLists.txt @@ -102,6 +102,10 @@ if(SMT) add_subdirectory(barretenberg/smt_verification) endif() +if(SMT AND ACIR_FORMAL_PROOFS) + add_subdirectory(barretenberg/acir_formal_proofs) +endif() + add_subdirectory(barretenberg/benchmark) include(GNUInstallDirs) diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/CMakeLists.txt b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/CMakeLists.txt new file mode 100644 index 00000000000..fcd338d4072 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/CMakeLists.txt @@ -0,0 +1 @@ +barretenberg_module(acir_formal_proofs dsl circuit_checker smt_verification common) \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md new file mode 100644 index 00000000000..5dd3a5a2918 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md @@ -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. \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.cpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.cpp new file mode 100644 index 00000000000..f45f9e7aba8 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.cpp @@ -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 +#include +#include + +std::vector 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 vec; + + vec.insert(vec.begin(), std::istream_iterator(file), std::istream_iterator()); + 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); +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.hpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.hpp new file mode 100644 index 00000000000..a201aa8bb1d --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.hpp @@ -0,0 +1,96 @@ +#pragma once +#include "barretenberg/dsl/acir_format/acir_format.hpp" +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "msgpack/v3/sbuffer_decl.hpp" +#include +#include +#include + +/** + * @brief Class for loading ACIR (Arithmetic Circuit Intermediate Representation) programs and converting them to SMT + * format + * + * This class handles loading ACIR programs from files and provides functionality to: + * - Convert the ACIR program to various SMT circuit representations + * - Access the underlying constraint systems + * - Build circuits for verification + * + * The loader reads an ACIR program file, creates constraint systems, and allows conversion + * to different SMT circuit types (bitvector, field, integer) for formal verification. + */ +class AcirToSmtLoader { + public: + // Deleted constructors/operators to prevent copying/moving + AcirToSmtLoader() = delete; + AcirToSmtLoader(const AcirToSmtLoader& other) = delete; + AcirToSmtLoader(AcirToSmtLoader&& other) = delete; + AcirToSmtLoader& operator=(const AcirToSmtLoader other) = delete; + AcirToSmtLoader&& operator=(AcirToSmtLoader&& other) = delete; + + ~AcirToSmtLoader() = default; + + /** + * @brief Constructs loader from an ACIR program file + * @param filename Path to the ACIR program file to load + * + * Reads the ACIR program from file, initializes the constraint system, + * and prepares the circuit buffer for later use. + */ + AcirToSmtLoader(std::string filename); + + /** + * @brief Gets the constraint systems from the loaded ACIR program + * @return Reference to the ACIR format constraint systems + */ + acir_format::AcirFormat& get_constraint_systems() { return this->constraint_system; } + + /** + * @brief Creates a circuit builder for the loaded program + * @return UltraCircuitBuilder instance + * + * Creates and returns a circuit builder with predefined variable names: + * - Variable 0 named "a" + * - Variable 1 named "b" + * - Variable 2 named "c" + */ + bb::UltraCircuitBuilder get_circuit_builder(); + + /** + * @brief Gets an SMT solver instance + * @return Solver instance for SMT solving + * + * Creates a solver configured with: + * - Circuit modulus from schema + * - Default solver configuration + * - Minimum bit width of 16 + * - Maximum bit width of 240 + */ + smt_solver::Solver get_smt_solver(); + + /** + * @brief Creates an SMT circuit for bitvector operations + * @param solver Pointer to SMT solver to use + * @return UltraCircuit configured for bitvector operations + */ + smt_circuit::UltraCircuit get_bitvec_smt_circuit(smt_solver::Solver* solver); + + /** + * @brief Creates an SMT circuit for field operations + * @param solver Pointer to SMT solver to use + * @return UltraCircuit configured for field operations + */ + smt_circuit::UltraCircuit get_field_smt_circuit(smt_solver::Solver* solver); + + /** + * @brief Creates an SMT circuit for integer operations + * @param solver Pointer to SMT solver to use + * @return UltraCircuit configured for integer operations + */ + smt_circuit::UltraCircuit get_integer_smt_circuit(smt_solver::Solver* solver); + + private: + std::string instruction_name; ///< Name of the instruction/filename being processed + std::vector acir_program_buf; ///< Buffer containing the raw ACIR program data read from file + acir_format::AcirFormat constraint_system; ///< The parsed constraint system from the ACIR program + msgpack::sbuffer circuit_buf; ///< Buffer for circuit serialization using MessagePack +}; \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.test.cpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.test.cpp new file mode 100644 index 00000000000..67cf4ac6457 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.test.cpp @@ -0,0 +1,490 @@ +/** + * @file acir_loader.test.cpp + * @brief Tests for verifying ACIR (Arithmetic Circuit Intermediate Representation) operations + * + * This test suite verifies the correctness of various arithmetic, logical, and bitwise operations + * implemented in ACIR format. It uses SMT solvers to formally verify the operations. + */ + +#include "acir_loader.hpp" +#include "barretenberg/circuit_checker/circuit_checker.hpp" +#include "barretenberg/common/test.hpp" +#include "barretenberg/dsl/acir_format/acir_format.hpp" +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "barretenberg/smt_verification/solver/solver.hpp" +#include "barretenberg/smt_verification/util/smt_util.hpp" +#include "barretenberg/stdlib/client_ivc_verifier/client_ivc_recursive_verifier.hpp" +#include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp" +#include "formal_proofs.hpp" +#include "helpers.hpp" +#include + +// Path to test artifacts containing ACIR programs and witness files +const std::string ARTIFACTS_PATH = "../src/barretenberg/acir_formal_proofs/artifacts/"; + +/** + * @brief Saves witness data when a bug is found during verification + * @param instruction_name Name of the instruction being tested + * @param circuit The circuit containing the bug + * + * Saves witness data to a file named {instruction_name}.witness in the artifacts directory + */ +void save_buggy_witness(std::string instruction_name, smt_circuit::UltraCircuit circuit) +{ + std::vector special_names; + info("Saving bug for op ", instruction_name); + default_model_single(special_names, circuit, ARTIFACTS_PATH + instruction_name + ".witness"); +} + +/** + * @brief Verifies a previously saved witness file for correctness + * @param instruction_name Name of the instruction to verify + * @return true if witness is valid, false otherwise + * + * Loads a witness file and verifies it against the corresponding ACIR program + */ +bool verify_buggy_witness(std::string instruction_name) +{ + std::vector witness = import_witness_single(ARTIFACTS_PATH + instruction_name + ".witness.pack"); + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + instruction_name + ".acir"); + bb::UltraCircuitBuilder builder = loader.get_circuit_builder(); + for (uint i = 0; i < witness.size(); i++) { + builder.variables[i] = witness[i]; + if (i < 100) { + info(witness[i]); + } + } + return bb::CircuitChecker::check(builder); +} + +/** + * @brief Tests 127-bit unsigned addition + * Verifies that the ACIR implementation of addition is correct + * Execution time: ~2.8 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_add) +{ + std::string TESTNAME = "Binary::Add_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_add(&solver, circuit); + EXPECT_FALSE(res); + + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 127-bit unsigned bitwise AND + * Verifies that the ACIR implementation of AND is correct + */ +TEST(acir_formal_proofs, uint_terms_and) +{ + std::string TESTNAME = "Binary::And_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_and(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 32-bit unsigned bitwise AND + * Verifies that the ACIR implementation of AND is correct + * Execution time: ~6.7 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_and32) +{ + std::string TESTNAME = "Binary::And_Unsigned_32_Unsigned_32"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_and(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 126-bit unsigned division + * Verifies that the ACIR implementation of division is correct + */ +TEST(acir_formal_proofs, uint_terms_div) +{ + std::string TESTNAME = "Binary::Div_Unsigned_126_Unsigned_126"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_div(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 127-bit unsigned equality comparison + * Verifies two cases: + * 1. When operands are equal, result must be 0 + * 2. When operands are not equal, result must be 1 + * Execution time: ~22.8 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_eq) +{ + std::string TESTNAME = "Binary::Eq_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver1 = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit1 = loader.get_bitvec_smt_circuit(&solver1); + + bool res1 = verify_eq_on_equlaity(&solver1, circuit1); + EXPECT_FALSE(res1); + if (res1) { + save_buggy_witness(TESTNAME, circuit1); + } + + smt_solver::Solver solver2 = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit2 = loader.get_bitvec_smt_circuit(&solver2); + + bool res2 = verify_eq_on_inequlaity(&solver2, circuit2); + EXPECT_FALSE(res2); + if (res2) { + save_buggy_witness(TESTNAME, circuit2); + } +} + +/** + * @brief Tests 127-bit unsigned less than comparison + * Verifies two cases: + * 1. When a < b, result must be 0 + * 2. When a >= b, result must be 1 + * Execution time: ~81.7 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_lt) +{ + std::string TESTNAME = "Binary::Lt_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver1 = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit1 = loader.get_bitvec_smt_circuit(&solver1); + + bool res1 = verify_lt(&solver1, circuit1); + EXPECT_FALSE(res1); + if (res1) { + save_buggy_witness(TESTNAME, circuit1); + } + + smt_solver::Solver solver2 = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit2 = loader.get_bitvec_smt_circuit(&solver2); + + bool res2 = verify_gt(&solver2, circuit2); + EXPECT_FALSE(res2); + if (res2) { + save_buggy_witness(TESTNAME, circuit2); + } +} + +/** + * @brief Tests 126-bit unsigned modulo + * Verifies that the ACIR implementation of modulo is correct + * Execution time: ??? seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_mod) +{ + std::string TESTNAME = "Binary::Mod_Unsigned_126_Unsigned_126"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_mod(&solver, circuit); + solver.print_assertions(); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 127-bit unsigned multiplication + * Verifies that the ACIR implementation of multiplication is correct + * Execution time: ~10.0 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_mul) +{ + std::string TESTNAME = "Binary::Mul_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_mul(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 127-bit unsigned bitwise OR + * Verifies that the ACIR implementation of OR is correct + */ +TEST(acir_formal_proofs, uint_terms_or) +{ + std::string TESTNAME = "Binary::Or_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_or(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 32-bit unsigned bitwise OR + * Verifies that the ACIR implementation of OR is correct + * Execution time: ~20.3 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_or32) +{ + std::string TESTNAME = "Binary::Or_Unsigned_32_Unsigned_32"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_or(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 64-bit left shift + * Verifies that the ACIR implementation of left shift is correct + * Execution time: ~4588 seconds on SMTBOX + * Memory usage: ~30GB RAM + */ +TEST(acir_formal_proofs, uint_terms_shl64) +{ + std::string TESTNAME = "Binary::Shl_Unsigned_64_Unsigned_8"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_shl64(&solver, circuit); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } + EXPECT_FALSE(res); +} + +/** + * @brief Tests 32-bit left shift + * Verifies that the ACIR implementation of left shift is correct + * Execution time: ~4574 seconds on SMTBOX + * Memory usage: ~30GB RAM + */ +TEST(acir_formal_proofs, uint_terms_shl32) +{ + std::string TESTNAME = "Binary::Shl_Unsigned_32_Unsigned_8"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_shl32(&solver, circuit); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } + EXPECT_FALSE(res); +} + +/** + * @brief Tests right shift operation + * Verifies that the ACIR implementation of right shift is correct + * Execution time: ~3927.88 seconds on SMTBOX + * Memory usage: ~10GB RAM + */ +TEST(acir_formal_proofs, uint_terms_shr) +{ + std::string TESTNAME = "Binary::Shr_Unsigned_64_Unsigned_8"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_shr(&solver, circuit); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } + EXPECT_FALSE(res); +} + +/** + * @brief Tests 127-bit unsigned subtraction + * Verifies that the ACIR implementation of subtraction is correct + * Execution time: ~2.6 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_sub) +{ + std::string TESTNAME = "Binary::Sub_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_sub(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 127-bit unsigned bitwise XOR + * Verifies that the ACIR implementation of XOR is correct + */ +TEST(acir_formal_proofs, uint_terms_xor) +{ + std::string TESTNAME = "Binary::Xor_Unsigned_127_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_xor(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 32-bit unsigned bitwise XOR + * Verifies that the ACIR implementation of XOR is correct + */ +TEST(acir_formal_proofs, uint_terms_xor32) +{ + std::string TESTNAME = "Binary::Xor_Unsigned_32_Unsigned_32"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_xor(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 127-bit unsigned bitwise NOT + * Verifies that the ACIR implementation of NOT is correct + * Execution time: ~21.3 seconds on SMTBOX + */ +TEST(acir_formal_proofs, uint_terms_not) +{ + std::string TESTNAME = "Not_Unsigned_127"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver); + bool res = verify_not_127(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests field addition + * Verifies that the ACIR implementation of field addition is correct + * Execution time: ~0.22 seconds on SMTBOX + */ +TEST(acir_formal_proofs, field_terms_add) +{ + std::string TESTNAME = "Binary::Add_Field_0_Field_0"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_field_smt_circuit(&solver); + bool res = verify_add(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests field division + * Verifies that the ACIR implementation of field division is correct + * Execution time: ~0.22 seconds on SMTBOX + */ +TEST(acir_formal_proofs, field_terms_div) +{ + std::string TESTNAME = "Binary::Div_Field_0_Field_0"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_field_smt_circuit(&solver); + bool res = verify_div_field(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests field equality comparison + * Verifies two cases: + * 1. When operands are equal, result must be 0 + * 2. When operands are not equal, result must be 1 + * Execution time: ~19.2 seconds on SMTBOX + */ +TEST(acir_formal_proofs, field_terms_eq) +{ + std::string TESTNAME = "Binary::Eq_Field_0_Field_0"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver1 = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit1 = loader.get_field_smt_circuit(&solver1); + + bool res1 = verify_eq_on_equlaity(&solver1, circuit1); + EXPECT_FALSE(res1); + if (res1) { + save_buggy_witness(TESTNAME, circuit1); + } + + smt_solver::Solver solver2 = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit2 = loader.get_field_smt_circuit(&solver2); + + bool res2 = verify_eq_on_inequlaity(&solver2, circuit2); + EXPECT_FALSE(res2); + if (res2) { + save_buggy_witness(TESTNAME, circuit2); + } +} + +/** + * @brief Tests field multiplication + * Verifies that the ACIR implementation of field multiplication is correct + * Execution time: ~0.22 seconds on SMTBOX + */ +TEST(acir_formal_proofs, field_terms_mul) +{ + std::string TESTNAME = "Binary::Mul_Field_0_Field_0"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_field_smt_circuit(&solver); + bool res = verify_mul(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} + +/** + * @brief Tests 126-bit signed division + * Verifies that the ACIR implementation of signed division is correct + * Execution time: >17 DAYS on SMTBOX + */ +TEST(acir_formal_proofs, integer_terms_div) +{ + std::string TESTNAME = "Binary::Div_Signed_126_Signed_126"; + AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir"); + smt_solver::Solver solver = loader.get_smt_solver(); + smt_circuit::UltraCircuit circuit = loader.get_integer_smt_circuit(&solver); + bool res = verify_div(&solver, circuit); + EXPECT_FALSE(res); + if (res) { + save_buggy_witness(TESTNAME, circuit); + } +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/formal_proofs.cpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/formal_proofs.cpp new file mode 100644 index 00000000000..4c8bc12ee6b --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/formal_proofs.cpp @@ -0,0 +1,272 @@ +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "barretenberg/smt_verification/solver/solver.hpp" +#include "barretenberg/smt_verification/util/smt_util.hpp" +#include "helpers.hpp" + +void debug_solution(smt_solver::Solver* solver, std::unordered_map terms) +{ + solver->print_assertions(); + std::unordered_map vals = solver->model(terms); + for (auto const& i : vals) { + info(i.first, " = ", i.second); + } +} + +bool verify_add(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = a + b; + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_sub(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = a - b; + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_mul(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = a * b; + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_div(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = a / b; + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_div_field(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + // c = a / b + // c * b = a + auto cr = c * b; + a != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_mod(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + smt_circuit::STerm c1 = a % b; + c != c1; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "c1", c1 } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_or(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = a | b; + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_and(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = a & b; + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_xor(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = a ^ b; + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +// takes 0.346 seconds on SMTBOX +bool verify_not_127(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + // 2**127 - 1 + auto mask = smt_terms::BVConst("170141183460469231731687303715884105727", solver, 10); + auto br = a ^ mask; + b != br; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "br", br } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_shl32(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = shl32(a, b, solver); + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_shl64(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = shl64(a, b, solver); + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_shr(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + auto cr = shr(a, b, solver); + c != cr; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_eq_on_equlaity(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + a == b; + c != 1; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_eq_on_inequlaity(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + a != b; + c != 0; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_lt(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + a < b; + c != 1; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c } }); + debug_solution(solver, terms); + } + return res; +} + +bool verify_gt(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit) +{ + auto a = circuit["a"]; + auto b = circuit["b"]; + auto c = circuit["c"]; + a > b; + c != 0; + bool res = solver->check(); + if (res) { + std::unordered_map terms({ { "a", a }, { "b", b }, { "c", c } }); + debug_solution(solver, terms); + } + return res; +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/formal_proofs.hpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/formal_proofs.hpp new file mode 100644 index 00000000000..6992c1d0386 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/formal_proofs.hpp @@ -0,0 +1,149 @@ +#pragma once +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "barretenberg/smt_verification/solver/solver.hpp" +#include "cvc5/cvc5.h" +#include +#include + +/** + * @brief Debug helper to print solver assertions and model values + * @param solver SMT solver instance + * @param terms Map of term names to CVC5 terms to evaluate + */ +void debug_solution(smt_solver::Solver* solver, std::unordered_map terms); + +/** + * @brief Verify addition operation: c = a + b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_add(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify subtraction operation: c = a - b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_sub(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify multiplication operation: c = a * b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_mul(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify integer division operation: c = a / b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_div(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify field division operation: c = a / b (in field) + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_div_field(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify modulo operation: c = a mod b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_mod(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify bitwise OR operation: c = a | b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_or(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify bitwise AND operation: c = a & b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_and(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify bitwise XOR operation: c = a ^ b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_xor(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify NOT operation on 127 bits: b = ~a + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b + * @return true if a counterexample is found (verification fails) + */ +bool verify_not_127(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify 32-bit left shift operation: c = a << b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_shl32(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify 64-bit left shift operation: c = a << b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_shl64(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify right shift operation: c = a >> b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_shr(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify equality comparison when values are equal + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_eq_on_equlaity(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify equality comparison when values are not equal + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_eq_on_inequlaity(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify less than comparison: a < b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_lt(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); + +/** + * @brief Verify greater than comparison: a > b + * @param solver SMT solver instance + * @param circuit Circuit containing variables a, b, c + * @return true if a counterexample is found (verification fails) + */ +bool verify_gt(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit); diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.cpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.cpp new file mode 100644 index 00000000000..a3ab02b5f58 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.cpp @@ -0,0 +1,63 @@ +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "barretenberg/smt_verification/solver/solver.hpp" +#include "barretenberg/smt_verification/util/smt_util.hpp" + +// used for base = 2; exp <= 8 so its okay +uint32_t pow_num(uint32_t base, uint32_t exp) +{ + uint32_t res = 1; + for (uint32_t i = 0; i < exp; i++) { + res *= base; + } + return res; +} + +// returns 2^v0 +smt_circuit::STerm pow2_8(smt_circuit::STerm v0, smt_solver::Solver* solver) +{ + uint32_t BIT_SIZE = 8; + auto one = smt_terms::BVConst("1", solver, 10); + auto two = smt_terms::BVConst("2", solver, 10); + smt_circuit::STerm res = smt_circuit::BVVar("res", solver); + res = one; + auto exp = v0; + for (uint32_t i = 1; i < BIT_SIZE + 1; i++) { + auto r2 = res * res; + auto mask = pow_num(2, BIT_SIZE - i); + // same thing as taking ith bit in little endian + auto b = (v0 & mask) >> (BIT_SIZE - i); + res = (r2 * two * b) + (1 - b) * r2; + } + return res; +} + +smt_circuit::STerm shl(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver) +{ + auto pow2_v1 = pow2_8(v1, solver); + return v0 * pow2_v1; +} + +smt_circuit::STerm shr(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver) +{ + auto pow2_v1 = pow2_8(v1, solver); + auto res = v0 / pow2_v1; + return res; +} + +smt_circuit::STerm shl64(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver) +{ + auto shifted = shl(v0, v1, solver); + // 2^64 - 1 + auto mask = smt_terms::BVConst("18446744073709551615", solver, 10); + auto res = shifted & mask; + return res; +} + +smt_circuit::STerm shl32(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver) +{ + auto shifted = shl(v0, v1, solver); + // 2^32 - 1 + auto mask = smt_terms::BVConst("4294967295", solver, 10); + auto res = shifted & mask; + return res; +} diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.hpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.hpp new file mode 100644 index 00000000000..d1e6fe4ab45 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.hpp @@ -0,0 +1,47 @@ +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "barretenberg/smt_verification/solver/solver.hpp" +#include "barretenberg/smt_verification/terms/term.hpp" + +/** + * @brief Left shift operation with 64-bit truncation + * @param v0 Value to shift + * @param v1 Number of bits to shift (8-bit value) + * @param solver SMT solver instance + * @return Result of (v0 << v1) truncated to 64 bits + */ +smt_circuit::STerm shl64(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver); + +/** + * @brief Left shift operation with 32-bit truncation + * @param v0 Value to shift + * @param v1 Number of bits to shift (8-bit value) + * @param solver SMT solver instance + * @return Result of (v0 << v1) truncated to 32 bits + */ +smt_circuit::STerm shl32(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver); + +/** + * @brief Calculates power of 2 + * @param v0 Exponent (8-bit value) + * @param solver SMT solver instance + * @return 2^v0 + */ +smt_circuit::STerm pow2_8(smt_circuit::STerm v0, smt_solver::Solver* solver); + +/** + * @brief Right shift operation + * @param v0 Value to shift + * @param v1 Number of bits to shift (8-bit value) + * @param solver SMT solver instance + * @return Result of (v0 >> v1) + */ +smt_circuit::STerm shr(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver); + +/** + * @brief Left shift operation without truncation + * @param v0 Value to shift + * @param v1 Number of bits to shift (8-bit value) + * @param solver SMT solver instance + * @return Result of (v0 << v1) without truncation + */ +smt_circuit::STerm shl(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver); \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.test.cpp b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.test.cpp new file mode 100644 index 00000000000..9918dcb6947 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.test.cpp @@ -0,0 +1,92 @@ +#include "helpers.hpp" +#include "barretenberg/common/test.hpp" +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "barretenberg/smt_verification/solver/solver.hpp" +#include "barretenberg/smt_verification/util/smt_util.hpp" +#include "barretenberg/stdlib/primitives/uint/uint.hpp" +#include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp" + +using namespace bb; +using witness_ct = stdlib::witness_t; +using uint_ct = stdlib::uint32; + +using namespace smt_terms; + +TEST(helpers, shl) +{ + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32); + + STerm x = BVVar("x", &s); + STerm y = BVVar("y", &s); + STerm z = shl(x, y, &s); + x == 5; + y == 1; + // z should be z == 10; + s.check(); + std::unordered_map terms({ { "x", x }, { "y", y }, { "z", z } }); + std::unordered_map vals = s.model(terms); + info("x = ", vals["x"]); + info("y = ", vals["y"]); + info("z = ", vals["z"]); + // z == 1010 in binary + EXPECT_TRUE(vals["z"] == "00000000000000000000000000001010"); +} + +TEST(helpers, shr) +{ + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32); + + STerm x = BVVar("x", &s); + STerm y = BVVar("y", &s); + STerm z = shr(x, y, &s); + x == 5; + y == 1; + // z should be z == 2; + s.check(); + std::unordered_map terms({ { "x", x }, { "y", y }, { "z", z } }); + std::unordered_map vals = s.model(terms); + info("x = ", vals["x"]); + info("y = ", vals["y"]); + info("z = ", vals["z"]); + // z == 10 in binary + EXPECT_TRUE(vals["z"] == "00000000000000000000000000000010"); +} + +TEST(helpers, buggy_shr) +{ + // using smt solver i found that 1879048194 >> 16 == 0 + // its strange... + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32); + + STerm x = BVVar("x", &s); + STerm y = BVVar("y", &s); + STerm z = shr(x, y, &s); + x == 1879048194; + y == 16; + // z should be z == 28672; + s.check(); + std::unordered_map terms({ { "x", x }, { "y", y }, { "z", z } }); + std::unordered_map vals = s.model(terms); + info("x = ", vals["x"]); + info("y = ", vals["y"]); + info("z = ", vals["z"]); + // z == 28672 in binary + EXPECT_TRUE(vals["z"] == "00000000000000000111000000000000"); +} + +TEST(helpers, pow2) +{ + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32); + + STerm x = BVVar("x", &s); + STerm z = pow2_8(x, &s); + x == 11; + // z should be z == 2048; + s.check(); + std::unordered_map terms({ { "x", x }, { "z", z } }); + std::unordered_map vals = s.model(terms); + info("x = ", vals["x"]); + info("z = ", vals["z"]); + // z == 2048 in binary + EXPECT_TRUE(vals["z"] == "00000000000000000000100000000000"); +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp index 01cb3728524..155a17c8c63 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp @@ -95,7 +95,7 @@ size_t UltraCircuit::handle_arithmetic_relation(size_t cursor, size_t idx) return cursor + 1; } - STerm res = this->symbolic_vars[0]; + STerm res = this->symbolic_vars[this->variable_names_inverse["zero"]]; static const bb::fr neg_half = bb::fr(-2).invert(); if (!q_arith.is_zero()) { diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp index 2219a05b0d4..943291bbf63 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp @@ -172,6 +172,9 @@ std::string Solver::stringify_term(const cvc5::Term& term, bool parenthesis) child_parenthesis = false; break; case cvc5::Kind::LT: + case cvc5::Kind::BITVECTOR_UDIV: + op = " / "; + break; case cvc5::Kind::BITVECTOR_ULT: op = " < "; break; @@ -187,6 +190,9 @@ std::string Solver::stringify_term(const cvc5::Term& term, bool parenthesis) case cvc5::Kind::BITVECTOR_UGE: op = " >= "; break; + case cvc5::Kind::BITVECTOR_UREM: + op = " % "; + break; case cvc5::Kind::XOR: case cvc5::Kind::BITVECTOR_XOR: op = " ^ "; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp index 8d2bc596703..cb55e0eed65 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp @@ -1,4 +1,5 @@ #include "barretenberg/smt_verification/terms/term.hpp" +#include "term.hpp" namespace smt_terms { @@ -265,6 +266,16 @@ void STerm::operator>=(const bb::fr& other) const this->solver->assertFormula(ge); } +STerm STerm::operator%(const STerm& other) const +{ + if (!this->operations.contains(OpType::MOD)) { + info("MOD is not compatible with ", this->type); + return *this; + } + cvc5::Term res = solver->term_manager.mkTerm(this->operations.at(OpType::MOD), { this->term, other.term }); + return { res, this->solver, this->type }; +} + STerm STerm::operator^(const STerm& other) const { if (!this->operations.contains(OpType::XOR)) { @@ -313,6 +324,38 @@ STerm STerm::operator|(const STerm& other) const return { res, this->solver, this->type }; } +void STerm::operator<(const STerm& other) const +{ + STerm left = *this; + STerm right = other; + left = this->type == TermType::FFITerm && left.term.getNumChildren() > 1 ? left.mod() : left; + right = this->type == TermType::FFITerm && right.term.getNumChildren() > 1 ? right.mod() : right; + + cvc5::Term eq = this->solver->term_manager.mkTerm(this->operations.at(OpType::LT), { left.term, right.term }); + this->solver->assertFormula(eq); +} + +void STerm::operator>(const STerm& other) const +{ + STerm left = *this; + STerm right = other; + left = this->type == TermType::FFITerm && left.term.getNumChildren() > 1 ? left.mod() : left; + right = this->type == TermType::FFITerm && right.term.getNumChildren() > 1 ? right.mod() : right; + + cvc5::Term eq = this->solver->term_manager.mkTerm(this->operations.at(OpType::GT), { left.term, right.term }); + this->solver->assertFormula(eq); +} + +STerm STerm::operator~() const +{ + if (!this->operations.contains(OpType::NOT)) { + info("NOT is not compatible with ", this->type); + return *this; + } + cvc5::Term res = solver->term_manager.mkTerm(this->operations.at(OpType::NOT), { this->term }); + return { res, this->solver, this->type }; +} + void STerm::operator|=(const STerm& other) { if (!this->operations.contains(OpType::OR)) { diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp index 35aff409795..a9ac3b56a47 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp @@ -15,7 +15,7 @@ using namespace smt_solver; enum class TermType { FFTerm, FFITerm, BVTerm, ITerm }; std::ostream& operator<<(std::ostream& os, TermType type); -enum class OpType : int32_t { ADD, SUB, MUL, DIV, NEG, XOR, AND, OR, GT, GE, LT, LE, MOD, RSH, LSH, ROTR, ROTL }; +enum class OpType : int32_t { ADD, SUB, MUL, DIV, NEG, XOR, AND, OR, GT, GE, LT, LE, MOD, RSH, LSH, ROTR, ROTL, NOT }; /** * @brief precomputed map that contains allowed @@ -73,7 +73,9 @@ const std::unordered_map> typed { OpType::ROTL, cvc5::Kind::BITVECTOR_ROTATE_LEFT }, { OpType::ROTR, cvc5::Kind::BITVECTOR_ROTATE_RIGHT }, { OpType::MOD, cvc5::Kind::BITVECTOR_UREM }, - { OpType::DIV, cvc5::Kind::BITVECTOR_UDIV } } } + { OpType::DIV, cvc5::Kind::BITVECTOR_UDIV }, + { OpType::NOT, cvc5::Kind::BITVECTOR_NOT }, + } } }; /** @@ -160,6 +162,10 @@ class STerm { void operator&=(const STerm& other); STerm operator|(const STerm& other) const; void operator|=(const STerm& other); + void operator<(const STerm& other) const; + void operator>(const STerm& other) const; + STerm operator%(const STerm& other) const; + STerm operator~() const; STerm operator<<(const uint32_t& n) const; void operator<<=(const uint32_t& n); STerm operator>>(const uint32_t& n) const;