feat: SMT Verificaiton Module: Data Structures (#13658)

This pr adds new Symbolic objects: Tuple, Array and Set 

# Data Structures

- Added `STuple`, `SymArray`, `SymSet` classes to ease up lookup tables
and ROM/RAM arrays symbolic translation
- Reflected new symbolic objects in `UltraCircuit`, `STerm` and `Solver`

- Added tests for all of the new structures
- Added pretty print for these structures

# Bool

added tests for symbolic bool class

# Solver

- Added a few more default solver configurations to use. 
- Added `ff_bitsum` option to solver config. It allows solver to
understand bitsums (namely constraints of the form `b0 + 2 * b1 + 4 * b2
+ ... == X`)
- Added few more debug solver options
- Added few options to handle arrays and sets
- Fixed a bug: `lookup_enabled` was not handled properly

Author: Sarkoxed

barretenberg/cpp/src/barretenberg/smt_verification/README.md

@@ -134,6 +134,8 @@ To store it on the disk just do the following
 
 4. Terms creation
 
+    ### Arithmetic Variables
+
     You can initialize symbolic variable via `STerm::Var(str name, &solver, TermType type)` or `STerm::Const(str val, &solver, TermType type, u32 base=16)`
 
     But also you can use `FFVar(str name, &Solver)` or equivalently via `FFIVar` and `BVVar` so you don't have to mess with types.
@@ -162,10 +164,12 @@ To store it on the disk just do the following
     - `STerm::in(cvc5::Term table&)` - simple set inclusion.
     - `static STerm::in_table(std::vector<STerm> entry, cvc5::Term& table)` - lookup table inclusion.
 
-    ---
+    --- 
+
+    ### Boolean Variables
 
 	There is a Bool type:
-	- `Bool Bool(STerm t)` or `Bool Bool(bool b, Solver* s)`
+	- `Bool Bool(STerm t)`, `Bool Bool(bool b, Solver* s)` or `Bool(str name, Solver* s)`
 
 	You can `|, &, ==, !=, !` these variables and also `batch_or`, `batch_and` them.
 	To create a constraint you should call `Bool::assert_term()` method.
@@ -175,6 +179,84 @@ To store it on the disk just do the following
     **!Note that constraint like `(Bool(STerm a) == Bool(STerm b)).assert_term()`, where a has `FFTerm` type and b has `FFITerm` type, won't work, since their types differ.**
     **!Note `Bool(a == b)` won't work since `a==b` will create an equality constraint as I mentioned earlier and the return type of this operation is `void`.**
 
+    --- 
+
+    ### Data Structures
+
+    There're three extra data structures:
+
+    #### STuple
+
+    Symbolic Tuple type. 
+    You can group several items in one term. 
+    **!Note Only compatible with `STerm` class**
+
+    `STuple STuple(vec<STerm>, Solver* slv)`
+
+    **!Note that you can not access the element of the tuple by its index after creation**
+
+    #### SymArray
+
+    Symbolic Array type. 
+    You can store symbolic values. And access them by symbolic index.
+
+    Both index and entry can be any of the symbolic types: `STerm`, `Bool`, `STuple`, `SymArray`, `SymSet`
+
+    Create an empty array:
+    `SymArray SymArray<sym_index, sym_entry>(cvc5:Sort idx_sort, TermType idx_type, cvc5::Sort entry_sort, TermType entry_type, Solver* s, str name = "")`
+
+    ***!Note passing cvc5 native types directly is a little bit advanced compared to the ordinary usage of this module. See the tests***
+
+    Create an array from indicies and entrys:
+    `SymArray SymArray<sym_index, sym_entry>(vector<sym_index> indicies, vec<sym_entry> entries, str name = "")`
+
+    Create an integer indexed array from entries:
+    `SymArray SymArray<sym_index, sym_entry>(vec<sym_entry> entries, STerm index_base, str name = "")`
+
+    **!Note you need to provide an example for the integer like index entry. Most of the time you'll be fine using: `index_base` = `FFConst(1, &slv)`| `FFIConst(1, &slv)`| `IConst(1, &slv)`| `BVConst(1, &slv)`**
+
+    After you've created an array you can put/overwrite elements in it by:
+
+    `arr.put(sym_idx, sym_entry)`
+
+    And access them:
+
+    `arr.get(sym_idx)`
+    `arr[sym_idx]`
+
+
+    For debugging purposes there's a `print_trace` method, that will print all the `put` operations
+
+    #### SymSet
+
+    Symbolic Set type. 
+    You can store symbolic values. You can check wheter an element belong to the set or not.
+
+    Entries can be any of the symbolic types: `STerm`, `Bool`, `STuple`, `SymArray`, `SymSet`
+
+    Create an empty set:
+    `SymSet SymSet<sym_entry>(cvc5::Sort entry_sort, TermType entry_type, Solver* s, str name = "")`
+
+    ***!Note passing cvc5 native types directly is a little bit advanced compared to the ordinary usage of this module. See the tests***
+
+    Create a set from vector of values:
+    `SymSet SymSet<sym_entry>(vec<sym_entry> entries, str name = "")`
+
+    After you've created a set you can put elements in it by:
+
+    `set.insert(sym_entry)`
+
+    And add inclusion constraints:
+
+    `set.contains(entry)`
+    `set.not_contains(entry)`
+
+    For debugging purposes there's a `print_trace` method, that will print all the `insert` operations
+
+    ---
+
+    All the types support printing their name in variable case and value in constant case
+
 ## 3. Post model checking
 After generating all the constrains you should call `bool res = solver.check()` and depending on your goal it could be `true` or `false`.
 
@@ -263,6 +345,10 @@ Avalaible test suits in `smt_verification_tests`:
 - `FFITerm*`
 - `ITerm*`
 - `BVTerm*`
+- `SymbolicBool*`
+- `SymbolicTuple*`
+- `SymbolicArray*`
+- `SymbolicSet*`
 ---
 
 - `Subcircuits*`
@@ -402,6 +488,8 @@ void model_variables(SymCircuit& c, Solver* s, FFTerm& evaluation)
 More examples can be found in
 
 - [terms/ffterm.test.cpp](terms/ffterm.test.cpp), [terms/ffiterm.test.cpp](terms/ffiterm.test.cpp), [terms/bvterm.test.cpp](terms/bvterm.test.cpp), [terms/iterm.test.cpp](terms/iterm.test.cpp)
+- [terms/bool.test.cpp](terms/bool.test.cpp)
+- [terms/data_types.test.cpp]
 - [circuit/standard_circuit.test.cpp](circuit/standard_circuit.test.cpp), [circuit/ultra_circuit](circuit/ultra_circuit.test.cpp)
 - [smt_polynomials.test.cpp](smt_polynomials.test.cpp), [smt_examples.test.cpp](smt_examples.test.cpp)
 - [bb_tests](bb_tests)

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

@@ -6,6 +6,7 @@
 #include <unordered_map>
 
 #include "barretenberg/smt_verification/terms/bool.hpp"
+#include "barretenberg/smt_verification/terms/data_structures.hpp"
 #include "barretenberg/smt_verification/terms/term.hpp"
 
 #include "subcircuits.hpp"

barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp

@@ -140,34 +140,38 @@ size_t UltraCircuit::handle_arithmetic_relation(size_t cursor, size_t idx)
 
 void UltraCircuit::process_new_table(uint32_t table_idx)
 {
-    std::vector<std::vector<cvc5::Term>> new_table;
+    std::vector<STuple> new_table;
     bool is_xor = true;
     bool is_and = true;
 
     for (auto table_entry : this->lookup_tables[table_idx]) {
-        std::vector<cvc5::Term> tmp_entry = {
+        STuple tmp_entry({
             STerm(table_entry[0], this->solver, this->type),
             STerm(table_entry[1], this->solver, this->type),
             STerm(table_entry[2], this->solver, this->type),
-        };
+        });
         new_table.push_back(tmp_entry);
 
         is_xor &= (static_cast<uint256_t>(table_entry[0]) ^ static_cast<uint256_t>(table_entry[1])) ==
                   static_cast<uint256_t>(table_entry[2]);
         is_and &= (static_cast<uint256_t>(table_entry[0]) & static_cast<uint256_t>(table_entry[1])) ==
                   static_cast<uint256_t>(table_entry[2]);
     }
-    this->cached_symbolic_tables.insert({ table_idx, this->solver->create_lookup_table(new_table) });
+    info("Creating lookup table №", this->cached_symbolic_tables.size());
+    std::string table_name;
     if (is_xor) {
+        table_name = "XOR_TABLE_" + std::to_string(new_table.size());
         this->tables_types.insert({ table_idx, TableType::XOR });
-        info("Encountered a XOR table");
     } else if (is_and) {
+        table_name = "AND_TABLE_" + std::to_string(new_table.size());
         this->tables_types.insert({ table_idx, TableType::AND });
-        info("Encountered an AND table");
     } else {
+        table_name = "UNK_TABLE_" + std::to_string(new_table.size());
         this->tables_types.insert({ table_idx, TableType::UNKNOWN });
-        info("Encountered an UNKNOWN table");
     }
+    info(table_name);
+    SymSet<STuple> new_stable(new_table, this->tag + table_name);
+    this->cached_symbolic_tables.insert({ table_idx, new_stable });
 }
 
 /**
@@ -213,7 +217,6 @@ size_t UltraCircuit::handle_lookup_relation(size_t cursor, size_t idx)
     STerm first_entry = this->symbolic_vars[w_l_idx] + q_r * this->symbolic_vars[w_l_shift_idx];
     STerm second_entry = this->symbolic_vars[w_r_idx] + q_m * this->symbolic_vars[w_r_shift_idx];
     STerm third_entry = this->symbolic_vars[w_o_idx] + q_c * this->symbolic_vars[w_o_shift_idx];
-    std::vector<STerm> entries = { first_entry, second_entry, third_entry };
 
     if (this->type == TermType::BVTerm && this->enable_optimizations) {
         // Sort of an optimization.
@@ -237,7 +240,8 @@ size_t UltraCircuit::handle_lookup_relation(size_t cursor, size_t idx)
         }
     }
     info("Unknown Table");
-    STerm::in_table(entries, this->cached_symbolic_tables[table_idx]);
+    STuple entries({ first_entry, second_entry, third_entry });
+    this->cached_symbolic_tables[table_idx].contains(entries);
     return cursor + 1;
 }
 
@@ -380,14 +384,16 @@ void UltraCircuit::handle_range_constraints()
             uint64_t range = this->range_tags[tag];
             if (this->type == TermType::FFTerm || !this->enable_optimizations) {
                 if (!this->cached_range_tables.contains(range)) {
-                    std::vector<cvc5::Term> new_range_table;
+                    std::vector<STerm> new_range_table;
                     for (size_t entry = 0; entry < range; entry++) {
                         new_range_table.push_back(STerm(entry, this->solver, this->type));
                     }
-                    this->cached_range_tables.insert({ range, this->solver->create_table(new_range_table) });
+                    std::string table_name = this->tag + "RANGE_" + std::to_string(range);
+                    SymSet<STerm> new_range_stable(new_range_table, table_name);
+                    info("Initialized new range: ", table_name);
+                    this->cached_range_tables.insert({ range, new_range_stable });
                 }
-
-                this->symbolic_vars[i].in(this->cached_range_tables[range]);
+                this->cached_range_tables[range].contains(this->symbolic_vars[i]);
             } else {
                 this->symbolic_vars[i] <= range;
             }

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

@@ -23,9 +23,9 @@ class UltraCircuit : public CircuitBase {
     std::vector<std::vector<std::vector<uint32_t>>> wires_idxs; // values of the gates' wires idxs
 
     std::vector<std::vector<std::vector<bb::fr>>> lookup_tables;
-    std::unordered_map<uint32_t, cvc5::Term> cached_symbolic_tables;
+    std::unordered_map<uint32_t, SymSet<STuple>> cached_symbolic_tables;
     std::unordered_map<uint32_t, TableType> tables_types;
-    std::unordered_map<uint64_t, cvc5::Term> cached_range_tables;
+    std::unordered_map<uint64_t, SymSet<STerm>> cached_range_tables;
 
     explicit UltraCircuit(CircuitSchema& circuit_info,
                           Solver* solver,