Documentation

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

@@ -1,6 +1,13 @@
 #include "circuit.hpp"
 namespace smt_circuit {
 
+/**
+ * @brief Construct a new Circuit::Circuit object
+ * 
+ * @param circuit_info CircuitShema object
+ * @param solver pointer to the global solver
+ * @param tag tag of the circuit. Empty by default.
+ */
 Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag)
     : public_inps(circuit_info.public_inps)
     , vars_of_interest(circuit_info.vars_of_interest)
@@ -48,6 +55,11 @@ Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string&
     this->add_gates();
 }
 
+/**
+ * Creates all the needed symbolic variables and constants
+ * which are used in circuit.
+ * 
+ */
 void Circuit::init()
 {
     size_t num_vars = variables.size();
@@ -56,7 +68,6 @@ void Circuit::init()
     vars.push_back(Var("zero" + this->tag, this->solver));
     vars.push_back(Var("one" + this->tag, this->solver));
 
-    // TODO(alex): maybe public variables should be Consts
     for (size_t i = 2; i < num_vars; i++) {
         if (vars_of_interest.contains(static_cast<uint32_t>(i))) {
             std::string name = vars_of_interest[static_cast<uint32_t>(i)];
@@ -74,6 +85,10 @@ void Circuit::init()
     }
 }
 
+/**
+ * @brief Adds all the gate constraints to the solver.
+ * 
+ */
 void Circuit::add_gates()
 {
     for (size_t i = 0; i < get_num_gates(); i++) {
@@ -113,6 +128,12 @@ void Circuit::add_gates()
     }
 }
 
+/**
+ * @brief Returns a previously named symbolic variable.
+ * 
+ * @param name 
+ * @return FFTerm 
+ */
 FFTerm Circuit::operator[](const std::string& name)
 {
     if (!this->terms.contains(name)) {
@@ -122,6 +143,14 @@ FFTerm Circuit::operator[](const std::string& name)
     return this->vars[idx];
 }
 
+/**
+ * @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;
@@ -146,13 +175,35 @@ CircuitSchema unpack_from_file(const std::string& filename)
     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
+ * 
+ * @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
+ * @return std::pair<Circuit, Circuit>
+ */
 std::pair<Circuit, Circuit> unique_witness(CircuitSchema& circuit_info,
                                            Solver* s,
                                            const std::vector<std::string>& equal,

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

@@ -19,6 +19,7 @@ using namespace smt_terms;
 const std::string p = "21888242871839275222246405745257275088548364400416034343698204186575808495617";
 
 struct CircuitSchema {
+    std::string modulus;
     std::vector<uint32_t> public_inps;
     std::unordered_map<uint32_t, std::string> vars_of_interest;
     std::vector<barretenberg::fr> variables;
@@ -27,23 +28,33 @@ struct CircuitSchema {
     MSGPACK_FIELDS(public_inps, vars_of_interest, variables, selectors, wits);
 };
 
-// TODO(alex): think on the partial value assertion inside the circuit.
-class Circuit { // SymCircuit?
+/**
+ * @brief Symbolic Circuit class.
+ * 
+ * @details Contains all the information about the circuit: gates, variables, 
+ * symbolic variables, specified names and global solver.
+ *
+ * @todo TODO(alex): think on the partial value assertion inside the circuit.
+ * @todo TODO(alex): class SymCircuit?
+ */
+class Circuit {
   private:
     void init();
     void add_gates();
 
   public:
-    std::vector<std::string> variables;
-    std::vector<uint32_t> public_inps;
-    std::unordered_map<uint32_t, std::string> vars_of_interest;
-    std::unordered_map<std::string, uint32_t> terms;
-    std::vector<std::vector<std::string>> selectors;
-    std::vector<std::vector<uint32_t>> wit_idxs;
-    std::vector<FFTerm> vars;
+    std::vector<std::string> variables;               // circuit witness
+    std::vector<uint32_t> public_inps;                // public inputs from the circuit
+    std::unordered_map<uint32_t, std::string> vars_of_interest; // names of the variables
+    std::unordered_map<std::string, uint32_t> terms;  // inverse map of the previous memeber
+    std::vector<std::vector<std::string>> selectors;  // selectors from the circuit
+    std::vector<std::vector<uint32_t>> wit_idxs;      // values used in gates from the circuit
+    std::vector<FFTerm> vars;                         // all the symbolic variables in the circuit
 
-    Solver* solver;
-    std::string tag;
+    Solver* solver;                                   // pointer to the solver
+    std::string tag;                                  // tag of the symbolic circuit. 
+                                                      // If not empty, will be added to the names
+                                                      // of symbolic variables to prevent collisions.
 
     explicit Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag = "");
 
@@ -62,8 +73,8 @@ std::pair<Circuit, Circuit> unique_witness(CircuitSchema& circuit_info,
                                            const std::vector<std::string>& eqall = {},
                                            const std::vector<std::string>& neqall = {});
 
-// void get_all_solutions(std::unordered_map<std::string, cvc5::Term>, std::unordered_map)
 // TODO(alex): Do we need the function that will do recheck based on the current model to consequently find all the
-// solutions.
+// solutions?
+// void get_all_solutions(std::unordered_map<std::string, cvc5::Term>, std::unordered_map)
 
 }; // namespace smt_circuit

cpp/src/barretenberg/smt_verification/solver/solver.cpp

@@ -3,8 +3,11 @@
 
 namespace smt_solver {
 
-// TODO(alex): timeouts are needed;
-
+/**
+ * Check if the symbolic model is solvable.
+ *
+ * @return true if the model is solvable.
+ * */
 bool Solver::check()
 {
     cvc5::Result result = this->s.checkSat();
@@ -13,6 +16,12 @@ bool Solver::check()
     return this->res;
 }
 
+/**
+ * If the system is solvable, extract the values for the given symbolic variables.
+ *
+ * @param terms A map containing pairs (name, symbolic term).
+ * @return A map containing pairs (name, value).
+ * */
 std::unordered_map<std::string, std::string> Solver::model(std::unordered_map<std::string, cvc5::Term>& terms) const
 {
     if (!this->res) {
@@ -25,5 +34,4 @@ std::unordered_map<std::string, std::string> Solver::model(std::unordered_map<st
     }
     return resulting_model;
 }
-
 }; // namespace smt_solver

cpp/src/barretenberg/smt_verification/solver/solver.hpp

@@ -4,6 +4,16 @@
 
 namespace smt_solver {
 
+/** 
+ * @brief Class for the solver.
+ *
+ * @details Solver class that can be used to create
+ * a solver, finite field terms and the circuit. 
+ * Check the satisfability of a system and get it's model.
+ *
+ * @todo TODO(alex): more cvc5 options inside the constructor.
+ * @todo TODO(alex) perhaps add the << operator to make it easier to read the constraints.
+ */
 class Solver {
   private:
     bool res = false;
@@ -13,7 +23,6 @@ class Solver {
     cvc5::Solver s;
     cvc5::Sort fp;
 
-    // TODO(alex): more options???
     explicit Solver(const std::string& modulus, bool produce_model = false, uint32_t base = 16, uint32_t timeout = 0)
     {
         fp = s.mkFiniteFieldSort(modulus, base);
@@ -35,13 +44,12 @@ class Solver {
     [[nodiscard]] std::string getResult() const
     {
         if (!checked) {
-            return "no result, yet";
+            return "No result, yet";
         }
         return res ? "SAT" : "UNSAT";
     }
 
     std::unordered_map<std::string, std::string> model(std::unordered_map<std::string, cvc5::Term>& terms) const;
     ~Solver() = default;
 };
-
 }; // namespace smt_solver

cpp/src/barretenberg/smt_verification/terms/bool.hpp

@@ -4,6 +4,13 @@
 namespace smt_terms {
 using namespace smt_solver;
 
+/**
+ * @brief Bool element class.
+ * 
+ * @details Can be used to create non trivial constraints.
+ * Supports basic boolean arithmetic: &, |.
+ *
+ */
 class Bool {
   public:
     cvc5::Solver* solver;

cpp/src/barretenberg/smt_verification/terms/ffterm.cpp

@@ -2,10 +2,26 @@
 
 namespace smt_terms {
 
+/**
+ * Create a finite field symbolic variable.
+ *
+ * @param name Name of the variable. Should be unique per variable.
+ * @param slv  Pointer to the global solver.
+ * @return Finite field symbolic variable.
+ * */
 FFTerm Var(const std::string& name, Solver* slv)
 {
     return FFTerm(name, slv);
 };
+
+/**
+ * Create a finite field numeric member.
+ *
+ * @param val  String representation of the value.
+ * @param slv  Pointer to the global solver.
+ * @param base Base of the string representation. 16 by default.
+ * @return Finite field constant.
+ * */
 FFTerm Const(const std::string& val, Solver* slv, uint32_t base)
 {
     return FFTerm(val, slv, true, base);
@@ -58,6 +74,16 @@ void FFTerm::operator*=(const FFTerm& other)
     this->term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term });
 }
 
+/**
+ * @brief Division operation
+ * 
+ * @details Returns a result of the division by
+ * creating a new symbolic variable and adding a new constraint 
+ * to the solver.
+ *
+ * @param other 
+ * @return FFTerm 
+ */
 FFTerm FFTerm::operator/(const FFTerm& other) const
 {
     cvc5::Term res = this->solver->s.mkConst(this->solver->fp,
@@ -80,12 +106,20 @@ void FFTerm::operator/=(const FFTerm& other)
     this->term = res;
 }
 
+/**
+ * Create an equality constraint between two finite field elements.
+ *
+ */
 void FFTerm::operator==(const FFTerm& other) const
 {
     cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term });
     this->solver->s.assertFormula(eq);
 }
 
+/**
+ * Create an inequality constraint between two finite field elements.
+ *
+ */
 void FFTerm::operator!=(const FFTerm& other) const
 {
     cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term });

cpp/src/barretenberg/smt_verification/terms/ffterm.hpp

@@ -4,6 +4,14 @@
 namespace smt_terms {
 using namespace smt_solver;
 
+/** 
+ * @brief Finite Field element class.
+ *
+ * @details Can be a finite field symbolic variable or a constant.
+ * Both of them support basic arithmetic operations: +, -, *, /.
+ * Check the satisfability of a system and get it's model.
+ *
+ */
 class FFTerm {
   public:
     Solver* solver;
@@ -36,11 +44,6 @@ class FFTerm {
     void operator==(const FFTerm& other) const;
     void operator!=(const FFTerm& other) const;
 
-    // TODO(alex): Maybe do the same thing with +, - but I don't see a point
-    // and also properlythink on how to implement this sh
-    // void operator==(const std::pair<std::string, uint32_t>& other) const;
-    // void operator!=(const std::pair<std::string, uint32_t>& other) const;
-
     operator std::string() const { return isconst ? term.getFiniteFieldValue() : term.toString(); };
     operator cvc5::Term() const { return term; };