feat: creating an SMT verification module

.gitmodules

@@ -10,3 +10,6 @@
 [submodule "build-system"]
 	path = build-system
 	url = [email protected]:AztecProtocol/build-system.git
+[submodule "cpp/src/cvc5"]
+	path = cpp/src/cvc5
+	url = [email protected]:Sarkoxed/cvc5.git

cpp/src/CMakeLists.txt

@@ -39,6 +39,29 @@ endif()
 
 include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/msgpack-c/include)
 
+#include(ExternalProject)
+#ExternalProject_Add(cvc5
+#    GIT_REPOSITORY https://github.com/Sarkoxed/cvc5
+#    GIT_TAG origin/finite-field-base-support
+#    SOURCE_DIR src/cvc5
+#    BINARY_DIR build-cvc5
+#    CMAKE_ARGS
+# #       -DCMAKE_INSTAL_PREFIX:PATH=    
+# #       -DCMAKE_PREFIX_PATH="${CMAKE_BINARY_DIR}/tmp"
+#        -DCMAKE_BUILD_TYPE=Production
+#        -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}
+#         -DCMAKE_C_COMPILER=/usr/bin/clang 
+#         -DCMAKE_CXX_COMPILER=/usr/bin/clang++ 
+#         -DENABLE_AUTO_DOWNLOAD=ON 
+#         -DBUILD_SHARED_LIBS=OFF 
+#         -DUSE_CRYPTOMINISAT=ON 
+#         -DUSE_POLY=ON 
+#         -DUSE_COCOA=ON 
+# )
+include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/tmp-lib/include)
+#add_subdirectory(cvc5)
+
+
 # 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)
@@ -68,6 +91,8 @@ add_subdirectory(barretenberg/solidity_helpers)
 add_subdirectory(barretenberg/wasi)
 add_subdirectory(barretenberg/grumpkin_srs_gen)
 add_subdirectory(barretenberg/bb)
+add_subdirectory(barretenberg/smt_verification)
+
 
 if(BENCHMARKS)
     add_subdirectory(barretenberg/benchmark)

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 calss). 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 into msgpack compatible buffer.
+     *
+     * @return msgpack compatible buffer
+     */
+    virtual msgpack::sbuffer export_circuit()
+    {
+        info("not implemented");
+        return { 0 };
+    };
+
     /**
      * Add a public variable to variables
      *

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,48 @@ template <typename FF> bool StandardCircuitBuilder_<FF>::check_circuit()
     }
     return true;
 }
+
+/**
+ * Export the existing circuit into msgpack compatible buffer.
+ *
+ * @return msgpack compatible buffer
+ */
+template <typename FF> msgpack::sbuffer StandardCircuitBuilder_<FF>::export_circuit()
+{
+    using base = CircuitBuilderBase<arithmetization::Standard<FF>>;
+
+    CircuitSchema cir;
+    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_wit = {
+            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.wits.push_back(tmp_wit);
+    }
+
+    msgpack::sbuffer buffer;
+    msgpack::pack(buffer, cir);
+    return buffer;
+    // info("Buffer size: ", buffer.size());
+    // out.write(buffer.data(), static_cast<long>(buffer.size()));
+}
+
 template class StandardCircuitBuilder_<barretenberg::fr>;
 template class StandardCircuitBuilder_<grumpkin::fr>;
+
 } // namespace proof_system

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

@@ -113,6 +113,18 @@ 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::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>> wits;
+        MSGPACK_FIELDS(public_inps, vars_of_interest, variables, selectors, wits);
+    } circuit_schema;
 };
 
 extern template class StandardCircuitBuilder_<barretenberg::fr>;

cpp/src/barretenberg/smt_verification/CMakeLists.txt

@@ -0,0 +1,5 @@
+barretenberg_module(smt_verification common ${CMAKE_SOURCE_DIR}/src/cvc5/tmp-lib/lib/libcvc5.so.1)
+
+barretenberg_module(smt_examples common proof_system stdlib_primitives smt_verification)
+#barretenberg_module(smt_polynomials common proof_system stdlib_primitives smt_verification)
+#barretenberg_module(smt_bigfield common proof_system stdlib_primitives smt_verification)