feat: extend SMT Utils (#7126)

This pr resolves several issues with Symbolic Circuits and adds new
functionality to smt_util

## CircuitBase / StandardCircuit / UltraCircuit

`bool optimizations` -> `bool enable_optimizations`

## STerm

Added comment about an origin of the division result name

## smt_util.cpp

- new function `bb::fr string_to_fr(std::string number, int base, size_t
step = 0)` allows to convert string values of an arbitrary base(but most
importantly 2, 10 and 16) to `bb::fr`. Need this because of the huge
witnesses, provided by the solver, that cause segfaults during ordinary
import.

- `default_model` and `default_model_single` now export the `msgpack`'d
version of a witness too.
- `import_witness`, `import_witness_single` imports the packed witness
from file

## README

added all this to README.md file

## Standard Symbolic Circuit

Fixed an issue that caused merging of two consecutive xors into one
while applying an optimization. It thought that two consecutive 32 bit
xors is one 64 bit xor. Now it's not.

+ added the test to check this behavior

## Ultra Symbolic Circuit

Moved lookup table initialization to the separate method. Added xor and
and tables detection with further optimizations.

Added two tests that check that everything is fine.

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

@@ -12,7 +12,7 @@ ExternalProject_Add(
     GIT_REPOSITORY "https://github.com/cvc5/cvc5.git"
     GIT_TAG main
     BUILD_IN_SOURCE YES
-    CONFIGURE_COMMAND ${SHELL} ./configure.sh production --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ --prefix=${CVC5_BUILD}
+    CONFIGURE_COMMAND ${SHELL} ./configure.sh production --gpl --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ --prefix=${CVC5_BUILD}
     BUILD_COMMAND make -C build
     INSTALL_COMMAND make -C build install
     UPDATE_COMMAND ""     # No update step

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

@@ -184,11 +184,17 @@ Now you have the values of the specified terms, which resulted into `true` resul
 **!Note that the return values are decimal strings/binary strings**, so if you want to use them later you should use `FFConst` with base 10, etc.
 
 Also, there is a header file "barretenberg/smt_verification/utl/smt_util.hpp" that contains two useful functions:
-- `default_model(verctor<str> special_names, circuit1, circuit2, *solver, fname="witness.out")`
-- `default_model_single(vector<str> special_names, circuit, *solver, fname="witness.out)`
+- `default_model(verctor<str> special_names, circuit1, circuit2, *solver, fname="witness.out", bool pack = true)`
+- `default_model_single(vector<str> special_names, circuit, *solver, fname="witness.out, bool pack = true)`
 
 These functions will write witness variables in c-like array format into file named `fname`.
 The vector of `special_names` is the values that you want ot see in stdout.
+`pack` argument tells this function to save an `msgpack` buffer of the witness on disk. Name of the file will be `fname`.pack 
+
+You can then import the saved witness using one of the following functions:
+
+- `vec<vec<fr>> import_witness(str fname)`
+- `vec<fr> import_witness_single(str fname)`
 
 ## 4. Automated verification of a unique witness
 There's a static member of `StandardCircuit` and `UltraCircuit` 
@@ -211,6 +217,7 @@ Besides already mentioned `smt_timer`, `default_model` and `default_model_single
 
 - `pair<vector<fr>, vector<fr>> base4(uint32_t el)` - that will return base4 accumulators
 - `void fix_range_lists(UltraCircuitBuilder& builder)` - Since we are not using the part of the witness, that contains range lists, they are set to 0 by the solver. We need to overwrite them to check the witness obtained by the solver.
+- `bb::fr string_to_fr(str num, int base, size_t step)` - converts string of an arbitrary base into `bb::fr` value. $\max_{step}(base^{step} \le 2^{64})$
 
 ```c++
     UltraCircuitBuilder builder;

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

@@ -11,14 +11,14 @@ CircuitBase::CircuitBase(std::unordered_map<uint32_t, std::string>& variable_nam
                          Solver* solver,
                          TermType type,
                          const std::string& tag,
-                         bool optimizations)
+                         bool enable_optimizations)
     : variables(variables)
     , 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)
+    , enable_optimizations(enable_optimizations)
     , solver(solver)
     , type(type)
     , tag(tag)

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

@@ -37,7 +37,7 @@ class CircuitBase {
     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
+    bool enable_optimizations;                    // flags to turn on circuit optimizations
     std::unordered_map<SubcircuitType, std::unordered_map<size_t, CircuitProps>>
         cached_subcircuits; // caches subcircuits during optimization
                             // No need to recompute them each time
@@ -58,7 +58,7 @@ class CircuitBase {
                 Solver* solver,
                 TermType type,
                 const std::string& tag = "",
-                bool optimizations = true);
+                bool enable_optimizations = true);
 
     STerm operator[](const std::string& name);
     STerm operator[](const uint32_t& idx) { return this->symbolic_vars[this->real_variable_index[idx]]; };

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

@@ -10,7 +10,7 @@ namespace smt_circuit {
  * @param tag tag of the circuit. Empty by default.
  */
 StandardCircuit::StandardCircuit(
-    CircuitSchema& circuit_info, Solver* solver, TermType type, const std::string& tag, bool optimizations)
+    CircuitSchema& circuit_info, Solver* solver, TermType type, const std::string& tag, bool enable_optimizations)
     : CircuitBase(circuit_info.vars_of_interest,
                   circuit_info.variables,
                   circuit_info.public_inps,
@@ -20,7 +20,7 @@ StandardCircuit::StandardCircuit(
                   solver,
                   type,
                   tag,
-                  optimizations)
+                  enable_optimizations)
     , selectors(circuit_info.selectors[0])
     , wires_idxs(circuit_info.wires[0])
 {
@@ -46,34 +46,34 @@ StandardCircuit::StandardCircuit(
  */
 size_t StandardCircuit::prepare_gates(size_t cursor)
 {
-    if (this->type == TermType::BVTerm && this->optimizations) {
+    if (this->type == TermType::BVTerm && this->enable_optimizations) {
         size_t res = handle_logic_constraint(cursor);
         if (res != static_cast<size_t>(-1)) {
             return res;
         }
     }
 
-    if ((this->type == TermType::BVTerm || this->type == TermType::FFITerm) && this->optimizations) {
+    if ((this->type == TermType::BVTerm || this->type == TermType::FFITerm) && this->enable_optimizations) {
         size_t res = handle_range_constraint(cursor);
         if (res != static_cast<size_t>(-1)) {
             return res;
         }
     }
 
-    if ((this->type == TermType::BVTerm) && this->optimizations) {
+    if ((this->type == TermType::BVTerm) && this->enable_optimizations) {
         size_t res = handle_ror_constraint(cursor);
         if (res != static_cast<size_t>(-1)) {
             return res;
         }
     }
 
-    if ((this->type == TermType::BVTerm) && this->optimizations) {
+    if ((this->type == TermType::BVTerm) && this->enable_optimizations) {
         size_t res = handle_shl_constraint(cursor);
         if (res != static_cast<size_t>(-1)) {
             return res;
         }
     }
-    if ((this->type == TermType::BVTerm) && this->optimizations) {
+    if ((this->type == TermType::BVTerm) && this->enable_optimizations) {
         size_t res = handle_shr_constraint(cursor);
         if (res != static_cast<size_t>(-1)) {
             return res;
@@ -182,6 +182,7 @@ void StandardCircuit::handle_univariate_constraint(
     }
 }
 
+// TODO(alex): Optimized out variables should be filled with proper values...
 /**
  * @brief Relaxes logic constraints(AND/XOR).
  * @details This function is needed when we use bitwise compatible
@@ -252,6 +253,20 @@ size_t StandardCircuit::handle_logic_constraint(size_t cursor)
                 xor_flag &= xor_circuit.selectors[0][j + xor_props.start_gate] == this->selectors[cursor + j];
                 and_flag &= and_circuit.selectors[0][j + and_props.start_gate] == this->selectors[cursor + j];
 
+                // Before this fix this routine simplified two consecutive n bit xors(ands) into one 2n bit xor(and)
+                // Now it checks out_accumulator_idx and new_out_accumulator_idx match
+                // 14 here is a size of one iteration of logic_gate for loop in term of gates
+                // 13 is the accumulator index relative to the beginning of the iteration
+
+                size_t single_iteration_size = 14;
+                size_t relative_acc_idx = 13;
+                xor_flag &=
+                    (j % single_iteration_size != relative_acc_idx) || (j == relative_acc_idx) ||
+                    (this->wires_idxs[j + cursor][0] == this->wires_idxs[j + cursor - single_iteration_size][2]);
+                and_flag &=
+                    (j % single_iteration_size != relative_acc_index) || (j == relative_acc_index) ||
+                    (this->wires_idxs[j + cursor][0] == this->wires_idxs[j + cursor - single_iteration_size][2]);
+
                 if (!xor_flag && !and_flag) {
                     // Won't match at any bit length
                     if (j == 0) {
@@ -411,17 +426,20 @@ size_t StandardCircuit::handle_range_constraint(size_t cursor)
         // preserving shifted values
         // we need this because even right shifts do not create
         // any additional gates and therefore are undetectible
+
+        // TODO(alex): I think I should simulate the whole subcircuit at that point
+        // Otherwise optimized out variables are not correct in the final witness
+        // And I can't fix them by hand each time
         size_t num_accs = range_props.gate_idxs.size() - 1;
         for (size_t j = 1; j < num_accs + 1 && (this->type == TermType::BVTerm); j++) {
             size_t acc_gate = range_props.gate_idxs[j];
             uint32_t acc_gate_idx = range_props.idxs[j];
 
             uint32_t acc_idx = this->real_variable_index[this->wires_idxs[cursor + acc_gate][acc_gate_idx]];
 
-            // TODO(alex): Is it better? Can't come up with why not right now
-            // STerm acc = this->symbolic_vars[acc_idx];
-            // acc == (left >> static_cast<uint32_t>(2 * j));
-            this->symbolic_vars[acc_idx] = (left >> static_cast<uint32_t>(2 * j));
+            this->symbolic_vars[acc_idx] == (left >> static_cast<uint32_t>(2 * j));
+            // I think the following is worse. The name of the variable is lost after that
+            // this->symbolic_vars[acc_idx] = (left >> static_cast<uint32_t>(2 * j));
         }
 
         left <= (bb::fr(2).pow(res) - 1);
@@ -812,10 +830,10 @@ std::pair<StandardCircuit, StandardCircuit> StandardCircuit::unique_witness_ext(
     const std::vector<std::string>& not_equal,
     const std::vector<std::string>& equal_at_the_same_time,
     const std::vector<std::string>& not_equal_at_the_same_time,
-    bool optimizations)
+    bool enable_optimizations)
 {
-    StandardCircuit c1(circuit_info, s, type, "circuit1", optimizations);
-    StandardCircuit c2(circuit_info, s, type, "circuit2", optimizations);
+    StandardCircuit c1(circuit_info, s, type, "circuit1", enable_optimizations);
+    StandardCircuit c2(circuit_info, s, type, "circuit2", enable_optimizations);
 
     for (const auto& term : equal) {
         c1[term] == c2[term];
@@ -863,11 +881,14 @@ std::pair<StandardCircuit, StandardCircuit> StandardCircuit::unique_witness_ext(
  * @param equal The list of names of variables which should be equal in both circuits(each is equal)
  * @return std::pair<Circuit, Circuit>
  */
-std::pair<StandardCircuit, StandardCircuit> StandardCircuit::unique_witness(
-    CircuitSchema& circuit_info, Solver* s, TermType type, const std::vector<std::string>& equal, bool optimizations)
+std::pair<StandardCircuit, StandardCircuit> StandardCircuit::unique_witness(CircuitSchema& circuit_info,
+                                                                            Solver* s,
+                                                                            TermType type,
+                                                                            const std::vector<std::string>& equal,
+                                                                            bool enable_optimizations)
 {
-    StandardCircuit c1(circuit_info, s, type, "circuit1", optimizations);
-    StandardCircuit c2(circuit_info, s, type, "circuit2", optimizations);
+    StandardCircuit c1(circuit_info, s, type, "circuit1", enable_optimizations);
+    StandardCircuit c2(circuit_info, s, type, "circuit2", enable_optimizations);
 
     for (const auto& term : equal) {
         c1[term] == c2[term];
@@ -893,4 +914,4 @@ std::pair<StandardCircuit, StandardCircuit> StandardCircuit::unique_witness(
     }
     return { c1, c2 };
 }
-}; // namespace smt_circuit
+}; // namespace smt_circuit

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

@@ -18,7 +18,7 @@ class StandardCircuit : public CircuitBase {
                              Solver* solver,
                              TermType type = TermType::FFTerm,
                              const std::string& tag = "",
-                             bool optimizations = true);
+                             bool enable_optimizations = true);
 
     inline size_t get_num_gates() const { return selectors.size(); };
 
@@ -40,12 +40,12 @@ class StandardCircuit : public CircuitBase {
         const std::vector<std::string>& not_equal = {},
         const std::vector<std::string>& equal_at_the_same_time = {},
         const std::vector<std::string>& not_equal_at_the_same_time = {},
-        bool optimizations = false);
+        bool enable_optimizations = false);
 
     static std::pair<StandardCircuit, StandardCircuit> unique_witness(CircuitSchema& circuit_info,
                                                                       Solver* s,
                                                                       TermType type,
                                                                       const std::vector<std::string>& equal = {},
-                                                                      bool optimizations = false);
+                                                                      bool enable_optimizations = false);
 };
 }; // namespace smt_circuit

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

@@ -356,3 +356,23 @@ TEST(standard_circuit, shr_relaxation)
         StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
     }
 }
+
+TEST(standard_circuit, check_double_xor_bug)
+{
+    StandardCircuitBuilder builder;
+    uint_ct a = witness_t(&builder, 10);
+    uint_ct b = witness_t(&builder, 10);
+
+    uint_ct c = a ^ b;
+    uint_ct d = a ^ b;
+    d = d ^ c;
+
+    c = a & b;
+    d = a & b;
+    d = d & c;
+
+    auto buf = builder.export_circuit();
+    CircuitSchema circuit_info = unpack_from_buffer(buf);
+    Solver s(circuit_info.modulus, default_solver_config, 16, 64);
+    StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
+}