feat: extend SMT Utils

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);
+}