feat: creating an SMT verification module (#1932)

This PR adds a module to symbolically verify circuits in our codebase

# Checklist:
Remove the checklist to signal you've completed it. Enable auto-merge if
the PR is ready to merge.
- [ x] If the pull request requires a cryptography review (e.g.
cryptographic algorithm implementations) I have added the 'crypto' tag.
- [x ] I have reviewed my diff in github, line by line and removed
unexpected formatting changes, testing logs, or commented-out code.
- [ x] Every change is related to the PR description.
- [x ] I have
[linked](https://docs.github.com/en/issues/tracking-your-work-with-issues/linking-a-pull-request-to-an-issue)
this pull request to relevant issues (if any exist).

---------

Co-authored-by: Innokentii Sennovskii <isennovskiy@gmail.com>

Author: Sarkoxed

circuits/cpp/barretenberg/cpp/CMakePresets.json

@@ -88,6 +88,16 @@
         "FUZZING": "ON"
       }
     },
+    {
+      "name": "smt-verification",
+      "displayName": "Build with smt verificaiton",
+      "description": "Build default preset but with smt library included",
+      "inherits": "clang16",
+      "binaryDir": "build-smt",
+      "cacheVariables": {
+        "SMT": "ON"
+      }
+    },
     {
       "name": "coverage",
       "displayName": "Build with coverage",
@@ -190,6 +200,11 @@
       "inherits": "default",
       "configurePreset": "fuzzing"
     },
+    { 
+      "name": "smt-verification",
+      "inherits": "clang16",
+      "configurePreset": "smt-verification"
+    },
     {
       "name": "coverage",
       "inherits": "default",
@@ -258,6 +273,11 @@
       "inherits": "default",
       "configurePreset": "fuzzing"
     },
+    {
+      "name": "smt-verification",
+      "inherits": "clang16",
+      "configurePreset": "smt-verification"
+    },
     {
       "name": "coverage",
       "inherits": "default",

circuits/cpp/barretenberg/cpp/src/CMakeLists.txt

@@ -39,6 +39,7 @@ endif()
 
 include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/msgpack-c/include)
 
+
 # I feel this should be limited to ecc, however it's currently used in headers that go across libraries,
 # and there currently isn't an easy way to inherit the DDISABLE_SHENANIGANS parameter.
 if(DISABLE_ASM)
@@ -69,6 +70,12 @@ add_subdirectory(barretenberg/wasi)
 add_subdirectory(barretenberg/grumpkin_srs_gen)
 add_subdirectory(barretenberg/bb)
 
+
+if(SMT)
+    include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include)
+    add_subdirectory(barretenberg/smt_verification)
+endif()
+
 if(BENCHMARKS)
     add_subdirectory(barretenberg/benchmark)
 endif()

circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp

@@ -3,8 +3,11 @@
 #include "barretenberg/ecc/curves/bn254/fr.hpp"
 #include "barretenberg/proof_system/arithmetization/arithmetization.hpp"
 #include "barretenberg/proof_system/arithmetization/gate_data.hpp"
+#include "barretenberg/serialize/cbind.hpp"
 #include <utility>
 
+#include <unordered_map>
+
 namespace proof_system {
 static constexpr uint32_t DUMMY_TAG = 0;
 
@@ -26,6 +29,8 @@ template <typename Arithmetization> class CircuitBuilderBase {
 
     std::vector<uint32_t> public_inputs;
     std::vector<FF> variables;
+    std::unordered_map<uint32_t, std::string> variable_names;
+
     // index of next variable in equivalence class (=REAL_VARIABLE if you're last)
     std::vector<uint32_t> next_var_index;
     // index of  previous variable in equivalence class (=FIRST if you're in a cycle alone)
@@ -57,6 +62,7 @@ template <typename Arithmetization> class CircuitBuilderBase {
         : selector_names_(std::move(selector_names))
     {
         variables.reserve(size_hint * 3);
+        variable_names.reserve(size_hint * 3);
         next_var_index.reserve(size_hint * 3);
         prev_var_index.reserve(size_hint * 3);
         real_variable_index.reserve(size_hint * 3);
@@ -187,6 +193,99 @@ template <typename Arithmetization> class CircuitBuilderBase {
         real_variable_tags.emplace_back(DUMMY_TAG);
         return index;
     }
+
+    /**
+     * Assign a name to a variable(equivalence class). Should be one name per equivalence class.
+     *
+     * @param index Index of the variable you want to name.
+     * @param name  Name of the variable.
+     *
+     */
+    virtual void set_variable_name(uint32_t index, const std::string& name)
+    {
+        ASSERT(variables.size() > index);
+        uint32_t first_idx = get_first_variable_in_class(index);
+
+        if (variable_names.contains(first_idx)) {
+            failure("Attempted to assign a name to a variable that already has a name");
+            return;
+        }
+        variable_names.insert({ first_idx, name });
+    }
+
+    /**
+     * After assert_equal() merge two class names if present.
+     * Preserves the first name in class.
+     *
+     * @param index Index of the variable you have previously named and used in assert_equal.
+     *
+     */
+    virtual void update_variable_names(uint32_t index)
+    {
+        uint32_t first_idx = get_first_variable_in_class(index);
+
+        uint32_t cur_idx = next_var_index[first_idx];
+        while (cur_idx != REAL_VARIABLE && !variable_names.contains(cur_idx)) {
+            cur_idx = next_var_index[cur_idx];
+        }
+
+        if (variable_names.contains(first_idx)) {
+            if (cur_idx != REAL_VARIABLE) {
+                variable_names.extract(cur_idx);
+            }
+            return;
+        }
+
+        if (cur_idx != REAL_VARIABLE) {
+            std::string var_name = variable_names.find(cur_idx)->second;
+            variable_names.erase(cur_idx);
+            variable_names.insert({ first_idx, var_name });
+            return;
+        }
+        failure("No previously assigned names found");
+    }
+
+    /**
+     * After finishing the circuit can be called for automatic merging
+     * all existing collisions.
+     *
+     */
+    virtual void finalize_variable_names()
+    {
+        std::vector<uint32_t> keys;
+        std::vector<uint32_t> firsts;
+
+        for (auto& tup : variable_names) {
+            keys.push_back(tup.first);
+            firsts.push_back(get_first_variable_in_class(tup.first));
+        }
+
+        for (size_t i = 0; i < keys.size() - 1; i++) {
+            for (size_t j = i + 1; j < keys.size(); i++) {
+                uint32_t first_idx_a = firsts[i];
+                uint32_t first_idx_b = firsts[j];
+                if (first_idx_a == first_idx_b) {
+                    std::string substr1 = variable_names[keys[i]];
+                    std::string substr2 = variable_names[keys[j]];
+                    failure("Variables from the same equivalence class have separate names: " + substr2 + ", " +
+                            substr2);
+                    update_variable_names(first_idx_b);
+                }
+            }
+        }
+    }
+
+    /**
+     * Export the existing circuit as msgpack compatible buffer.
+     *
+     * @return msgpack compatible buffer
+     */
+    virtual msgpack::sbuffer export_circuit()
+    {
+        info("not implemented");
+        return { 0 };
+    };
+
     /**
      * Add a public variable to variables
      *

circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp

@@ -4,6 +4,9 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#include "barretenberg/serialize/cbind.hpp"
+#include "barretenberg/serialize/msgpack.hpp"
+
 using namespace barretenberg;
 
 namespace proof_system {
@@ -507,6 +510,56 @@ template <typename FF> bool StandardCircuitBuilder_<FF>::check_circuit()
     }
     return true;
 }
+
+/**
+ * Export the existing circuit as msgpack compatible buffer.
+ *
+ * @return msgpack compatible buffer
+ */
+template <typename FF> msgpack::sbuffer StandardCircuitBuilder_<FF>::export_circuit()
+{
+    using base = CircuitBuilderBase<arithmetization::Standard<FF>>;
+    CircuitSchema cir;
+    
+    uint64_t modulus[4] = {FF::Params::modulus_0, FF::Params::modulus_1, FF::Params::modulus_2, FF::Params::modulus_3};
+    std::stringstream buf;
+    buf << std::hex << std::setfill('0') 
+        << std::setw(16) << modulus[3] 
+        << std::setw(16) << modulus[2] 
+        << std::setw(16) << modulus[1] 
+        << std::setw(16) << modulus[0];
+
+    cir.modulus = buf.str();
+    
+    for (uint32_t i = 0; i < this->get_num_public_inputs(); i++) {
+        cir.public_inps.push_back(this->real_variable_index[this->public_inputs[i]]);
+    }
+
+    for (auto& tup : base::variable_names) {
+        cir.vars_of_interest.insert({ this->real_variable_index[tup.first], tup.second });
+    }
+
+    for (auto var : this->variables) {
+        cir.variables.push_back(var);
+    }
+
+    for (size_t i = 0; i < this->num_gates; i++) {
+        std::vector<FF> tmp_sel = { q_m[i], q_1[i], q_2[i], q_3[i], q_c[i] };
+        std::vector<uint32_t> tmp_w = {
+            this->real_variable_index[w_l[i]],
+            this->real_variable_index[w_r[i]],
+            this->real_variable_index[w_o[i]],
+        };
+        cir.selectors.push_back(tmp_sel);
+        cir.wires.push_back(tmp_w);
+    }
+
+    msgpack::sbuffer buffer;
+    msgpack::pack(buffer, cir);
+    return buffer;
+}
+
 template class StandardCircuitBuilder_<barretenberg::fr>;
 template class StandardCircuitBuilder_<grumpkin::fr>;
+
 } // namespace proof_system

circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp

@@ -113,6 +113,19 @@ template <typename FF> class StandardCircuitBuilder_ : public CircuitBuilderBase
     size_t get_num_constant_gates() const override { return 0; }
 
     bool check_circuit();
+
+    msgpack::sbuffer export_circuit() override;
+
+  private:
+    struct CircuitSchema {
+        std::string modulus;
+        std::vector<uint32_t> public_inps;
+        std::unordered_map<uint32_t, std::string> vars_of_interest;
+        std::vector<FF> variables;
+        std::vector<std::vector<FF>> selectors;
+        std::vector<std::vector<uint32_t>> wires;
+        MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wires);
+    } circuit_schema;
 };
 
 extern template class StandardCircuitBuilder_<barretenberg::fr>;

circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt

@@ -0,0 +1,2 @@
+#barretenberg_module(smt_verification common ${CMAKE_SOURCE_DIR}/src/cvc5/tmp-lib/lib/libcvc5.so.1)
+barretenberg_module(smt_verification common proof_system stdlib_primitives $ENV{HOME}/cvc5/tmp-lib/lib/libcvc5.so.1)