feat: SMT Verifier for Ultra Arithmetization (#7067)

This pr adds a new Circuit Verifier for Ultra arithmetization.

## `circuit_builder_base.cpp` / `ultra_circuit_builder.cpp` /
CircuitSchema

CircuitSchema object now includes `real_variable_tag` and
`range_tags`(maps tags to ranges) for range constraint detection.

##  UltraCircuit

Translates all(except for aux gates) constraints to solver, including:

- Arithmetic gates - `handle_arithmetic_relation`
- Elliptic gates - `handle_elliptic_relation`
- Lookup constraints - `handle_lookup_relation`
- Range constraints - `handle_range_constraints`
- Delta range constraints, that are skipped for now -
`handle_delta_range_relation`

Also `ultra_circuit.test.cpp` checks that everything is handled
properly.

## Solver

- Moved `stringify_term` inside the solver class, because of set
inclusion logging.
- Added logging for set inclusion
- Added ordinary set creation via `create_table`
- Added `ultra_solver_config` that enables set logic


## STerm

Now has `in` method for set inclusion.

---------

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

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
  *