feat: SMT Standard Circuit separation

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

@@ -0,0 +1,82 @@
+#include "circuit_base.hpp"
+
+namespace smt_circuit {
+
+CircuitBase::CircuitBase(std::unordered_map<uint32_t, std::string>& variable_names,
+                         std::vector<bb::fr>& variables,
+                         std::vector<uint32_t>& public_inps,
+                         std::vector<uint32_t>& real_variable_index,
+                         Solver* solver,
+                         TermType type,
+                         const std::string& tag,
+                         bool optimizations)
+    : variables(variables)
+    , public_inps(public_inps)
+    , variable_names(variable_names)
+    , real_variable_index(real_variable_index)
+    , optimizations(optimizations)
+    , solver(solver)
+    , type(type)
+    , tag(tag)
+{
+    if (!this->tag.empty() && tag[0] != '_') {
+        this->tag = "_" + this->tag;
+    }
+
+    for (auto& x : variable_names) {
+        variable_names_inverse.insert({ x.second, x.first });
+    }
+
+    this->init();
+
+    for (const auto& i : this->public_inps) {
+        this->symbolic_vars[this->real_variable_index[i]] == this->variables[i];
+    }
+}
+
+/**
+ * Creates all the needed symbolic variables and constants
+ * which are used in circuit.
+ *
+ */
+void CircuitBase::init()
+{
+    variable_names.insert({ 0, "zero" });
+    variable_names_inverse.insert({ "zero", 0 });
+    symbolic_vars.insert({ 0, STerm::Var("zero" + this->tag, this->solver, this->type) });
+    optimized.insert({ 0, false });
+
+    size_t num_vars = variables.size();
+
+    for (uint32_t i = 1; i < num_vars; i++) {
+        uint32_t real_idx = this->real_variable_index[i];
+        if (this->symbolic_vars.contains(real_idx)) {
+            continue;
+        }
+
+        std::string name = variable_names.contains(real_idx) ? variable_names[real_idx] : "var_" + std::to_string(i);
+        name += this->tag;
+        symbolic_vars.insert({ real_idx, STerm::Var(name, this->solver, this->type) });
+
+        optimized.insert({ real_idx, true });
+    }
+
+    symbolic_vars[0] == bb::fr(0);
+}
+
+/**
+ * @brief Returns a previously named symbolic variable.
+ *
+ * @param name
+ * @return STerm
+ */
+STerm CircuitBase::operator[](const std::string& name)
+{
+    if (!this->variable_names_inverse.contains(name)) {
+        throw std::invalid_argument("No such an item `" + name + "` in vars or it vas not declared as interesting");
+    }
+    uint32_t idx = this->variable_names_inverse[name];
+    return this->symbolic_vars[idx];
+}
+
+} // namespace smt_circuit

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

@@ -0,0 +1,74 @@
+#pragma once
+
+#include <limits>
+#include <sstream>
+#include <string>
+#include <unordered_map>
+
+#include "barretenberg/smt_verification/terms/bool.hpp"
+#include "barretenberg/smt_verification/terms/term.hpp"
+
+#include "subcircuits.hpp"
+
+namespace smt_circuit {
+using namespace smt_solver;
+using namespace smt_terms;
+using namespace smt_circuit_schema;
+using namespace smt_subcircuits;
+
+enum class SubcircuitType { XOR, AND, RANGE, ROR, SHL, SHR };
+
+/**
+ * @brief Base class for symbolic circuits
+ *
+ * @details Contains all the information about the circuit: gates, variables,
+ * symbolic variables, specified names, global solver and optimiztaions.
+ *
+ */
+class CircuitBase {
+  public:
+    std::vector<bb::fr> variables;                                    // circuit witness
+    std::vector<uint32_t> public_inps;                                // public inputs from the circuit
+    std::unordered_map<uint32_t, std::string> variable_names;         // names of the variables
+    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::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
+    std::unordered_map<SubcircuitType, std::unordered_map<size_t, CircuitProps>>
+        cached_subcircuits; // caches subcircuits during optimization
+                            // No need to recompute them each time
+
+    Solver* solver; // pointer to the solver
+    TermType type;  // Type of the underlying Symbolic Terms
+
+    std::string tag; // tag of the symbolic circuit.
+                     // If not empty, will be added to the names
+                     // of symbolic variables to prevent collisions.
+
+    CircuitBase(std::unordered_map<uint32_t, std::string>& variable_names,
+                std::vector<bb::fr>& variables,
+                std::vector<uint32_t>& public_inps,
+                std::vector<uint32_t>& real_variable_index,
+                Solver* solver,
+                TermType type,
+                const std::string& tag = "",
+                bool optimizations = true);
+
+    STerm operator[](const std::string& name);
+    STerm operator[](const uint32_t& idx) { return this->symbolic_vars[this->real_variable_index[idx]]; };
+    inline size_t get_num_real_vars() const { return symbolic_vars.size(); };
+    inline size_t get_num_vars() const { return variables.size(); };
+
+    void init();
+    virtual bool simulate_circuit_eval(std::vector<bb::fr>& witness) const = 0;
+
+    CircuitBase(const CircuitBase& other) = default;
+    CircuitBase(CircuitBase&& other) noexcept = default;
+    CircuitBase& operator=(const CircuitBase& other) = default;
+    CircuitBase& operator=(CircuitBase&& other) noexcept = default;
+    virtual ~CircuitBase() = default;
+};
+
+}; // namespace smt_circuit