feat: SMT Verifier for Ultra Arithmetization

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

@@ -26,7 +26,7 @@ add_dependencies(cvc5-lib cvc5)
 include_directories(${CVC5_INCLUDE})
 set_target_properties(cvc5-lib PROPERTIES IMPORTED_LOCATION ${CVC5_LIB})
 
-barretenberg_module(smt_verification common stdlib_primitives stdlib_sha256 circuit_checker transcript plonk cvc5-lib)
+barretenberg_module(smt_verification common stdlib_primitives stdlib_sha256 circuit_checker transcript plonk stdlib_pedersen_commitment cvc5-lib)
 # We have no easy way to add a dependency to an external target, we list the built targets explicit. Could be cleaner.
 add_dependencies(smt_verification cvc5)
 add_dependencies(smt_verification_objects cvc5)

barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp

@@ -6,6 +6,8 @@ CircuitBase::CircuitBase(std::unordered_map<uint32_t, std::string>& variable_nam
                          std::vector<bb::fr>& variables,
                          std::vector<uint32_t>& public_inps,
                          std::vector<uint32_t>& real_variable_index,
+                         std::vector<uint32_t>& real_variable_tags,
+                         std::unordered_map<uint32_t, uint64_t>& range_tags,
                          Solver* solver,
                          TermType type,
                          const std::string& tag,
@@ -14,6 +16,8 @@ CircuitBase::CircuitBase(std::unordered_map<uint32_t, std::string>& variable_nam
     , public_inps(public_inps)
     , variable_names(variable_names)
     , real_variable_index(real_variable_index)
+    , real_variable_tags(real_variable_tags)
+    , range_tags(range_tags)
     , optimizations(optimizations)
     , solver(solver)
     , type(type)

barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp

@@ -33,6 +33,8 @@ class CircuitBase {
     std::unordered_map<std::string, uint32_t> variable_names_inverse; // inverse map of the previous memeber
     std::unordered_map<uint32_t, STerm> symbolic_vars;                // all the symbolic variables from the circuit
     std::vector<uint32_t> real_variable_index;                        // indexes for assert_equal'd wires
+    std::vector<uint32_t> real_variable_tags;                         // tags of the variables in the circuit
+    std::unordered_map<uint32_t, uint64_t> range_tags;                // ranges associated with a certain tag
     std::unordered_map<uint32_t, bool> optimized; // keeps track of the variables that were excluded from symbolic
                                                   // circuit during optimizations
     bool optimizations;                           // flags to turn on circuit optimizations
@@ -51,6 +53,8 @@ class CircuitBase {
                 std::vector<bb::fr>& variables,
                 std::vector<uint32_t>& public_inps,
                 std::vector<uint32_t>& real_variable_index,
+                std::vector<uint32_t>& real_variable_tags,
+                std::unordered_map<uint32_t, uint64_t>& range_tags,
                 Solver* solver,
                 TermType type,
                 const std::string& tag = "",

barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp

@@ -31,8 +31,18 @@ struct CircuitSchema {
     std::vector<std::vector<std::vector<uint32_t>>> wires;
     std::vector<uint32_t> real_variable_index;
     std::vector<std::vector<std::vector<bb::fr>>> lookup_tables;
-    MSGPACK_FIELDS(
-        modulus, public_inps, vars_of_interest, variables, selectors, wires, real_variable_index, lookup_tables);
+    std::vector<uint32_t> real_variable_tags;
+    std::unordered_map<uint32_t, uint64_t> range_tags;
+    MSGPACK_FIELDS(modulus,
+                   public_inps,
+                   vars_of_interest,
+                   variables,
+                   selectors,
+                   wires,
+                   real_variable_index,
+                   lookup_tables,
+                   real_variable_tags,
+                   range_tags);
 };
 
 CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf);

barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp

@@ -15,6 +15,8 @@ StandardCircuit::StandardCircuit(
                   circuit_info.variables,
                   circuit_info.public_inps,
                   circuit_info.real_variable_index,
+                  circuit_info.real_variable_tags,
+                  circuit_info.range_tags,
                   solver,
                   type,
                   tag,
@@ -438,7 +440,7 @@ size_t StandardCircuit::handle_range_constraint(size_t cursor)
  * It compares the chunk of selectors of the current circuit
  * with pure shift left from uint/logic.cpp
  * After a match is found, it updates the cursor to skip all the
- * redundant constraints and adds a pure b = a.ror(n)
+ * redundant constraints and adds a pure b = a >> n
  * constraint to solver.
  * If there's no match, it will return -1
  *
@@ -547,7 +549,7 @@ size_t StandardCircuit::handle_shr_constraint(size_t cursor)
  * It compares the chunk of selectors of the current circuit
  * with pure shift left from uint/logic.cpp
  * After a match is found, it updates the cursor to skip all the
- * redundant constraints and adds a pure b = a.ror(n)
+ * redundant constraints and adds a pure b = a << n
  * constraint to solver.
  * If there's no match, it will return -1
  *