From 6cb7fb24e03233850a8cb1ab6b39724bb7be76fd Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 5 Dec 2024 19:49:47 +0000 Subject: [PATCH 1/8] Added post processing functionality to symbolic circuit --- .../smt_verification/circuit/circuit_base.hpp | 6 +++ .../smt_verification/util/smt_util.cpp | 50 ++++++++++++++----- .../smt_verification/util/smt_util.hpp | 18 +++---- 3 files changed, 52 insertions(+), 22 deletions(-) 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 e39d46a88e07..815843336565 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp @@ -41,6 +41,12 @@ class CircuitBase { std::unordered_map> cached_subcircuits; // caches subcircuits during optimization // No need to recompute them each time + std::unordered_map> + post_process; // Values idxs that should be post processed after the solver returns a witness. + // Basically it affects only optimized out variables. + // Because in BitVector case we can't collect negative values since they will not be + // the same in the field. That's why we store the expression and calculate it after the witness is + // obtained. Solver* solver; // pointer to the solver TermType type; // Type of the underlying Symbolic Terms diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp index 2a2ec75c54bf..fee89b1ae20d 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp @@ -51,11 +51,11 @@ bb::fr string_to_fr(const std::string& number, int base, size_t step) * @param fname file to store the resulting witness if succeded * @param pack flags out to pack the resulting witness using msgpack */ -void default_model(const std::vector& special, - smt_circuit::CircuitBase& c1, - smt_circuit::CircuitBase& c2, - const std::string& fname, - bool pack) +std::vector> default_model(const std::vector& special, + smt_circuit::CircuitBase& c1, + smt_circuit::CircuitBase& c2, + const std::string& fname, + bool pack) { std::vector vterms1; std::vector vterms2; @@ -91,13 +91,24 @@ void default_model(const std::vector& special, info(RED, new_line, RESET); } myfile << new_line << std::endl; - ; - packed_witness.push_back({ string_to_fr(mmap1[vname1], base), string_to_fr(mmap2[vname2], base) }); } myfile << "};"; myfile.close(); + for (const auto& post : c1.post_process) { + uint32_t res_idx = post.first; + auto left_idx = static_cast(post.second[0]); + auto right_idx = static_cast(post.second[1]); + bb::fr q_m = post.second[2]; + bb::fr q_l = post.second[3]; + bb::fr q_r = post.second[4]; + bb::fr q_c = post.second[5]; + packed_witness[res_idx][0] = q_m * packed_witness[left_idx][0] * packed_witness[right_idx][0] + + q_l * packed_witness[left_idx][0] + q_r * packed_witness[right_idx][0] + q_c; + packed_witness[res_idx][1] = q_m * packed_witness[left_idx][1] * packed_witness[right_idx][1] + + q_l * packed_witness[left_idx][1] + q_r * packed_witness[right_idx][1] + q_c; + } if (pack) { msgpack::sbuffer buffer; msgpack::pack(buffer, packed_witness); @@ -119,6 +130,7 @@ void default_model(const std::vector& special, for (const auto& vname : special) { info(vname, "_1, ", vname, "_2 = ", mmap[vname + "_1"], ", ", mmap[vname + "_2"]); } + return packed_witness; } /** @@ -135,10 +147,10 @@ void default_model(const std::vector& special, * @param fname file to store the resulting witness if succeded * @param pack flags out to pack the resulting witness using msgpack */ -void default_model_single(const std::vector& special, - smt_circuit::CircuitBase& c, - const std::string& fname, - bool pack) +std::vector default_model_single(const std::vector& special, + smt_circuit::CircuitBase& c, + const std::string& fname, + bool pack) { std::vector vterms; vterms.reserve(c.get_num_vars()); @@ -157,7 +169,7 @@ void default_model_single(const std::vector& special, packed_witness.reserve(c.get_num_vars()); int base = c.type == smt_terms::TermType::BVTerm ? 2 : 10; - for (size_t i = 0; i < c.get_num_vars(); i++) { + for (uint32_t i = 0; i < c.get_num_vars(); i++) { std::string vname = vterms[i].toString(); std::string new_line = mmap[vname] + ", // " + vname; if (c.real_variable_index[i] != i) { @@ -169,6 +181,17 @@ void default_model_single(const std::vector& special, myfile << "};"; myfile.close(); + for (const auto& post : c.post_process) { + uint32_t res_idx = post.first; + auto left_idx = static_cast(post.second[0]); + auto right_idx = static_cast(post.second[1]); + bb::fr q_m = post.second[2]; + bb::fr q_l = post.second[3]; + bb::fr q_r = post.second[4]; + bb::fr q_c = post.second[5]; + packed_witness[res_idx] = q_m * packed_witness[left_idx] * packed_witness[right_idx] + + q_l * packed_witness[left_idx] + q_r * packed_witness[right_idx] + q_c; + } if (pack) { msgpack::sbuffer buffer; msgpack::pack(buffer, packed_witness); @@ -189,6 +212,7 @@ void default_model_single(const std::vector& special, for (const auto& vname : special) { info(vname, " = ", mmap1[vname]); } + return packed_witness; } /** @@ -311,4 +335,4 @@ void fix_range_lists(bb::UltraCircuitBuilder& builder) } builder.variables[list.second.variable_indices[num_multiples_of_three + 1]] = list.first; } -} \ No newline at end of file +} diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp index dcf084180286..5241960f5bff 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp @@ -6,15 +6,15 @@ #define RED "\033[31m" #define RESET "\033[0m" -void default_model(const std::vector& special, - smt_circuit::CircuitBase& c1, - smt_circuit::CircuitBase& c2, - const std::string& fname = "witness.out", - bool pack = true); -void default_model_single(const std::vector& special, - smt_circuit::CircuitBase& c, - const std::string& fname = "witness.out", - bool pack = true); +std::vector> default_model(const std::vector& special, + smt_circuit::CircuitBase& c1, + smt_circuit::CircuitBase& c2, + const std::string& fname = "witness.out", + bool pack = true); +std::vector default_model_single(const std::vector& special, + smt_circuit::CircuitBase& c, + const std::string& fname = "witness.out", + bool pack = true); bool smt_timer(smt_solver::Solver* s); std::pair, std::vector> base4(uint32_t el); From 3910c9ec1da08ba05a6e0789afd697c349b0a54d Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 5 Dec 2024 19:54:21 +0000 Subject: [PATCH 2/8] Added finalized flag to schema --- .../barretenberg/smt_verification/circuit/circuit_schema.hpp | 1 + .../stdlib_circuit_builders/circuit_builder_base.hpp | 1 + .../stdlib_circuit_builders/standard_circuit_builder.cpp | 1 + .../stdlib_circuit_builders/ultra_circuit_builder.cpp | 2 ++ 4 files changed, 5 insertions(+) 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 cc3b37e8e418..099e60c1c732 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp @@ -33,6 +33,7 @@ struct CircuitSchema { std::vector>> lookup_tables; std::vector real_variable_tags; std::unordered_map range_tags; + bool circuit_finalized; MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, 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 28b2c9ad8f67..b2eedbd74e56 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 @@ -251,6 +251,7 @@ template struct CircuitSchemaInternal { std::vector>> lookup_tables; std::vector real_variable_tags; std::unordered_map range_tags; + bool circuit_finalized; MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, 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 09e74567e40d..03effb888410 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 @@ -565,6 +565,7 @@ template msgpack::sbuffer StandardCircuitBuilder_::export_circ cir.wires.push_back(arith_wires); cir.real_variable_index = this->real_variable_index; + cir.circuit_finalized = true; msgpack::sbuffer buffer; msgpack::pack(buffer, cir); 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 29bf01cc42cf..b49b3a7ad7c8 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 @@ -2956,6 +2956,8 @@ template msgpack::sbuffer UltraCircuitBuilder_circuit_finalized; + msgpack::sbuffer buffer; msgpack::pack(buffer, cir); return buffer; From 855a907b84397c4b0aecf1161cb1ed7b66478431 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 5 Dec 2024 20:08:40 +0000 Subject: [PATCH 3/8] Use post processing to calculate final witness for standard standard circuits --- .../circuit/standard_circuit.cpp | 200 +++++++++++++++--- .../circuit/standard_circuit.test.cpp | 131 ++++++++++++ 2 files changed, 302 insertions(+), 29 deletions(-) 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 5b47ba23afbc..d06f5feb6d4b 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp @@ -103,32 +103,32 @@ size_t StandardCircuit::prepare_gates(size_t cursor) // 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(this->symbolic_vars[w_l]) == Bool(STerm(0, this->solver, this->type)) | // STerm(0, this->solver, this->type)) | - Bool(symbolic_vars[w_l]) == + Bool(this->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]; + STerm eq = this->symbolic_vars[this->variable_names_inverse["zero"]]; // mul selector if (q_m != 0) { - eq += symbolic_vars[w_l] * symbolic_vars[w_r] * q_m; + eq += this->symbolic_vars[w_l] * this->symbolic_vars[w_r] * q_m; } // left selector if (q_1 != 0) { - eq += symbolic_vars[w_l] * q_1; + eq += this->symbolic_vars[w_l] * q_1; } // right selector if (q_2 != 0) { - eq += symbolic_vars[w_r] * q_2; + eq += this->symbolic_vars[w_r] * q_2; } // out selector if (q_3 != 0) { - eq += symbolic_vars[w_o] * q_3; + eq += this->symbolic_vars[w_o] * q_3; } // constant selector if (q_c != 0) { @@ -157,7 +157,7 @@ void StandardCircuit::handle_univariate_constraint( bb::fr b = q_1 + q_2 + q_3; if (q_m == 0) { - symbolic_vars[w] == -q_c / b; + this->symbolic_vars[w] == -q_c / b; return; } @@ -169,10 +169,10 @@ void StandardCircuit::handle_univariate_constraint( bb::fr x2 = (-b - d.second) / (bb::fr(2) * q_m); if (d.second == 0) { - symbolic_vars[w] == STerm(x1, this->solver, type); + this->symbolic_vars[w] == STerm(x1, this->solver, type); } else { - ((Bool(symbolic_vars[w]) == Bool(STerm(x1, this->solver, this->type))) | - (Bool(symbolic_vars[w]) == Bool(STerm(x2, this->solver, this->type)))) + ((Bool(this->symbolic_vars[w]) == Bool(STerm(x1, this->solver, this->type))) | + (Bool(this->symbolic_vars[w]) == Bool(STerm(x2, this->solver, this->type)))) .assert_term(); } } @@ -285,8 +285,6 @@ size_t StandardCircuit::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)) { CircuitProps xor_props = get_standard_logic_circuit(res, true); CircuitProps and_props = get_standard_logic_circuit(res, false); @@ -307,6 +305,45 @@ size_t StandardCircuit::handle_logic_constraint(size_t cursor) STerm right = this->symbolic_vars[right_idx]; STerm out = this->symbolic_vars[out_idx]; + // Simulate the logic constraint circuit using the bitwise operations + size_t num_bits = res; + size_t processed_gates = 0; + for (size_t i = num_bits - 1; i < num_bits; i -= 2) { + // 8 here is the number of gates we have to skip to get proper indices + processed_gates += 8; + uint32_t left_quad_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + uint32_t left_lo_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][1]]; + uint32_t left_hi_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + processed_gates += 1; + uint32_t right_quad_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + uint32_t right_lo_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][1]]; + uint32_t right_hi_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + processed_gates += 1; + uint32_t out_quad_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + uint32_t out_lo_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][1]]; + uint32_t out_hi_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + processed_gates += 1; + uint32_t old_left_acc_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + processed_gates += 1; + uint32_t old_right_acc_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + processed_gates += 1; + uint32_t old_out_acc_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + processed_gates += 1; + + this->symbolic_vars[old_left_acc_idx] == (left >> static_cast(i - 1)); + this->symbolic_vars[left_quad_idx] == (this->symbolic_vars[old_left_acc_idx] & 3); + this->symbolic_vars[left_lo_idx] == (this->symbolic_vars[left_quad_idx] & 1); + this->symbolic_vars[left_hi_idx] == (this->symbolic_vars[left_quad_idx] >> 1); + this->symbolic_vars[old_right_acc_idx] == (right >> static_cast(i - 1)); + this->symbolic_vars[right_quad_idx] == (this->symbolic_vars[old_right_acc_idx] & 3); + this->symbolic_vars[right_lo_idx] == (this->symbolic_vars[right_quad_idx] & 1); + this->symbolic_vars[right_hi_idx] == (this->symbolic_vars[right_quad_idx] >> 1); + this->symbolic_vars[old_out_acc_idx] == (out >> static_cast(i - 1)); + this->symbolic_vars[out_quad_idx] == (this->symbolic_vars[old_out_acc_idx] & 3); + this->symbolic_vars[out_lo_idx] == (this->symbolic_vars[out_quad_idx] & 1); + this->symbolic_vars[out_hi_idx] == (this->symbolic_vars[out_quad_idx] >> 1); + } + if (logic_flag) { (left ^ right) == out; } else { @@ -422,19 +459,41 @@ size_t StandardCircuit::handle_range_constraint(size_t cursor) // we need this because even right shifts do not create // any additional gates and therefore are undetectible - // TODO(alex): I think I should simulate the whole subcircuit at that point - // Otherwise optimized out variables are not correct in the final witness - // And I can't fix them by hand each time - 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]; + // Simulate the range constraint circuit using the bitwise operations + size_t num_bits = res; + size_t num_quads = num_bits >> 1; + num_quads += num_bits & 1; + uint32_t processed_gates = 0; + + for (size_t i = num_quads - 1; i < num_quads; i--) { + uint32_t lo_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + processed_gates += 1; + uint32_t quad_idx = 0; + uint32_t old_accumulator_idx = 0; + uint32_t hi_idx = 0; + + if (i == num_quads - 1 && ((num_bits & 1) == 1)) { + quad_idx = lo_idx; + } else { + hi_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + processed_gates += 1; + quad_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + processed_gates += 1; + } - uint32_t acc_idx = this->real_variable_index[this->wires_idxs[cursor + acc_gate][acc_gate_idx]]; + if (i == num_quads - 1) { + old_accumulator_idx = quad_idx; + } else { + old_accumulator_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + processed_gates += 1; + } - this->symbolic_vars[acc_idx] == (left >> static_cast(2 * j)); - // I think the following is worse. The name of the variable is lost after that - // this->symbolic_vars[acc_idx] = (left >> static_cast(2 * j)); + this->symbolic_vars[old_accumulator_idx] == (left >> static_cast(2 * i)); + this->symbolic_vars[quad_idx] == (this->symbolic_vars[old_accumulator_idx] & 3); + this->symbolic_vars[lo_idx] == (this->symbolic_vars[quad_idx] & 1); + if (i != (num_quads - 1) || ((num_bits)&1) != 1) { + this->symbolic_vars[hi_idx] == (this->symbolic_vars[quad_idx] >> 1); + } } left <= (bb::fr(2).pow(res) - 1); @@ -545,8 +604,35 @@ size_t StandardCircuit::handle_shr_constraint(size_t cursor) STerm left = this->symbolic_vars[left_idx]; STerm out = this->symbolic_vars[out_idx]; - STerm shled = left >> nr.second; - out == shled; + // Simulate the shr circuit using bitwise ops + uint32_t shift = nr.second; + if ((shift & 1) == 1) { + size_t processed_gates = 0; + uint32_t c_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + uint32_t delta_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[delta_idx] == (this->symbolic_vars[c_idx] & 3); + STerm delta = this->symbolic_vars[delta_idx]; + processed_gates += 1; + uint32_t r0_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + + // this->symbolic_vars[r0_idx] == (-2 * delta * delta + 9 * delta - 7); + this->post_process.insert({ r0_idx, { delta_idx, delta_idx, -2, 9, 0, -7 } }); + + processed_gates += 1; + uint32_t r1_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[r1_idx] == (delta >> 1) * 6; + processed_gates += 1; + uint32_t r2_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[r2_idx] == (left >> shift) * 6; + processed_gates += 1; + uint32_t temp_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + + // this->symbolic_vars[temp_idx] == -6 * out; + this->post_process.insert({ temp_idx, { out_idx, out_idx, 0, -6, 0, 0 } }); + } + + STerm shred = left >> nr.second; + out == shred; // You have to mark these arguments so they won't be optimized out optimized[left_idx] = false; @@ -652,7 +738,35 @@ size_t StandardCircuit::handle_shl_constraint(size_t cursor) 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); + // Simulate the shr circuit using bitwise ops + uint32_t num_bits = nr.first; + uint32_t shift = nr.second; + if ((shift & 1) == 1) { + size_t processed_gates = 0; + uint32_t c_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + uint32_t delta_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[delta_idx] == (this->symbolic_vars[c_idx] & 3); + STerm delta = this->symbolic_vars[delta_idx]; + processed_gates += 1; + uint32_t r0_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + + // this->symbolic_vars[r0_idx] == (-2 * delta * delta + 9 * delta - 7); + this->post_process.insert({ r0_idx, { delta_idx, delta_idx, -2, 9, 0, -7 } }); + + processed_gates += 1; + uint32_t r1_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[r1_idx] == (delta >> 1) * 6; + processed_gates += 1; + uint32_t r2_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[r2_idx] == (left >> (num_bits - shift)) * 6; + processed_gates += 1; + uint32_t temp_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + + // this->symbolic_vraiables[temp_idx] == -6 * r2 + this->post_process.insert({ temp_idx, { r2_idx, r2_idx, 0, -1, 0, 0 } }); + } + + STerm shled = (left << shift) & (bb::fr(2).pow(num_bits) - 1); out == shled; // You have to mark these arguments so they won't be optimized out @@ -760,7 +874,35 @@ size_t StandardCircuit::handle_ror_constraint(size_t cursor) 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); + // Simulate the ror circuit using bitwise ops + uint32_t num_bits = nr.first; + uint32_t rotation = nr.second; + if ((rotation & 1) == 1) { + size_t processed_gates = 0; + uint32_t c_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; + uint32_t delta_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[delta_idx] == (this->symbolic_vars[c_idx] & 3); + STerm delta = this->symbolic_vars[delta_idx]; + processed_gates += 1; + uint32_t r0_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + + // this->symbolic_vars[r0_idx] == (-2 * delta * delta + 9 * delta - 7); + this->post_process.insert({ r0_idx, { delta_idx, delta_idx, -2, 9, 0, -7 } }); + + processed_gates += 1; + uint32_t r1_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[r1_idx] == (delta >> 1) * 6; + processed_gates += 1; + uint32_t r2_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + this->symbolic_vars[r2_idx] == (left >> rotation) * 6; + processed_gates += 1; + uint32_t temp_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][2]]; + + // this->symbolic_vraiables[temp_idx] == -6 * r2 + this->post_process.insert({ temp_idx, { r2_idx, r2_idx, 0, -1, 0, 0 } }); + } + + STerm rored = ((left >> rotation) | (left << (num_bits - rotation))) & (bb::fr(2).pow(num_bits) - 1); out == rored; // You have to mark these arguments so they won't be optimized out @@ -909,4 +1051,4 @@ std::pair StandardCircuit::unique_witness(Circ } return { c1, c2 }; } -}; // namespace smt_circuit +}; // namespace smt_circuit \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp index ffded6864dde..030cd97b60dc 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp @@ -376,3 +376,134 @@ TEST(standard_circuit, check_double_xor_bug) Solver s(circuit_info.modulus, default_solver_config, 16, 64); StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); } + +TEST(standard_circuit, optimized_range_witness) +{ + uint32_t rbit = static_cast(bb::fr::random_element()) & 1; + uint32_t num_bits = 32 + rbit; + info(num_bits); + + StandardCircuitBuilder builder; + field_t a = witness_t(&builder, static_cast(bb::fr::random_element()) % (uint256_t(1) << num_bits)); + builder.create_range_constraint(a.get_witness_index(), num_bits); + builder.set_variable_name(a.get_witness_index(), "a"); + + CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + circuit["a"] == a.get_value(); + + bool res = smt_timer(&s); + ASSERT_TRUE(res); + auto model_witness = default_model_single({ "a" }, circuit, "optimized_range_check.out"); + + ASSERT_EQ(model_witness.size(), builder.get_num_variables()); + for (size_t i = 0; i < model_witness.size(); i++) { + ASSERT_EQ(model_witness[i], builder.variables[i]); + } +} + +TEST(standard_circuit, optimized_logic_witness) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + builder.set_variable_name(a.get_witness_index(), "a"); + uint_ct b = witness_t(&builder, static_cast(bb::fr::random_element())); + builder.set_variable_name(b.get_witness_index(), "b"); + uint_ct c = a ^ b; + uint_ct d = a & b; + builder.set_variable_name(c.get_witness_index(), "c"); + builder.set_variable_name(d.get_witness_index(), "d"); + + CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + circuit["a"] == a.get_value(); + circuit["b"] == b.get_value(); + + bool res = smt_timer(&s); + ASSERT_TRUE(res); + auto model_witness = default_model_single({ "a", "b", "c", "d" }, circuit, "optimized_xor_check.out"); + + ASSERT_EQ(model_witness.size(), builder.get_num_variables()); + for (size_t i = 0; i < model_witness.size(); i++) { + ASSERT_EQ(model_witness[i], builder.variables[i]); + } +} + +TEST(standard_circuit, optimized_shr_witness) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + builder.set_variable_name(a.get_witness_index(), "a"); + uint_ct b = a >> 0; + for (uint32_t i = 1; i < 32; i++) { + b = a >> i; + } + + CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + circuit["a"] == a.get_value(); + bool res = smt_timer(&s); + ASSERT_TRUE(res); + auto model_witness = default_model_single({ "a" }, circuit, "optimized_xor_check.out"); + + ASSERT_EQ(model_witness.size(), builder.get_num_variables()); + for (size_t i = 0; i < model_witness.size(); i++) { + EXPECT_EQ(model_witness[i], builder.variables[i]); + } +} + +TEST(standard_circuit, optimized_shl_witness) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + builder.set_variable_name(a.get_witness_index(), "a"); + uint_ct b = a << 0; + for (uint32_t i = 1; i < 32; i++) { + b = a << i; + } + + CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + circuit[a.get_witness_index()] == a.get_value(); + bool res = smt_timer(&s); + ASSERT_TRUE(res); + auto model_witness = default_model_single({ "a" }, circuit, "optimized_xor_check.out"); + + ASSERT_EQ(model_witness.size(), builder.get_num_variables()); + for (size_t i = 0; i < model_witness.size(); i++) { + EXPECT_EQ(model_witness[i], builder.variables[i]); + } +} + +TEST(standard_circuit, optimized_ror_witness) +{ + StandardCircuitBuilder builder; + uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + builder.set_variable_name(a.get_witness_index(), "a"); + uint_ct b = a.ror(0); + for (uint32_t i = 1; i < 32; i++) { + b = a.ror(i); + } + + CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit()); + Solver s(circuit_info.modulus, default_solver_config, 16, 64); + StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); + + circuit[a.get_witness_index()] == a.get_value(); + bool res = smt_timer(&s); + ASSERT_TRUE(res); + auto model_witness = default_model_single({ "a" }, circuit, "optimized_xor_check.out"); + + ASSERT_EQ(model_witness.size(), builder.get_num_variables()); + for (size_t i = 0; i < model_witness.size(); i++) { + EXPECT_EQ(model_witness[i], builder.variables[i]); + } +} \ No newline at end of file From c6ab952f39f8936a3368e852916bdccaec7a3d2a Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Sat, 7 Dec 2024 07:46:49 +0000 Subject: [PATCH 4/8] Adding comments + switching to get_random_uint32 --- .../circuit/standard_circuit.test.cpp | 14 +++++++------- .../smt_verification/util/smt_util.cpp | 8 ++++++++ 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp index 030cd97b60dc..61df28970fbc 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp @@ -379,12 +379,12 @@ TEST(standard_circuit, check_double_xor_bug) TEST(standard_circuit, optimized_range_witness) { - uint32_t rbit = static_cast(bb::fr::random_element()) & 1; + uint32_t rbit = engine.get_random_uint8() & 1; uint32_t num_bits = 32 + rbit; info(num_bits); StandardCircuitBuilder builder; - field_t a = witness_t(&builder, static_cast(bb::fr::random_element()) % (uint256_t(1) << num_bits)); + field_t a = witness_t(&builder, engine.get_random_uint256() % (uint256_t(1) << num_bits)); builder.create_range_constraint(a.get_witness_index(), num_bits); builder.set_variable_name(a.get_witness_index(), "a"); @@ -407,9 +407,9 @@ TEST(standard_circuit, optimized_range_witness) TEST(standard_circuit, optimized_logic_witness) { StandardCircuitBuilder builder; - uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + uint_ct a = witness_t(&builder, engine.get_random_uint32()); builder.set_variable_name(a.get_witness_index(), "a"); - uint_ct b = witness_t(&builder, static_cast(bb::fr::random_element())); + uint_ct b = witness_t(&builder, engine.get_random_uint32()); builder.set_variable_name(b.get_witness_index(), "b"); uint_ct c = a ^ b; uint_ct d = a & b; @@ -436,7 +436,7 @@ TEST(standard_circuit, optimized_logic_witness) TEST(standard_circuit, optimized_shr_witness) { StandardCircuitBuilder builder; - uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + uint_ct a = witness_t(&builder, engine.get_random_uint32()); builder.set_variable_name(a.get_witness_index(), "a"); uint_ct b = a >> 0; for (uint32_t i = 1; i < 32; i++) { @@ -461,7 +461,7 @@ TEST(standard_circuit, optimized_shr_witness) TEST(standard_circuit, optimized_shl_witness) { StandardCircuitBuilder builder; - uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + uint_ct a = witness_t(&builder, engine.get_random_uint32()); builder.set_variable_name(a.get_witness_index(), "a"); uint_ct b = a << 0; for (uint32_t i = 1; i < 32; i++) { @@ -486,7 +486,7 @@ TEST(standard_circuit, optimized_shl_witness) TEST(standard_circuit, optimized_ror_witness) { StandardCircuitBuilder builder; - uint_ct a = witness_t(&builder, static_cast(bb::fr::random_element())); + uint_ct a = witness_t(&builder, engine.get_random_uint32()); builder.set_variable_name(a.get_witness_index(), "a"); uint_ct b = a.ror(0); for (uint32_t i = 1; i < 32; i++) { diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp index fee89b1ae20d..cb4bcb2b5e16 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp @@ -96,6 +96,10 @@ std::vector> default_model(const std::vector& s myfile << "};"; myfile.close(); + // Accessing post processing functionality of the symbolic circuit + // Once we obtained the witness, compatible with current configuration(e.g. BVTerm) + // We can further compute the remaining witness entries, which were optimized and hence + // are not provided by the solver for (const auto& post : c1.post_process) { uint32_t res_idx = post.first; auto left_idx = static_cast(post.second[0]); @@ -181,6 +185,10 @@ std::vector default_model_single(const std::vector& special myfile << "};"; myfile.close(); + // Accessing post processing functionality of the symbolic circuit + // Once we obtained the witness, compatible with current configuration(e.g. BVTerm) + // We can further compute the remaining witness entries, which were optimized and hence + // are not provided by the solver for (const auto& post : c.post_process) { uint32_t res_idx = post.first; auto left_idx = static_cast(post.second[0]); From d59ead6c92b9f4f0e207e970dbec8f1da3f8cfba Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Sat, 7 Dec 2024 07:47:36 +0000 Subject: [PATCH 5/8] switching to engine --- .../smt_verification/terms/bvterm.test.cpp | 36 +++++++++---------- .../smt_verification/terms/iterm.test.cpp | 16 ++++----- 2 files changed, 26 insertions(+), 26 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp index 05d942cdcad7..bb7de54a063e 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp @@ -18,8 +18,8 @@ using namespace smt_terms; TEST(BVTerm, addition) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); + uint_ct b = witness_ct(&builder, engine.get_random_uint32()); uint_ct c = a + b; uint32_t modulus_base = 16; @@ -47,8 +47,8 @@ TEST(BVTerm, addition) TEST(BVTerm, subtraction) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); + uint_ct b = witness_ct(&builder, engine.get_random_uint32()); uint_ct c = a - b; uint32_t modulus_base = 16; @@ -76,8 +76,8 @@ TEST(BVTerm, subtraction) TEST(BVTerm, xor) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); + uint_ct b = witness_ct(&builder, engine.get_random_uint32()); uint_ct c = a ^ b; uint32_t modulus_base = 16; @@ -105,7 +105,7 @@ TEST(BVTerm, xor) TEST(BVTerm, rotr) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); uint_ct b = a.ror(10); uint32_t modulus_base = 16; @@ -131,7 +131,7 @@ TEST(BVTerm, rotr) TEST(BVTerm, rotl) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); uint_ct b = a.rol(10); uint32_t modulus_base = 16; @@ -158,8 +158,8 @@ TEST(BVTerm, rotl) TEST(BVTerm, mul) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); + uint_ct b = witness_ct(&builder, engine.get_random_uint32()); uint_ct c = a * b; uint32_t modulus_base = 16; @@ -187,8 +187,8 @@ TEST(BVTerm, mul) TEST(BVTerm, and) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); + uint_ct b = witness_ct(&builder, engine.get_random_uint32()); uint_ct c = a & b; uint32_t modulus_base = 16; @@ -216,8 +216,8 @@ TEST(BVTerm, and) TEST(BVTerm, or) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); + uint_ct b = witness_ct(&builder, engine.get_random_uint32()); uint_ct c = a | b; uint32_t modulus_base = 16; @@ -245,8 +245,8 @@ TEST(BVTerm, or) TEST(BVTerm, div) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); + uint_ct b = witness_ct(&builder, engine.get_random_uint32()); uint_ct c = a / b; uint32_t modulus_base = 16; @@ -274,7 +274,7 @@ TEST(BVTerm, div) TEST(BVTerm, shr) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); uint_ct b = a >> 5; uint32_t modulus_base = 16; @@ -300,7 +300,7 @@ TEST(BVTerm, shr) TEST(BVTerm, shl) { StandardCircuitBuilder builder; - uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct a = witness_ct(&builder, engine.get_random_uint32()); uint_ct b = a << 5; uint32_t modulus_base = 16; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp index d86081a24bc0..24710d7b9389 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp @@ -17,8 +17,8 @@ using namespace smt_terms; TEST(ITerm, addition) { StandardCircuitBuilder builder; - uint64_t a = static_cast(fr::random_element()) % (static_cast(1) << 31); - uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t a = engine.get_random_uint32() % (static_cast(1) << 31); + uint64_t b = engine.get_random_uint32() % (static_cast(1) << 31); uint64_t c = a + b; Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); @@ -41,8 +41,8 @@ TEST(ITerm, addition) TEST(ITerm, subtraction) { StandardCircuitBuilder builder; - uint64_t c = static_cast(fr::random_element()) % (static_cast(1) << 31); - uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t c = engine.get_random_uint32() % (static_cast(1) << 31); + uint64_t b = engine.get_random_uint32() % (static_cast(1) << 31); uint64_t a = c + b; Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); @@ -65,8 +65,8 @@ TEST(ITerm, subtraction) TEST(ITerm, mul) { StandardCircuitBuilder builder; - uint64_t a = static_cast(fr::random_element()) % (static_cast(1) << 31); - uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t a = engine.get_random_uint32() % (static_cast(1) << 31); + uint64_t b = engine.get_random_uint32() % (static_cast(1) << 31); uint64_t c = a * b; Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); @@ -89,8 +89,8 @@ TEST(ITerm, mul) TEST(ITerm, div) { StandardCircuitBuilder builder; - uint64_t a = static_cast(fr::random_element()) % (static_cast(1) << 31); - uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31) + 1; + uint64_t a = engine.get_random_uint32() % (static_cast(1) << 31); + uint64_t b = engine.get_random_uint32() % (static_cast(1) << 31) + 1; uint64_t c = a / b; Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); From ab5fd16fc283ee06adb2b9abfa7905bb08169983 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Sat, 7 Dec 2024 08:03:10 +0000 Subject: [PATCH 6/8] Adding a description for circuit simulation --- .../smt_verification/circuit/standard_circuit.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) 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 d06f5feb6d4b..fd36bc243f07 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp @@ -465,6 +465,9 @@ size_t StandardCircuit::handle_range_constraint(size_t cursor) num_quads += num_bits & 1; uint32_t processed_gates = 0; + // Initializing the parts of the witness that were optimized + // during the symbolic constraints initialization + // i.e. simulating the decompose_into_base4_accumulators gate by gate using BitVectors/Integers for (size_t i = num_quads - 1; i < num_quads; i--) { uint32_t lo_idx = this->real_variable_index[this->wires_idxs[cursor + processed_gates][0]]; processed_gates += 1; @@ -604,7 +607,9 @@ size_t StandardCircuit::handle_shr_constraint(size_t cursor) STerm left = this->symbolic_vars[left_idx]; STerm out = this->symbolic_vars[out_idx]; - // Simulate the shr circuit using bitwise ops + // Initializing the parts of the witness that were optimized + // during the symbolic constraints initialization + // i.e. simulating the uint's operator>> gate by gate using BitVectors/Integers uint32_t shift = nr.second; if ((shift & 1) == 1) { size_t processed_gates = 0; @@ -738,7 +743,9 @@ size_t StandardCircuit::handle_shl_constraint(size_t cursor) STerm left = this->symbolic_vars[left_idx]; STerm out = this->symbolic_vars[out_idx]; - // Simulate the shr circuit using bitwise ops + // Initializing the parts of the witness that were optimized + // during the symbolic constraints initialization + // i.e. simulating the uint's operator<< gate by gate using BitVectors/Integers uint32_t num_bits = nr.first; uint32_t shift = nr.second; if ((shift & 1) == 1) { @@ -874,7 +881,9 @@ size_t StandardCircuit::handle_ror_constraint(size_t cursor) STerm left = this->symbolic_vars[left_idx]; STerm out = this->symbolic_vars[out_idx]; - // Simulate the ror circuit using bitwise ops + // Initializing the parts of the witness that were optimized + // during the symbolic constraints initialization + // i.e. simulating the uint's rotate_right gate by gate using BitVectors/Integers uint32_t num_bits = nr.first; uint32_t rotation = nr.second; if ((rotation & 1) == 1) { From 82fe2bf122e1ffc58230c95d1dc4a103d70431ea Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Sat, 7 Dec 2024 08:03:35 +0000 Subject: [PATCH 7/8] Adding comments to the tests --- .../smt_verification/circuit/standard_circuit.test.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp index 61df28970fbc..3d9917d89979 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp @@ -377,6 +377,8 @@ TEST(standard_circuit, check_double_xor_bug) StandardCircuit circuit(circuit_info, &s, TermType::BVTerm); } +// Check that witness provided by the solver is the same as builder's witness +// Check that all the optimized out values are initialized and computed properly during post proccessing TEST(standard_circuit, optimized_range_witness) { uint32_t rbit = engine.get_random_uint8() & 1; @@ -404,6 +406,8 @@ TEST(standard_circuit, optimized_range_witness) } } +// Check that witness provided by the solver is the same as builder's witness +// Check that all the optimized out values are initialized and computed properly during post proccessing TEST(standard_circuit, optimized_logic_witness) { StandardCircuitBuilder builder; @@ -433,6 +437,8 @@ TEST(standard_circuit, optimized_logic_witness) } } +// Check that witness provided by the solver is the same as builder's witness +// Check that all the optimized out values are initialized and computed properly during post proccessing TEST(standard_circuit, optimized_shr_witness) { StandardCircuitBuilder builder; @@ -458,6 +464,8 @@ TEST(standard_circuit, optimized_shr_witness) } } +// Check that witness provided by the solver is the same as builder's witness +// Check that all the optimized out values are initialized and computed properly during post proccessing TEST(standard_circuit, optimized_shl_witness) { StandardCircuitBuilder builder; @@ -483,6 +491,8 @@ TEST(standard_circuit, optimized_shl_witness) } } +// Check that witness provided by the solver is the same as builder's witness +// Check that all the optimized out values are initialized and computed properly during post proccessing TEST(standard_circuit, optimized_ror_witness) { StandardCircuitBuilder builder; From c474fb7062e96194399e57a636be2d2fb82bbc7a Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Sat, 7 Dec 2024 08:07:44 +0000 Subject: [PATCH 8/8] adding one extra comment --- .../smt_verification/circuit/standard_circuit.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 fd36bc243f07..bd49b18b82a1 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp @@ -305,7 +305,9 @@ size_t StandardCircuit::handle_logic_constraint(size_t cursor) STerm right = this->symbolic_vars[right_idx]; STerm out = this->symbolic_vars[out_idx]; - // Simulate the logic constraint circuit using the bitwise operations + // Initializing the parts of the witness that were optimized + // during the symbolic constraints initialization + // i.e. simulating the create_logic_constraint gate by gate using BitVectors/Integers size_t num_bits = res; size_t processed_gates = 0; for (size_t i = num_bits - 1; i < num_bits; i -= 2) {