From 6692ac831ab980d9623442236c21b499a7238966 Mon Sep 17 00:00:00 2001 From: Sarkoxed <75146596+Sarkoxed@users.noreply.github.com> Date: Mon, 17 Jun 2024 20:33:29 +0300 Subject: [PATCH] feat: SMT Verifier for Ultra Arithmetization (#7067) This pr adds a new Circuit Verifier for Ultra arithmetization. ## `circuit_builder_base.cpp` / `ultra_circuit_builder.cpp` / CircuitSchema CircuitSchema object now includes `real_variable_tag` and `range_tags`(maps tags to ranges) for range constraint detection. ## UltraCircuit Translates all(except for aux gates) constraints to solver, including: - Arithmetic gates - `handle_arithmetic_relation` - Elliptic gates - `handle_elliptic_relation` - Lookup constraints - `handle_lookup_relation` - Range constraints - `handle_range_constraints` - Delta range constraints, that are skipped for now - `handle_delta_range_relation` Also `ultra_circuit.test.cpp` checks that everything is handled properly. ## Solver - Moved `stringify_term` inside the solver class, because of set inclusion logging. - Added logging for set inclusion - Added ordinary set creation via `create_table` - Added `ultra_solver_config` that enables set logic ## STerm Now has `in` method for set inclusion. --------- Co-authored-by: Innokentii Sennovskii --- .../smt_verification/CMakeLists.txt | 2 +- .../smt_verification/circuit/circuit_base.cpp | 4 + .../smt_verification/circuit/circuit_base.hpp | 4 + .../circuit/circuit_schema.hpp | 14 +- .../circuit/standard_circuit.cpp | 6 +- ...uit.test.hpp => standard_circuit.test.cpp} | 0 .../circuit/ultra_circuit.cpp | 485 ++++++++++++++++++ .../circuit/ultra_circuit.hpp | 65 +++ .../circuit/ultra_circuit.test.cpp | 242 +++++++++ .../smt_verification/smt_examples.test.cpp | 27 +- .../smt_verification/smt_polynomials.test.cpp | 14 +- .../smt_verification/solver/solver.cpp | 61 ++- .../smt_verification/solver/solver.hpp | 24 +- .../smt_verification/terms/term.cpp | 13 + .../smt_verification/terms/term.hpp | 4 +- .../circuit_builder_base.hpp | 35 +- .../standard_circuit_builder.cpp | 2 +- .../ultra_circuit_builder.cpp | 24 +- 18 files changed, 966 insertions(+), 60 deletions(-) rename barretenberg/cpp/src/barretenberg/smt_verification/circuit/{standard_circuit.test.hpp => standard_circuit.test.cpp} (100%) create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.test.cpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt index 5428aeae1c7..265a64887e6 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt +++ b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt @@ -26,7 +26,7 @@ add_dependencies(cvc5-lib cvc5) include_directories(${CVC5_INCLUDE}) set_target_properties(cvc5-lib PROPERTIES IMPORTED_LOCATION ${CVC5_LIB}) -barretenberg_module(smt_verification common stdlib_primitives stdlib_sha256 circuit_checker transcript plonk cvc5-lib) +barretenberg_module(smt_verification common stdlib_primitives stdlib_sha256 circuit_checker transcript plonk stdlib_pedersen_commitment 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) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp index 6d53857d5fa..b4c6d1c872b 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp @@ -6,6 +6,8 @@ CircuitBase::CircuitBase(std::unordered_map& variable_nam std::vector& variables, std::vector& public_inps, std::vector& real_variable_index, + std::vector& real_variable_tags, + std::unordered_map& range_tags, Solver* solver, TermType type, const std::string& tag, @@ -14,6 +16,8 @@ CircuitBase::CircuitBase(std::unordered_map& variable_nam , public_inps(public_inps) , variable_names(variable_names) , real_variable_index(real_variable_index) + , real_variable_tags(real_variable_tags) + , range_tags(range_tags) , optimizations(optimizations) , solver(solver) , type(type) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp index e37bfcd06d5..5d551406a4c 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp @@ -33,6 +33,8 @@ class CircuitBase { std::unordered_map variable_names_inverse; // inverse map of the previous memeber std::unordered_map symbolic_vars; // all the symbolic variables from the circuit std::vector real_variable_index; // indexes for assert_equal'd wires + std::vector real_variable_tags; // tags of the variables in the circuit + std::unordered_map range_tags; // ranges associated with a certain tag std::unordered_map optimized; // keeps track of the variables that were excluded from symbolic // circuit during optimizations bool optimizations; // flags to turn on circuit optimizations @@ -51,6 +53,8 @@ class CircuitBase { std::vector& variables, std::vector& public_inps, std::vector& real_variable_index, + std::vector& real_variable_tags, + std::unordered_map& range_tags, Solver* solver, TermType type, const std::string& tag = "", 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 dbfb885ad3f..cc3b37e8e41 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp @@ -31,8 +31,18 @@ struct CircuitSchema { 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); + std::vector real_variable_tags; + std::unordered_map range_tags; + MSGPACK_FIELDS(modulus, + public_inps, + vars_of_interest, + variables, + selectors, + wires, + real_variable_index, + lookup_tables, + real_variable_tags, + range_tags); }; CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp index 709fe8414e0..e72d626580a 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp @@ -15,6 +15,8 @@ StandardCircuit::StandardCircuit( circuit_info.variables, circuit_info.public_inps, circuit_info.real_variable_index, + circuit_info.real_variable_tags, + circuit_info.range_tags, solver, type, tag, @@ -438,7 +440,7 @@ size_t StandardCircuit::handle_range_constraint(size_t cursor) * It compares the chunk of selectors of the current circuit * with pure shift left from uint/logic.cpp * After a match is found, it updates the cursor to skip all the - * redundant constraints and adds a pure b = a.ror(n) + * redundant constraints and adds a pure b = a >> n * constraint to solver. * If there's no match, it will return -1 * @@ -547,7 +549,7 @@ size_t StandardCircuit::handle_shr_constraint(size_t cursor) * It compares the chunk of selectors of the current circuit * with pure shift left from uint/logic.cpp * After a match is found, it updates the cursor to skip all the - * redundant constraints and adds a pure b = a.ror(n) + * redundant constraints and adds a pure b = a << n * constraint to solver. * If there's no match, it will return -1 * diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp similarity index 100% rename from barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.hpp rename to barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp new file mode 100644 index 00000000000..0b4a0b757eb --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp @@ -0,0 +1,485 @@ +#include "ultra_circuit.hpp" +#include "barretenberg/common/log.hpp" + +namespace smt_circuit { + +/** + * @brief Construct a new UltraCircuit object + * + * @param circuit_info CircuitShema object + * @param solver pointer to the global solver + * @param tag tag of the circuit. Empty by default. + */ +UltraCircuit::UltraCircuit( + CircuitSchema& circuit_info, Solver* solver, TermType type, const std::string& tag, bool optimizations) + : CircuitBase(circuit_info.vars_of_interest, + circuit_info.variables, + circuit_info.public_inps, + circuit_info.real_variable_index, + circuit_info.real_variable_tags, + circuit_info.range_tags, + solver, + type, + tag, + optimizations) + , selectors(circuit_info.selectors) + , wires_idxs(circuit_info.wires) + , lookup_tables(circuit_info.lookup_tables) +{ + info("Arithmetic gates: ", selectors[1].size()); + info("Delta Range gates: ", selectors[2].size()); + info("Elliptic gates: ", selectors[3].size()); + info("Aux gates: ", selectors[4].size()); + info("Lookup gates: ", selectors[5].size()); + + // Perform all relaxations for gates or + // add gate in its normal state to solver + + size_t arith_cursor = 0; + while (arith_cursor < this->selectors[1].size()) { + arith_cursor = this->handle_arithmetic_relation(arith_cursor, 1); + } + + size_t lookup_cursor = 0; + while (lookup_cursor < this->selectors[5].size()) { + lookup_cursor = this->handle_lookup_relation(lookup_cursor, 5); + } + + size_t elliptic_cursor = 0; + while (elliptic_cursor < this->selectors[3].size()) { + elliptic_cursor = this->handle_elliptic_relation(elliptic_cursor, 3); + } + + // size_t delta_range_cursor = 0; + // while(delta_range_cursor < this->selectors[2].size()){ + // delta_range_cursor = this->handle_delta_range_relation(delta_range_cursor, 2); + // } + handle_range_constraints(); + + // TODO(alex): aux +} + +/** + * @brief Adds all the arithmetic gate constraints to the solver. + * Relaxes constraint system for non-ff solver engines + * via removing subcircuits that were already proved being correct. + * + * @param cusor current selector + * @param idx arithmthetic selectors position in all selectors + * @return new cursor value + */ +size_t UltraCircuit::handle_arithmetic_relation(size_t cursor, size_t idx) +{ + bb::fr q_m = this->selectors[idx][cursor][0]; + bb::fr q_l = this->selectors[idx][cursor][1]; + bb::fr q_r = this->selectors[idx][cursor][2]; + bb::fr q_o = this->selectors[idx][cursor][3]; + bb::fr q_4 = this->selectors[idx][cursor][4]; + bb::fr q_c = this->selectors[idx][cursor][5]; + bb::fr q_arith = this->selectors[idx][cursor][6]; + + uint32_t w_l_idx = this->wires_idxs[idx][cursor][0]; + uint32_t w_r_idx = this->wires_idxs[idx][cursor][1]; + uint32_t w_o_idx = this->wires_idxs[idx][cursor][2]; + uint32_t w_4_idx = this->wires_idxs[idx][cursor][3]; + uint32_t w_l_shift_idx = this->wires_idxs[idx][cursor][4]; + uint32_t w_4_shift_idx = this->wires_idxs[idx][cursor][7]; + + STerm w_l = this->symbolic_vars[w_l_idx]; + STerm w_r = this->symbolic_vars[w_r_idx]; + STerm w_o = this->symbolic_vars[w_o_idx]; + STerm w_4 = this->symbolic_vars[w_4_idx]; + STerm w_4_shift = this->symbolic_vars[w_4_shift_idx]; + STerm w_l_shift = this->symbolic_vars[w_l_shift_idx]; + + std::vector boolean_gate = { 1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0 }; + bool boolean_gate_flag = + (boolean_gate == selectors[1][cursor]) && (w_l_idx == w_r_idx) && (w_o_idx == 0) && (w_4_idx == 0); + if (boolean_gate_flag) { + (Bool(w_l) == Bool(STerm(0, this->solver, this->type)) | Bool(w_l) == Bool(STerm(1, this->solver, this->type))) + .assert_term(); + return cursor + 1; + } + + STerm res = this->symbolic_vars[0]; + static const bb::fr neg_half = bb::fr(-2).invert(); + + if (!q_arith.is_zero()) { + if (q_m != 0) { + res += ((q_arith - 3) * q_m * neg_half) * w_r * w_l; + } + if (q_l != 0) { + res += (q_l * w_l); + } + if (q_r != 0) { + res += (q_r * w_r); + } + if (q_o != 0) { + res += (q_o * w_o); + } + if (q_4 != 0) { + res += (q_4 * w_4); + } + if (q_c != 0) { + res += q_c; + } + if (q_arith != 1) { + res += (q_arith - 1) * w_4_shift; + } + // res *= q_arith; + res == bb::fr::zero(); + + optimized[w_l_idx] = false; + optimized[w_r_idx] = false; + optimized[w_o_idx] = false; + optimized[w_4_idx] = false; + } + + if (q_arith * (q_arith - 1) * (q_arith - 2) != 0) { + res = w_l + w_4 - w_l_shift + q_m; + res == bb::fr::zero(); + optimized[w_l_shift_idx] = false; + } + + return cursor + 1; +} + +/** + * @brief Adds all the lookup gate constraints to the solver. + * Relaxes constraint system for non-ff solver engines + * via removing subcircuits that were already proved being correct. + * + * @param cusor current selector + * @param idx lookup selectors position in all selectors + * @return new cursor value + */ +size_t UltraCircuit::handle_lookup_relation(size_t cursor, size_t idx) +{ + bb::fr q_m = this->selectors[idx][cursor][0]; + bb::fr q_r = this->selectors[idx][cursor][2]; + bb::fr q_o = this->selectors[idx][cursor][3]; + bb::fr q_c = this->selectors[idx][cursor][5]; + bb::fr q_lookup = this->selectors[idx][cursor][10]; + + if (q_lookup.is_zero()) { + return cursor + 1; + } + + uint32_t w_l_idx = this->wires_idxs[idx][cursor][0]; + uint32_t w_r_idx = this->wires_idxs[idx][cursor][1]; + uint32_t w_o_idx = this->wires_idxs[idx][cursor][2]; + uint32_t w_l_shift_idx = this->wires_idxs[idx][cursor][4]; + uint32_t w_r_shift_idx = this->wires_idxs[idx][cursor][5]; + uint32_t w_o_shift_idx = this->wires_idxs[idx][cursor][6]; + + optimized[w_l_idx] = false; + optimized[w_r_idx] = false; + optimized[w_o_idx] = false; + optimized[w_l_shift_idx] = false; + optimized[w_r_shift_idx] = false; + optimized[w_o_shift_idx] = false; + + auto table_idx = static_cast(q_o); + if (!this->cached_symbolic_tables.contains(table_idx)) { + std::vector> new_table; + for (auto table_entry : this->lookup_tables[table_idx]) { + std::vector tmp_entry = { + STerm(table_entry[0], this->solver, this->type), + STerm(table_entry[1], this->solver, this->type), + STerm(table_entry[2], this->solver, this->type), + }; + new_table.push_back(tmp_entry); + } + this->cached_symbolic_tables.insert({ table_idx, this->solver->create_lookup_table(new_table) }); + } + + STerm first_entry = this->symbolic_vars[w_l_idx] + q_r * this->symbolic_vars[w_l_shift_idx]; + STerm second_entry = this->symbolic_vars[w_r_idx] + q_m * this->symbolic_vars[w_r_shift_idx]; + STerm third_entry = this->symbolic_vars[w_o_idx] + q_c * this->symbolic_vars[w_o_shift_idx]; + + std::vector entries = { first_entry, second_entry, third_entry }; + STerm::in_table(entries, this->cached_symbolic_tables[table_idx]); + return cursor + 1; +} + +/** + * @brief Adds all the elliptic gate constraints to the solver. + * + * @param cusor current selector + * @param idx elliptic selectors position in all selectors + * @return new cursor value + */ +size_t UltraCircuit::handle_elliptic_relation(size_t cursor, size_t idx) +{ + bb::fr q_is_double = this->selectors[idx][cursor][0]; + bb::fr q_sign = this->selectors[idx][cursor][1]; + bb::fr q_elliptic = this->selectors[idx][cursor][8]; + if (q_elliptic.is_zero()) { + return cursor + 1; + } + + uint32_t w_r_idx = this->wires_idxs[idx][cursor][1]; + uint32_t w_o_idx = this->wires_idxs[idx][cursor][2]; + uint32_t w_l_shift_idx = this->wires_idxs[idx][cursor][4]; + uint32_t w_r_shift_idx = this->wires_idxs[idx][cursor][5]; + uint32_t w_o_shift_idx = this->wires_idxs[idx][cursor][6]; + uint32_t w_4_shift_idx = this->wires_idxs[idx][cursor][7]; + optimized[w_r_idx] = false; + optimized[w_o_idx] = false; + optimized[w_l_shift_idx] = false; + optimized[w_r_shift_idx] = false; + optimized[w_o_shift_idx] = false; + optimized[w_4_shift_idx] = false; + + STerm x_1 = this->symbolic_vars[w_r_idx]; + STerm y_1 = this->symbolic_vars[w_o_idx]; + STerm x_2 = this->symbolic_vars[w_l_shift_idx]; + STerm y_2 = this->symbolic_vars[w_4_shift_idx]; + STerm x_3 = this->symbolic_vars[w_r_shift_idx]; + STerm y_3 = this->symbolic_vars[w_o_shift_idx]; + + auto x_diff = (x_2 - x_1); + auto y2_sqr = (y_2 * y_2); + auto y1_sqr = (y_1 * y_1); + auto y1y2 = y_1 * y_2 * q_sign; + auto x_add_identity = (x_3 + x_2 + x_1) * x_diff * x_diff - y2_sqr - y1_sqr + y1y2 + y1y2; + + auto y1_plus_y3 = y_1 + y_3; + auto y_diff = y_2 * q_sign - y_1; + auto y_add_identity = y1_plus_y3 * x_diff + (x_3 - x_1) * y_diff; + + if (q_is_double.is_zero()) { + x_add_identity == 0; // scaling_factor = 1 + y_add_identity == 0; // scaling_factor = 1 + } + + bb::fr curve_b = this->selectors[3][cursor][11]; + auto x_pow_4 = (y1_sqr - curve_b) * x_1; + auto y1_sqr_mul_4 = y1_sqr + y1_sqr; + y1_sqr_mul_4 += y1_sqr_mul_4; + auto x1_pow_4_mul_9 = x_pow_4 * 9; + auto x_double_identity = (x_3 + x_1 + x_1) * y1_sqr_mul_4 - x1_pow_4_mul_9; + + auto x1_sqr_mul_3 = (x_1 + x_1 + x_1) * x_1; + auto y_double_identity = x1_sqr_mul_3 * (x_1 - x_3) - (y_1 + y_1) * (y_1 + y_3); + + if (!q_is_double.is_zero()) { + x_double_identity == 0; // scaling_factor = 1 + y_double_identity == 0; // scaling_factor = 1 + } + + return cursor + 1; +} + +/** + * @brief Adds all the delta_range gate constraints to the solver. + * + * @param cusor current selector + * @param idx delta_range selectors position in all selectors + * @return new cursor value + * @todo Useless? + */ +size_t UltraCircuit::handle_delta_range_relation(size_t cursor, size_t idx) +{ + bb::fr q_delta_range = this->selectors[idx][cursor][7]; + if (q_delta_range == 0) { + return cursor + 1; + } + + uint32_t w_l_idx = this->wires_idxs[idx][cursor][0]; + uint32_t w_r_idx = this->wires_idxs[idx][cursor][1]; + uint32_t w_o_idx = this->wires_idxs[idx][cursor][2]; + uint32_t w_4_idx = this->wires_idxs[idx][cursor][3]; + uint32_t w_l_shift_idx = this->wires_idxs[idx][cursor][4]; + + STerm w_1 = this->symbolic_vars[w_l_idx]; + STerm w_2 = this->symbolic_vars[w_r_idx]; + STerm w_3 = this->symbolic_vars[w_o_idx]; + STerm w_4 = this->symbolic_vars[w_4_idx]; + STerm w_1_shift = this->symbolic_vars[w_l_shift_idx]; + + STerm delta_1 = w_2 - w_1; + STerm delta_2 = w_3 - w_2; + STerm delta_3 = w_4 - w_3; + STerm delta_4 = w_1_shift - w_4; + + STerm tmp = (delta_1 - 1) * (delta_1 - 1) - 1; + tmp *= (delta_1 - 2) * (delta_1 - 2) - 1; + tmp == 0; + + tmp = (delta_2 - 1) * (delta_2 - 1) - 1; + tmp *= (delta_2 - 2) * (delta_2 - 2) - 1; + tmp == 0; + + tmp = (delta_3 - 1) * (delta_3 - 1) - 1; + tmp *= (delta_3 - 2) * (delta_3 - 2) - 1; + tmp == 0; + + tmp = (delta_4 - 1) * (delta_4 - 1) - 1; + tmp *= (delta_4 - 2) * (delta_4 - 2) - 1; + tmp == 0; + + return cursor + 1; +} + +/** + * @brief Adds all the range constraints to the solver. + * + * @param cusor current selector + * @param idx delta_range selectors position in all selectors + * @return new cursor value + */ +void UltraCircuit::handle_range_constraints() +{ + for (uint32_t i = 0; i < this->get_num_vars(); i++) { + if (i != this->real_variable_index[i] || optimized[i]) { + continue; + } + + uint32_t tag = this->real_variable_tags[this->real_variable_index[i]]; + if (tag != 0 && this->range_tags.contains(tag)) { + uint64_t range = this->range_tags[tag]; + if ((this->type != TermType::FFITerm) && (this->type != TermType::BVTerm)) { + if (!this->cached_range_tables.contains(range)) { + std::vector new_range_table; + for (size_t entry = 0; entry < range; entry++) { + new_range_table.push_back(STerm(entry, this->solver, this->type)); + } + this->cached_range_tables.insert({ range, this->solver->create_table(new_range_table) }); + } + + this->symbolic_vars[i].in(this->cached_range_tables[range]); + } else { + this->symbolic_vars[i] <= range; + } + } + } +} +/** + * @brief Similar functionality to old .check_circuit() method + * in standard circuit builder. + * + * @param witness + * @return true + * @return false + * + * @todo Do we actually need this here? + */ +bool UltraCircuit::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()) + + + std::to_string(witness.size())); + } + return true; +} + +/** + * @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, + * 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 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 + */ +std::pair UltraCircuit::unique_witness_ext( + CircuitSchema& circuit_info, + Solver* s, + TermType type, + 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) +{ + // TODO(alex): set optimizations to be true once they are confirmed + UltraCircuit c1(circuit_info, s, type, "circuit1", false); + UltraCircuit c2(circuit_info, s, type, "circuit2", false); + + for (const auto& term : equal) { + c1[term] == c2[term]; + } + for (const auto& term : not_equal) { + c1[term] != c2[term]; + } + + std::vector eqs; + for (const auto& term : equal_at_the_same_time) { + Bool tmp = Bool(c1[term]) == Bool(c2[term]); + eqs.push_back(tmp); + } + + if (eqs.size() > 1) { + batch_or(eqs).assert_term(); + } else if (eqs.size() == 1) { + eqs[0].assert_term(); + } + + std::vector neqs; + for (const auto& term : not_equal_at_the_same_time) { + Bool tmp = Bool(c1[term]) != Bool(c2[term]); + 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 }; +} + +/** + * @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, + * 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 + */ +std::pair UltraCircuit::unique_witness(CircuitSchema& circuit_info, + Solver* s, + TermType type, + const std::vector& equal) +{ + // TODO(alex): set optimizations to be true once they are confirmed + UltraCircuit c1(circuit_info, s, type, "circuit1", false); + UltraCircuit c2(circuit_info, s, type, "circuit2", false); + + 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; + } + if (c1.optimized[i]) { + 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 }; +} +}; // namespace smt_circuit \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp new file mode 100644 index 00000000000..3d1316d023a --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp @@ -0,0 +1,65 @@ +#pragma once +#include "circuit_base.hpp" + +namespace smt_circuit { + +/** + * @brief Symbolic Circuit class for Standard Circuit Builder. + * + * @details Contains all the information about the circuit: gates, variables, + * symbolic variables, specified names and global solver. + */ +class UltraCircuit : public CircuitBase { + public: + // TODO(alex): check that there's no actual pub_inputs block + std::vector>> selectors; // all selectors from the circuit + // 1st entry are arithmetic selectors + // 2nd entry are delta_range selectors + // 3rd entry are elliptic selectors + // 4th entry are aux selectors + // 5th entry are lookup selectors + std::vector>> wires_idxs; // values of the gates' wires idxs + + std::vector>> lookup_tables; + std::unordered_map cached_symbolic_tables; + std::unordered_map cached_range_tables; + + explicit UltraCircuit(CircuitSchema& circuit_info, + Solver* solver, + TermType type = TermType::FFTerm, + const std::string& tag = "", + bool optimizations = true); + UltraCircuit(const UltraCircuit& other) = default; + UltraCircuit(UltraCircuit&& other) = default; + UltraCircuit& operator=(const UltraCircuit& other) = default; + UltraCircuit& operator=(UltraCircuit&& other) = default; + ~UltraCircuit() override = default; + + inline size_t get_num_gates() const + { + return selectors[0].size() + selectors[1].size() + selectors[2].size() + selectors[3].size() + + selectors[4].size() + selectors[5].size(); + }; + + bool simulate_circuit_eval(std::vector& witness) const override; + + size_t handle_arithmetic_relation(size_t cursor, size_t idx); + size_t handle_lookup_relation(size_t cursor, size_t idx); + size_t handle_elliptic_relation(size_t cursor, size_t idx); + size_t handle_delta_range_relation(size_t cursor, size_t idx); + void handle_range_constraints(); + + static std::pair unique_witness_ext( + CircuitSchema& circuit_info, + Solver* s, + TermType type, + 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 = {}); + static std::pair unique_witness(CircuitSchema& circuit_info, + Solver* s, + TermType type, + const std::vector& equal = {}); +}; +}; // namespace smt_circuit \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.test.cpp new file mode 100644 index 00000000000..bdff9b10774 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.test.cpp @@ -0,0 +1,242 @@ +#include +#include +#include + +#include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp" + +#include "barretenberg/crypto/pedersen_commitment/pedersen.hpp" +#include "barretenberg/stdlib/primitives/field/field.hpp" +#include "barretenberg/stdlib/primitives/uint/uint.hpp" + +#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp" +#include "barretenberg/smt_verification/util/smt_util.hpp" + +#include + +using namespace bb; +using namespace smt_circuit; + +namespace { +auto& engine = numeric::get_debug_randomness(); +} + +using field_t = stdlib::field_t; +using witness_t = stdlib::witness_t; +using pub_witness_t = stdlib::public_witness_t; +using uint_t = stdlib::uint32; + +TEST(ultra_circuit, assert_equal) +{ + auto builder = UltraCircuitBuilder(); + + field_t a(witness_t(&builder, fr::random_element())); + field_t b(witness_t(&builder, fr::random_element())); + builder.set_variable_name(a.witness_index, "a"); + builder.set_variable_name(b.witness_index, "b"); + field_t c = (a + a) / (b + b + b); + builder.set_variable_name(c.witness_index, "c"); + + field_t d(witness_t(&builder, a.get_value())); + field_t e(witness_t(&builder, b.get_value())); + field_t f(witness_t(&builder, c.get_value())); + builder.assert_equal(d.get_witness_index(), a.get_witness_index()); + builder.assert_equal(e.get_witness_index(), b.get_witness_index()); + + field_t g = d + d; + field_t h = e + e + e; + field_t i = g / h; + builder.assert_equal(i.get_witness_index(), c.get_witness_index()); + field_t j(witness_t(&builder, i.get_value())); + field_t k(witness_t(&builder, j.get_value())); + builder.assert_equal(i.get_witness_index(), j.get_witness_index()); + builder.assert_equal(i.get_witness_index(), k.get_witness_index()); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, ultra_solver_config); + UltraCircuit circuit(circuit_info, &s, TermType::FFTerm); + + ASSERT_EQ(circuit[k.get_witness_index()].term, circuit["c"].term); + ASSERT_EQ(circuit[d.get_witness_index()].term, circuit["a"].term); + ASSERT_EQ(circuit[e.get_witness_index()].term, circuit["b"].term); + + ASSERT_EQ(circuit[i.get_witness_index()].term, circuit[k.get_witness_index()].term); + ASSERT_EQ(circuit[i.get_witness_index()].term, circuit[j.get_witness_index()].term); +} + +TEST(ultra_circuit, arithmetic) +{ + UltraCircuitBuilder builder; + + field_t a(witness_t(&builder, fr::random_element())); + field_t b(witness_t(&builder, fr::random_element())); + field_t c = a * a * b / (a + b * 3) - b / a; + + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + builder.set_variable_name(c.get_witness_index(), "c"); + + auto circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, ultra_solver_config); + UltraCircuit cir(circuit_info, &s); + ASSERT_EQ(cir.get_num_gates(), builder.get_num_gates()); + + cir["a"] == a.get_value(); + cir["b"] == b.get_value(); + + bool res = s.check(); + ASSERT_TRUE(res); + + std::string c_solver_val = s.getValue(cir["c"]).getFiniteFieldValue(); + std::string c_builder_val = STerm(c.get_value(), &s, TermType::FFTerm).term.getFiniteFieldValue(); + ASSERT_EQ(c_solver_val, c_builder_val); +} + +TEST(ultra_circuit, elliptic_add) +{ + UltraCircuitBuilder builder; + + bb::grumpkin::g1::affine_element p1 = bb::crypto::pedersen_commitment::commit_native({ bb::fr::one() }, 0); + bb::grumpkin::g1::affine_element p2 = bb::crypto::pedersen_commitment::commit_native({ bb::fr::one() }, 1); + bb::grumpkin::g1::affine_element p3 = bb::grumpkin::g1::element(p1) + bb::grumpkin::g1::element(p2); + + uint32_t x1 = builder.add_variable(p1.x); + uint32_t y1 = builder.add_variable(p1.y); + uint32_t x2 = builder.add_variable(p2.x); + uint32_t y2 = builder.add_variable(p2.y); + uint32_t x3 = builder.add_variable(p3.x); + uint32_t y3 = builder.add_variable(p3.y); + + builder.set_variable_name(x1, "x1"); + builder.set_variable_name(x2, "x2"); + builder.set_variable_name(x3, "x3"); + builder.set_variable_name(y1, "y1"); + builder.set_variable_name(y2, "y2"); + builder.set_variable_name(y3, "y3"); + + builder.create_ecc_add_gate({ x1, y1, x2, y2, x3, y3, 1 }); + + auto circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, ultra_solver_config); + UltraCircuit cir(circuit_info, &s); + ASSERT_EQ(cir.get_num_gates(), builder.get_num_gates()); + + cir["x1"] == builder.get_variable(x1); + cir["x2"] == builder.get_variable(x2); + cir["y1"] == builder.get_variable(y1); + cir["y2"] == builder.get_variable(y2); + + bool res = s.check(); + ASSERT_TRUE(res); + + std::string x3_solver_val = s.getValue(cir["x3"]).getFiniteFieldValue(); + std::string y3_solver_val = s.getValue(cir["y3"]).getFiniteFieldValue(); + + std::string x3_builder_val = STerm(builder.get_variable(x3), &s, TermType::FFTerm).term.getFiniteFieldValue(); + std::string y3_builder_val = STerm(builder.get_variable(y3), &s, TermType::FFTerm).term.getFiniteFieldValue(); + + ASSERT_EQ(x3_solver_val, x3_builder_val); + ASSERT_EQ(y3_solver_val, y3_builder_val); + + ((Bool(cir["x3"]) != Bool(STerm(builder.get_variable(x3), &s, TermType::FFTerm))) | + (Bool(cir["y3"]) != Bool(STerm(builder.get_variable(y3), &s, TermType::FFTerm)))) + .assert_term(); + res = s.check(); + ASSERT_FALSE(res); +} + +TEST(ultra_circuit, elliptic_dbl) +{ + UltraCircuitBuilder builder; + + bb::grumpkin::g1::affine_element p1 = bb::crypto::pedersen_commitment::commit_native({ bb::fr::one() }, 0); + bb::grumpkin::g1::affine_element p3 = bb::grumpkin::g1::element(p1).dbl(); + + uint32_t x1 = builder.add_variable(p1.x); + uint32_t y1 = builder.add_variable(p1.y); + uint32_t x3 = builder.add_variable(p3.x); + uint32_t y3 = builder.add_variable(p3.y); + builder.set_variable_name(x1, "x1"); + builder.set_variable_name(x3, "x3"); + builder.set_variable_name(y1, "y1"); + builder.set_variable_name(y3, "y3"); + + builder.create_ecc_dbl_gate({ x1, y1, x3, y3 }); + + auto circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, ultra_solver_config); + UltraCircuit cir(circuit_info, &s); + ASSERT_EQ(cir.get_num_gates(), builder.get_num_gates()); + + cir["x1"] == builder.get_variable(x1); + cir["y1"] == builder.get_variable(y1); + + bool res = s.check(); + ASSERT_TRUE(res); + + std::string x3_solver_val = s.getValue(cir["x3"]).getFiniteFieldValue(); + std::string y3_solver_val = s.getValue(cir["y3"]).getFiniteFieldValue(); + + std::string x3_builder_val = STerm(builder.get_variable(x3), &s, TermType::FFTerm).term.getFiniteFieldValue(); + std::string y3_builder_val = STerm(builder.get_variable(y3), &s, TermType::FFTerm).term.getFiniteFieldValue(); + + ASSERT_EQ(x3_solver_val, x3_builder_val); + ASSERT_EQ(y3_solver_val, y3_builder_val); + + ((Bool(cir["x3"]) != Bool(STerm(builder.get_variable(x3), &s, TermType::FFTerm))) | + (Bool(cir["y3"]) != Bool(STerm(builder.get_variable(y3), &s, TermType::FFTerm)))) + .assert_term(); + res = s.check(); + ASSERT_FALSE(res); +} + +TEST(ultra_circuit, ranges) +{ + UltraCircuitBuilder builder; + + uint_t a(witness_t(&builder, static_cast(bb::fr::random_element()))); + builder.set_variable_name(a.get_witness_index(), "a"); + builder.finalize_circuit(); + + auto circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, ultra_solver_config); + UltraCircuit cir(circuit_info, &s, TermType::BVTerm); + ASSERT_EQ(cir.get_num_gates(), builder.get_num_gates()); + + cir["a"] == a.get_value(); + s.print_assertions(); + + bool res = s.check(); + ASSERT_TRUE(res); +} + +TEST(ultra_circuit, lookup_tables) +{ + UltraCircuitBuilder builder; + + uint_t a(witness_t(&builder, static_cast(bb::fr::random_element()))); + uint_t b(witness_t(&builder, static_cast(bb::fr::random_element()))); + uint_t c = a ^ b; + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + builder.set_variable_name(c.get_witness_index(), "c"); + builder.finalize_circuit(); + + auto circuit_info = unpack_from_buffer(builder.export_circuit()); + uint32_t modulus_base = 16; + uint32_t bvsize = 32; + Solver s(circuit_info.modulus, ultra_solver_config, modulus_base, bvsize); + UltraCircuit cir(circuit_info, &s, TermType::BVTerm); + ASSERT_EQ(cir.get_num_gates(), builder.get_num_gates()); + + cir["a"] == a.get_value(); + cir["b"] == b.get_value(); + s.print_assertions(); + + bool res = s.check(); + ASSERT_TRUE(res); + + std::string c_solver_val = s.getValue(cir["c"]).getBitVectorValue(); + std::string c_builder_val = STerm(c.get_value(), &s, TermType::BVTerm).term.getBitVectorValue(); + ASSERT_EQ(c_solver_val, c_builder_val); +} \ No newline at end of file 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 ccca774985b..89a10ab5363 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp @@ -34,9 +34,9 @@ TEST(SMT_Example, multiplication_true) auto buf = builder.export_circuit(); - smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - smt_circuit::Circuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); + smt_circuit::StandardCircuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); smt_terms::STerm a1 = circuit["a"]; smt_terms::STerm b1 = circuit["b"]; smt_terms::STerm c1 = circuit["c"]; @@ -65,9 +65,9 @@ TEST(SMT_Example, multiplication_true_kind) auto buf = builder.export_circuit(); - smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - smt_circuit::Circuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); + smt_circuit::StandardCircuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); smt_terms::STerm a1 = circuit["a"]; smt_terms::STerm b1 = circuit["b"]; smt_terms::STerm c1 = circuit["c"]; @@ -96,9 +96,9 @@ TEST(SMT_Example, multiplication_false) auto buf = builder.export_circuit(); - smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - smt_circuit::Circuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); + smt_circuit::StandardCircuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); smt_terms::STerm a1 = circuit["a"]; smt_terms::STerm b1 = circuit["b"]; @@ -141,11 +141,12 @@ TEST(SMT_Example, unique_witness_ext) auto buf = builder.export_circuit(); - smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - std::pair cirs = - smt_circuit::unique_witness_ext(circuit_info, &s, smt_terms::TermType::FFTerm, { "ev" }, { "z" }); + std::pair cirs = + smt_circuit::StandardCircuit::unique_witness_ext( + circuit_info, &s, smt_terms::TermType::FFTerm, { "ev" }, { "z" }); bool res = s.check(); ASSERT_TRUE(res); @@ -173,11 +174,11 @@ TEST(SMT_Example, unique_witness) auto buf = builder.export_circuit(); - smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - std::pair cirs = - smt_circuit::unique_witness(circuit_info, &s, smt_terms::TermType::FFTerm, { "ev" }); + std::pair cirs = + smt_circuit::StandardCircuit::unique_witness(circuit_info, &s, smt_terms::TermType::FFTerm, { "ev" }); bool res = s.check(); ASSERT_TRUE(res); @@ -185,4 +186,4 @@ TEST(SMT_Example, unique_witness) std::unordered_map terms = { { "z_c1", cirs.first["z"] }, { "z_c2", cirs.second["z"] } }; std::unordered_map vals = s.model(terms); ASSERT_NE(vals["z_c1"], vals["z_c2"]); -} +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp index f3d9582a13b..f8e74061d44 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp @@ -8,7 +8,7 @@ #include "barretenberg/stdlib/primitives/field/field.hpp" #include "barretenberg/stdlib_circuit_builders/standard_circuit_builder.hpp" -#include "barretenberg/smt_verification/circuit/circuit.hpp" +#include "barretenberg/smt_verification/circuit/standard_circuit.hpp" #include "barretenberg/smt_verification/util/smt_util.hpp" using namespace bb; @@ -54,7 +54,7 @@ msgpack::sbuffer create_polynomial_evaluation_circuit(size_t n, bool pub_coeffs) return builder.export_circuit(); } -STerm direct_polynomial_evaluation(Circuit& c, size_t n) +STerm direct_polynomial_evaluation(StandardCircuit& c, size_t n) { STerm point = c["point"]; STerm result = c["result"]; @@ -65,7 +65,7 @@ STerm direct_polynomial_evaluation(Circuit& c, size_t n) return ev; } -void model_variables(Circuit& c, Solver* s, STerm& evaluation) +void model_variables(StandardCircuit& c, Solver* s, STerm& evaluation) { std::unordered_map terms; terms.insert({ "point", c["point"] }); @@ -86,11 +86,11 @@ TEST(polynomial_evaluation, public) CircuitSchema circuit_info = unpack_from_buffer(buf); Solver s(circuit_info.modulus); - Circuit circuit(circuit_info, &s, TermType::FFTerm); + StandardCircuit circuit(circuit_info, &s, TermType::FFTerm); STerm ev = direct_polynomial_evaluation(circuit, n); ev != circuit["result"]; - bool res = smt_timer(&s, false); + bool res = smt_timer(&s); ASSERT_FALSE(res); } @@ -101,11 +101,11 @@ TEST(polynomial_evaluation, private) CircuitSchema circuit_info = unpack_from_buffer(buf); Solver s(circuit_info.modulus); - Circuit circuit(circuit_info, &s, TermType::FFTerm); + StandardCircuit circuit(circuit_info, &s, TermType::FFTerm); STerm ev = direct_polynomial_evaluation(circuit, n); ev != circuit["result"]; - bool res = smt_timer(&s, false); + bool res = smt_timer(&s); ASSERT_FALSE(res); info("Gates: ", circuit.get_num_gates()); info("Result: ", s.getResult()); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp index 093b237b750..3fde6d7d09f 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp @@ -105,7 +105,7 @@ std::unordered_map Solver::model(std::vector bool_res = { "false", "true" }; return bool_res[static_cast(term.getBooleanValue())]; } + // handling tuples + if (term.getKind() == cvc5::Kind::APPLY_CONSTRUCTOR) { + std::string res = "("; + for (const auto& t : term) { + res += stringify_term(t) + ", "; + } + return res + ")"; + } + if (term.getKind() == cvc5::Kind::INTERNAL_KIND) { + return "set_" + std::to_string(this->tables[term]); + } + if (term.getKind() == cvc5::Kind::SET_INSERT || term.getKind() == cvc5::Kind::SET_EMPTY) { + return ""; + } std::string res; std::string op; @@ -184,11 +198,9 @@ std::string stringify_term(const cvc5::Term& term, bool parenthesis) op = " & "; break; case cvc5::Kind::BITVECTOR_SHL: - back = true; op = " << "; break; case cvc5::Kind::BITVECTOR_LSHR: - back = true; op = " >> "; break; case cvc5::Kind::BITVECTOR_ROTATE_LEFT: @@ -209,8 +221,13 @@ std::string stringify_term(const cvc5::Term& term, bool parenthesis) op = " % "; parenthesis = true; break; + case cvc5::Kind::SET_MEMBER: + op = " in "; + parenthesis = true; + break; default: info("Invalid operand :", term.getKind()); + info(term); break; } @@ -239,33 +256,51 @@ std::string stringify_term(const cvc5::Term& term, bool parenthesis) * Output assertions in human readable format. * * */ -void Solver::print_assertions() const +void Solver::print_assertions() { for (const auto& t : this->solver.getAssertions()) { - info(stringify_term(t)); + info(this->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; + children.reserve(table.size() + 1); 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); + cvc5::Term res = this->term_manager.mkTerm(cvc5::Kind::SET_INSERT, children); + size_t cursize = this->tables.size(); + info("Creating table for op: ", children.size(), ", № ", cursize); + this->tables.insert({ res, cursize }); + return res; +} + +cvc5::Term Solver::create_table(std::vector& table) +{ + cvc5::Term tmp = table[0]; + cvc5::Sort relation = this->term_manager.mkSetSort(tmp.getSort()); + cvc5::Term resulting_table = this->term_manager.mkEmptySet(relation); + + std::vector children; + children.reserve(table.size() + 1); + for (auto& table_entry : table) { + children.push_back(table_entry); + } + children.push_back(resulting_table); + cvc5::Term res = this->term_manager.mkTerm(cvc5::Kind::SET_INSERT, children); + size_t cursize = this->tables.size(); + info("Creating table for range: ", children.size(), ", № ", cursize); + + this->tables.insert({ res, cursize }); + return res; } }; // 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 0151c1bb857..e6720e95c99 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -14,8 +14,10 @@ namespace smt_solver { * @param timeout tells solver to stop trying after `timeout` msecs. * @param debug set verbosity of cvc5: 0, 1, 2. * - * @param ff_disjunctive_bit tells solver to change all ((x = 0) | (x = 1)) to x*x = x. + * @param ff_elim_disjunctive_bit tells solver to change all ((x = 0) | (x = 1)) to x*x = x. * @param ff_solver tells solver which finite field solver to use: "gb", "split". + * + * @param lookup_enabled tells solver to enable sets when we deal with lookups */ struct SolverConfiguration { bool produce_models; @@ -24,9 +26,12 @@ struct SolverConfiguration { bool ff_elim_disjunctive_bit; std::string ff_solver; + + bool lookup_enabled; }; -const SolverConfiguration default_solver_config = { true, 0, 0, false, "" }; +const SolverConfiguration default_solver_config = { true, 0, 0, false, "", false }; +const SolverConfiguration ultra_solver_config = { true, 0, 0, false, "", true }; /** * @brief Class for the solver. @@ -46,6 +51,8 @@ class Solver { cvc5::Result cvc_result; bool checked = false; + std::unordered_map tables; + explicit Solver(const std::string& modulus, const SolverConfiguration& config = default_solver_config, uint32_t base = 16, @@ -88,6 +95,13 @@ class Solver { solver.setOption("ff-solver", config.ff_solver); } + if (lookup_enabled) { + this->solver.setLogic("ALL"); + this->solver.setOption("finite-model-find", "true"); + this->solver.setOption("sets-ext", "true"); + lookup_enabled = true; + } + solver.setOption("output", "incomplete"); } @@ -99,6 +113,7 @@ class Solver { bool lookup_enabled = false; cvc5::Term create_lookup_table(std::vector>& table); + cvc5::Term create_table(std::vector& table); void assertFormula(const cvc5::Term& term) const { this->solver.assertFormula(term); } @@ -117,11 +132,10 @@ class Solver { std::unordered_map model(std::unordered_map& terms) const; std::unordered_map model(std::vector& terms) const; - void print_assertions() const; + void print_assertions(); + std::string stringify_term(const cvc5::Term& term, bool parenthesis = false); ~Solver() = default; }; -std::string stringify_term(const cvc5::Term& term, bool parenthesis = false); - }; // namespace smt_solver diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp index 7ab111cb86c..21cdeea09a8 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp @@ -371,6 +371,19 @@ STerm STerm::rotl(const uint32_t& n) const return { res, this->solver, this->type }; } +/** + * @brief Create an inclusion constraint + * + * @param entry entry to be checked + * @param table table that consists of elements, ranges mostly + */ +void STerm::in(const cvc5::Term& table) const +{ + Solver* slv = this->solver; + cvc5::Term inc = slv->term_manager.mkTerm(cvc5::Kind::SET_MEMBER, { this->term, table }); + slv->assertFormula(inc); +} + STerm operator+(const bb::fr& lhs, const STerm& rhs) { return rhs + lhs; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp index 60c1f3df300..cef9d44e8a0 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp @@ -153,7 +153,9 @@ class STerm { STerm rotr(const uint32_t& n) const; STerm rotl(const uint32_t& n) const; - operator std::string() const { return smt_solver::stringify_term(term); }; + void in(const cvc5::Term& table) const; + + operator std::string() const { return this->solver->stringify_term(term); }; operator cvc5::Term() const { return term; }; ~STerm() = default; 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 ff516661c1d..c99ebcc0f39 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,7 +223,26 @@ template class CircuitBuilderBase { void failure(std::string msg); }; -template struct CircuitSchema { +/** + * @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_interest Map wires indices 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 indices for each selector + * @param real_variable_index Encoded copy constraints + * @param lookup_tables List of lookup tables + * @param real_variable_tag Variables' tags for range constraints + * @param range_lists Existing range lists + */ +template struct CircuitSchemaInternal { std::string modulus; std::vector public_inps; std::unordered_map vars_of_interest; @@ -232,8 +251,18 @@ template struct CircuitSchema { 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); + std::vector real_variable_tags; + std::unordered_map range_tags; + MSGPACK_FIELDS(modulus, + public_inps, + vars_of_interest, + variables, + selectors, + wires, + real_variable_index, + lookup_tables, + real_variable_tags, + range_tags); }; } // namespace bb 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 94e10887fba..b2fada856cb 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 @@ -520,7 +520,7 @@ void StandardCircuitBuilder_::assert_equal_constant(uint32_t const a_idx, FF template msgpack::sbuffer StandardCircuitBuilder_::export_circuit() { using base = CircuitBuilderBase; - CircuitSchema cir; + CircuitSchemaInternal cir; uint64_t modulus[4] = { FF::Params::modulus_0, FF::Params::modulus_1, FF::Params::modulus_2, FF::Params::modulus_3 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 f498411d97b..4325a52985f 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 @@ -2727,13 +2727,14 @@ template uint256_t UltraCircuitBuilder_ msgpack::sbuffer UltraCircuitBuilder_::export_circuit() { using base = CircuitBuilderBase; - CircuitSchema cir; + CircuitSchemaInternal cir; uint64_t modulus[4] = { FF::Params::modulus_0, FF::Params::modulus_1, FF::Params::modulus_2, FF::Params::modulus_3 @@ -2770,17 +2771,10 @@ template msgpack::sbuffer UltraCircuitBuilder_> 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_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_delta_range()[idx], block.q_elliptic()[idx], + block.q_aux()[idx], block.q_lookup_type()[idx], curve_b }; std::vector tmp_w = { this->real_variable_index[block.w_l()[idx]], @@ -2821,6 +2815,12 @@ template msgpack::sbuffer UltraCircuitBuilder_real_variable_tags; + + for (const auto& list : range_lists) { + cir.range_tags[list.second.range_tag] = list.first; + } + msgpack::sbuffer buffer; msgpack::pack(buffer, cir); return buffer;