From e5b81830480b35ed8ab320333b6060d9895f84ee Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 15:46:21 +0000 Subject: [PATCH 1/8] Separated CircuitSchema object and relevant functions from circuit --- .../circuit/circuit_schema.cpp | 102 ++++++++++++++++++ .../circuit/circuit_schema.hpp | 23 ++++ 2 files changed, 125 insertions(+) create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp new file mode 100644 index 00000000000..ef73f233f0d --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp @@ -0,0 +1,102 @@ +#include "circuit_schema.hpp" + +namespace smt_circuit_schema { + +/** + * @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::max()); + std::streamsize fsize = fin.gcount(); + fin.clear(); + fin.seekg(0, std::ios_base::beg); + + CircuitSchema cir; + char* encoded_data = (char*)aligned_alloc(64, static_cast(fsize)); + fin.read(encoded_data, fsize); + msgpack::unpack((const char*)encoded_data, static_cast(fsize)).get().convert(cir); + return cir; +} + +/** + * @brief Translates the schema to python format + * @details Returns the conetents of the .py file + * that can be further imported by python script + * + * @example output.py + * variables = ["zero", "one", "my_input1", "var3", ..., "var_n"] - variable names + * public = [[0, 0x000...0], [1, 0x000...1], [2, 0x000..abcd]] - (index, value) + * gates = [ + * [[0x000...0, 0x000...1, 0x000...0, 0x000...0, 0x000...0], [0, 0, 0]], ... + * ] + */ +void print_schema_for_use_in_python(CircuitSchema& cir) +{ + info("variable_names = ["); + for (uint32_t i = 0; i < static_cast(cir.variables.size()); i++) { + if (cir.vars_of_interest.contains(i)) { + info('"', cir.vars_of_interest[i], "\","); + } else { + info("\"v", i, "\","); + } + } + info("]"); + info("public = ["); + for (auto i : cir.public_inps) { + info("[", i, ", ", cir.variables[i], "],"); + } + info("]"); + info("gates = ["); + + for (size_t i = 0; i < cir.selectors.size(); i++) { + info("[", + "[", + cir.selectors[i][0], + ", ", + cir.selectors[i][1], + ", ", + cir.selectors[i][2], + ", ", + cir.selectors[i][3], + ", ", + cir.selectors[i][4], + "], [", + cir.wires[i][0], + ", ", + cir.wires[i][1], + ", ", + cir.wires[i][2], + "]],"); + } + info("]"); +} + +/** + * @brief Get the CircuitSchema object + * @details Initialize the CircuitSchema 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; +} +} // namespace smt_circuit_schema \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp new file mode 100644 index 00000000000..1669127c65c --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp @@ -0,0 +1,23 @@ +#pragma once +#include + +#include "barretenberg/serialize/cbind.hpp" +#include "barretenberg/serialize/msgpack.hpp" + +namespace smt_circuit_schema { + +struct CircuitSchema { + std::string modulus; + std::vector public_inps; + std::unordered_map vars_of_interest; + std::vector variables; + std::vector> selectors; + std::vector> wires; + std::vector real_variable_index; + MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wires, real_variable_index); +}; + +CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf); +CircuitSchema unpack_from_file(const std::string& filename); +void print_schema_for_use_in_python(CircuitSchema& cir); +} // namespace smt_circuit_schema \ No newline at end of file From 1cf6e29e74a0529c9b8176e0bd9456718c1b6ef9 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 15:50:27 +0000 Subject: [PATCH 2/8] Subcircuits that will be removed from the full circuit when work with integers/bitvectors --- .../smt_verification/circuit/subcircuits.cpp | 24 +++++++++++++++++++ .../smt_verification/circuit/subcircuits.hpp | 11 +++++++++ 2 files changed, 35 insertions(+) create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp new file mode 100644 index 00000000000..2870a623a53 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp @@ -0,0 +1,24 @@ +#include "subcircuits.hpp" + +namespace smt_subcircuits { + +CircuitSchema get_standard_range_constraint_circuit(size_t n) +{ + bb::StandardCircuitBuilder builder = bb::StandardCircuitBuilder(); + uint32_t a_idx = builder.add_variable(bb::fr::random_element()); + builder.set_variable_name(a_idx, "a"); + builder.create_range_constraint(a_idx, n); + return unpack_from_buffer(builder.export_circuit()); +} + +CircuitSchema get_standard_logic_circuit(size_t n, bool is_xor) +{ + bb::StandardCircuitBuilder builder = bb::StandardCircuitBuilder(); + uint32_t a_idx = builder.add_variable(bb::fr::random_element()); + uint32_t b_idx = builder.add_variable(bb::fr::random_element()); + builder.set_variable_name(a_idx, "a"); + builder.set_variable_name(b_idx, "b"); + builder.create_logic_constraint(a_idx, b_idx, n, is_xor); + return unpack_from_buffer(builder.export_circuit()); +} +} // namespace smt_subcircuits \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp new file mode 100644 index 00000000000..4e49113887a --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp @@ -0,0 +1,11 @@ +#pragma once +#include "barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp" + +#include "barretenberg/smt_verification/circuit/circuit_schema.hpp" + +namespace smt_subcircuits { +using namespace smt_circuit_schema; + +CircuitSchema get_standard_range_constraint_circuit(size_t n); +CircuitSchema get_standard_logic_circuit(size_t n, bool is_xor); +} // namespace smt_subcircuits \ No newline at end of file From 5cd925617f9d55af106077f9cf381620f7eae3b2 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 16:54:06 +0000 Subject: [PATCH 3/8] Updated Circuit class - New member of CircuitSchema: real_variable_index - New member of Circuit class: variable_names_inverse - Changed add_gates method to prepare_gates which works a little bit different - Added new function unique_witness and renamed old unique_witness --- .../standard_circuit_builder.cpp | 2 + .../standard_circuit_builder.hpp | 3 +- .../smt_verification/circuit/circuit.cpp | 120 +++---- .../smt_verification/circuit/circuit.hpp | 320 +++++++++++------- 4 files changed, 271 insertions(+), 174 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp index 44546102f99..351c3ed0eb4 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp @@ -559,6 +559,8 @@ template msgpack::sbuffer StandardCircuitBuilder_::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; diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp index ee41b73f7ab..82b8dcc4b0b 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp @@ -115,7 +115,8 @@ template class StandardCircuitBuilder_ : public CircuitBuilderBase std::vector variables; std::vector> selectors; std::vector> wires; - MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wires); + std::vector real_variable_index; + MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wires, real_variable_index); } circuit_schema; }; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp index 7ff95288576..138f1efcf0b 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp @@ -2,52 +2,6 @@ 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::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(fsize)); - fin.read(encoded_data, fsize); - msgpack::unpack((const char*)encoded_data, static_cast(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 * @@ -57,19 +11,19 @@ CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf) * * @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 */ template -std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, - Solver* s, - const std::vector& equal, - const std::vector& not_equal, - const std::vector& equal_at_the_same_time, - const std::vector& not_equal_at_the_same_time) +std::pair, Circuit> unique_witness_ext(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal, + const std::vector& not_equal, + const std::vector& equal_at_the_same_time, + const std::vector& not_equal_at_the_same_time) { Circuit c1(circuit_info, s, "circuit1"); Circuit c2(circuit_info, s, "circuit2"); @@ -107,7 +61,7 @@ std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, return { c1, c2 }; } -template std::pair, Circuit> unique_witness( +template std::pair, Circuit> unique_witness_ext( CircuitSchema& circuit_info, Solver* s, const std::vector& equal = {}, @@ -115,7 +69,7 @@ template std::pair, Circuit> unique_witness( const std::vector& equal_at_the_same_time = {}, const std::vector& not_eqaul_at_the_same_time = {}); -template std::pair, Circuit> unique_witness( +template std::pair, Circuit> unique_witness_ext( CircuitSchema& circuit_info, Solver* s, const std::vector& equal = {}, @@ -123,4 +77,54 @@ template std::pair, Circuit> unique_witness( const std::vector& equal_at_the_same_time = {}, const std::vector& not_eqaul_at_the_same_time = {}); +/** + * @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 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 + */ +template +std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal) +{ + Circuit c1(circuit_info, s, "circuit1"); + Circuit c2(circuit_info, s, "circuit2"); + + for (const auto& term : equal) { + c1[term] == c2[term]; + } + + std::vector 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> unique_witness(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal = {}); + +template std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal = {}); }; // namespace smt_circuit \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp index 57ed452b7ba..d8f7f5f3777 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp @@ -1,30 +1,20 @@ #pragma once -#include #include #include #include #include -#include "barretenberg/serialize/cbind.hpp" -#include "barretenberg/serialize/msgpack.hpp" - #include "barretenberg/smt_verification/terms/bool.hpp" #include "barretenberg/smt_verification/terms/ffiterm.hpp" #include "barretenberg/smt_verification/terms/ffterm.hpp" +#include "subcircuits.hpp" + namespace smt_circuit { using namespace smt_solver; using namespace smt_terms; - -struct CircuitSchema { - std::string modulus; - std::vector public_inps; - std::unordered_map vars_of_interest; - std::vector variables; - std::vector> selectors; - std::vector> wires; - MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wires); -}; +using namespace smt_circuit_schema; +using namespace smt_subcircuits; /** * @brief Symbolic Circuit class. @@ -37,16 +27,19 @@ struct CircuitSchema { template class Circuit { private: void init(); - void add_gates(); + + size_t prepare_gates(size_t cursor); + void univariate_handler(bb::fr q_m, bb::fr q_1, bb::fr q_2, bb::fr q_3, bb::fr q_c, uint32_t w); public: - 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> wires_idxs; // values of the gates' wires - std::vector vars; // all the symbolic variables from the circuit + std::vector variables; // circuit witness + std::vector public_inps; // public inputs from the circuit + std::unordered_map variable_names; // names of the variables + std::unordered_map variable_names_inverse; // inverse map of the previous memeber + std::vector> selectors; // selectors from the circuit + std::vector> wires_idxs; // values of the gates' wires + std::unordered_map symbolic_vars; // all the symbolic variables from the circuit + std::vector real_variable_index; // indexes for assert_equal'd wires Solver* solver; // pointer to the solver std::string tag; // tag of the symbolic circuit. @@ -56,9 +49,12 @@ template class Circuit { explicit Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag = ""); FF operator[](const std::string& name); - FF operator[](const uint32_t& idx) { return vars[idx]; }; - inline uint32_t get_num_gates() const { return static_cast(selectors.size()); }; - inline uint32_t get_num_vars() const { return static_cast(vars.size()); }; + FF operator[](const uint32_t& idx) { return symbolic_vars[this->real_variable_index[idx]]; }; + inline size_t get_num_gates() const { return selectors.size(); }; + inline size_t get_num_real_vars() const { return symbolic_vars.size(); }; + inline size_t get_num_vars() const { return variables.size(); }; + + bool simulate_circuit_eval(std::vector& witness) const; }; /** @@ -70,9 +66,12 @@ template class Circuit { */ template 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) + : variables(circuit_info.variables) + , public_inps(circuit_info.public_inps) + , variable_names(circuit_info.vars_of_interest) + , selectors(circuit_info.selectors) , wires_idxs(circuit_info.wires) + , real_variable_index(circuit_info.real_variable_index) , solver(solver) , tag(tag) { @@ -82,37 +81,23 @@ Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, const std::str } } - for (auto var : circuit_info.variables) { - std::stringstream buf; // TODO(alex): looks bad. Would be great to create tostring() converter - buf << var; - std::string tmp = buf.str(); - tmp[1] = '0'; // avoiding `x` in 0x prefix - variables.push_back(tmp); + for (auto& x : variable_names) { + variable_names_inverse.insert({ x.second, x.first }); } - for (auto& x : vars_of_interest) { - terms.insert({ x.second, x.first }); - } - - vars_of_interest.insert({ 0, "zero" }); - vars_of_interest.insert({ 1, "one" }); - terms.insert({ "zero", 0 }); - terms.insert({ "one", 1 }); - - for (auto sel : circuit_info.selectors) { - std::vector tmp_sel; - for (size_t j = 0; j < 5; j++) { - std::stringstream buf; // TODO(alex): #2 - buf << sel[j]; - std::string q_i = buf.str(); - q_i[1] = '0'; // avoiding `x` in 0x prefix - tmp_sel.push_back(q_i); - } - selectors.push_back(tmp_sel); - } + variable_names.insert({ 0, "zero" }); + variable_names.insert({ 1, "one" }); + variable_names_inverse.insert({ "zero", 0 }); + variable_names_inverse.insert({ "one", 1 }); this->init(); - this->add_gates(); + + // Perform all relaxation for gates or + // add gate in its normal state to solver + size_t i = 0; + while (i < this->get_num_gates()) { + i = this->prepare_gates(i); + } } /** @@ -124,80 +109,129 @@ template void Circuit::init() { size_t num_vars = variables.size(); - vars.push_back(FF::Var("zero" + this->tag, this->solver)); - vars.push_back(FF::Var("one" + this->tag, this->solver)); + symbolic_vars.insert({ 0, FF::Var("zero" + this->tag, this->solver) }); + symbolic_vars.insert({ 1, FF::Var("one" + this->tag, this->solver) }); - 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)]; - vars.push_back(FF::Var(name + this->tag, this->solver)); + for (uint32_t i = 2; i < num_vars; i++) { + uint32_t real_idx = this->real_variable_index[i]; + if (this->symbolic_vars.contains(real_idx)) { + continue; + } + + if (variable_names.contains(real_idx)) { + std::string name = variable_names[real_idx]; + symbolic_vars.insert({ real_idx, FF::Var(name + this->tag, this->solver) }); } else { - vars.push_back(FF::Var("var_" + std::to_string(i) + this->tag, this->solver)); + symbolic_vars.insert({ real_idx, FF::Var("var_" + std::to_string(i) + this->tag, this->solver) }); } } - vars[0] == FF::Const("0", this->solver); - vars[1] == FF::Const("1", this->solver); + symbolic_vars[0] == bb::fr(0); + symbolic_vars[1] == bb::fr(1); +} + +/** + * @brief Relaxes univariate polynomial constraints. + * TODO(alex): probably won't be necessary in the nearest future + * because of new solver + * + * @param q_m multiplication selector + * @param q_1 l selector + * @param q_2 r selector + * @param q_3 o selector + * @param q_c constant + * @param w witness index + */ +template +void Circuit::univariate_handler(bb::fr q_m, bb::fr q_1, bb::fr q_2, bb::fr q_3, bb::fr q_c, uint32_t w) +{ + bb::fr b = q_1 + q_2 + q_3; + + if (q_m == 0) { + symbolic_vars[w] == -q_c / b; + return; + } - for (auto i : public_inps) { - vars[i] == FF::Const(variables[i], this->solver); + std::pair d = (b * b - bb::fr(4) * q_m * q_c).sqrt(); + if (!d.first) { + throw std::invalid_argument("There're no roots of quadratic polynomial"); + } + bb::fr x1 = (-b + d.second) / (bb::fr(2) * q_m); + bb::fr x2 = (-b - d.second) / (bb::fr(2) * q_m); + + if (d.second == 0) { + symbolic_vars[w] == FF(x1, this->solver); + } else { + ((Bool(symbolic_vars[w]) == Bool(FF(x1, this->solver))) | + (Bool(symbolic_vars[w]) == Bool(FF(x2, this->solver)))) + .assert_term(); } } /** * @brief Adds all the gate constraints to the solver. + * Relaxes constraint system for non-ff solver engines + * via removing subcircuits that were already proved being correct. * */ -template void Circuit::add_gates() +template size_t Circuit::prepare_gates(size_t cursor) { - for (size_t i = 0; i < get_num_gates(); i++) { - FF q_m = FF::Const(selectors[i][0], this->solver); - FF q_1 = FF::Const(selectors[i][1], this->solver); - FF q_2 = FF::Const(selectors[i][2], this->solver); - FF q_3 = FF::Const(selectors[i][3], this->solver); - FF q_c = FF::Const(selectors[i][4], this->solver); - - uint32_t w_l = wires_idxs[i][0]; - uint32_t w_r = wires_idxs[i][1]; - uint32_t w_o = wires_idxs[i][2]; - - // Binary gate. Relaxes the solver. - // TODO(alex): Probably we can add other basic gates here too to relax the stuff. - // TODO(alex): Theoretically this can be applyed after we ensure that the block of polynomial equations holds - // and then simplify that block in future to relax the solver constraint system. Seems like a hard one to - // implement or actually to automate, but I'll think on it for a while. it will probably require to split - // add_gates and init methods into more complex/generalized parts. - if (w_l == w_r && w_r == w_o) { - if (std::string(q_m) == "1" && std::string(q_1) == "0" && std::string(q_2) == "0" && - std::string(q_3) == "-1" && std::string(q_c) == "0") { // squaring gate - (Bool(vars[w_l]) == Bool(vars[0]) | Bool(vars[w_l]) == Bool(vars[1])).assert_term(); - } - } + // TODO(alex): Here'll be the operator relaxation that is coming + // in the next pr - FF eq = vars[0]; + bb::fr q_m = this->selectors[cursor][0]; + bb::fr q_1 = this->selectors[cursor][1]; + bb::fr q_2 = this->selectors[cursor][2]; + bb::fr q_3 = this->selectors[cursor][3]; + bb::fr q_c = this->selectors[cursor][4]; - // mult selector - if (std::string(q_m) != "0") { - eq += q_m * vars[w_l] * vars[w_r]; + uint32_t w_l = this->wires_idxs[cursor][0]; + uint32_t w_r = this->wires_idxs[cursor][1]; + uint32_t w_o = this->wires_idxs[cursor][2]; + + bool univariate_flag = w_l == w_r && w_r == w_o; + univariate_flag |= w_l == w_r && q_3 == 0; + univariate_flag |= w_l == w_o && q_2 == 0 && q_m == 0; + univariate_flag |= w_r == w_o && q_1 == 0 && q_m == 0; + univariate_flag |= q_m == 0 && q_1 == 0 && q_3 == 0; + univariate_flag |= q_m == 0 && q_2 == 0 && q_3 == 0; + univariate_flag |= q_m == 0 && q_1 == 0 && q_2 == 0; + + // Univariate gate. Relaxes the solver. Or is it? + // TODO(alex): Test the effect of this relaxation after the tests are merged. + if (univariate_flag) { + if (q_m == 1 && q_1 == 0 && q_2 == 0 && q_3 == -1 && q_c == 0) { + (Bool(symbolic_vars[w_l]) == Bool(symbolic_vars[0]) | Bool(symbolic_vars[w_l]) == Bool(symbolic_vars[1])) + .assert_term(); + } else { + this->univariate_handler(q_m, q_1, q_2, q_3, q_c, w_l); } - // w_l selector - if (std::string(q_1) != "0") { - eq += q_1 * vars[w_l]; + } else { + FF eq = symbolic_vars[0]; + + // mul selector + if (q_m != 0) { + eq += symbolic_vars[w_l] * symbolic_vars[w_r] * q_m; // TODO(alex): Is there a way to do lmul? + } + // left selector + if (q_1 != 0) { + eq += symbolic_vars[w_l] * q_1; } - // w_r selector - if (std::string(q_2) != "0") { - eq += q_2 * vars[w_r]; + // right selector + if (q_2 != 0) { + eq += symbolic_vars[w_r] * q_2; } - // w_o selector - if (std::string(q_3) != "0") { - eq += q_3 * vars[w_o]; + // out selector + if (q_3 != 0) { + eq += symbolic_vars[w_o] * q_3; } - // w_c selector - if (std::string(q_c) != "0") { + // constant selector + if (q_c != 0) { eq += q_c; } - eq == vars[0]; + eq == symbolic_vars[0]; } + return cursor + 1; } /** @@ -208,22 +242,78 @@ template void Circuit::add_gates() */ template FF Circuit::operator[](const std::string& name) { - if (!this->terms.contains(name)) { - throw std::length_error("No such an item " + name + " in vars or it vas not declared as interesting"); + 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]; +} + +/** + * @brief Similar functionality to old .check_circuit() method + * in standard circuit builder. + * + * @param witness + * @return true + * @return false + */ +template bool Circuit::simulate_circuit_eval(std::vector& witness) const +{ + if (witness.size() != this->get_num_vars()) { + throw std::invalid_argument("Witness size should be " + std::to_string(this->get_num_vars()) + ", not " + + std::to_string(witness.size())); + } + for (size_t i = 0; i < this->selectors.size(); i++) { + bb::fr res = 0; + bb::fr x = witness[this->wires_idxs[i][0]]; + bb::fr y = witness[this->wires_idxs[i][1]]; + bb::fr o = witness[this->wires_idxs[i][2]]; + res += this->selectors[i][0] * x * y; + res += this->selectors[i][1] * x; + res += this->selectors[i][2] * y; + res += this->selectors[i][3] * o; + res += this->selectors[i][4]; + if (res != 0) { + return false; + } } - uint32_t idx = this->terms[name]; - return this->vars[idx]; + return true; } -CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf); -CircuitSchema unpack_from_file(const std::string& fname); +template +std::pair, Circuit> unique_witness_ext(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal = {}, + const std::vector& not_equal = {}, + const std::vector& equal_at_the_same_time = {}, + const std::vector& not_equal_at_the_same_time = {}); + +extern template std::pair, Circuit> unique_witness_ext( + CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal = {}, + const std::vector& not_equal = {}, + const std::vector& equal_at_the_same_time = {}, + const std::vector& not_equal_at_the_same_time = {}); + +extern template std::pair, Circuit> unique_witness_ext( + CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal = {}, + const std::vector& not_equal = {}, + const std::vector& equal_at_the_same_time = {}, + const std::vector& not_equal_at_the_same_time = {}); template std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, Solver* s, - const std::vector& equal = {}, - const std::vector& not_equal = {}, - const std::vector& equal_at_the_same_time = {}, - const std::vector& not_eqaul_at_the_same_time = {}); + const std::vector& equal = {}); + +extern template std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal = {}); + +extern template std::pair, Circuit> unique_witness( + CircuitSchema& circuit_info, Solver* s, const std::vector& equal = {}); }; // namespace smt_circuit From 465d70b2cf07e9e4a5cd053c63ef37d9fdaf214c Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 17:19:33 +0000 Subject: [PATCH 4/8] Rename the unique_witness function --- .../cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp | 2 +- .../cpp/src/barretenberg/smt_verification/smt_examples.test.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp index 330340e3505..6ac6cfe8d89 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp @@ -208,7 +208,7 @@ TEST(bigfield, unique_square) Solver s(circuit_info.modulus); std::pair, Circuit> cs = - unique_witness(circuit_info, + unique_witness_ext(circuit_info, &s, { "a_limb_0", "a_limb_1", "a_limb_2", "a_limb_3" }, { "c_limb_0", "c_limb_1", "c_limb_2", "c_limb_3" }); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp index e62f94195e1..b8a28418023 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp @@ -143,7 +143,7 @@ TEST(circuit_verifiaction, unique_witness) smt_solver::Solver s(circuit_info.modulus); std::pair, smt_circuit::Circuit> cirs = - smt_circuit::unique_witness(circuit_info, &s, { "ev" }, { "z" }); + smt_circuit::unique_witness_ext(circuit_info, &s, { "ev" }, { "z" }); bool res = s.check(); ASSERT_TRUE(res); From 44547d8722f53ae65c3fa9d61dcb2ecceeeeee46 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 21:08:52 +0000 Subject: [PATCH 5/8] Typos, documentation and new readfile --- .../smt_verification/circuit/circuit.cpp | 2 +- .../smt_verification/circuit/circuit_schema.cpp | 15 +++++++-------- .../smt_verification/circuit/circuit_schema.hpp | 16 ++++++++++++++++ 3 files changed, 24 insertions(+), 9 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp index 138f1efcf0b..153e55631b7 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp @@ -78,7 +78,7 @@ template std::pair, Circuit> unique_witness_ext( const std::vector& not_eqaul_at_the_same_time = {}); /** - * @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 equal in both cases, diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp index ef73f233f0d..9fd45b7ebb4 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp @@ -4,7 +4,7 @@ namespace smt_circuit_schema { /** * @brief Get the CircuitSchema object - * @details Initialize the CircuitSchmea from the binary file + * @details Initialize the CircuitSchema from the binary file * that contains an msgpack compatible buffer. * * @param filename @@ -21,21 +21,20 @@ CircuitSchema unpack_from_file(const std::string& filename) throw std::invalid_argument("something went wrong"); } - fin.ignore(std::numeric_limits::max()); - std::streamsize fsize = fin.gcount(); - fin.clear(); + fin.seekg(std::ios::end); + uint64_t fsize = static_cast(fin.tellg()); fin.seekg(0, std::ios_base::beg); CircuitSchema cir; - char* encoded_data = (char*)aligned_alloc(64, static_cast(fsize)); - fin.read(encoded_data, fsize); - msgpack::unpack((const char*)encoded_data, static_cast(fsize)).get().convert(cir); + char* encoded_data = new char[fsize]; + fin.read(encoded_data, static_cast(fsize)); + msgpack::unpack(encoded_data, fsize).get().convert(cir); return cir; } /** * @brief Translates the schema to python format - * @details Returns the conetents of the .py file + * @details Returns the contents of the .py file * that can be further imported by python script * * @example output.py diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp index 1669127c65c..930ff36eaff 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp @@ -6,6 +6,22 @@ namespace smt_circuit_schema { +/** + * @brief Serialized state of a circuit + * + * @details Used to transfer the state of the circuit + * to Symbolic Circuit class. + * Symbolic circuit is then used to produce SMT statements + * that describe needed properties of the circuit. + * + * @param modulus Modulus of the field we are working with + * @param public_inps Public inputs to the current circuit + * @param vars_of_interes Map wires indicies to their given names + * @param variables List of wires values in the current circuit + * @param selectors List of selectors in the current circuit + * @param wires List of wires indicies for each selector + * @param real_variable_index Encoded copy constraints + */ struct CircuitSchema { std::string modulus; std::vector public_inps; From 66f49ee477585da387badbee13fa05481d2b02bc Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 21:09:49 +0000 Subject: [PATCH 6/8] formatting --- .../src/barretenberg/smt_verification/smt_bigfield.test.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp index 6ac6cfe8d89..1578c2474b1 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp @@ -209,9 +209,9 @@ TEST(bigfield, unique_square) std::pair, Circuit> cs = unique_witness_ext(circuit_info, - &s, - { "a_limb_0", "a_limb_1", "a_limb_2", "a_limb_3" }, - { "c_limb_0", "c_limb_1", "c_limb_2", "c_limb_3" }); + &s, + { "a_limb_0", "a_limb_1", "a_limb_2", "a_limb_3" }, + { "c_limb_0", "c_limb_1", "c_limb_2", "c_limb_3" }); auto start = std::chrono::high_resolution_clock::now(); bool res = s.check(); From 874020639d7b978ea45121d63450db51d7d986db Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 21:18:35 +0000 Subject: [PATCH 7/8] Another typo --- .../cpp/src/barretenberg/smt_verification/circuit/circuit.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp index 153e55631b7..d8c2c666a6c 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp @@ -3,7 +3,7 @@ namespace smt_circuit { /** - * @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, From e48cdec9291dc4bfd49be55f09e894710c0dc7ef Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 8 Mar 2024 23:46:44 +0000 Subject: [PATCH 8/8] Readfile fix --- .../barretenberg/smt_verification/circuit/circuit_schema.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp index 9fd45b7ebb4..919ebd3b4c3 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp @@ -13,7 +13,7 @@ namespace smt_circuit_schema { CircuitSchema unpack_from_file(const std::string& filename) { std::ifstream fin; - fin.open(filename, std::ios::in | std::ios::binary); + fin.open(filename, std::ios::ate | std::ios::binary); if (!fin.is_open()) { throw std::invalid_argument("file not found"); } @@ -21,7 +21,6 @@ CircuitSchema unpack_from_file(const std::string& filename) throw std::invalid_argument("something went wrong"); } - fin.seekg(std::ios::end); uint64_t fsize = static_cast(fin.tellg()); fin.seekg(0, std::ios_base::beg);