diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp new file mode 100644 index 00000000000..6d53857d5fa --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp @@ -0,0 +1,82 @@ +#include "circuit_base.hpp" + +namespace smt_circuit { + +CircuitBase::CircuitBase(std::unordered_map& variable_names, + std::vector& variables, + std::vector& public_inps, + std::vector& real_variable_index, + Solver* solver, + TermType type, + const std::string& tag, + bool optimizations) + : variables(variables) + , public_inps(public_inps) + , variable_names(variable_names) + , real_variable_index(real_variable_index) + , optimizations(optimizations) + , solver(solver) + , type(type) + , tag(tag) +{ + if (!this->tag.empty() && tag[0] != '_') { + this->tag = "_" + this->tag; + } + + for (auto& x : variable_names) { + variable_names_inverse.insert({ x.second, x.first }); + } + + this->init(); + + for (const auto& i : this->public_inps) { + this->symbolic_vars[this->real_variable_index[i]] == this->variables[i]; + } +} + +/** + * Creates all the needed symbolic variables and constants + * which are used in circuit. + * + */ +void CircuitBase::init() +{ + variable_names.insert({ 0, "zero" }); + variable_names_inverse.insert({ "zero", 0 }); + symbolic_vars.insert({ 0, STerm::Var("zero" + this->tag, this->solver, this->type) }); + optimized.insert({ 0, false }); + + size_t num_vars = variables.size(); + + for (uint32_t i = 1; i < num_vars; i++) { + uint32_t real_idx = this->real_variable_index[i]; + if (this->symbolic_vars.contains(real_idx)) { + continue; + } + + std::string name = variable_names.contains(real_idx) ? variable_names[real_idx] : "var_" + std::to_string(i); + name += this->tag; + symbolic_vars.insert({ real_idx, STerm::Var(name, this->solver, this->type) }); + + optimized.insert({ real_idx, true }); + } + + symbolic_vars[0] == bb::fr(0); +} + +/** + * @brief Returns a previously named symbolic variable. + * + * @param name + * @return STerm + */ +STerm CircuitBase::operator[](const std::string& name) +{ + 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]; +} + +} // namespace smt_circuit \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp new file mode 100644 index 00000000000..e37bfcd06d5 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp @@ -0,0 +1,74 @@ +#pragma once + +#include +#include +#include +#include + +#include "barretenberg/smt_verification/terms/bool.hpp" +#include "barretenberg/smt_verification/terms/term.hpp" + +#include "subcircuits.hpp" + +namespace smt_circuit { +using namespace smt_solver; +using namespace smt_terms; +using namespace smt_circuit_schema; +using namespace smt_subcircuits; + +enum class SubcircuitType { XOR, AND, RANGE, ROR, SHL, SHR }; + +/** + * @brief Base class for symbolic circuits + * + * @details Contains all the information about the circuit: gates, variables, + * symbolic variables, specified names, global solver and optimiztaions. + * + */ +class CircuitBase { + public: + 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::unordered_map symbolic_vars; // all the symbolic variables from the circuit + std::vector real_variable_index; // indexes for assert_equal'd wires + 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 + std::unordered_map> + cached_subcircuits; // caches subcircuits during optimization + // No need to recompute them each time + + Solver* solver; // pointer to the solver + TermType type; // Type of the underlying Symbolic Terms + + std::string tag; // tag of the symbolic circuit. + // If not empty, will be added to the names + // of symbolic variables to prevent collisions. + + CircuitBase(std::unordered_map& variable_names, + std::vector& variables, + std::vector& public_inps, + std::vector& real_variable_index, + Solver* solver, + TermType type, + const std::string& tag = "", + bool optimizations = true); + + STerm operator[](const std::string& name); + STerm operator[](const uint32_t& idx) { return this->symbolic_vars[this->real_variable_index[idx]]; }; + inline size_t get_num_real_vars() const { return symbolic_vars.size(); }; + inline size_t get_num_vars() const { return variables.size(); }; + + void init(); + virtual bool simulate_circuit_eval(std::vector& witness) const = 0; + + CircuitBase(const CircuitBase& other) = default; + CircuitBase(CircuitBase&& other) noexcept = default; + CircuitBase& operator=(const CircuitBase& other) = default; + CircuitBase& operator=(CircuitBase&& other) noexcept = default; + virtual ~CircuitBase() = default; +}; + +}; // namespace smt_circuit \ No newline at end of file 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 38fc7faf0f9..709fe8414e0 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp @@ -1,83 +1,145 @@ -#include "circuit.hpp" +#include "standard_circuit.hpp" namespace smt_circuit { /** - * @brief Construct a new Circuit::Circuit object + * @brief Construct a new StandardCircuit object * * @param circuit_info CircuitShema object * @param solver pointer to the global solver * @param tag tag of the circuit. Empty by default. */ -Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, TermType type, const std::string& tag, bool optimizations) - : 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) - , optimizations(optimizations) - , solver(solver) - , type(type) - , tag(tag) +StandardCircuit::StandardCircuit( + 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, + solver, + type, + tag, + optimizations) + , selectors(circuit_info.selectors[0]) + , wires_idxs(circuit_info.wires[0]) { - if (!this->tag.empty()) { - if (this->tag[0] != '_') { - this->tag = "_" + this->tag; - } - } - - for (auto& x : variable_names) { - variable_names_inverse.insert({ x.second, x.first }); - } - - variable_names.insert({ 0, "zero" }); - variable_names.insert({ 1, "one" }); - variable_names_inverse.insert({ "zero", 0 }); + variable_names[1] = "one"; variable_names_inverse.insert({ "one", 1 }); - optimized.insert({ 0, false }); - optimized.insert({ 1, false }); + symbolic_vars[1] = STerm::Var("one" + this->tag, this->solver, this->type); + symbolic_vars[1] == 1; + optimized[1] = false; - this->init(); - - // Perform all relaxation for gates or + // Perform all relaxations 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); } - - for (const auto& i : this->public_inps) { - this->symbolic_vars[this->real_variable_index[i]] == this->variables[i]; - } } /** - * Creates all the needed symbolic variables and constants - * which are used in circuit. + * @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. * */ -void Circuit::init() +size_t StandardCircuit::prepare_gates(size_t cursor) { - size_t num_vars = variables.size(); - symbolic_vars.insert({ 0, STerm::Var("zero" + this->tag, this->solver, this->type) }); - symbolic_vars.insert({ 1, STerm::Var("one" + this->tag, this->solver, this->type) }); + if (this->type == TermType::BVTerm && this->optimizations) { + size_t res = handle_logic_constraint(cursor); + if (res != static_cast(-1)) { + return res; + } + } - 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 ((this->type == TermType::BVTerm || this->type == TermType::FFITerm) && this->optimizations) { + size_t res = handle_range_constraint(cursor); + if (res != static_cast(-1)) { + return res; } + } - std::string name = variable_names.contains(real_idx) ? variable_names[real_idx] : "var_" + std::to_string(i); - name += this->tag; - symbolic_vars.insert({ real_idx, STerm::Var(name, this->solver, this->type) }); + if ((this->type == TermType::BVTerm) && this->optimizations) { + size_t res = handle_ror_constraint(cursor); + if (res != static_cast(-1)) { + return res; + } + } - optimized.insert({ real_idx, true }); + if ((this->type == TermType::BVTerm) && this->optimizations) { + size_t res = handle_shl_constraint(cursor); + if (res != static_cast(-1)) { + return res; + } + } + if ((this->type == TermType::BVTerm) && this->optimizations) { + size_t res = handle_shr_constraint(cursor); + if (res != static_cast(-1)) { + return res; + } } - symbolic_vars[0] == bb::fr(0); - symbolic_vars[1] == bb::fr(1); + 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]; + 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]; + optimized[w_l] = false; + optimized[w_r] = false; + optimized[w_o] = false; + + // Handles the case when we have univariate polynomial as constraint + // by simply finding the roots via quadratic formula(or linear) + // There're 7 possibilities of that, which are present below + bool univariate_flag = false; + 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(STerm(0, this->solver, this->type)) | // STerm(0, this->solver, this->type)) | + Bool(symbolic_vars[w_l]) == + Bool(STerm(1, this->solver, this->type))) // STerm(1, this->solver, this->type))) + .assert_term(); + } else { + this->handle_univariate_constraint(q_m, q_1, q_2, q_3, q_c, w_l); + } + } else { + STerm eq = symbolic_vars[0]; + + // mul selector + if (q_m != 0) { + eq += symbolic_vars[w_l] * symbolic_vars[w_r] * q_m; + } + // left selector + if (q_1 != 0) { + eq += symbolic_vars[w_l] * q_1; + } + // right selector + if (q_2 != 0) { + eq += symbolic_vars[w_r] * q_2; + } + // out selector + if (q_3 != 0) { + eq += symbolic_vars[w_o] * q_3; + } + // constant selector + if (q_c != 0) { + eq += q_c; + } + eq == 0; + } + return cursor + 1; } /** @@ -92,7 +154,8 @@ void Circuit::init() * @param q_c constant * @param w witness index */ -void Circuit::handle_univariate_constraint(bb::fr q_m, bb::fr q_1, bb::fr q_2, bb::fr q_3, bb::fr q_c, uint32_t w) +void StandardCircuit::handle_univariate_constraint( + 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; @@ -133,7 +196,7 @@ void Circuit::handle_univariate_constraint(bb::fr q_m, bb::fr q_1, bb::fr q_2, b * @param cursor current position * @return next position or -1 */ -size_t Circuit::handle_logic_constraint(size_t cursor) +size_t StandardCircuit::handle_logic_constraint(size_t cursor) { // Initialize binary search. Logic gate can only accept even bit lengths // So we need to find a match among [1, 127] and then multiply the result by 2 @@ -148,9 +211,6 @@ size_t Circuit::handle_logic_constraint(size_t cursor) bool and_flag = true; // Indicates the logic operation(true - XOR, false - AND) if the match is found. bool logic_flag = true; - CircuitProps xor_props; - CircuitProps and_props; - bool stop_flag = false; while (beg <= end) { @@ -170,13 +230,13 @@ size_t Circuit::handle_logic_constraint(size_t cursor) this->cached_subcircuits[SubcircuitType::XOR].insert( { mid * 2, get_standard_logic_circuit(mid * 2, true) }); } - xor_props = this->cached_subcircuits[SubcircuitType::XOR][mid * 2]; + CircuitProps xor_props = this->cached_subcircuits[SubcircuitType::XOR][mid * 2]; if (!this->cached_subcircuits[SubcircuitType::AND].contains(mid * 2)) { this->cached_subcircuits[SubcircuitType::AND].insert( { mid * 2, get_standard_logic_circuit(mid * 2, false) }); } - and_props = this->cached_subcircuits[SubcircuitType::AND][mid * 2]; + CircuitProps and_props = this->cached_subcircuits[SubcircuitType::AND][mid * 2]; CircuitSchema xor_circuit = xor_props.circuit; CircuitSchema and_circuit = and_props.circuit; @@ -187,8 +247,8 @@ size_t Circuit::handle_logic_constraint(size_t cursor) for (size_t j = 0; j < xor_props.num_gates; j++) { // It is possible for gates to be equal but wires to be not, but I think it's very // unlikely to happen - xor_flag &= xor_circuit.selectors[j + xor_props.start_gate] == this->selectors[cursor + j]; - and_flag &= and_circuit.selectors[j + and_props.start_gate] == this->selectors[cursor + j]; + xor_flag &= xor_circuit.selectors[0][j + xor_props.start_gate] == this->selectors[cursor + j]; + and_flag &= and_circuit.selectors[0][j + and_props.start_gate] == this->selectors[cursor + j]; if (!xor_flag && !and_flag) { // Won't match at any bit length @@ -216,8 +276,8 @@ size_t Circuit::handle_logic_constraint(size_t cursor) // TODO(alex): Figure out if I need to create range constraint here too or it'll be // created anyway in any circuit if (res != static_cast(-1)) { - xor_props = get_standard_logic_circuit(res, true); - and_props = get_standard_logic_circuit(res, false); + CircuitProps xor_props = get_standard_logic_circuit(res, true); + CircuitProps and_props = get_standard_logic_circuit(res, false); info("Logic constraint optimization: ", std::to_string(res), " bits. is_xor: ", logic_flag); size_t left_gate = xor_props.gate_idxs[0]; @@ -266,14 +326,13 @@ size_t Circuit::handle_logic_constraint(size_t cursor) * @param cursor current position * @return next position or -1 */ -size_t Circuit::handle_range_constraint(size_t cursor) +size_t StandardCircuit::handle_range_constraint(size_t cursor) { // Indicates that current bit length is a match bool range_flag = true; size_t mid = 0; auto res = static_cast(-1); - CircuitProps range_props; // Range constraints differ depending on oddness of bit_length // That's why we need to handle these cases separately for (size_t odd = 0; odd < 2; odd++) { @@ -300,7 +359,7 @@ size_t Circuit::handle_range_constraint(size_t cursor) this->cached_subcircuits[SubcircuitType::RANGE].insert( { 2 * mid + odd, get_standard_range_constraint_circuit(2 * mid + odd) }); } - range_props = this->cached_subcircuits[SubcircuitType::RANGE][2 * mid + odd]; + CircuitProps range_props = this->cached_subcircuits[SubcircuitType::RANGE][2 * mid + odd]; CircuitSchema range_circuit = range_props.circuit; range_flag = cursor + range_props.num_gates <= this->get_num_gates(); @@ -308,7 +367,7 @@ size_t Circuit::handle_range_constraint(size_t cursor) for (size_t j = 0; j < range_props.num_gates; j++) { // It is possible for gates to be equal but wires to be not, but I think it's very // unlikely to happen - range_flag &= range_circuit.selectors[j + range_props.start_gate] == this->selectors[cursor + j]; + range_flag &= range_circuit.selectors[0][j + range_props.start_gate] == this->selectors[cursor + j]; if (!range_flag) { // Won't match at any bit length @@ -339,13 +398,30 @@ size_t Circuit::handle_range_constraint(size_t cursor) if (range_flag) { info("Range constraint optimization: ", std::to_string(res), " bits"); - range_props = get_standard_range_constraint_circuit(res); + CircuitProps range_props = get_standard_range_constraint_circuit(res); size_t left_gate = range_props.gate_idxs[0]; uint32_t left_gate_idx = range_props.idxs[0]; uint32_t left_idx = this->real_variable_index[this->wires_idxs[cursor + left_gate][left_gate_idx]]; STerm left = this->symbolic_vars[left_idx]; + + // preserving shifted values + // we need this because even right shifts do not create + // any additional gates and therefore are undetectible + size_t num_accs = range_props.gate_idxs.size() - 1; + for (size_t j = 1; j < num_accs + 1 && (this->type == TermType::BVTerm); j++) { + size_t acc_gate = range_props.gate_idxs[j]; + uint32_t acc_gate_idx = range_props.idxs[j]; + + uint32_t acc_idx = this->real_variable_index[this->wires_idxs[cursor + acc_gate][acc_gate_idx]]; + + // TODO(alex): Is it better? Can't come up with why not right now + // STerm acc = this->symbolic_vars[acc_idx]; + // acc == (left >> static_cast(2 * j)); + this->symbolic_vars[acc_idx] = (left >> static_cast(2 * j)); + } + left <= (bb::fr(2).pow(res) - 1); // You have to mark these arguments so they won't be optimized out @@ -356,103 +432,328 @@ size_t Circuit::handle_range_constraint(size_t cursor) } /** - * @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. + * @brief Relaxes shr constraints. + * @details This function is needed when we use bitwise compatible + * symbolic terms. + * 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) + * constraint to solver. + * If there's no match, it will return -1 * + * @param cursor current position + * @return next position or -1 */ -size_t Circuit::prepare_gates(size_t cursor) +size_t StandardCircuit::handle_shr_constraint(size_t cursor) { - // TODO(alex): implement bitvector class and compute offsets - if (this->type == TermType::BVTerm && this->optimizations) { - size_t res = handle_logic_constraint(cursor); - if (res != static_cast(-1)) { - return res; + auto res = static_cast(-1); + + // Take a pure shr circuit for the current bit length + // and compare it's selectors to selectors of the global circuit + // at current position(cursor). + // If they are equal, we can apply an optimization + // However, if we have a match at bit length 2, it is possible + // to have a match at higher bit lengths. That's why we store + // the current match as `res` and proceed with ordinary binary search. + // and we can skip this whole section. + // The key is simply two bytes: uint type and sh + + const auto find_nr = [this, &cursor](auto& n, bool& shr_flag) { + // Since shift right for even values of shift is pointless to check + // we iterate only over odd ones + for (uint32_t r = 1; r < static_cast(n); r += 2) { + uint32_t key = static_cast(n) + 256 * r; + if (!this->cached_subcircuits[SubcircuitType::SHR].contains(key)) { + this->cached_subcircuits[SubcircuitType::SHR].insert({ key, get_standard_shift_right_circuit(n, r) }); + } + CircuitProps shr_props = this->cached_subcircuits[SubcircuitType::SHR][key]; + CircuitSchema shr_circuit = shr_props.circuit; + + shr_flag = cursor + shr_props.num_gates <= this->selectors.size(); + if (!shr_flag) { + continue; + } + + for (size_t j = 0; j < shr_props.num_gates; j++) { + // It is possible for gates to be equal but wires to be not, but I think it's very + // unlikely to happen + shr_flag &= shr_circuit.selectors[0][j + shr_props.start_gate] == this->selectors[cursor + j]; + + if (!shr_flag) { + break; + } + } + if (shr_flag) { + return std::pair(n, r); + } } + return std::pair(-1, -1); + }; + + bool shr_flag = false; + std::pair nr; + + if (!shr_flag) { + unsigned char n = 8; + nr = find_nr(n, shr_flag); + } + if (!shr_flag) { + uint16_t n = 16; + nr = find_nr(n, shr_flag); + } + if (!shr_flag) { + uint32_t n = 32; + nr = find_nr(n, shr_flag); + } + if (!shr_flag) { + uint64_t n = 64; + nr = find_nr(n, shr_flag); } - if ((this->type == TermType::BVTerm || this->type == TermType::FFITerm) && this->optimizations) { - size_t res = handle_range_constraint(cursor); - if (res != static_cast(-1)) { - return res; - } + if (shr_flag) { + info("SHR constraint optimization: ", + std::to_string(nr.first), + " bits ,", + std::to_string(nr.second), + " shift right"); + CircuitProps shr_props = this->cached_subcircuits[SubcircuitType::SHR][nr.first + 256 * nr.second]; + + size_t left_gate = shr_props.gate_idxs[0]; + uint32_t left_gate_idx = shr_props.idxs[0]; + uint32_t left_idx = this->real_variable_index[this->wires_idxs[cursor + left_gate][left_gate_idx]]; + + size_t out_gate = shr_props.gate_idxs[1]; + uint32_t out_gate_idx = shr_props.idxs[1]; + uint32_t out_idx = this->real_variable_index[this->wires_idxs[cursor + out_gate][out_gate_idx]]; + + STerm left = this->symbolic_vars[left_idx]; + STerm out = this->symbolic_vars[out_idx]; + + STerm shled = left >> nr.second; + out == shled; + + // You have to mark these arguments so they won't be optimized out + optimized[left_idx] = false; + optimized[out_idx] = false; + return cursor + shr_props.num_gates; } + return res; +} +/** + * @brief Relaxes shl constraints. + * @details This function is needed when we use bitwise compatible + * symbolic terms. + * 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) + * constraint to solver. + * If there's no match, it will return -1 + * + * @param cursor current position + * @return next position or -1 + */ +size_t StandardCircuit::handle_shl_constraint(size_t cursor) +{ + auto res = static_cast(-1); - 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]; + // Take a pure shl circuit for the current bit length + // and compare it's selectors to selectors of the global circuit + // at current position(cursor). + // If they are equal, we can apply an optimization + // However, if we have a match at bit length 2, it is possible + // to have a match at higher bit lengths. That's why we store + // the current match as `res` and proceed with ordinary binary search. + // and we can skip this whole section. + // The key is simply two bytes: uint type and sh + + const auto find_nr = [this, &cursor](auto& n, bool& shl_flag) { + for (uint32_t r = 1; r < static_cast(n); r++) { + uint32_t key = static_cast(n) + 256 * r; + if (!this->cached_subcircuits[SubcircuitType::SHL].contains(key)) { + this->cached_subcircuits[SubcircuitType::SHL].insert({ key, get_standard_shift_left_circuit(n, r) }); + } + CircuitProps shl_props = this->cached_subcircuits[SubcircuitType::SHL][key]; + CircuitSchema shl_circuit = shl_props.circuit; - 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]; - optimized[w_l] = false; - optimized[w_r] = false; - optimized[w_o] = false; + shl_flag = cursor + shl_props.num_gates <= this->selectors.size(); + if (!shl_flag) { + continue; + } - // Handles the case when we have univariate polynomial as constraint - // by simply finding the roots via quadratic formula(or linear) - // There're 7 possibilities of that, which are present below - bool univariate_flag = false; - 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); + for (size_t j = 0; j < shl_props.num_gates; j++) { + // It is possible for gates to be equal but wires to be not, but I think it's very + // unlikely to happen + shl_flag &= shl_circuit.selectors[0][j + shl_props.start_gate] == this->selectors[cursor + j]; - // 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->handle_univariate_constraint(q_m, q_1, q_2, q_3, q_c, w_l); + if (!shl_flag) { + break; + } + } + if (shl_flag) { + return std::pair(n, r); + } } - } else { - STerm eq = symbolic_vars[0]; + return std::pair(-1, -1); + }; - // mul selector - if (q_m != 0) { - eq += symbolic_vars[w_l] * symbolic_vars[w_r] * q_m; - } - // left selector - if (q_1 != 0) { - eq += symbolic_vars[w_l] * q_1; - } - // right selector - if (q_2 != 0) { - eq += symbolic_vars[w_r] * q_2; - } - // out selector - if (q_3 != 0) { - eq += symbolic_vars[w_o] * q_3; - } - // constant selector - if (q_c != 0) { - eq += q_c; - } - eq == symbolic_vars[0]; + bool shl_flag = false; + std::pair nr; + + if (!shl_flag) { + unsigned char n = 8; + nr = find_nr(n, shl_flag); } - return cursor + 1; + if (!shl_flag) { + uint16_t n = 16; + nr = find_nr(n, shl_flag); + } + if (!shl_flag) { + uint32_t n = 32; + nr = find_nr(n, shl_flag); + } + if (!shl_flag) { + uint64_t n = 64; + nr = find_nr(n, shl_flag); + } + + if (shl_flag) { + info("SHL constraint optimization: ", + std::to_string(nr.first), + " bits ,", + std::to_string(nr.second), + " shift left"); + CircuitProps shl_props = this->cached_subcircuits[SubcircuitType::SHL][nr.first + 256 * nr.second]; + + size_t left_gate = shl_props.gate_idxs[0]; + uint32_t left_gate_idx = shl_props.idxs[0]; + uint32_t left_idx = this->real_variable_index[this->wires_idxs[cursor + left_gate][left_gate_idx]]; + + size_t out_gate = shl_props.gate_idxs[1]; + uint32_t out_gate_idx = shl_props.idxs[1]; + uint32_t out_idx = this->real_variable_index[this->wires_idxs[cursor + out_gate][out_gate_idx]]; + + STerm left = this->symbolic_vars[left_idx]; + STerm out = this->symbolic_vars[out_idx]; + + STerm shled = (left << nr.second) & (bb::fr(2).pow(nr.first) - 1); + out == shled; + + // You have to mark these arguments so they won't be optimized out + optimized[left_idx] = false; + optimized[out_idx] = false; + return cursor + shl_props.num_gates; + } + return res; } /** - * @brief Returns a previously named symbolic variable. + * @brief Relaxes ror constraints. + * @details This function is needed when we use bitwise compatible + * symbolic terms. + * It compares the chunk of selectors of the current circuit + * with pure ror 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) + * constraint to solver. + * If there's no match, it will return -1 * - * @param name - * @return STerm + * @param cursor current position + * @return next position or -1 */ -STerm Circuit::operator[](const std::string& name) +size_t StandardCircuit::handle_ror_constraint(size_t cursor) { - 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"); + auto res = static_cast(-1); + + // Take a pure ror circuit for the current bit length + // and compare it's selectors to selectors of the global circuit + // at current position(cursor). + // If they are equal, we can apply an optimization + // However, if we have a match at bit length 2, it is possible + // to have a match at higher bit lengths. That's why we store + // the current match as `res` and proceed with ordinary binary search. + // and we can skip this whole section. + // The key is simply two bytes: uint type and sh + + const auto find_nr = [this, &cursor](auto& n, bool& ror_flag) { + for (uint32_t r = 1; r < static_cast(n); r++) { + uint32_t key = static_cast(n) + 256 * r; + if (!this->cached_subcircuits[SubcircuitType::ROR].contains(key)) { + this->cached_subcircuits[SubcircuitType::ROR].insert({ key, get_standard_ror_circuit(n, r) }); + } + CircuitProps ror_props = this->cached_subcircuits[SubcircuitType::ROR][key]; + CircuitSchema ror_circuit = ror_props.circuit; + + ror_flag = cursor + ror_props.num_gates <= this->selectors.size(); + if (!ror_flag) { + continue; + } + + for (size_t j = 0; j < ror_props.num_gates; j++) { + // It is possible for gates to be equal but wires to be not, but I think it's very + // unlikely to happen + ror_flag &= ror_circuit.selectors[0][j + ror_props.start_gate] == this->selectors[cursor + j]; + + if (!ror_flag) { + break; + } + } + if (ror_flag) { + return std::pair(n, r); + } + } + return std::pair(-1, -1); + }; + + bool ror_flag = false; + std::pair nr; + + if (!ror_flag) { + unsigned char n = 8; + nr = find_nr(n, ror_flag); + } + if (!ror_flag) { + uint16_t n = 16; + nr = find_nr(n, ror_flag); } - uint32_t idx = this->variable_names_inverse[name]; - return this->symbolic_vars[idx]; + if (!ror_flag) { + uint32_t n = 32; + nr = find_nr(n, ror_flag); + } + if (!ror_flag) { + uint64_t n = 64; + nr = find_nr(n, ror_flag); + } + + if (ror_flag) { + info("ROR constraint optimization: ", + std::to_string(nr.first), + " bits ,", + std::to_string(nr.second), + " rotation right"); + CircuitProps ror_props = this->cached_subcircuits[SubcircuitType::ROR][nr.first + 256 * nr.second]; + + size_t left_gate = ror_props.gate_idxs[0]; + uint32_t left_gate_idx = ror_props.idxs[0]; + uint32_t left_idx = this->real_variable_index[this->wires_idxs[cursor + left_gate][left_gate_idx]]; + + size_t out_gate = ror_props.gate_idxs[1]; + uint32_t out_gate_idx = ror_props.idxs[1]; + uint32_t out_idx = this->real_variable_index[this->wires_idxs[cursor + out_gate][out_gate_idx]]; + + STerm left = this->symbolic_vars[left_idx]; + STerm out = this->symbolic_vars[out_idx]; + + STerm rored = ((left >> nr.second) | (left << (nr.first - nr.second))) & (bb::fr(2).pow(nr.first) - 1); + out == rored; + + // You have to mark these arguments so they won't be optimized out + optimized[left_idx] = false; + optimized[out_idx] = false; + return cursor + ror_props.num_gates; + } + return res; } /** @@ -463,7 +764,7 @@ STerm Circuit::operator[](const std::string& name) * @return true * @return false */ -bool Circuit::simulate_circuit_eval(std::vector& witness) const +bool StandardCircuit::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 " + @@ -501,17 +802,19 @@ bool Circuit::simulate_circuit_eval(std::vector& witness) const * @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 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) +std::pair StandardCircuit::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, + bool optimizations) { // TODO(alex): set optimizations to be true once they are confirmed - Circuit c1(circuit_info, s, type, "circuit1", false); - Circuit c2(circuit_info, s, type, "circuit2", false); + StandardCircuit c1(circuit_info, s, type, "circuit1", optimizations); + StandardCircuit c2(circuit_info, s, type, "circuit2", optimizations); for (const auto& term : equal) { c1[term] == c2[term]; @@ -559,14 +862,12 @@ std::pair unique_witness_ext(CircuitSchema& circuit_info, * @param equal The list of names of variables which should be equal in both circuits(each is equal) * @return std::pair */ -std::pair unique_witness(CircuitSchema& circuit_info, - Solver* s, - TermType type, - const std::vector& equal) +std::pair StandardCircuit::unique_witness( + CircuitSchema& circuit_info, Solver* s, TermType type, const std::vector& equal, bool optimizations) { // TODO(alex): set optimizations to be true once they are confirmed - Circuit c1(circuit_info, s, type, "circuit1", false); - Circuit c2(circuit_info, s, type, "circuit2", false); + StandardCircuit c1(circuit_info, s, type, "circuit1", optimizations); + StandardCircuit c2(circuit_info, s, type, "circuit2", optimizations); for (const auto& term : equal) { c1[term] == c2[term]; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.hpp index 0c956acd83d..03d0a4393f1 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.hpp @@ -1,86 +1,51 @@ #pragma once -#include -#include -#include -#include - -#include "barretenberg/smt_verification/terms/bool.hpp" -#include "barretenberg/smt_verification/terms/term.hpp" - -#include "subcircuits.hpp" +#include "circuit_base.hpp" namespace smt_circuit { -using namespace smt_solver; -using namespace smt_terms; -using namespace smt_circuit_schema; -using namespace smt_subcircuits; - -enum class SubcircuitType { XOR, AND, RANGE }; /** - * @brief Symbolic Circuit class. + * @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 Circuit { - private: - void init(); - size_t prepare_gates(size_t cursor); - - void handle_univariate_constraint(bb::fr q_m, bb::fr q_1, bb::fr q_2, bb::fr q_3, bb::fr q_c, uint32_t w); - size_t handle_logic_constraint(size_t cursor); - size_t handle_range_constraint(size_t cursor); - +class StandardCircuit : public CircuitBase { public: - 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 - 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 - std::unordered_map> - cached_subcircuits; // caches subcircuits during optimization - // No need to recompute them each time - - Solver* solver; // pointer to the solver - TermType type; // Type of the underlying Symbolic Terms + std::vector> selectors; // selectors from the circuit + std::vector> wires_idxs; // values of the gates' wires - std::string tag; // tag of the symbolic circuit. - // If not empty, will be added to the names - // of symbolic variables to prevent collisions. + explicit StandardCircuit(CircuitSchema& circuit_info, + Solver* solver, + TermType type = TermType::FFTerm, + const std::string& tag = "", + bool optimizations = true); - explicit Circuit(CircuitSchema& circuit_info, - Solver* solver, - TermType type = TermType::FFTerm, - const std::string& tag = "", - bool optimizations = true); - - STerm operator[](const std::string& name); - STerm operator[](const uint32_t& idx) { return this->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; -}; -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 = {}); - -std::pair unique_witness(CircuitSchema& circuit_info, - Solver* s, - TermType type, - const std::vector& equal = {}); + size_t prepare_gates(size_t cursor); + bool simulate_circuit_eval(std::vector& witness) const override; -}; // namespace smt_circuit + void handle_univariate_constraint(bb::fr q_m, bb::fr q_1, bb::fr q_2, bb::fr q_3, bb::fr q_c, uint32_t w); + size_t handle_logic_constraint(size_t cursor); + size_t handle_range_constraint(size_t cursor); + size_t handle_ror_constraint(size_t cursor); + size_t handle_shr_constraint(size_t cursor); + size_t handle_shl_constraint(size_t cursor); + + 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 = {}, + bool optimizations = false); + + static std::pair unique_witness(CircuitSchema& circuit_info, + Solver* s, + TermType type, + const std::vector& equal = {}, + bool optimizations = false); +}; +}; // namespace smt_circuit \ No newline at end of file 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.hpp index ff4815fc633..4c885ba6cd3 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.hpp @@ -6,7 +6,7 @@ #include "barretenberg/stdlib/primitives/uint/uint.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" #include @@ -23,7 +23,7 @@ using witness_t = stdlib::witness_t; using pub_witness_t = stdlib::public_witness_t; using uint_ct = stdlib::uint32; -TEST(circuit, assert_equal) +TEST(standard_circuit, assert_equal) { StandardCircuitBuilder builder = StandardCircuitBuilder(); @@ -52,7 +52,7 @@ TEST(circuit, assert_equal) auto buf = builder.export_circuit(); 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); ASSERT_EQ(circuit[k.get_witness_index()].term, circuit["c"].term); ASSERT_EQ(circuit[d.get_witness_index()].term, circuit["a"].term); @@ -62,7 +62,7 @@ TEST(circuit, assert_equal) ASSERT_EQ(circuit[i.get_witness_index()].term, circuit[j.get_witness_index()].term); } -TEST(circuit, cached_subcircuits) +TEST(standard_circuit, cached_subcircuits) { StandardCircuitBuilder builder = StandardCircuitBuilder(); field_t a(witness_t(&builder, fr::zero())); @@ -75,11 +75,11 @@ TEST(circuit, cached_subcircuits) auto buf = builder.export_circuit(); CircuitSchema circuit_info = unpack_from_buffer(buf); Solver s(circuit_info.modulus); - Circuit circuit(circuit_info, &s, TermType::FFITerm); + StandardCircuit circuit(circuit_info, &s, TermType::FFITerm); s.print_assertions(); } -TEST(circuit, range_relaxation_assertions) +TEST(standard_circuit, range_relaxation_assertions) { StandardCircuitBuilder builder = StandardCircuitBuilder(); field_t a(witness_t(&builder, fr(120))); @@ -94,13 +94,13 @@ TEST(circuit, range_relaxation_assertions) auto buf = builder.export_circuit(); CircuitSchema circuit_info = unpack_from_buffer(buf); - Solver s(circuit_info.modulus); - Circuit circuit(circuit_info, &s, TermType::FFITerm); + Solver s(circuit_info.modulus, default_solver_config, 16, 32); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); s.print_assertions(); } -TEST(circuit, range_relaxation) +TEST(standard_circuit, range_relaxation) { for (size_t i = 2; i < 256; i++) { StandardCircuitBuilder builder = StandardCircuitBuilder(); @@ -110,11 +110,11 @@ TEST(circuit, range_relaxation) auto buf = builder.export_circuit(); CircuitSchema circuit_info = unpack_from_buffer(buf); Solver s(circuit_info.modulus); - Circuit circuit(circuit_info, &s, TermType::FFITerm); + StandardCircuit circuit(circuit_info, &s, TermType::FFITerm); } } -TEST(circuit, xor_relaxation_assertions) +TEST(standard_circuit, xor_relaxation_assertions) { StandardCircuitBuilder builder = StandardCircuitBuilder(); uint_ct a(witness_t(&builder, static_cast(fr(120)))); @@ -127,12 +127,27 @@ TEST(circuit, xor_relaxation_assertions) auto buf = builder.export_circuit(); CircuitSchema circuit_info = unpack_from_buffer(buf); Solver s(circuit_info.modulus, default_solver_config, 16, 32); - Circuit circuit(circuit_info, &s, TermType::BVTerm); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); s.print_assertions(); } -TEST(circuit, and_relaxation_assertions) +TEST(standard_circuit, xor_relaxation) +{ + for (size_t i = 2; i < 256; i += 2) { + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint32_t a_idx = builder.add_variable(0); + uint32_t b_idx = builder.add_variable(0); + builder.create_logic_constraint(a_idx, b_idx, i, true); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 32); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } +} + +TEST(standard_circuit, and_relaxation_assertions) { StandardCircuitBuilder builder = StandardCircuitBuilder(); uint_ct a(witness_t(&builder, static_cast(fr(120)))); @@ -145,7 +160,199 @@ TEST(circuit, and_relaxation_assertions) auto buf = builder.export_circuit(); CircuitSchema circuit_info = unpack_from_buffer(buf); Solver s(circuit_info.modulus, default_solver_config, 16, 32); - Circuit circuit(circuit_info, &s, TermType::BVTerm); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + s.print_assertions(); +} + +TEST(standard_circuit, ror_relaxation_assertions) +{ + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, static_cast(fr(120)))); + uint_ct b = a.ror(17); + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 32); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + s.print_assertions(); +} + +TEST(standard_circuit, ror_relaxation) +{ + for (size_t i = 1; i < 8; i++) { + using uint_ct = stdlib::uint8; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a.ror(i); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 16; i++) { + using uint_ct = stdlib::uint16; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a.ror(i); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 32; i++) { + using uint_ct = stdlib::uint32; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a.ror(i); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 64; i++) { + using uint_ct = stdlib::uint64; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a.ror(i); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } +} + +TEST(standard_circuit, shl_relaxation_assertions) +{ + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, static_cast(fr(120)))); + uint_ct b = a << 17; + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 32); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); s.print_assertions(); -} \ No newline at end of file +} + +TEST(standard_circuit, shl_relaxation) +{ + for (size_t i = 1; i < 8; i++) { + using uint_ct = stdlib::uint8; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a << i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 16; i++) { + using uint_ct = stdlib::uint16; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a << i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 32; i++) { + using uint_ct = stdlib::uint32; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a << i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 64; i++) { + using uint_ct = stdlib::uint64; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a << i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } +} + +TEST(standard_circuit, shr_relaxation_assertions) +{ + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, static_cast(fr(120)))); + uint_ct b = a >> 17; + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 32); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + s.print_assertions(); +} + +TEST(standard_circuit, shr_relaxation) +{ + for (size_t i = 1; i < 8; i += 2) { + using uint_ct = stdlib::uint8; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a >> i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 16; i += 2) { + using uint_ct = stdlib::uint16; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a >> i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 32; i += 2) { + using uint_ct = stdlib::uint32; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a >> i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } + for (size_t i = 1; i < 64; i += 2) { + using uint_ct = stdlib::uint64; + StandardCircuitBuilder builder = StandardCircuitBuilder(); + uint_ct a(witness_t(&builder, 0)); + uint_ct b = a >> i; + + auto buf = builder.export_circuit(); + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + } +} diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp index 792f2d2d8bb..ddbd0cb06db 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp @@ -5,22 +5,37 @@ namespace smt_subcircuits { CircuitProps get_standard_range_constraint_circuit(size_t n) { bb::StandardCircuitBuilder builder = bb::StandardCircuitBuilder(); - uint32_t a_idx = builder.add_variable(bb::fr(0)); + uint32_t a_idx = builder.add_variable(bb::fr(0xabbba)); builder.set_variable_name(a_idx, "a"); size_t start_gate = builder.get_num_gates(); - builder.decompose_into_base4_accumulators(a_idx, n); + auto accumulators = builder.decompose_into_base4_accumulators(a_idx, n); size_t num_gates = builder.get_num_gates() - start_gate; + // give names to accumulators for tests + size_t num_accs = accumulators.size(); + for (size_t i = 0; i < num_accs - 1; i++) { + builder.set_variable_name(accumulators[i], "acc_" + std::to_string(i)); + } + CircuitSchema exported = unpack_from_buffer(builder.export_circuit()); - // relative offstes in the circuit are calculated manually, according to decompose_into_base4_accumulators method + // relative offsets in the circuit are calculated manually, according to decompose_into_base4_accumulators method // lhs position in the gate uint32_t lhs_position = 2; // number of the gate that contains lhs size_t gate_number = num_gates - 1; - return { exported, start_gate, num_gates, { lhs_position }, { gate_number } }; + std::vector idxs = { lhs_position }; + std::vector gate_idxs = { gate_number }; + + // same thing for accumulators + for (size_t i = 0; i < num_accs - 1; i++) { + idxs.push_back(0); + gate_idxs.push_back(gate_number - 4 * i); + } + + return { exported, start_gate, num_gates, idxs, gate_idxs }; } CircuitProps get_standard_logic_circuit(size_t n, bool is_xor) @@ -39,7 +54,7 @@ CircuitProps get_standard_logic_circuit(size_t n, bool is_xor) CircuitSchema exported = unpack_from_buffer(builder.export_circuit()); - // relative offstes in the circuit are calculated manually, according to create_logic_constraint method + // relative offsets in the circuit are calculated manually, according to create_logic_constraint method // lhs, rhs and out positions in the corresponding gates uint32_t lhs_position = 2; uint32_t rhs_position = 2; @@ -55,4 +70,4 @@ CircuitProps get_standard_logic_circuit(size_t n, bool is_xor) { lhs_position, rhs_position, out_position }, { lhs_gate_number, rhs_gate_number, out_gate_number } }; } -} // namespace smt_subcircuits \ No newline at end of file +} // namespace smt_subcircuits diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp index bd2e9896aec..e4fcfa845c9 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.hpp @@ -1,4 +1,5 @@ #pragma once +#include "barretenberg/stdlib/primitives/uint/uint.hpp" #include "barretenberg/stdlib_circuit_builders/standard_circuit_builder.hpp" #include "barretenberg/smt_verification/circuit/circuit_schema.hpp" @@ -25,4 +26,81 @@ struct CircuitProps { CircuitProps get_standard_range_constraint_circuit(size_t n); CircuitProps get_standard_logic_circuit(size_t n, bool is_xor); + +template CircuitProps get_standard_ror_circuit(T n, size_t sh) +{ + using witness_ct = bb::stdlib::witness_t; + bb::StandardCircuitBuilder builder = bb::StandardCircuitBuilder(); + bb::stdlib::uint a = witness_ct(&builder, n); + + size_t start_gate = builder.get_num_gates(); + auto b = a.ror(sh); + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + + size_t num_gates = builder.get_num_gates() - start_gate; + CircuitSchema exported = unpack_from_buffer(builder.export_circuit()); + + // relative offsets in the circuit are calculated manually, according to decompose_into_base4_accumulators method + // lhs, rhs positions in the gate + uint32_t a_position = (sh & 1) == 1 ? 1 : 0; + uint32_t b_position = (sh & 1) == 1 ? 0 : 2; + // number of the gate that contains lhs, rhs + size_t a_gate_number = (sh & 1) == 1 ? num_gates - 2 : num_gates - 1; + size_t b_gate_number = (sh & 1) == 1 ? num_gates - 2 : num_gates - 1; + + return { exported, start_gate, num_gates, { a_position, b_position }, { a_gate_number, b_gate_number } }; +} + +template CircuitProps get_standard_shift_right_circuit(T n, uint32_t sh) +{ + // sh have to be even, otherwise the resulting circuit will be empty + if ((sh & 1) == 0) { + throw std::invalid_argument("sh value should be odd"); + } + using witness_ct = bb::stdlib::witness_t; + bb::StandardCircuitBuilder builder = bb::StandardCircuitBuilder(); + bb::stdlib::uint a = witness_ct(&builder, n); + size_t start_gate = builder.get_num_gates(); + auto b = a >> sh; + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + + size_t num_gates = builder.get_num_gates() - start_gate; + CircuitSchema exported = unpack_from_buffer(builder.export_circuit()); + + // relative offsets in the circuit are calculated manually, according to decompose_into_base4_accumulators method + // lhs, rhs positions in the gate + uint32_t acc_position = 0; + uint32_t b_position = 1; + // number of the gate that contains lhs, rhs + size_t acc_gate_number = num_gates - 1; + size_t b_gate_number = num_gates - 2; + + return { exported, start_gate, num_gates, { acc_position, b_position }, { acc_gate_number, b_gate_number } }; +} + +template CircuitProps get_standard_shift_left_circuit(T n, uint32_t sh) +{ + using witness_ct = bb::stdlib::witness_t; + bb::StandardCircuitBuilder builder = bb::StandardCircuitBuilder(); + bb::stdlib::uint a = witness_ct(&builder, n); + size_t start_gate = builder.get_num_gates(); + auto b = a << sh; + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + + size_t num_gates = builder.get_num_gates() - start_gate; + CircuitSchema exported = unpack_from_buffer(builder.export_circuit()); + + // relative offsets in the circuit are calculated manually, according to decompose_into_base4_accumulators method + // lhs, rhs positions in the gate + uint32_t a_position = (sh & 1) == 1 ? 1 : 0; + uint32_t b_position = (sh & 1) == 1 ? 0 : 2; + // number of the gate that contains lhs, rhs + size_t a_gate_number = (sh & 1) == 1 ? num_gates - 2 : num_gates - 1; + size_t b_gate_number = (sh & 1) == 1 ? num_gates - 2 : num_gates - 1; + + return { exported, start_gate, num_gates, { a_position, b_position }, { a_gate_number, b_gate_number } }; +} } // namespace smt_subcircuits diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.test.cpp index 650c9cdda4c..4b27fbbfc08 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.test.cpp @@ -18,7 +18,7 @@ auto& engine = numeric::get_debug_randomness(); // I.e. I can find an operand at the index, given by get_standard_range_constraint_circuit TEST(subcircuits, range_circuit) { - for (size_t i = 1; i < 256; i++) { + for (size_t i = 1; i < 255; i++) { smt_subcircuits::CircuitProps range_props = smt_subcircuits::get_standard_range_constraint_circuit(i); smt_circuit_schema::CircuitSchema circuit = range_props.circuit; @@ -27,7 +27,17 @@ TEST(subcircuits, range_circuit) size_t start_gate = range_props.start_gate; ASSERT_EQ( - "a", circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[start_gate + a_gate][a_gate_idx]]]); + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t num_accs = range_props.gate_idxs.size() - 1; + for (size_t j = 1; j < num_accs + 1; j++) { + size_t acc_gate = range_props.gate_idxs[j]; + uint32_t acc_gate_idx = range_props.idxs[j]; + ASSERT_EQ("acc_" + std::to_string(num_accs - j), + circuit.vars_of_interest + [circuit.real_variable_index[circuit.wires[0][start_gate + acc_gate][acc_gate_idx]]]); + } } } // Check that all the relative offsets are calculated correctly. @@ -42,16 +52,232 @@ TEST(subcircuits, logic_circuit) uint32_t a_gate_idx = logic_props.idxs[0]; size_t start_gate = logic_props.start_gate; ASSERT_EQ( - "a", circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[start_gate + a_gate][a_gate_idx]]]); + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); size_t b_gate = logic_props.gate_idxs[1]; uint32_t b_gate_idx = logic_props.idxs[1]; ASSERT_EQ( - "b", circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[start_gate + b_gate][b_gate_idx]]]); + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); size_t c_gate = logic_props.gate_idxs[2]; uint32_t c_gate_idx = logic_props.idxs[2]; ASSERT_EQ( - "c", circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[start_gate + c_gate][c_gate_idx]]]); + "c", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + c_gate][c_gate_idx]]]); + } +} + +// Check that all the relative offsets are calculated correctly. +// I.e. I can find all three operands at the indices, given by get_standard_logic_circuit +TEST(subcircuits, ror_circuit) +{ + for (uint32_t r = 1; r < 8; r += 1) { + unsigned char n = 8; + smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = ror_props.circuit; + + size_t a_gate = ror_props.gate_idxs[0]; + uint32_t a_gate_idx = ror_props.idxs[0]; + size_t start_gate = ror_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = ror_props.gate_idxs[1]; + uint32_t b_gate_idx = ror_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); } -} \ No newline at end of file + for (uint32_t r = 1; r < 16; r += 1) { + uint16_t n = 16; + smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = ror_props.circuit; + + size_t a_gate = ror_props.gate_idxs[0]; + uint32_t a_gate_idx = ror_props.idxs[0]; + size_t start_gate = ror_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = ror_props.gate_idxs[1]; + uint32_t b_gate_idx = ror_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 32; r += 1) { + uint32_t n = 16; + smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = ror_props.circuit; + + size_t a_gate = ror_props.gate_idxs[0]; + uint32_t a_gate_idx = ror_props.idxs[0]; + size_t start_gate = ror_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = ror_props.gate_idxs[1]; + uint32_t b_gate_idx = ror_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 64; r += 1) { + uint64_t n = 16; + smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = ror_props.circuit; + + size_t a_gate = ror_props.gate_idxs[0]; + uint32_t a_gate_idx = ror_props.idxs[0]; + size_t start_gate = ror_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = ror_props.gate_idxs[1]; + uint32_t b_gate_idx = ror_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } +} + +// Check that all the relative offsets are calculated correctly. +// I.e. I can find all three operands at the indices, given by get_standard_logic_circuit +TEST(subcircuits, shl_circuit) +{ + for (uint32_t r = 1; r < 8; r += 1) { + unsigned char n = 8; + smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit; + + size_t a_gate = shift_left_props.gate_idxs[0]; + uint32_t a_gate_idx = shift_left_props.idxs[0]; + size_t start_gate = shift_left_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = shift_left_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_left_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 16; r += 1) { + uint16_t n = 16; + smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit; + + size_t a_gate = shift_left_props.gate_idxs[0]; + uint32_t a_gate_idx = shift_left_props.idxs[0]; + size_t start_gate = shift_left_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = shift_left_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_left_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 32; r += 1) { + uint32_t n = 16; + smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit; + + size_t a_gate = shift_left_props.gate_idxs[0]; + uint32_t a_gate_idx = shift_left_props.idxs[0]; + size_t start_gate = shift_left_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = shift_left_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_left_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 64; r += 1) { + uint64_t n = 16; + smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit; + + size_t a_gate = shift_left_props.gate_idxs[0]; + uint32_t a_gate_idx = shift_left_props.idxs[0]; + size_t start_gate = shift_left_props.start_gate; + ASSERT_EQ( + "a", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + a_gate][a_gate_idx]]]); + + size_t b_gate = shift_left_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_left_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } +} + +// Check that all the relative offsets are calculated correctly. +// I.e. I can find all three operands at the indices, given by get_standard_logic_circuit +// I can't check the position of the lhs here, since shr doesn't use the witness directly but +// it's accumulators. +// However, according to standard_circuit test they seem fine. +TEST(subcircuits, shr_circuit) +{ + for (uint32_t r = 1; r < 8; r += 2) { + unsigned char n = 8; + smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit; + + size_t start_gate = shift_right_props.start_gate; + size_t b_gate = shift_right_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_right_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 16; r += 2) { + uint16_t n = 16; + smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit; + + size_t start_gate = shift_right_props.start_gate; + size_t b_gate = shift_right_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_right_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 32; r += 2) { + uint32_t n = 16; + smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit; + + size_t start_gate = shift_right_props.start_gate; + size_t b_gate = shift_right_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_right_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } + for (uint32_t r = 1; r < 64; r += 2) { + uint64_t n = 16; + smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r); + smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit; + + size_t start_gate = shift_right_props.start_gate; + size_t b_gate = shift_right_props.gate_idxs[1]; + uint32_t b_gate_idx = shift_right_props.idxs[1]; + ASSERT_EQ( + "b", + circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate + b_gate][b_gate_idx]]]); + } +} 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 f4a5355533f..ccca774985b 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp @@ -7,7 +7,7 @@ #include "barretenberg/stdlib/primitives/field/field.hpp" -#include "barretenberg/smt_verification/circuit/circuit.hpp" +#include "barretenberg/smt_verification/circuit/standard_circuit.hpp" using namespace bb; @@ -185,4 +185,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 +}