diff --git a/barretenberg/cpp/src/barretenberg/relations/ultra_arithmetic_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/ultra_arithmetic_relation.hpp index d99b57fb716..55f4a38b211 100644 --- a/barretenberg/cpp/src/barretenberg/relations/ultra_arithmetic_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/ultra_arithmetic_relation.hpp @@ -57,7 +57,7 @@ template class UltraArithmeticRelationImpl { * at the next gate. Then we can treat (q_arith - 1) as a simulated q_6 selector and scale q_m to handle (q_arith - * 3) at product. * - * The The relation is + * The relation is * defined as C(in(X)...) = q_arith * [ -1/2(q_arith - 3)(q_m * w_r * w_l) + (q_l * w_l) + (q_r * w_r) + * (q_o * w_o) + (q_4 * w_4) + q_c + (q_arith - 1)w_4_shift ] * diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt index 21766db4baf..5428aeae1c7 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt +++ b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt @@ -26,9 +26,9 @@ add_dependencies(cvc5-lib cvc5) include_directories(${CVC5_INCLUDE}) set_target_properties(cvc5-lib PROPERTIES IMPORTED_LOCATION ${CVC5_LIB}) -barretenberg_module(smt_verification common proof_system stdlib_primitives stdlib_sha256 circuit_checker transcript plonk cvc5-lib) +barretenberg_module(smt_verification common stdlib_primitives stdlib_sha256 circuit_checker transcript plonk cvc5-lib) # We have no easy way to add a dependency to an external target, we list the built targets explicit. Could be cleaner. add_dependencies(smt_verification cvc5) add_dependencies(smt_verification_objects cvc5) add_dependencies(smt_verification_tests cvc5) -add_dependencies(smt_verification_test_objects cvc5) \ No newline at end of file +add_dependencies(smt_verification_test_objects cvc5) 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 919ebd3b4c3..5af909c3d63 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.cpp @@ -31,6 +31,20 @@ CircuitSchema unpack_from_file(const std::string& filename) return cir; } +/** + * @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; +} + /** * @brief Translates the schema to python format * @details Returns the contents of the .py file @@ -42,6 +56,7 @@ CircuitSchema unpack_from_file(const std::string& filename) * gates = [ * [[0x000...0, 0x000...1, 0x000...0, 0x000...0, 0x000...0], [0, 0, 0]], ... * ] + * @todo UltraCircuitSchema output */ void print_schema_for_use_in_python(CircuitSchema& cir) { @@ -64,37 +79,23 @@ void print_schema_for_use_in_python(CircuitSchema& cir) for (size_t i = 0; i < cir.selectors.size(); i++) { info("[", "[", - cir.selectors[i][0], + cir.selectors[0][i][0], ", ", - cir.selectors[i][1], + cir.selectors[0][i][1], ", ", - cir.selectors[i][2], + cir.selectors[0][i][2], ", ", - cir.selectors[i][3], + cir.selectors[0][i][3], ", ", - cir.selectors[i][4], + cir.selectors[0][i][4], "], [", - cir.wires[i][0], + cir.wires[0][i][0], ", ", - cir.wires[i][1], + cir.wires[0][i][1], ", ", - cir.wires[i][2], + cir.wires[0][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 index 0111614115a..dbfb885ad3f 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp @@ -27,10 +27,12 @@ struct CircuitSchema { std::vector public_inps; std::unordered_map vars_of_interest; std::vector variables; - std::vector> selectors; - std::vector> wires; + 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); + std::vector>> lookup_tables; + MSGPACK_FIELDS( + modulus, public_inps, vars_of_interest, variables, selectors, wires, real_variable_index, lookup_tables); }; CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp similarity index 100% rename from barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp rename to barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.hpp similarity index 100% rename from barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp rename to barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.hpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.hpp similarity index 100% rename from barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.test.cpp rename to barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.hpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp index e3924f0774e..093b237b750 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp @@ -1,5 +1,5 @@ #include "solver.hpp" -#include +#include "barretenberg/common/log.hpp" namespace smt_solver { @@ -47,6 +47,8 @@ std::unordered_map Solver::model(std::unordered_map Solver::model(std::vectorsolver.getAssertions()) { + for (const auto& t : this->solver.getAssertions()) { info(stringify_term(t)); } } + +cvc5::Term Solver::create_lookup_table(std::vector>& table) +{ + if (!lookup_enabled) { + this->solver.setLogic("ALL"); + this->solver.setOption("finite-model-find", "true"); + this->solver.setOption("sets-ext", "true"); + lookup_enabled = true; + } + + cvc5::Term tmp = table[0][0]; + cvc5::Sort tuple_sort = this->term_manager.mkTupleSort({ tmp.getSort(), tmp.getSort(), tmp.getSort() }); + cvc5::Sort relation = this->term_manager.mkSetSort(tuple_sort); + cvc5::Term resulting_table = this->term_manager.mkEmptySet(relation); + + std::vector children; + for (auto& table_entry : table) { + cvc5::Term entry = this->term_manager.mkTuple(table_entry); + children.push_back(entry); + } + children.push_back(resulting_table); + return this->term_manager.mkTerm(cvc5::Kind::SET_INSERT, children); +} }; // namespace smt_solver diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp index d7593663d04..0151c1bb857 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -22,7 +22,7 @@ struct SolverConfiguration { uint64_t timeout; uint32_t debug; - bool ff_disjunctive_bit; + bool ff_elim_disjunctive_bit; std::string ff_solver; }; @@ -76,8 +76,8 @@ class Solver { // Cause bit constraints are part of the split-gb optimization // and without them it will probably perform less efficient // TODO(alex): test this `probably` after finishing the pr sequence - if (config.ff_disjunctive_bit) { - solver.setOption("ff-disjunctive-bit", "true"); + if (!config.ff_elim_disjunctive_bit) { + solver.setOption("ff-elim-disjunctive-bit", "false"); } // split-gb is an updated version of gb ff-solver // It basically SPLITS the polynomials in the system into subsets @@ -96,6 +96,10 @@ class Solver { Solver& operator=(const Solver& other) = delete; Solver& operator=(Solver&& other) = delete; + bool lookup_enabled = false; + + cvc5::Term create_lookup_table(std::vector>& table); + void assertFormula(const cvc5::Term& term) const { this->solver.assertFormula(term); } cvc5::Term getValue(const cvc5::Term& term) const { return this->solver.getValue(term); } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp index c393fd5297f..ad76add64ad 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp @@ -154,7 +154,145 @@ TEST(BVTerm, rotl) ASSERT_EQ(bvals, xvals); } -// MUL, LSH, RSH, AND and OR are not tested, since they are not bijective +// non bijective operators +TEST(BVTerm, mul) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct c = a * b; + + uint32_t modulus_base = 16; + uint32_t bitvector_size = 32; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", + default_solver_config, + modulus_base, + bitvector_size); + + STerm x = BVVar("x", &s); + STerm y = BVVar("y", &s); + STerm z = x * y; + + x == a.get_value(); + y == b.get_value(); + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(z.term).getBitVectorValue(); + STerm bval = STerm(c.get_value(), &s, TermType::BVTerm); + std::string bvals = s.getValue(bval.term).getBitVectorValue(); + ASSERT_EQ(bvals, xvals); +} + +TEST(BVTerm, and) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct c = a & b; + + uint32_t modulus_base = 16; + uint32_t bitvector_size = 32; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", + default_solver_config, + modulus_base, + bitvector_size); + + STerm x = BVVar("x", &s); + STerm y = BVVar("y", &s); + STerm z = x & y; + + x == a.get_value(); + y == b.get_value(); + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(z.term).getBitVectorValue(); + STerm bval = STerm(c.get_value(), &s, TermType::BVTerm); + std::string bvals = s.getValue(bval.term).getBitVectorValue(); + ASSERT_EQ(bvals, xvals); +} + +TEST(BVTerm, or) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct c = a | b; + + uint32_t modulus_base = 16; + uint32_t bitvector_size = 32; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", + default_solver_config, + modulus_base, + bitvector_size); + + STerm x = BVVar("x", &s); + STerm y = BVVar("y", &s); + STerm z = x | y; + + x == a.get_value(); + y == b.get_value(); + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(z.term).getBitVectorValue(); + STerm bval = STerm(c.get_value(), &s, TermType::BVTerm); + std::string bvals = s.getValue(bval.term).getBitVectorValue(); + ASSERT_EQ(bvals, xvals); +} + +TEST(BVTerm, shr) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct b = a >> 5; + + uint32_t modulus_base = 16; + uint32_t bitvector_size = 32; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", + default_solver_config, + modulus_base, + bitvector_size); + + STerm x = BVVar("x", &s); + STerm y = x >> 5; + + x == a.get_value(); + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(y.term).getBitVectorValue(); + STerm bval = STerm(b.get_value(), &s, TermType::BVTerm); + std::string bvals = s.getValue(bval.term).getBitVectorValue(); + ASSERT_EQ(bvals, xvals); +} + +TEST(BVTerm, shl) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct b = a << 5; + + uint32_t modulus_base = 16; + uint32_t bitvector_size = 32; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", + default_solver_config, + modulus_base, + bitvector_size); + + STerm x = BVVar("x", &s); + STerm y = x << 5; + + x == a.get_value(); + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(y.term).getBitVectorValue(); + STerm bval = STerm(b.get_value(), &s, TermType::BVTerm); + std::string bvals = s.getValue(bval.term).getBitVectorValue(); + ASSERT_EQ(bvals, xvals); +} // This test aims to check for the absence of unintended // behavior. If an unsupported operator is called, an info message appears in stderr diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp index ee2b118f37e..8ba3f52844e 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp @@ -98,6 +98,31 @@ TEST(FFTerm, division) ASSERT_EQ(bvals, yvals); } +TEST(FFTerm, set_inclusion) +{ + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); + + std::vector> table = { { FFConst("1", &s), FFConst("2", &s), FFConst("3", &s) }, + { FFConst("4", &s), FFConst("5", &s), FFConst("6", &s) } }; + cvc5::Term symbolic_table = s.create_lookup_table(table); + + STerm x = FFVar("x", &s); + STerm y = FFVar("y", &s); + STerm z = FFVar("z", &s); + std::vector tmp_vec = { x, y, z }; + STerm::in_table(tmp_vec, symbolic_table); + x != 4; + + ASSERT_TRUE(s.check()); + + std::string xval = s.getValue(x).getFiniteFieldValue(); + ASSERT_EQ(xval, "1"); + std::string yval = s.getValue(y).getFiniteFieldValue(); + ASSERT_EQ(yval, "2"); + std::string zval = s.getValue(z).getFiniteFieldValue(); + ASSERT_EQ(zval, "3"); +} + // This test aims to check for the absence of unintended // behavior. If an unsupported operator is called, an info message appears in stderr // and the value is supposed to remain unchanged. diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp index ae16d144a9b..7ab111cb86c 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp @@ -313,8 +313,8 @@ STerm STerm::operator<<(const uint32_t& n) const info("SHIFT LEFT is not compatible with ", this->type); return *this; } - cvc5::Op lsh = solver->term_manager.mkOp(this->operations.at(OpType::LSH), { n }); - cvc5::Term res = solver->term_manager.mkTerm(lsh, { this->term }); + cvc5::Term shift = this->solver->term_manager.mkBitVector(this->solver->bv_sort.getBitVectorSize(), n); + cvc5::Term res = this->solver->term_manager.mkTerm(this->operations.at(OpType::LSH), { this->term, shift }); return { res, this->solver, this->type }; } @@ -324,29 +324,29 @@ void STerm::operator<<=(const uint32_t& n) info("SHIFT LEFT is not compatible with ", this->type); return; } - cvc5::Op lsh = solver->term_manager.mkOp(this->operations.at(OpType::LSH), { n }); - this->term = solver->term_manager.mkTerm(lsh, { this->term }); + cvc5::Term shift = solver->term_manager.mkBitVector(this->solver->bv_sort.getBitVectorSize(), n); + this->term = this->solver->term_manager.mkTerm(this->operations.at(OpType::LSH), { this->term, shift }); } STerm STerm::operator>>(const uint32_t& n) const { if (!this->operations.contains(OpType::RSH)) { - info("RIGHT LEFT is not compatible with ", this->type); + info("SHIFT RIGHT is not compatible with ", this->type); return *this; } - cvc5::Op rsh = solver->term_manager.mkOp(this->operations.at(OpType::RSH), { n }); - cvc5::Term res = solver->term_manager.mkTerm(rsh, { this->term }); + cvc5::Term shift = this->solver->term_manager.mkBitVector(this->solver->bv_sort.getBitVectorSize(), n); + cvc5::Term res = this->solver->term_manager.mkTerm(this->operations.at(OpType::RSH), { this->term, shift }); return { res, this->solver, this->type }; } void STerm::operator>>=(const uint32_t& n) { if (!this->operations.contains(OpType::RSH)) { - info("RIGHT LEFT is not compatible with ", this->type); + info("SHIFT RIGHT is not compatible with ", this->type); return; } - cvc5::Op rsh = solver->term_manager.mkOp(this->operations.at(OpType::RSH), { n }); - this->term = solver->term_manager.mkTerm(rsh, { this->term }); + cvc5::Term shift = this->solver->term_manager.mkBitVector(this->solver->bv_sort.getBitVectorSize(), n); + this->term = this->solver->term_manager.mkTerm(this->operations.at(OpType::RSH), { this->term, shift }); } STerm STerm::rotr(const uint32_t& n) const diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp index 685bf446462..60c1f3df300 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp @@ -163,7 +163,7 @@ class STerm { return out << static_cast(term); }; - friend STerm batch_add(const std::vector& children) + static STerm batch_add(const std::vector& children) { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); @@ -171,7 +171,7 @@ class STerm { return { res, slv }; } - friend STerm batch_mul(const std::vector& children) + static STerm batch_mul(const std::vector& children) { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); @@ -179,6 +179,20 @@ class STerm { return { res, slv }; } + /** + * @brief Create an inclusion constraint + * + * @param entry the tuple entry to be checked + * @param table lookup table that consists of tuples of lenght 3 + */ + static void in_table(std::vector& entry, cvc5::Term& table) + { + Solver* slv = entry[0].solver; + cvc5::Term sym_entry = slv->term_manager.mkTuple({ entry[0], entry[1], entry[2] }); + cvc5::Term inc = slv->term_manager.mkTerm(cvc5::Kind::SET_MEMBER, { sym_entry, table }); + slv->assertFormula(inc); + } + // arithmetic compatibility with Fr STerm operator+(const bb::fr& other) const { return *this + STerm(other, this->solver, this->type); } @@ -187,8 +201,8 @@ class STerm { void operator-=(const bb::fr& other) { *this -= STerm(other, this->solver, this->type); } STerm operator*(const bb::fr& other) const { return *this * STerm(other, this->solver, this->type); } void operator*=(const bb::fr& other) { *this *= STerm(other, this->solver, this->type); } - STerm operator/(const bb::fr& other) const { return *this / STerm(other, this->solver, this->type); } - void operator/=(const bb::fr& other) { *this /= STerm(other, this->solver, this->type); } + STerm operator/(const bb::fr& other) const { return *this * STerm(other.invert(), this->solver, this->type); } + void operator/=(const bb::fr& other) { *this *= STerm(other.invert(), this->solver, this->type); } void operator==(const bb::fr& other) const { *this == STerm(other, this->solver, this->type); } void operator!=(const bb::fr& other) const { *this != STerm(other, this->solver, this->type); } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp index 3e4b7eb1c66..d3a1c7a2bab 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp @@ -15,23 +15,22 @@ * @param fname file to store the resulting witness if succeded */ void default_model(const std::vector& special, - smt_circuit::Circuit& c1, - smt_circuit::Circuit& c2, - smt_solver::Solver* s, + smt_circuit::CircuitBase& c1, + smt_circuit::CircuitBase& c2, const std::string& fname) { std::vector vterms1; std::vector vterms2; - vterms1.reserve(c1.get_num_real_vars()); - vterms2.reserve(c1.get_num_real_vars()); + vterms1.reserve(c1.get_num_vars()); + vterms2.reserve(c1.get_num_vars()); for (uint32_t i = 0; i < c1.get_num_vars(); i++) { vterms1.push_back(c1.symbolic_vars[c1.real_variable_index[i]]); vterms2.push_back(c2.symbolic_vars[c2.real_variable_index[i]]); } - std::unordered_map mmap1 = s->model(vterms1); - std::unordered_map mmap2 = s->model(vterms2); + std::unordered_map mmap1 = c1.solver->model(vterms1); + std::unordered_map mmap2 = c1.solver->model(vterms2); std::fstream myfile; myfile.open(fname, std::ios::out | std::ios::trunc | std::ios::binary); @@ -42,9 +41,25 @@ void default_model(const std::vector& special, if (c1.real_variable_index[i] == i) { myfile << "{" << mmap1[vname1] << ", " << mmap2[vname2] << "}"; myfile << ", // " << vname1 << ", " << vname2 << std::endl; + if (mmap1[vname1] != mmap2[vname2]) { + info("{", mmap1[vname1], ", ", mmap2[vname2], "}", ", // ", vname1, ", ", vname2); + } } else { myfile << "{" << mmap1[vname1] << ", " + mmap2[vname2] << "}"; myfile << ", // " << vname1 << " ," << vname2 << " -> " << c1.real_variable_index[i] << std::endl; + if (mmap1[vname1] != mmap2[vname2]) { + info("{", + mmap1[vname1], + ", ", + mmap2[vname2], + "}", + ", // ", + vname1, + ", ", + vname2, + " -> ", + c1.real_variable_index[i]); + } } } myfile << "};"; @@ -56,7 +71,7 @@ void default_model(const std::vector& special, vterms.insert({ vname + "_2", c2[vname] }); } - std::unordered_map mmap = s->model(vterms); + std::unordered_map mmap = c1.solver->model(vterms); for (const auto& vname : special) { info(vname, "_1, ", vname, "_2 = ", mmap[vname + "_1"], ", ", mmap[vname + "_2"]); } @@ -76,18 +91,17 @@ void default_model(const std::vector& special, * @param fname file to store the resulting witness if succeded */ void default_model_single(const std::vector& special, - smt_circuit::Circuit& c, - smt_solver::Solver* s, + smt_circuit::CircuitBase& c, const std::string& fname) { std::vector vterms; - vterms.reserve(c.get_num_real_vars()); + vterms.reserve(c.get_num_vars()); for (uint32_t i = 0; i < c.get_num_vars(); i++) { - vterms.push_back(c.symbolic_vars[i]); + vterms.push_back(c.symbolic_vars[c.real_variable_index[i]]); } - std::unordered_map mmap = s->model(vterms); + std::unordered_map mmap = c.solver->model(vterms); std::fstream myfile; myfile.open(fname, std::ios::out | std::ios::trunc | std::ios::binary); @@ -108,7 +122,7 @@ void default_model_single(const std::vector& special, vterms1.insert({ vname, c[vname] }); } - std::unordered_map mmap1 = s->model(vterms1); + std::unordered_map mmap1 = c.solver->model(vterms1); for (const auto& vname : special) { info(vname, " = ", mmap1[vname]); } @@ -121,19 +135,13 @@ void default_model_single(const std::vector& special, * @param s * @return bool is system satisfiable? */ -bool smt_timer(smt_solver::Solver* s, bool mins) +bool smt_timer(smt_solver::Solver* s) { auto start = std::chrono::high_resolution_clock::now(); bool res = s->check(); auto stop = std::chrono::high_resolution_clock::now(); - double duration = 0.0; - if (mins) { - duration = static_cast(duration_cast(stop - start).count()); - info("Time elapsed: ", duration, " min"); - } else { - duration = static_cast(duration_cast(stop - start).count()); - info("Time elapsed: ", duration, " sec"); - } + uint32_t duration_secs = static_cast(duration_cast(stop - start).count()); + info("Time elapsed: ", duration_secs / 60, " min ", duration_secs % 60, " sec"); info(s->cvc_result); return res; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp index 3b0211272c8..559b8fff7ee 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp @@ -1,17 +1,15 @@ #pragma once #include -#include "barretenberg/smt_verification/circuit/circuit.hpp" +#include "barretenberg/smt_verification/circuit/circuit_base.hpp" void default_model(const std::vector& special, - smt_circuit::Circuit& c1, - smt_circuit::Circuit& c2, - smt_solver::Solver* s, + smt_circuit::CircuitBase& c1, + smt_circuit::CircuitBase& c2, const std::string& fname = "witness.out"); void default_model_single(const std::vector& special, - smt_circuit::Circuit& c, - smt_solver::Solver* s, + smt_circuit::CircuitBase& c, const std::string& fname = "witness.out"); -bool smt_timer(smt_solver::Solver* s, bool mins = true); +bool smt_timer(smt_solver::Solver* s); std::pair, std::vector> base4(uint32_t el); \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/circuit_builder_base.hpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/circuit_builder_base.hpp index 9b954bd912b..ff516661c1d 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/circuit_builder_base.hpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/circuit_builder_base.hpp @@ -223,6 +223,18 @@ template class CircuitBuilderBase { void failure(std::string msg); }; +template 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; + std::vector>> lookup_tables; + MSGPACK_FIELDS( + modulus, public_inps, vars_of_interest, variables, selectors, wires, real_variable_index, lookup_tables); +}; } // namespace bb // TODO(#217)(Cody): This will need updating based on the approach we take to ensure no multivariate is zero. diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp index 351c3ed0eb4..7fdb267df0d 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp @@ -521,7 +521,7 @@ void StandardCircuitBuilder_::assert_equal_constant(uint32_t const a_idx, FF template msgpack::sbuffer StandardCircuitBuilder_::export_circuit() { using base = CircuitBuilderBase; - CircuitSchema cir; + CircuitSchema cir; uint64_t modulus[4] = { FF::Params::modulus_0, FF::Params::modulus_1, FF::Params::modulus_2, FF::Params::modulus_3 @@ -544,6 +544,8 @@ template msgpack::sbuffer StandardCircuitBuilder_::export_circ cir.variables.push_back(var); } + std::vector> arith_selectors; + std::vector> arith_wires; for (size_t i = 0; i < this->num_gates; i++) { std::vector tmp_sel = { blocks.arithmetic.q_m()[i], blocks.arithmetic.q_1()[i], @@ -555,9 +557,11 @@ template msgpack::sbuffer StandardCircuitBuilder_::export_circ this->real_variable_index[blocks.arithmetic.w_r()[i]], this->real_variable_index[blocks.arithmetic.w_o()[i]], }; - cir.selectors.push_back(tmp_sel); - cir.wires.push_back(tmp_w); + arith_selectors.push_back(tmp_sel); + arith_wires.push_back(tmp_w); } + cir.selectors.push_back(arith_selectors); + cir.wires.push_back(arith_wires); cir.real_variable_index = this->real_variable_index; @@ -569,4 +573,4 @@ template msgpack::sbuffer StandardCircuitBuilder_::export_circ template class StandardCircuitBuilder_; template class StandardCircuitBuilder_; -} // namespace bb \ No newline at end of file +} // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.hpp index e6ede171ffa..d2ce11c094a 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.hpp @@ -106,18 +106,6 @@ template class StandardCircuitBuilder_ : public CircuitBuilderBase size_t get_num_constant_gates() const override { return 0; } msgpack::sbuffer export_circuit() override; - - private: - 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); - } circuit_schema; }; using StandardCircuitBuilder = StandardCircuitBuilder_; diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp index 25322635586..e96c234c5ab 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp @@ -2716,9 +2716,110 @@ template uint256_t UltraCircuitBuilder_(crypto::sha256(to_hash)); } +/** + * Export the existing circuit as msgpack compatible buffer. + * + * @return msgpack compatible buffer + */ +template msgpack::sbuffer UltraCircuitBuilder_::export_circuit() +{ + using base = CircuitBuilderBase; + CircuitSchema cir; + + uint64_t modulus[4] = { + FF::Params::modulus_0, FF::Params::modulus_1, FF::Params::modulus_2, FF::Params::modulus_3 + }; + std::stringstream buf; + buf << std::hex << std::setfill('0') << std::setw(16) << modulus[3] << std::setw(16) << modulus[2] << std::setw(16) + << modulus[1] << std::setw(16) << modulus[0]; + + cir.modulus = buf.str(); + + for (uint32_t i = 0; i < this->get_num_public_inputs(); i++) { + cir.public_inps.push_back(this->real_variable_index[this->public_inputs[i]]); + } + + for (auto& tup : base::variable_names) { + cir.vars_of_interest.insert({ this->real_variable_index[tup.first], tup.second }); + } + + for (auto var : this->variables) { + cir.variables.push_back(var); + } + // TODO(alex): manage non native gates + + FF curve_b; + if constexpr (FF::modulus == bb::fq::modulus) { + curve_b = bb::g1::curve_b; + } else if constexpr (FF::modulus == grumpkin::fq::modulus) { + curve_b = grumpkin::g1::curve_b; + } else { + curve_b = 0; + } + + for (auto& block : blocks.get()) { + std::vector> block_selectors; + std::vector> block_wires; + for (size_t idx = 0; idx < block.size(); ++idx) { + std::vector tmp_sel = { block.q_m()[idx], + block.q_1()[idx], + block.q_2()[idx], + block.q_3()[idx], + block.q_4()[idx], + block.q_c()[idx], + block.q_arith()[idx], + block.q_lookup_type()[idx], + block.q_elliptic()[idx], + block.q_aux()[idx], + curve_b }; + + std::vector tmp_w = { + this->real_variable_index[block.w_l()[idx]], + this->real_variable_index[block.w_r()[idx]], + this->real_variable_index[block.w_o()[idx]], + this->real_variable_index[block.w_4()[idx]], + }; + + if (idx < block.size() - 1) { + // TODO(alex): don't forget to handle memory_data later + tmp_w.push_back(block.w_l()[idx + 1]); + tmp_w.push_back(block.w_r()[idx + 1]); + tmp_w.push_back(block.w_o()[idx + 1]); + tmp_w.push_back(block.w_4()[idx + 1]); + } else { + tmp_w.push_back(0); + tmp_w.push_back(0); + tmp_w.push_back(0); + tmp_w.push_back(0); + } + + block_selectors.push_back(tmp_sel); + block_wires.push_back(tmp_w); + } + cir.selectors.push_back(block_selectors); + cir.wires.push_back(block_wires); + } + + cir.real_variable_index = this->real_variable_index; + + for (const auto& table : this->lookup_tables) { + const FF table_index(table.table_index); + info("Table no: ", table.table_index); + std::vector> tmp_table; + for (size_t i = 0; i < table.size; ++i) { + tmp_table.push_back({ table.column_1[i], table.column_2[i], table.column_3[i] }); + } + cir.lookup_tables.push_back(tmp_table); + } + + msgpack::sbuffer buffer; + msgpack::pack(buffer, cir); + return buffer; +} + template class UltraCircuitBuilder_>; template class UltraCircuitBuilder_>; // To enable this we need to template plookup // template class UltraCircuitBuilder_; -} // namespace bb \ No newline at end of file +} // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp index ccc52083641..286ce0b165b 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp @@ -11,6 +11,9 @@ #include #include +#include "barretenberg/serialize/cbind.hpp" +#include "barretenberg/serialize/msgpack.hpp" + namespace bb { template struct non_native_field_witnesses { @@ -811,6 +814,8 @@ class UltraCircuitBuilder_ : public CircuitBuilderBase>; } // namespace bb