diff --git a/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp b/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp index 8d0c234b9..d1f13f501 100644 --- a/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp +++ b/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(i))) { std::string name = vars_of_interest[static_cast(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,6 +175,13 @@ 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; @@ -153,6 +189,21 @@ CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf) 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 + */ std::pair unique_witness(CircuitSchema& circuit_info, Solver* s, const std::vector& equal, diff --git a/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp index 272661afd..ca51dc25c 100644 --- a/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp +++ b/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 public_inps; std::unordered_map vars_of_interest; std::vector 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 variables; - std::vector public_inps; - std::unordered_map vars_of_interest; - std::unordered_map terms; - std::vector> selectors; - std::vector> wit_idxs; - std::vector vars; + std::vector variables; // circuit witness + std::vector public_inps; // public inputs from the circuit + std::unordered_map vars_of_interest; // names of the variables + std::unordered_map terms; // inverse map of the previous memeber + std::vector> selectors; // selectors from the circuit + std::vector> wit_idxs; // values used in gates from the circuit + std::vector 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 unique_witness(CircuitSchema& circuit_info, const std::vector& eqall = {}, const std::vector& neqall = {}); -// void get_all_solutions(std::unordered_map, 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::unordered_map) }; // namespace smt_circuit \ No newline at end of file diff --git a/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/cpp/src/barretenberg/smt_verification/solver/solver.cpp index de66f0b6b..7ae827fc3 100644 --- a/cpp/src/barretenberg/smt_verification/solver/solver.cpp +++ b/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 Solver::model(std::unordered_map& terms) const { if (!this->res) { @@ -25,5 +34,4 @@ std::unordered_map Solver::model(std::unordered_map model(std::unordered_map& terms) const; ~Solver() = default; }; - }; // namespace smt_solver \ No newline at end of file diff --git a/cpp/src/barretenberg/smt_verification/terms/bool.hpp b/cpp/src/barretenberg/smt_verification/terms/bool.hpp index f34d8aefa..83d9be913 100644 --- a/cpp/src/barretenberg/smt_verification/terms/bool.hpp +++ b/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; diff --git a/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index 16a363d61..08c17af1d 100644 --- a/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/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 }); diff --git a/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index 5607bbeb3..14add1d7c 100644 --- a/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/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& other) const; - // void operator!=(const std::pair& other) const; - operator std::string() const { return isconst ? term.getFiniteFieldValue() : term.toString(); }; operator cvc5::Term() const { return term; };