feat: Acir formal proofs (#10973)

The ACIR formal verification. Combines a test generator in the Noir
repository with a formal verifier in Barretenberg to mathematically
prove the correctness of ACIR instructions using SMT solving. Verifies
range of operations including 127-bit arithmetic (addition, subtraction,
multiplication), 126-bit division, bitwise operations (though currently
limited to 32-bit for AND/OR/XOR), shift operations, field operations
(ADD, MUL, DIV), and comparison operations

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)

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,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.

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 <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);
+}

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
+};