feat: Update the core of SMT Circuit class (#5096)

This pr massively updates the Circuit class and does a little
refactoring to corresponding c++ files

### circuit_schema

Moved CircuitSchema structure and the corresponding function to the
separate file

Fixed the `read_from_file` function.

### subcircuits

These files will contain calls to the circuitbuilder to get the basic
constraints for native operations(like +, ^ for uints). They will be
used to relax the constraint system when working with Integers or
BitVectors

### Circuit and standard circuit builder

- New member of CircuitSchema and Circuit: real_variable_index.
Previously all the variables(even copied ones) were passed into solver
and it lead to unreliable results. Won't happen anymore.
- New member of Circuit: variable_names_inverse. Helps to identify
existing named variables
- `add_gates()` method now renamed to `prepare_gates()` and behaves
differently. Going to include optimizations from subcircuits.


- New function `unique_witness`
- Previous `unique_witness` was renamed to `unique_witness_ext` since
it's the extended version of the new one. It has more flexible inputs.

---------

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

barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp

@@ -559,6 +559,8 @@ template <typename FF> msgpack::sbuffer StandardCircuitBuilder_<FF>::export_circ
         cir.wires.push_back(tmp_w);
     }
 
+    cir.real_variable_index = this->real_variable_index;
+
     msgpack::sbuffer buffer;
     msgpack::pack(buffer, cir);
     return buffer;

barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp

@@ -115,7 +115,8 @@ template <typename FF> class StandardCircuitBuilder_ : public CircuitBuilderBase
         std::vector<FF> variables;
         std::vector<std::vector<FF>> selectors;
         std::vector<std::vector<uint32_t>> wires;
-        MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wires);
+        std::vector<uint32_t> real_variable_index;
+        MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wires, real_variable_index);
     } circuit_schema;
 };
 

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

@@ -3,73 +3,27 @@
 namespace smt_circuit {
 
 /**
- * @brief Get the CircuitSchema object
- * @details Initialize the CircuitSchmea from the binary file
- * that contains an msgpack compatible buffer.
- *
- * @param filename
- * @return CircuitSchema
- */
-CircuitSchema unpack_from_file(const std::string& filename)
-{
-    std::ifstream fin;
-    fin.open(filename, std::ios::in | std::ios::binary);
-    if (!fin.is_open()) {
-        throw std::invalid_argument("file not found");
-    }
-    if (fin.tellg() == -1) {
-        throw std::invalid_argument("something went wrong");
-    }
-
-    fin.ignore(std::numeric_limits<std::streamsize>::max()); // ohboy
-    std::streamsize fsize = fin.gcount();
-    fin.clear();
-    fin.seekg(0, std::ios_base::beg);
-    info("File size: ", fsize);
-
-    CircuitSchema cir;
-    char* encoded_data = (char*)aligned_alloc(64, static_cast<size_t>(fsize));
-    fin.read(encoded_data, fsize);
-    msgpack::unpack((const char*)encoded_data, static_cast<size_t>(fsize)).get().convert(cir);
-    return cir;
-}
-
-/**
- * @brief Get the CircuitSchema object
- * @details Initialize the CircuitSchmea from the msgpack compatible buffer.
- *
- * @param buf
- * @return CircuitSchema
- */
-CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf)
-{
-    CircuitSchema cir;
-    msgpack::unpack(buf.data(), buf.size()).get().convert(cir);
-    return cir;
-}
-
-/**
- * @brief Check your circuit for witness uniqness
+ * @brief Check your circuit for witness uniqueness
  *
  * @details Creates two Circuit objects that represent the same
  * circuit, however you can choose which variables should be (not) equal in both cases,
  * and also the variables that should (not) be equal at the same time.
  *
  * @param circuit_info
  * @param s pointer to the global solver
- * @param equal all the variables that should be equal in both circuits
- * @param nequal all the variables that should be different in both circuits
- * @param eqall all the variables that should not be equal at the same time
- * @param neqall all the variables that should not be different at the same time
+ * @param equal The list of names of variables which should be equal in both circuits(each is equal)
+ * @param not_equal The list of names of variables which should not be equal in both circuits(each is not equal)
+ * @param equal_at_the_same_time The list of variables, where at least one pair has to be equal
+ * @param not_equal_at_the_same_time The list of variables, where at least one pair has to be distinct
  * @return std::pair<Circuit, Circuit>
  */
 template <typename FF>
-std::pair<Circuit<FF>, Circuit<FF>> unique_witness(CircuitSchema& circuit_info,
-                                                   Solver* s,
-                                                   const std::vector<std::string>& equal,
-                                                   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)
+std::pair<Circuit<FF>, Circuit<FF>> unique_witness_ext(CircuitSchema& circuit_info,
+                                                       Solver* s,
+                                                       const std::vector<std::string>& equal,
+                                                       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)
 {
     Circuit<FF> c1(circuit_info, s, "circuit1");
     Circuit<FF> c2(circuit_info, s, "circuit2");
@@ -107,20 +61,70 @@ std::pair<Circuit<FF>, Circuit<FF>> unique_witness(CircuitSchema& circuit_info,
     return { c1, c2 };
 }
 
-template std::pair<Circuit<FFTerm>, Circuit<FFTerm>> unique_witness(
+template std::pair<Circuit<FFTerm>, Circuit<FFTerm>> unique_witness_ext(
     CircuitSchema& circuit_info,
     Solver* s,
     const std::vector<std::string>& equal = {},
     const std::vector<std::string>& not_equal = {},
     const std::vector<std::string>& equal_at_the_same_time = {},
     const std::vector<std::string>& not_eqaul_at_the_same_time = {});
 
-template std::pair<Circuit<FFITerm>, Circuit<FFITerm>> unique_witness(
+template std::pair<Circuit<FFITerm>, Circuit<FFITerm>> unique_witness_ext(
     CircuitSchema& circuit_info,
     Solver* s,
     const std::vector<std::string>& equal = {},
     const std::vector<std::string>& not_equal = {},
     const std::vector<std::string>& equal_at_the_same_time = {},
     const std::vector<std::string>& not_eqaul_at_the_same_time = {});
 
+/**
+ * @brief Check your circuit for witness uniqueness
+ *
+ * @details Creates two Circuit objects that represent the same
+ * circuit, however you can choose which variables should be equal in both cases,
+ * other witness members will be marked as not equal at the same time
+ * or basically they will have to differ by at least one element.
+ *
+ * @param circuit_info
+ * @param s pointer to the global solver
+ * @param equal The list of names of variables which should be equal in both circuits(each is equal)
+ * @return std::pair<Circuit, Circuit>
+ */
+template <typename FF>
+std::pair<Circuit<FF>, Circuit<FF>> unique_witness(CircuitSchema& circuit_info,
+                                                   Solver* s,
+                                                   const std::vector<std::string>& equal)
+{
+    Circuit<FF> c1(circuit_info, s, "circuit1");
+    Circuit<FF> c2(circuit_info, s, "circuit2");
+
+    for (const auto& term : equal) {
+        c1[term] == c2[term];
+    }
+
+    std::vector<Bool> neqs;
+    for (const auto& node : c1.symbolic_vars) {
+        uint32_t i = node.first;
+        if (std::find(equal.begin(), equal.end(), std::string(c1.variable_names[i])) != equal.end()) {
+            continue;
+        }
+        Bool tmp = Bool(c1[i]) != Bool(c2[i]);
+        neqs.push_back(tmp);
+    }
+
+    if (neqs.size() > 1) {
+        batch_or(neqs).assert_term();
+    } else if (neqs.size() == 1) {
+        neqs[0].assert_term();
+    }
+    return { c1, c2 };
+}
+
+template std::pair<Circuit<FFTerm>, Circuit<FFTerm>> unique_witness(CircuitSchema& circuit_info,
+                                                                    Solver* s,
+                                                                    const std::vector<std::string>& equal = {});
+
+template std::pair<Circuit<FFITerm>, Circuit<FFITerm>> unique_witness(CircuitSchema& circuit_info,
+                                                                      Solver* s,
+                                                                      const std::vector<std::string>& equal = {});
 }; // namespace smt_circuit