feat: Acir formal proofs

barretenberg/cpp/src/CMakeLists.txt

@@ -96,6 +96,7 @@ add_subdirectory(barretenberg/ultra_honk)
 add_subdirectory(barretenberg/vm)
 add_subdirectory(barretenberg/wasi)
 add_subdirectory(barretenberg/world_state)
+add_subdirectory(barretenberg/acir_formal_proofs)
 
 if(SMT)
     add_subdirectory(barretenberg/smt_verification)

barretenberg/cpp/src/barretenberg/acir_formal_proofs/CMakeLists.txt

@@ -0,0 +1 @@
+barretenberg_module(acir_formal_proofs dsl circuit_checker smt_verification common)

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

@@ -0,0 +1,50 @@
+# 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.
+The test suite verifies correctness of ACIR operations through SMT solving:
+
+### Arithmetic Tests
+
+- `uint_terms_add`: Tests 127-bit unsigned addition. Execution time: ~2.8s
+- `uint_terms_sub`: Tests 127-bit unsigned subtraction. Execution time: ~2.6s
+- `uint_terms_mul`: Tests 127-bit unsigned multiplication. Execution time: ~10.0s
+- `uint_terms_div`: Tests 126-bit unsigned division
+- `integer_terms_div`: Tests 126-bit signed division. Execution time: >10 days
+- `field_terms_div`: Tests field division. Execution time: ~0.22s
+- `uint_terms_mod`: Tests 126-bit unsigned modulo. Execution time: ???. Unknown time due to bug found during reviewing.
+
+### Bitwise Tests
+
+- `uint_terms_and`: Tests 127-bit unsigned bitwise AND DOESNT WORK\*
+- `uint_terms_or`: Tests 127-bit unsigned bitwise OR DOESNT WORK\*
+- `uint_terms_xor`: Tests 127-bit unsigned bitwise XOR DOESNT WORK\*
+- `uint_terms_not`: Tests 127-bit unsigned bitwise NOT
+
+### Shift Tests
+
+- `uint_terms_shl32`: Tests 32-bit left shift. Execution time: ~4574s, Memory: ~30GB
+- `uint_terms_shl64`: Tests 64-bit left shift. Execution time: ~4588s, Memory: ~30GB
+- `uint_terms_shr`: Tests right shift. Execution time: ~3927.88s, Memory: ~10GB
+
+### Comparison Tests
+
+- `uint_terms_eq`: Tests 127-bit unsigned equality comparison. Verifies both equal and unequal cases. Execution time: ~22.8s
+- `uint_terms_lt`: Tests 127-bit unsigned less than comparison. Verifies both a < b and a >= b cases. Execution time: ~56.7s
+
+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.
+
+\*Note: The bitwise tests are not working yet. (probably because of bug in the SMT solver). It works only for variables with 32 bits.

barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.cpp

@@ -0,0 +1,69 @@
+#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);
+    // for shl i have variable with bit length 197... for some reason
+    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);
+}

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 <cstdint>
+#include <string>
+#include <vector>
+
+/**
+ * @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<uint8_t> 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
+};