diff --git a/barretenberg/cpp/src/barretenberg/circuit_checker/mega_circuit_builder.test.cpp b/barretenberg/cpp/src/barretenberg/circuit_checker/mega_circuit_builder.test.cpp index 3a97736afa4c..686652cb9543 100644 --- a/barretenberg/cpp/src/barretenberg/circuit_checker/mega_circuit_builder.test.cpp +++ b/barretenberg/cpp/src/barretenberg/circuit_checker/mega_circuit_builder.test.cpp @@ -13,21 +13,20 @@ namespace bb { TEST(MegaCircuitBuilder, CopyConstructor) { - MegaCircuitBuilder circuit_constructor = MegaCircuitBuilder(); + MegaCircuitBuilder builder = MegaCircuitBuilder(); fr a = fr::one(); - circuit_constructor.add_public_variable(a); + builder.add_public_variable(a); for (size_t i = 0; i < 16; ++i) { for (size_t j = 0; j < 16; ++j) { uint64_t left = static_cast(j); uint64_t right = static_cast(i); - uint32_t left_idx = circuit_constructor.add_variable(fr(left)); - uint32_t right_idx = circuit_constructor.add_variable(fr(right)); - uint32_t result_idx = circuit_constructor.add_variable(fr(left ^ right)); + uint32_t left_idx = builder.add_variable(fr(left)); + uint32_t right_idx = builder.add_variable(fr(right)); + uint32_t result_idx = builder.add_variable(fr(left ^ right)); - uint32_t add_idx = - circuit_constructor.add_variable(fr(left) + fr(right) + circuit_constructor.get_variable(result_idx)); - circuit_constructor.create_big_add_gate( + uint32_t add_idx = builder.add_variable(fr(left) + fr(right) + builder.get_variable(result_idx)); + builder.create_big_add_gate( { left_idx, right_idx, result_idx, add_idx, fr(1), fr(1), fr(1), fr(-1), fr(0) }); } } @@ -38,25 +37,25 @@ TEST(MegaCircuitBuilder, CopyConstructor) auto z = fr::random_element(); // Add gates corresponding to the above operations - circuit_constructor.queue_ecc_add_accum(P1); - circuit_constructor.queue_ecc_mul_accum(P2, z); - circuit_constructor.queue_ecc_eq(); + builder.queue_ecc_add_accum(P1); + builder.queue_ecc_mul_accum(P2, z); + builder.queue_ecc_eq(); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); - MegaCircuitBuilder duplicate_circuit_constructor{ circuit_constructor }; + MegaCircuitBuilder duplicate_builder{ builder }; - EXPECT_EQ(duplicate_circuit_constructor, circuit_constructor); - EXPECT_TRUE(CircuitChecker::check(duplicate_circuit_constructor)); + EXPECT_EQ(duplicate_builder, builder); + EXPECT_TRUE(CircuitChecker::check(duplicate_builder)); } TEST(MegaCircuitBuilder, BaseCase) { - MegaCircuitBuilder circuit_constructor = MegaCircuitBuilder(); + MegaCircuitBuilder builder = MegaCircuitBuilder(); fr a = fr::one(); - circuit_constructor.add_public_variable(a); - bool result = CircuitChecker::check(circuit_constructor); + builder.add_public_variable(a); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } diff --git a/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.cpp b/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.cpp new file mode 100644 index 000000000000..e6eb5fae36f1 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.cpp @@ -0,0 +1,457 @@ +#include "barretenberg/circuit_checker/translator_circuit_checker.hpp" +#include "barretenberg/translator_vm/translator_circuit_builder.hpp" + +namespace bb { +TranslatorCircuitChecker::RelationInputs TranslatorCircuitChecker::compute_relation_inputs_limbs( + const Fq& batching_challenge_v, const Fq& evaluation_input_x) +{ + Fq v_squared = batching_challenge_v * batching_challenge_v; + Fq v_cubed = v_squared * batching_challenge_v; + Fq v_quarted = v_cubed * batching_challenge_v; + return RelationInputs{ + .x_limbs = Builder::split_fq_into_limbs(evaluation_input_x), + .v_limbs = Builder::split_fq_into_limbs(batching_challenge_v), + .v_squared_limbs = Builder::split_fq_into_limbs(v_squared), + .v_cubed_limbs = Builder::split_fq_into_limbs(v_cubed), + .v_quarted_limbs = Builder::split_fq_into_limbs(v_quarted), + }; +} + +bool TranslatorCircuitChecker::check(const Builder& circuit) +{ + + auto wires = circuit.wires; + // Compute the limbs of evaluation_input_x and powers of batching_challenge_v (these go into the relation) + RelationInputs relation_inputs = + compute_relation_inputs_limbs(circuit.batching_challenge_v, circuit.evaluation_input_x); + // Get the main wires (we will operate with range constraint wires mainly through indices, since this is + // easier) + auto& op_wire = std::get(circuit.wires); + auto& x_lo_y_hi_wire = std::get(circuit.wires); + auto& x_hi_z_1_wire = std::get(circuit.wires); + auto& y_lo_z_2_wire = std::get(circuit.wires); + auto& p_x_0_p_x_1_wire = std::get(circuit.wires); + auto& p_x_2_p_x_3_wire = std::get(circuit.wires); + auto& p_y_0_p_y_1_wire = std::get(circuit.wires); + auto& p_y_2_p_y_3_wire = std::get(circuit.wires); + auto& z_lo_wire = std::get(circuit.wires); + auto& z_hi_wire = std::get(circuit.wires); + auto& accumulators_binary_limbs_0_wire = std::get(circuit.wires); + auto& accumulators_binary_limbs_1_wire = std::get(circuit.wires); + auto& accumulators_binary_limbs_2_wire = std::get(circuit.wires); + auto& accumulators_binary_limbs_3_wire = std::get(circuit.wires); + auto& quotient_low_binary_limbs = std::get(circuit.wires); + auto& quotient_high_binary_limbs = std::get(circuit.wires); + auto& relation_wide_limbs_wire = std::get(circuit.wires); + auto reconstructed_evaluation_input_x = Fr(uint256_t(circuit.evaluation_input_x)); + auto reconstructed_batching_evaluation_v = Fr(uint256_t(circuit.batching_challenge_v)); + auto reconstructed_batching_evaluation_v2 = Fr(uint256_t(circuit.batching_challenge_v.pow(2))); + auto reconstructed_batching_evaluation_v3 = Fr(uint256_t(circuit.batching_challenge_v.pow(3))); + auto reconstructed_batching_evaluation_v4 = Fr(uint256_t(circuit.batching_challenge_v.pow(4))); + /** + * @brief Get elements at the same index from several sequential circuit.wires and put them into a vector + * + */ + auto get_sequential_micro_chunks = [&](size_t gate_index, WireIds starting_wire_index, size_t chunk_count) { + std::vector chunks; + for (size_t i = starting_wire_index; i < starting_wire_index + chunk_count; i++) { + chunks.push_back(circuit.get_variable(circuit.wires[i][gate_index])); + } + return chunks; + }; + + /** + * @brief Reconstruct the value of one regular limb used in relation computation from micro chunks used to + * create range constraints + * + * @details We might want to skip several items at the end, since those will be shifted or used + * for another decomposition + * + */ + auto accumulate_limb_from_micro_chunks = [](const std::vector& chunks, const int skipped_at_end = 1) { + Fr mini_accumulator(0); + auto end = chunks.end(); + std::advance(end, -skipped_at_end); + for (auto it = end; it != chunks.begin();) { + --it; + mini_accumulator = mini_accumulator * TranslatorCircuitBuilder::MICRO_SHIFT + *it; + } + return mini_accumulator; + }; + /** + * @brief Go through each gate + * + */ + for (size_t i = 1; i < circuit.num_gates - 1; i++) { + bool gate_is_odd = i & 1; + // The main relation is computed between odd and the next even indices. For example, 1 and 2 + if (gate_is_odd) { + // Get the values of P.x + Fr op_code = circuit.get_variable(op_wire[i]); + Fr p_x_lo = circuit.get_variable(x_lo_y_hi_wire[i]); + Fr p_x_hi = circuit.get_variable(x_hi_z_1_wire[i]); + Fr p_x_0 = circuit.get_variable(p_x_0_p_x_1_wire[i]); + Fr p_x_1 = circuit.get_variable(p_x_0_p_x_1_wire[i + 1]); + Fr p_x_2 = circuit.get_variable(p_x_2_p_x_3_wire[i]); + Fr p_x_3 = circuit.get_variable(p_x_2_p_x_3_wire[i + 1]); + const std::vector p_x_binary_limbs = { p_x_0, p_x_1, p_x_2, p_x_3 }; + + // P.y + Fr p_y_lo = circuit.get_variable(y_lo_z_2_wire[i]); + Fr p_y_hi = circuit.get_variable(x_lo_y_hi_wire[i + 1]); + Fr p_y_0 = circuit.get_variable(p_y_0_p_y_1_wire[i]); + Fr p_y_1 = circuit.get_variable(p_y_0_p_y_1_wire[i + 1]); + Fr p_y_2 = circuit.get_variable(p_y_2_p_y_3_wire[i]); + Fr p_y_3 = circuit.get_variable(p_y_2_p_y_3_wire[i + 1]); + const std::vector p_y_binary_limbs = { p_y_0, p_y_1, p_y_2, p_y_3 }; + // z1, z2 + Fr z_1 = circuit.get_variable(x_hi_z_1_wire[i + 1]); + Fr z_2 = circuit.get_variable(y_lo_z_2_wire[i + 1]); + + Fr z_1_lo = circuit.get_variable(z_lo_wire[i]); + Fr z_2_lo = circuit.get_variable(z_lo_wire[i + 1]); + Fr z_1_hi = circuit.get_variable(z_hi_wire[i]); + Fr z_2_hi = circuit.get_variable(z_hi_wire[i + 1]); + + const std::vector z_1_binary_limbs = { z_1_lo, z_1_hi }; + const std::vector z_2_binary_limbs = { z_2_lo, z_2_hi }; + // Relation limbs + Fr low_wide_relation_limb = circuit.get_variable(relation_wide_limbs_wire[i]); + Fr high_wide_relation_limb = circuit.get_variable(relation_wide_limbs_wire[i + 1]); + + // Current accumulator (updated value) + const std::vector current_accumulator_binary_limbs = { + circuit.get_variable(accumulators_binary_limbs_0_wire[i]), + circuit.get_variable(accumulators_binary_limbs_1_wire[i]), + circuit.get_variable(accumulators_binary_limbs_2_wire[i]), + circuit.get_variable(accumulators_binary_limbs_3_wire[i]), + }; + + // Previous accumulator + const std::vector previous_accumulator_binary_limbs = { + circuit.get_variable(accumulators_binary_limbs_0_wire[i + 1]), + circuit.get_variable(accumulators_binary_limbs_1_wire[i + 1]), + circuit.get_variable(accumulators_binary_limbs_2_wire[i + 1]), + circuit.get_variable(accumulators_binary_limbs_3_wire[i + 1]), + }; + + // Quotient + const std::vector quotient_binary_limbs = { + circuit.get_variable(quotient_low_binary_limbs[i]), + circuit.get_variable(quotient_low_binary_limbs[i + 1]), + circuit.get_variable(quotient_high_binary_limbs[i]), + circuit.get_variable(quotient_high_binary_limbs[i + 1]), + }; + + const size_t NUM_MICRO_LIMBS = Builder::NUM_MICRO_LIMBS; + + // Get micro chunks for checking decomposition and range + auto p_x_micro_chunks = { + get_sequential_micro_chunks(i, WireIds::P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i, WireIds::P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS) + }; + auto p_y_micro_chunks = { + get_sequential_micro_chunks(i, WireIds::P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i, WireIds::P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS) + }; + auto z_1_micro_chunks = { + get_sequential_micro_chunks(i, WireIds::Z_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i, WireIds::Z_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + }; + + auto z_2_micro_chunks = { + + get_sequential_micro_chunks(i + 1, WireIds::Z_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::Z_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS) + }; + + auto current_accumulator_micro_chunks = { + get_sequential_micro_chunks(i, WireIds::ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i, WireIds::ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), + }; + auto quotient_micro_chunks = { + get_sequential_micro_chunks(i, WireIds::QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i, WireIds::QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), + get_sequential_micro_chunks(i + 1, WireIds::QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), + }; + + // Lambda for checking the correctness of decomposition of values in the Queue into limbs for + // checking the relation + auto check_wide_limb_into_binary_limb_relation = [](const std::vector& wide_limbs, + const std::vector& binary_limbs) { + ASSERT(wide_limbs.size() * 2 == binary_limbs.size()); + for (size_t i = 0; i < wide_limbs.size(); i++) { + if ((binary_limbs[i * 2] + Fr(Builder::SHIFT_1) * binary_limbs[i * 2 + 1]) != wide_limbs[i]) { + return false; + } + } + return true; + }; + // Check that everything has been decomposed correctly + // P.xₗₒ = P.xₗₒ_0 + SHIFT_1 * P.xₗₒ_1 + // P.xₕᵢ = P.xₕᵢ_0 + SHIFT_1 * P.xₕᵢ_1 + // z_1 = z_1ₗₒ + SHIFT_1 * z_1ₕᵢ + // z_2 = z_2ₗₒ + SHIFT_2 * z_1ₕᵢ + if (!(check_wide_limb_into_binary_limb_relation({ p_x_lo, p_x_hi }, p_x_binary_limbs) && + check_wide_limb_into_binary_limb_relation({ p_y_lo, p_y_hi }, p_y_binary_limbs) && + check_wide_limb_into_binary_limb_relation({ z_1 }, z_1_binary_limbs) && + check_wide_limb_into_binary_limb_relation({ z_2 }, z_2_binary_limbs))) { + return false; + } + + enum LimbSeriesType { STANDARD_COORDINATE, Z_SCALAR, QUOTIENT }; + + // Check that limbs have been decomposed into microlimbs correctly + // value = ∑ (2ˡ)ⁱ⋅ chunkᵢ, where 2ˡ is the shift + auto check_micro_limb_decomposition_correctness = [&accumulate_limb_from_micro_chunks]( + const std::vector& binary_limbs, + const std::vector>& micro_limbs, + const LimbSeriesType limb_series_type) { + // Shifts for decompositions + constexpr auto SHIFT_12_TO_14 = Fr(4); + constexpr auto SHIFT_10_TO_14 = Fr(16); + constexpr auto SHIFT_8_TO_14 = Fr(64); + constexpr auto SHIFT_4_TO_14 = Fr(1024); + + ASSERT(binary_limbs.size() == micro_limbs.size()); + // First check that all the microlimbs are properly range constrained + for (auto& micro_limb_series : micro_limbs) { + for (auto& micro_limb : micro_limb_series) { + if (uint256_t(micro_limb) > Builder::MAX_MICRO_LIMB_SIZE) { + return false; + } + } + } + // For low limbs the last microlimb is used with the shift, so we skip it when reconstructing + // the limb + const size_t SKIPPED_FOR_LOW_LIMBS = 1; + for (size_t i = 0; i < binary_limbs.size() - 1; i++) { + if (binary_limbs[i] != accumulate_limb_from_micro_chunks(micro_limbs[i], SKIPPED_FOR_LOW_LIMBS)) { + return false; + } + // Check last additional constraint (68->70) + if (micro_limbs[i][NUM_MICRO_LIMBS - 1] != (SHIFT_12_TO_14 * micro_limbs[i][NUM_MICRO_LIMBS - 2])) { + return false; + } + } + + const size_t SKIPPED_FOR_STANDARD = 2; + const size_t SKIPPED_FOR_Z_SCALARS = 1; + const size_t SKIPPED_FOR_QUOTIENT = 2; + switch (limb_series_type) { + case STANDARD_COORDINATE: + // For standard Fq value the highest limb is 50 bits, so we skip the top 2 microlimbs + if (binary_limbs[binary_limbs.size() - 1] != + accumulate_limb_from_micro_chunks(micro_limbs[binary_limbs.size() - 1], SKIPPED_FOR_STANDARD)) { + return false; + } + // Check last additional constraint (50->56) + if (micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_STANDARD] != + (SHIFT_8_TO_14 * + micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_STANDARD - 1])) { + + return false; + } + break; + // For z top limbs we need as many microlimbs as for the low limbs + case Z_SCALAR: + if (binary_limbs[binary_limbs.size() - 1] != + accumulate_limb_from_micro_chunks(micro_limbs[binary_limbs.size() - 1], + SKIPPED_FOR_Z_SCALARS)) { + return false; + } + // Check last additional constraint (60->70) + if (micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_Z_SCALARS] != + (SHIFT_4_TO_14 * + micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_Z_SCALARS - 1])) { + return false; + } + break; + // Quotient also doesn't need the top 2 + case QUOTIENT: + if (binary_limbs[binary_limbs.size() - 1] != + accumulate_limb_from_micro_chunks(micro_limbs[binary_limbs.size() - 1], SKIPPED_FOR_QUOTIENT)) { + return false; + } + // Check last additional constraint (52->56) + if (micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_QUOTIENT] != + (SHIFT_10_TO_14 * + micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_QUOTIENT - 1])) { + return false; + } + break; + default: + abort(); + } + + return true; + }; + // Check all micro limb decompositions + if (!check_micro_limb_decomposition_correctness(p_x_binary_limbs, p_x_micro_chunks, STANDARD_COORDINATE)) { + return false; + } + if (!check_micro_limb_decomposition_correctness(p_y_binary_limbs, p_y_micro_chunks, STANDARD_COORDINATE)) { + return false; + } + if (!check_micro_limb_decomposition_correctness(z_1_binary_limbs, z_1_micro_chunks, Z_SCALAR)) { + return false; + } + if (!check_micro_limb_decomposition_correctness(z_2_binary_limbs, z_2_micro_chunks, Z_SCALAR)) { + return false; + } + if (!check_micro_limb_decomposition_correctness( + current_accumulator_binary_limbs, current_accumulator_micro_chunks, STANDARD_COORDINATE)) { + return false; + } + if (!check_micro_limb_decomposition_correctness(quotient_binary_limbs, quotient_micro_chunks, QUOTIENT)) { + return false; + } + + // The logic we are trying to enforce is: + // current_accumulator = previous_accumulator ⋅ x + op_code + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ + // v⁴ mod Fq To ensure this we transform the relation into the form: previous_accumulator ⋅ x + op + + // P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ - quotient ⋅ p - current_accumulator = 0 However, we + // don't have integers. Despite that, we can approximate integers for a certain range, if we know + // that there will not be any overflows. For now we set the range to 2²⁷² ⋅ r. We can evaluate the + // logic modulo 2²⁷² with range constraints and r is native. + // + // previous_accumulator ⋅ x + op + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ - quotient ⋅ p - + // current_accumulator = 0 => + // 1. previous_accumulator ⋅ x + op + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ + quotient ⋅ (-p mod + // 2²⁷²) - current_accumulator = 0 mod 2²⁷² + // 2. previous_accumulator ⋅ x + op + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ - quotient ⋅ p - + // current_accumulator = 0 mod r + // + // The second relation is straightforward and easy to check. The first, not so much. We have to + // evaluate certain bit chunks of the equation and ensure that they are zero. For example, for the + // lowest limb it would be (inclusive ranges): + // + // previous_accumulator[0:67] ⋅ x[0:67] + op + P.x[0:67] ⋅ v[0:67] + P.y[0:67] ⋅ v²[0:67] + + // z_1[0:67] ⋅ v³[0:67] + z_2[0:67] ⋅ v⁴[0:67] + quotient[0:67] ⋅ (-p mod 2²⁷²)[0:67] - + // current_accumulator[0:67] = intermediate_value; (we don't take parts of op, because it's supposed + // to be between 0 and 3) + // + // We could check that this intermediate_value is equal to 0 mod 2⁶⁸ by dividing it by 2⁶⁸ and + // constraining it. For efficiency, we actually compute wider evaluations for 136 bits, which + // require us to also obtain and shift products of [68:135] by [0:67] and [0:67] by [68:135] bits. + // The result of division goes into the next evaluation (the same as a carry flag would) + // So the lowest wide limb is : (∑everything[0:67]⋅everything[0:67] + + // 2⁶⁸⋅(∑everything[0:67]⋅everything[68:135]))/ 2¹³⁶ + // + // The high is: + // (low_limb + ∑everything[0:67]⋅everything[136:203] + ∑everything[68:135]⋅everything[68:135] + + // 2⁶⁸(∑everything[0:67]⋅everything[204:271] + ∑everything[68:135]⋅everything[136:203])) / 2¹³⁶ + // + // We also limit computation on limbs of op, z_1 and z_2, since we know that op has only the lowest + // limb and z_1 and z_2 have only the two lowest limbs + const std::array NEGATIVE_MODULUS_LIMBS = Builder::NEGATIVE_MODULUS_LIMBS; + const uint256_t SHIFT_1 = Builder::SHIFT_1; + const uint256_t SHIFT_2 = Builder::SHIFT_2; + const uint256_t SHIFT_3 = Builder::SHIFT_3; + Fr low_wide_limb_relation_check = + + (previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[0] + op_code + + relation_inputs.v_limbs[0] * p_x_0 + relation_inputs.v_squared_limbs[0] * p_y_0 + + relation_inputs.v_cubed_limbs[0] * z_1_lo + relation_inputs.v_quarted_limbs[0] * z_2_lo + + quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[0] - current_accumulator_binary_limbs[0]) + + (previous_accumulator_binary_limbs[1] * relation_inputs.x_limbs[0] + + relation_inputs.v_limbs[1] * p_x_0 + relation_inputs.v_squared_limbs[1] * p_y_0 + + relation_inputs.v_cubed_limbs[1] * z_1_lo + relation_inputs.v_quarted_limbs[1] * z_2_lo + + quotient_binary_limbs[1] * NEGATIVE_MODULUS_LIMBS[0] + + previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[1] + + relation_inputs.v_limbs[0] * p_x_1 + relation_inputs.v_squared_limbs[0] * p_y_1 + + relation_inputs.v_cubed_limbs[0] * z_1_hi + relation_inputs.v_quarted_limbs[0] * z_2_hi + + quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[1] - current_accumulator_binary_limbs[1]) * + Fr(SHIFT_1); + if (low_wide_limb_relation_check != (low_wide_relation_limb * SHIFT_2)) { + return false; + } + Fr high_wide_relation_limb_check = + low_wide_relation_limb + previous_accumulator_binary_limbs[2] * relation_inputs.x_limbs[0] + + previous_accumulator_binary_limbs[1] * relation_inputs.x_limbs[1] + + previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[2] + relation_inputs.v_limbs[2] * p_x_0 + + relation_inputs.v_limbs[1] * p_x_1 + relation_inputs.v_limbs[0] * p_x_2 + + relation_inputs.v_squared_limbs[2] * p_y_0 + relation_inputs.v_squared_limbs[1] * p_y_1 + + relation_inputs.v_squared_limbs[0] * p_y_2 + relation_inputs.v_cubed_limbs[2] * z_1_lo + + relation_inputs.v_cubed_limbs[1] * z_1_hi + relation_inputs.v_quarted_limbs[2] * z_2_lo + + relation_inputs.v_quarted_limbs[1] * z_2_hi + quotient_binary_limbs[2] * NEGATIVE_MODULUS_LIMBS[0] + + quotient_binary_limbs[1] * NEGATIVE_MODULUS_LIMBS[1] + + quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[2] - current_accumulator_binary_limbs[2] + + (previous_accumulator_binary_limbs[3] * relation_inputs.x_limbs[0] + + previous_accumulator_binary_limbs[2] * relation_inputs.x_limbs[1] + + previous_accumulator_binary_limbs[1] * relation_inputs.x_limbs[2] + + previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[3] + + relation_inputs.v_limbs[3] * p_x_0 + relation_inputs.v_limbs[2] * p_x_1 + + relation_inputs.v_limbs[1] * p_x_2 + relation_inputs.v_limbs[0] * p_x_3 + + relation_inputs.v_squared_limbs[3] * p_y_0 + relation_inputs.v_squared_limbs[2] * p_y_1 + + relation_inputs.v_squared_limbs[1] * p_y_2 + relation_inputs.v_squared_limbs[0] * p_y_3 + + relation_inputs.v_cubed_limbs[3] * z_1_lo + relation_inputs.v_cubed_limbs[2] * z_1_hi + + relation_inputs.v_quarted_limbs[3] * z_2_lo + relation_inputs.v_quarted_limbs[2] * z_2_hi + + quotient_binary_limbs[3] * NEGATIVE_MODULUS_LIMBS[0] + + quotient_binary_limbs[2] * NEGATIVE_MODULUS_LIMBS[1] + + quotient_binary_limbs[1] * NEGATIVE_MODULUS_LIMBS[2] + + quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[3] - current_accumulator_binary_limbs[3]) * + SHIFT_1; + if (high_wide_relation_limb_check != (high_wide_relation_limb * SHIFT_2)) { + return false; + } + // Apart from checking the correctness of the evaluation modulo 2²⁷² we also need to ensure that the + // logic works in our scalar field. For this we reconstruct the scalar field values from individual + // limbs + auto reconstructed_p_x = (p_x_0 + p_x_1 * SHIFT_1 + p_x_2 * SHIFT_2 + p_x_3 * SHIFT_3); + auto reconstructed_p_y = (p_y_0 + p_y_1 * SHIFT_1 + p_y_2 * SHIFT_2 + p_y_3 * SHIFT_3); + auto reconstructed_current_accumulator = + (current_accumulator_binary_limbs[0] + current_accumulator_binary_limbs[1] * SHIFT_1 + + current_accumulator_binary_limbs[2] * SHIFT_2 + current_accumulator_binary_limbs[3] * SHIFT_3); + auto reconstructed_previous_accumulator = + (previous_accumulator_binary_limbs[0] + previous_accumulator_binary_limbs[1] * SHIFT_1 + + previous_accumulator_binary_limbs[2] * SHIFT_2 + previous_accumulator_binary_limbs[3] * SHIFT_3); + + auto reconstructed_z1 = (z_1_lo + z_1_hi * SHIFT_1); + auto reconstructed_z2 = (z_2_lo + z_2_hi * SHIFT_1); + auto reconstructed_quotient = (quotient_binary_limbs[0] + quotient_binary_limbs[1] * SHIFT_1 + + quotient_binary_limbs[2] * SHIFT_2 + quotient_binary_limbs[3] * SHIFT_3); + + // Check the relation + if (!(reconstructed_previous_accumulator * reconstructed_evaluation_input_x + op_code + + reconstructed_p_x * reconstructed_batching_evaluation_v + + reconstructed_p_y * reconstructed_batching_evaluation_v2 + + reconstructed_z1 * reconstructed_batching_evaluation_v3 + + reconstructed_z2 * reconstructed_batching_evaluation_v4 + + reconstructed_quotient * NEGATIVE_MODULUS_LIMBS[4] - reconstructed_current_accumulator) + .is_zero()) { + return false; + }; + + } else { + // Check the accumulator is copied correctly + const std::vector current_accumulator_binary_limbs_copy = { + circuit.get_variable(accumulators_binary_limbs_0_wire[i]), + circuit.get_variable(accumulators_binary_limbs_1_wire[i]), + circuit.get_variable(accumulators_binary_limbs_2_wire[i]), + circuit.get_variable(accumulators_binary_limbs_3_wire[i]), + }; + const std::vector current_accumulator_binary_limbs = { + circuit.get_variable(accumulators_binary_limbs_0_wire[i + 1]), + circuit.get_variable(accumulators_binary_limbs_1_wire[i + 1]), + circuit.get_variable(accumulators_binary_limbs_2_wire[i + 1]), + circuit.get_variable(accumulators_binary_limbs_3_wire[i + 1]), + }; + + for (size_t j = 0; j < current_accumulator_binary_limbs.size(); j++) { + if (current_accumulator_binary_limbs_copy[j] != current_accumulator_binary_limbs[j]) { + return false; + } + } + } + } + return true; +}; +}; // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.hpp b/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.hpp new file mode 100644 index 000000000000..e160292075fa --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.hpp @@ -0,0 +1,59 @@ +#pragma once +#include "barretenberg/translator_vm/translator_circuit_builder.hpp" +namespace bb { +class TranslatorCircuitChecker { + using Fr = bb::fr; + using Fq = bb::fq; + using Builder = TranslatorCircuitBuilder; + using WireIds = Builder::WireIds; + + // Number of limbs used to decompose a 254-bit value for modular arithmetic + static constexpr size_t NUM_BINARY_LIMBS = Builder::NUM_BINARY_LIMBS; + + public: + struct RelationInputs { + std::array x_limbs; + std::array v_limbs; + std::array v_squared_limbs = { 0 }; + std::array v_cubed_limbs = { 0 }; + std::array v_quarted_limbs = { 0 }; + }; + TranslatorCircuitChecker() = default; + + /** + * @brief Get the result of accumulation, stored as 4 binary limbs in the first row of the circuit. + * + */ + static Fq get_computation_result(const Builder& circuit) + { + const size_t RESULT_ROW = 1; + ASSERT(circuit.num_gates > RESULT_ROW); + return Fq( + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_0][RESULT_ROW]) + + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_1][RESULT_ROW]) * Builder::SHIFT_1 + + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_2][RESULT_ROW]) * Builder::SHIFT_2 + + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_3][RESULT_ROW]) * Builder::SHIFT_3); + } + + /** + * @brief Create limb representations of x and powers of v that are needed to compute the witness or check + * circuit correctness + * + * @param evaluation_input_x The point at which the polynomials are being evaluated + * @param batching_challenge_v The batching challenge + * @return RelationInputs + */ + static RelationInputs compute_relation_inputs_limbs(const Fq& batching_challenge_v, const Fq& evaluation_input_x); + + /** + * @brief Check the witness satisifies the circuit + * + * @details Goes through each gate and checks the correctness of accumulation + * + * @return true + * @return false + */ + + static bool check(const Builder& circuit); +}; +} // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/circuit_checker/ultra_circuit_builder.test.cpp b/barretenberg/cpp/src/barretenberg/circuit_checker/ultra_circuit_builder.test.cpp index ae2b514f4346..ee0eaecd232a 100644 --- a/barretenberg/cpp/src/barretenberg/circuit_checker/ultra_circuit_builder.test.cpp +++ b/barretenberg/cpp/src/barretenberg/circuit_checker/ultra_circuit_builder.test.cpp @@ -12,39 +12,35 @@ namespace { auto& engine = numeric::get_debug_randomness(); } namespace bb { -using plookup::ColumnIdx; -using plookup::MultiTableId; -TEST(UltraCircuitConstructor, CopyConstructor) +TEST(UltraCircuitBuilder, CopyConstructor) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); for (size_t i = 0; i < 16; ++i) { for (size_t j = 0; j < 16; ++j) { uint64_t left = static_cast(j); uint64_t right = static_cast(i); - uint32_t left_idx = circuit_constructor.add_variable(fr(left)); - uint32_t right_idx = circuit_constructor.add_variable(fr(right)); - uint32_t result_idx = circuit_constructor.add_variable(fr(left ^ right)); + uint32_t left_idx = builder.add_variable(fr(left)); + uint32_t right_idx = builder.add_variable(fr(right)); + uint32_t result_idx = builder.add_variable(fr(left ^ right)); - uint32_t add_idx = - circuit_constructor.add_variable(fr(left) + fr(right) + circuit_constructor.get_variable(result_idx)); - circuit_constructor.create_big_add_gate( + uint32_t add_idx = builder.add_variable(fr(left) + fr(right) + builder.get_variable(result_idx)); + builder.create_big_add_gate( { left_idx, right_idx, result_idx, add_idx, fr(1), fr(1), fr(1), fr(-1), fr(0) }); } } - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); - UltraCircuitBuilder duplicate_circuit_constructor{ circuit_constructor }; + UltraCircuitBuilder duplicate_builder{ builder }; - EXPECT_EQ(duplicate_circuit_constructor.get_estimated_num_finalized_gates(), - circuit_constructor.get_estimated_num_finalized_gates()); - EXPECT_TRUE(CircuitChecker::check(duplicate_circuit_constructor)); + EXPECT_EQ(duplicate_builder.get_estimated_num_finalized_gates(), builder.get_estimated_num_finalized_gates()); + EXPECT_TRUE(CircuitChecker::check(duplicate_builder)); } -TEST(UltraCircuitConstructor, CreateGatesFromPlookupAccumulators) +TEST(UltraCircuitBuilder, CreateGatesFromPlookupAccumulators) { UltraCircuitBuilder circuit_builder = UltraCircuitBuilder(); @@ -106,7 +102,7 @@ TEST(UltraCircuitConstructor, CreateGatesFromPlookupAccumulators) EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, BadLookupFailure) +TEST(UltraCircuitBuilder, BadLookupFailure) { UltraCircuitBuilder builder; MockCircuits::add_lookup_gates(builder); @@ -122,214 +118,208 @@ TEST(UltraCircuitConstructor, BadLookupFailure) EXPECT_FALSE(CircuitChecker::check(builder)); } -TEST(UltraCircuitConstructor, BaseCase) +TEST(UltraCircuitBuilder, BaseCase) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fr a = fr::one(); - circuit_constructor.add_public_variable(a); - bool result = CircuitChecker::check(circuit_constructor); + builder.add_public_variable(a); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, TestNoLookupProof) +TEST(UltraCircuitBuilder, TestNoLookupProof) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); for (size_t i = 0; i < 16; ++i) { for (size_t j = 0; j < 16; ++j) { uint64_t left = static_cast(j); uint64_t right = static_cast(i); - uint32_t left_idx = circuit_constructor.add_variable(fr(left)); - uint32_t right_idx = circuit_constructor.add_variable(fr(right)); - uint32_t result_idx = circuit_constructor.add_variable(fr(left ^ right)); + uint32_t left_idx = builder.add_variable(fr(left)); + uint32_t right_idx = builder.add_variable(fr(right)); + uint32_t result_idx = builder.add_variable(fr(left ^ right)); - uint32_t add_idx = - circuit_constructor.add_variable(fr(left) + fr(right) + circuit_constructor.get_variable(result_idx)); - circuit_constructor.create_big_add_gate( + uint32_t add_idx = builder.add_variable(fr(left) + fr(right) + builder.get_variable(result_idx)); + builder.create_big_add_gate( { left_idx, right_idx, result_idx, add_idx, fr(1), fr(1), fr(1), fr(-1), fr(0) }); } } - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, TestEllipticGate) +TEST(UltraCircuitBuilder, TestEllipticGate) { typedef grumpkin::g1::affine_element affine_element; typedef grumpkin::g1::element element; - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); affine_element p1 = crypto::pedersen_commitment::commit_native({ bb::fr(1) }, 0); affine_element p2 = crypto::pedersen_commitment::commit_native({ bb::fr(1) }, 1); affine_element p3(element(p1) + element(p2)); - uint32_t x1 = circuit_constructor.add_variable(p1.x); - uint32_t y1 = circuit_constructor.add_variable(p1.y); - uint32_t x2 = circuit_constructor.add_variable(p2.x); - uint32_t y2 = circuit_constructor.add_variable(p2.y); - uint32_t x3 = circuit_constructor.add_variable(p3.x); - uint32_t y3 = circuit_constructor.add_variable(p3.y); + uint32_t x1 = builder.add_variable(p1.x); + uint32_t y1 = builder.add_variable(p1.y); + uint32_t x2 = builder.add_variable(p2.x); + uint32_t y2 = builder.add_variable(p2.y); + uint32_t x3 = builder.add_variable(p3.x); + uint32_t y3 = builder.add_variable(p3.y); - circuit_constructor.create_ecc_add_gate({ x1, y1, x2, y2, x3, y3, 1 }); + builder.create_ecc_add_gate({ x1, y1, x2, y2, x3, y3, 1 }); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); - circuit_constructor.create_ecc_add_gate({ x1 + 1, y1, x2, y2, x3, y3, 1 }); + builder.create_ecc_add_gate({ x1 + 1, y1, x2, y2, x3, y3, 1 }); - EXPECT_EQ(CircuitChecker::check(circuit_constructor), false); + EXPECT_EQ(CircuitChecker::check(builder), false); } -TEST(UltraCircuitConstructor, TestEllipticDoubleGate) +TEST(UltraCircuitBuilder, TestEllipticDoubleGate) { typedef grumpkin::g1::affine_element affine_element; typedef grumpkin::g1::element element; - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); affine_element p1 = crypto::pedersen_commitment::commit_native({ bb::fr(1) }, 0); affine_element p3(element(p1).dbl()); - uint32_t x1 = circuit_constructor.add_variable(p1.x); - uint32_t y1 = circuit_constructor.add_variable(p1.y); - uint32_t x3 = circuit_constructor.add_variable(p3.x); - uint32_t y3 = circuit_constructor.add_variable(p3.y); + uint32_t x1 = builder.add_variable(p1.x); + uint32_t y1 = builder.add_variable(p1.y); + uint32_t x3 = builder.add_variable(p3.x); + uint32_t y3 = builder.add_variable(p3.y); - circuit_constructor.create_ecc_dbl_gate({ x1, y1, x3, y3 }); + builder.create_ecc_dbl_gate({ x1, y1, x3, y3 }); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, NonTrivialTagPermutation) +TEST(UltraCircuitBuilder, NonTrivialTagPermutation) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fr a = fr::random_element(); fr b = -a; - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(b); - auto c_idx = circuit_constructor.add_variable(b); - auto d_idx = circuit_constructor.add_variable(a); + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(b); + auto c_idx = builder.add_variable(b); + auto d_idx = builder.add_variable(a); - circuit_constructor.create_add_gate( - { a_idx, b_idx, circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), fr::zero() }); - circuit_constructor.create_add_gate( - { c_idx, d_idx, circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), fr::zero() }); + builder.create_add_gate({ a_idx, b_idx, builder.zero_idx, fr::one(), fr::one(), fr::zero(), fr::zero() }); + builder.create_add_gate({ c_idx, d_idx, builder.zero_idx, fr::one(), fr::one(), fr::zero(), fr::zero() }); - circuit_constructor.create_tag(1, 2); - circuit_constructor.create_tag(2, 1); + builder.create_tag(1, 2); + builder.create_tag(2, 1); - circuit_constructor.assign_tag(a_idx, 1); - circuit_constructor.assign_tag(b_idx, 1); - circuit_constructor.assign_tag(c_idx, 2); - circuit_constructor.assign_tag(d_idx, 2); + builder.assign_tag(a_idx, 1); + builder.assign_tag(b_idx, 1); + builder.assign_tag(c_idx, 2); + builder.assign_tag(d_idx, 2); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); // Break the tag - circuit_constructor.real_variable_tags[circuit_constructor.real_variable_index[a_idx]] = 2; - EXPECT_EQ(CircuitChecker::check(circuit_constructor), false); + builder.real_variable_tags[builder.real_variable_index[a_idx]] = 2; + EXPECT_EQ(CircuitChecker::check(builder), false); } -TEST(UltraCircuitConstructor, NonTrivialTagPermutationAndCycles) +TEST(UltraCircuitBuilder, NonTrivialTagPermutationAndCycles) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fr a = fr::random_element(); fr c = -a; - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(a); - circuit_constructor.assert_equal(a_idx, b_idx); - auto c_idx = circuit_constructor.add_variable(c); - auto d_idx = circuit_constructor.add_variable(c); - circuit_constructor.assert_equal(c_idx, d_idx); - auto e_idx = circuit_constructor.add_variable(a); - auto f_idx = circuit_constructor.add_variable(a); - circuit_constructor.assert_equal(e_idx, f_idx); - auto g_idx = circuit_constructor.add_variable(c); - auto h_idx = circuit_constructor.add_variable(c); - circuit_constructor.assert_equal(g_idx, h_idx); - - circuit_constructor.create_tag(1, 2); - circuit_constructor.create_tag(2, 1); - - circuit_constructor.assign_tag(a_idx, 1); - circuit_constructor.assign_tag(c_idx, 1); - circuit_constructor.assign_tag(e_idx, 2); - circuit_constructor.assign_tag(g_idx, 2); - - circuit_constructor.create_add_gate( - { b_idx, a_idx, circuit_constructor.zero_idx, fr::one(), fr::neg_one(), fr::zero(), fr::zero() }); - circuit_constructor.create_add_gate( - { c_idx, g_idx, circuit_constructor.zero_idx, fr::one(), -fr::one(), fr::zero(), fr::zero() }); - circuit_constructor.create_add_gate( - { e_idx, f_idx, circuit_constructor.zero_idx, fr::one(), -fr::one(), fr::zero(), fr::zero() }); - - bool result = CircuitChecker::check(circuit_constructor); + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(a); + builder.assert_equal(a_idx, b_idx); + auto c_idx = builder.add_variable(c); + auto d_idx = builder.add_variable(c); + builder.assert_equal(c_idx, d_idx); + auto e_idx = builder.add_variable(a); + auto f_idx = builder.add_variable(a); + builder.assert_equal(e_idx, f_idx); + auto g_idx = builder.add_variable(c); + auto h_idx = builder.add_variable(c); + builder.assert_equal(g_idx, h_idx); + + builder.create_tag(1, 2); + builder.create_tag(2, 1); + + builder.assign_tag(a_idx, 1); + builder.assign_tag(c_idx, 1); + builder.assign_tag(e_idx, 2); + builder.assign_tag(g_idx, 2); + + builder.create_add_gate({ b_idx, a_idx, builder.zero_idx, fr::one(), fr::neg_one(), fr::zero(), fr::zero() }); + builder.create_add_gate({ c_idx, g_idx, builder.zero_idx, fr::one(), -fr::one(), fr::zero(), fr::zero() }); + builder.create_add_gate({ e_idx, f_idx, builder.zero_idx, fr::one(), -fr::one(), fr::zero(), fr::zero() }); + + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); // Break the tag - circuit_constructor.real_variable_tags[circuit_constructor.real_variable_index[a_idx]] = 2; - EXPECT_EQ(CircuitChecker::check(circuit_constructor), false); + builder.real_variable_tags[builder.real_variable_index[a_idx]] = 2; + EXPECT_EQ(CircuitChecker::check(builder), false); } -TEST(UltraCircuitConstructor, BadTagPermutation) +TEST(UltraCircuitBuilder, BadTagPermutation) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fr a = fr::random_element(); fr b = -a; - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(b); - auto c_idx = circuit_constructor.add_variable(b); - auto d_idx = circuit_constructor.add_variable(a + 1); + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(b); + auto c_idx = builder.add_variable(b); + auto d_idx = builder.add_variable(a + 1); - circuit_constructor.create_add_gate({ a_idx, b_idx, circuit_constructor.zero_idx, 1, 1, 0, 0 }); - circuit_constructor.create_add_gate({ c_idx, d_idx, circuit_constructor.zero_idx, 1, 1, 0, -1 }); + builder.create_add_gate({ a_idx, b_idx, builder.zero_idx, 1, 1, 0, 0 }); + builder.create_add_gate({ c_idx, d_idx, builder.zero_idx, 1, 1, 0, -1 }); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); - circuit_constructor.create_tag(1, 2); - circuit_constructor.create_tag(2, 1); + builder.create_tag(1, 2); + builder.create_tag(2, 1); - circuit_constructor.assign_tag(a_idx, 1); - circuit_constructor.assign_tag(b_idx, 1); - circuit_constructor.assign_tag(c_idx, 2); - circuit_constructor.assign_tag(d_idx, 2); + builder.assign_tag(a_idx, 1); + builder.assign_tag(b_idx, 1); + builder.assign_tag(c_idx, 2); + builder.assign_tag(d_idx, 2); - result = CircuitChecker::check(circuit_constructor); + result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } -TEST(UltraCircuitConstructor, SortWidget) +TEST(UltraCircuitBuilder, SortWidget) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fr a = fr::one(); fr b = fr(2); fr c = fr(3); fr d = fr(4); - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(b); - auto c_idx = circuit_constructor.add_variable(c); - auto d_idx = circuit_constructor.add_variable(d); - circuit_constructor.create_sort_constraint({ a_idx, b_idx, c_idx, d_idx }); + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(b); + auto c_idx = builder.add_variable(c); + auto d_idx = builder.add_variable(d); + builder.create_sort_constraint({ a_idx, b_idx, c_idx, d_idx }); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -std::vector add_variables(UltraCircuitBuilder& circuit_constructor, std::vector variables) +std::vector add_variables(UltraCircuitBuilder& builder, std::vector variables) { std::vector res; for (size_t i = 0; i < variables.size(); i++) { - res.emplace_back(circuit_constructor.add_variable(variables[i])); + res.emplace_back(builder.add_variable(variables[i])); } return res; } -TEST(UltraCircuitConstructor, SortWithEdgesGate) +TEST(UltraCircuitBuilder, SortWithEdgesGate) { fr a = fr::one(); fr b = fr(2); @@ -341,259 +331,246 @@ TEST(UltraCircuitConstructor, SortWithEdgesGate) fr h = fr(8); { - UltraCircuitBuilder circuit_constructor; - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(b); - auto c_idx = circuit_constructor.add_variable(c); - auto d_idx = circuit_constructor.add_variable(d); - auto e_idx = circuit_constructor.add_variable(e); - auto f_idx = circuit_constructor.add_variable(f); - auto g_idx = circuit_constructor.add_variable(g); - auto h_idx = circuit_constructor.add_variable(h); - circuit_constructor.create_sort_constraint_with_edges( - { a_idx, b_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, a, h); - bool result = CircuitChecker::check(circuit_constructor); + UltraCircuitBuilder builder; + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(b); + auto c_idx = builder.add_variable(c); + auto d_idx = builder.add_variable(d); + auto e_idx = builder.add_variable(e); + auto f_idx = builder.add_variable(f); + auto g_idx = builder.add_variable(g); + auto h_idx = builder.add_variable(h); + builder.create_sort_constraint_with_edges({ a_idx, b_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, a, h); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } { - UltraCircuitBuilder circuit_constructor; - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(b); - auto c_idx = circuit_constructor.add_variable(c); - auto d_idx = circuit_constructor.add_variable(d); - auto e_idx = circuit_constructor.add_variable(e); - auto f_idx = circuit_constructor.add_variable(f); - auto g_idx = circuit_constructor.add_variable(g); - auto h_idx = circuit_constructor.add_variable(h); - circuit_constructor.create_sort_constraint_with_edges( - { a_idx, b_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, a, g); - - bool result = CircuitChecker::check(circuit_constructor); + UltraCircuitBuilder builder; + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(b); + auto c_idx = builder.add_variable(c); + auto d_idx = builder.add_variable(d); + auto e_idx = builder.add_variable(e); + auto f_idx = builder.add_variable(f); + auto g_idx = builder.add_variable(g); + auto h_idx = builder.add_variable(h); + builder.create_sort_constraint_with_edges({ a_idx, b_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, a, g); + + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } { - UltraCircuitBuilder circuit_constructor; - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(b); - auto c_idx = circuit_constructor.add_variable(c); - auto d_idx = circuit_constructor.add_variable(d); - auto e_idx = circuit_constructor.add_variable(e); - auto f_idx = circuit_constructor.add_variable(f); - auto g_idx = circuit_constructor.add_variable(g); - auto h_idx = circuit_constructor.add_variable(h); - circuit_constructor.create_sort_constraint_with_edges( - { a_idx, b_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, b, h); - - bool result = CircuitChecker::check(circuit_constructor); + UltraCircuitBuilder builder; + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(b); + auto c_idx = builder.add_variable(c); + auto d_idx = builder.add_variable(d); + auto e_idx = builder.add_variable(e); + auto f_idx = builder.add_variable(f); + auto g_idx = builder.add_variable(g); + auto h_idx = builder.add_variable(h); + builder.create_sort_constraint_with_edges({ a_idx, b_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, b, h); + + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } { - UltraCircuitBuilder circuit_constructor; - auto a_idx = circuit_constructor.add_variable(a); - auto c_idx = circuit_constructor.add_variable(c); - auto d_idx = circuit_constructor.add_variable(d); - auto e_idx = circuit_constructor.add_variable(e); - auto f_idx = circuit_constructor.add_variable(f); - auto g_idx = circuit_constructor.add_variable(g); - auto h_idx = circuit_constructor.add_variable(h); - auto b2_idx = circuit_constructor.add_variable(fr(15)); - circuit_constructor.create_sort_constraint_with_edges( - { a_idx, b2_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, b, h); - bool result = CircuitChecker::check(circuit_constructor); + UltraCircuitBuilder builder; + auto a_idx = builder.add_variable(a); + auto c_idx = builder.add_variable(c); + auto d_idx = builder.add_variable(d); + auto e_idx = builder.add_variable(e); + auto f_idx = builder.add_variable(f); + auto g_idx = builder.add_variable(g); + auto h_idx = builder.add_variable(h); + auto b2_idx = builder.add_variable(fr(15)); + builder.create_sort_constraint_with_edges({ a_idx, b2_idx, c_idx, d_idx, e_idx, f_idx, g_idx, h_idx }, b, h); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto idx = add_variables(circuit_constructor, { 1, 2, 5, 6, 7, 10, 11, 13, 16, 17, 20, 22, 22, 25, - 26, 29, 29, 32, 32, 33, 35, 38, 39, 39, 42, 42, 43, 45 }); - circuit_constructor.create_sort_constraint_with_edges(idx, 1, 45); - bool result = CircuitChecker::check(circuit_constructor); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto idx = add_variables(builder, { 1, 2, 5, 6, 7, 10, 11, 13, 16, 17, 20, 22, 22, 25, + 26, 29, 29, 32, 32, 33, 35, 38, 39, 39, 42, 42, 43, 45 }); + builder.create_sort_constraint_with_edges(idx, 1, 45); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto idx = add_variables(circuit_constructor, { 1, 2, 5, 6, 7, 10, 11, 13, 16, 17, 20, 22, 22, 25, - 26, 29, 29, 32, 32, 33, 35, 38, 39, 39, 42, 42, 43, 45 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto idx = add_variables(builder, { 1, 2, 5, 6, 7, 10, 11, 13, 16, 17, 20, 22, 22, 25, + 26, 29, 29, 32, 32, 33, 35, 38, 39, 39, 42, 42, 43, 45 }); - circuit_constructor.create_sort_constraint_with_edges(idx, 1, 29); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_sort_constraint_with_edges(idx, 1, 29); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } } -TEST(UltraCircuitConstructor, RangeConstraint) +TEST(UltraCircuitBuilder, RangeConstraint) { { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto indices = add_variables(circuit_constructor, { 1, 2, 3, 4, 5, 6, 7, 8 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto indices = add_variables(builder, { 1, 2, 3, 4, 5, 6, 7, 8 }); for (size_t i = 0; i < indices.size(); i++) { - circuit_constructor.create_new_range_constraint(indices[i], 8); + builder.create_new_range_constraint(indices[i], 8); } // auto ind = {a_idx,b_idx,c_idx,d_idx,e_idx,f_idx,g_idx,h_idx}; - circuit_constructor.create_sort_constraint(indices); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_sort_constraint(indices); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto indices = add_variables(circuit_constructor, { 3 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto indices = add_variables(builder, { 3 }); for (size_t i = 0; i < indices.size(); i++) { - circuit_constructor.create_new_range_constraint(indices[i], 3); + builder.create_new_range_constraint(indices[i], 3); } // auto ind = {a_idx,b_idx,c_idx,d_idx,e_idx,f_idx,g_idx,h_idx}; - circuit_constructor.create_dummy_constraints(indices); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_dummy_constraints(indices); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto indices = add_variables(circuit_constructor, { 1, 2, 3, 4, 5, 6, 8, 25 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto indices = add_variables(builder, { 1, 2, 3, 4, 5, 6, 8, 25 }); for (size_t i = 0; i < indices.size(); i++) { - circuit_constructor.create_new_range_constraint(indices[i], 8); + builder.create_new_range_constraint(indices[i], 8); } - circuit_constructor.create_sort_constraint(indices); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_sort_constraint(indices); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto indices = add_variables(circuit_constructor, - { 1, 2, 3, 4, 5, 6, 10, 8, 15, 11, 32, 21, 42, 79, 16, 10, 3, 26, 19, 51 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto indices = + add_variables(builder, { 1, 2, 3, 4, 5, 6, 10, 8, 15, 11, 32, 21, 42, 79, 16, 10, 3, 26, 19, 51 }); for (size_t i = 0; i < indices.size(); i++) { - circuit_constructor.create_new_range_constraint(indices[i], 128); + builder.create_new_range_constraint(indices[i], 128); } - circuit_constructor.create_dummy_constraints(indices); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_dummy_constraints(indices); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto indices = add_variables(circuit_constructor, - { 1, 2, 3, 80, 5, 6, 29, 8, 15, 11, 32, 21, 42, 79, 16, 10, 3, 26, 13, 14 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto indices = + add_variables(builder, { 1, 2, 3, 80, 5, 6, 29, 8, 15, 11, 32, 21, 42, 79, 16, 10, 3, 26, 13, 14 }); for (size_t i = 0; i < indices.size(); i++) { - circuit_constructor.create_new_range_constraint(indices[i], 79); + builder.create_new_range_constraint(indices[i], 79); } - circuit_constructor.create_dummy_constraints(indices); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_dummy_constraints(indices); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto indices = add_variables(circuit_constructor, - { 1, 0, 3, 80, 5, 6, 29, 8, 15, 11, 32, 21, 42, 79, 16, 10, 3, 26, 13, 14 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto indices = + add_variables(builder, { 1, 0, 3, 80, 5, 6, 29, 8, 15, 11, 32, 21, 42, 79, 16, 10, 3, 26, 13, 14 }); for (size_t i = 0; i < indices.size(); i++) { - circuit_constructor.create_new_range_constraint(indices[i], 79); + builder.create_new_range_constraint(indices[i], 79); } - circuit_constructor.create_dummy_constraints(indices); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_dummy_constraints(indices); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } } -TEST(UltraCircuitConstructor, RangeWithGates) +TEST(UltraCircuitBuilder, RangeWithGates) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto idx = add_variables(circuit_constructor, { 1, 2, 3, 4, 5, 6, 7, 8 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto idx = add_variables(builder, { 1, 2, 3, 4, 5, 6, 7, 8 }); for (size_t i = 0; i < idx.size(); i++) { - circuit_constructor.create_new_range_constraint(idx[i], 8); + builder.create_new_range_constraint(idx[i], 8); } - circuit_constructor.create_add_gate( - { idx[0], idx[1], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -3 }); - circuit_constructor.create_add_gate( - { idx[2], idx[3], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -7 }); - circuit_constructor.create_add_gate( - { idx[4], idx[5], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -11 }); - circuit_constructor.create_add_gate( - { idx[6], idx[7], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -15 }); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_add_gate({ idx[0], idx[1], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -3 }); + builder.create_add_gate({ idx[2], idx[3], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -7 }); + builder.create_add_gate({ idx[4], idx[5], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -11 }); + builder.create_add_gate({ idx[6], idx[7], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -15 }); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, RangeWithGatesWhereRangeIsNotAPowerOfTwo) +TEST(UltraCircuitBuilder, RangeWithGatesWhereRangeIsNotAPowerOfTwo) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); - auto idx = add_variables(circuit_constructor, { 1, 2, 3, 4, 5, 6, 7, 8 }); + UltraCircuitBuilder builder = UltraCircuitBuilder(); + auto idx = add_variables(builder, { 1, 2, 3, 4, 5, 6, 7, 8 }); for (size_t i = 0; i < idx.size(); i++) { - circuit_constructor.create_new_range_constraint(idx[i], 12); + builder.create_new_range_constraint(idx[i], 12); } - circuit_constructor.create_add_gate( - { idx[0], idx[1], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -3 }); - circuit_constructor.create_add_gate( - { idx[2], idx[3], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -7 }); - circuit_constructor.create_add_gate( - { idx[4], idx[5], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -11 }); - circuit_constructor.create_add_gate( - { idx[6], idx[7], circuit_constructor.zero_idx, fr::one(), fr::one(), fr::zero(), -15 }); - bool result = CircuitChecker::check(circuit_constructor); + builder.create_add_gate({ idx[0], idx[1], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -3 }); + builder.create_add_gate({ idx[2], idx[3], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -7 }); + builder.create_add_gate({ idx[4], idx[5], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -11 }); + builder.create_add_gate({ idx[6], idx[7], builder.zero_idx, fr::one(), fr::one(), fr::zero(), -15 }); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, SortWidgetComplex) +TEST(UltraCircuitBuilder, SortWidgetComplex) { { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); std::vector a = { 1, 3, 4, 7, 7, 8, 11, 14, 15, 15, 18, 19, 21, 21, 24, 25, 26, 27, 30, 32 }; std::vector ind; for (size_t i = 0; i < a.size(); i++) - ind.emplace_back(circuit_constructor.add_variable(a[i])); - circuit_constructor.create_sort_constraint(ind); + ind.emplace_back(builder.add_variable(a[i])); + builder.create_sort_constraint(ind); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); std::vector a = { 1, 3, 4, 7, 7, 8, 16, 14, 15, 15, 18, 19, 21, 21, 24, 25, 26, 27, 30, 32 }; std::vector ind; for (size_t i = 0; i < a.size(); i++) - ind.emplace_back(circuit_constructor.add_variable(a[i])); - circuit_constructor.create_sort_constraint(ind); + ind.emplace_back(builder.add_variable(a[i])); + builder.create_sort_constraint(ind); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } } -TEST(UltraCircuitConstructor, SortWidgetNeg) +TEST(UltraCircuitBuilder, SortWidgetNeg) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fr a = fr::one(); fr b = fr(2); fr c = fr(3); fr d = fr(8); - auto a_idx = circuit_constructor.add_variable(a); - auto b_idx = circuit_constructor.add_variable(b); - auto c_idx = circuit_constructor.add_variable(c); - auto d_idx = circuit_constructor.add_variable(d); - circuit_constructor.create_sort_constraint({ a_idx, b_idx, c_idx, d_idx }); + auto a_idx = builder.add_variable(a); + auto b_idx = builder.add_variable(b); + auto c_idx = builder.add_variable(c); + auto d_idx = builder.add_variable(d); + builder.create_sort_constraint({ a_idx, b_idx, c_idx, d_idx }); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, false); } -TEST(UltraCircuitConstructor, ComposedRangeConstraint) +TEST(UltraCircuitBuilder, ComposedRangeConstraint) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); auto c = fr::random_element(); auto d = uint256_t(c).slice(0, 133); auto e = fr(d); - auto a_idx = circuit_constructor.add_variable(fr(e)); - circuit_constructor.create_add_gate( - { a_idx, circuit_constructor.zero_idx, circuit_constructor.zero_idx, 1, 0, 0, -fr(e) }); - circuit_constructor.decompose_into_default_range(a_idx, 134); + auto a_idx = builder.add_variable(fr(e)); + builder.create_add_gate({ a_idx, builder.zero_idx, builder.zero_idx, 1, 0, 0, -fr(e) }); + builder.decompose_into_default_range(a_idx, 134); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, NonNativeFieldMultiplication) +TEST(UltraCircuitBuilder, NonNativeFieldMultiplication) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fq a = fq::random_element(); fq b = fq::random_element(); @@ -621,10 +598,10 @@ TEST(UltraCircuitConstructor, NonNativeFieldMultiplication) const auto get_limb_witness_indices = [&](const std::array& limbs) { std::array limb_indices; - limb_indices[0] = circuit_constructor.add_variable(limbs[0]); - limb_indices[1] = circuit_constructor.add_variable(limbs[1]); - limb_indices[2] = circuit_constructor.add_variable(limbs[2]); - limb_indices[3] = circuit_constructor.add_variable(limbs[3]); + limb_indices[0] = builder.add_variable(limbs[0]); + limb_indices[1] = builder.add_variable(limbs[1]); + limb_indices[2] = builder.add_variable(limbs[2]); + limb_indices[3] = builder.add_variable(limbs[3]); return limb_indices; }; const uint512_t BINARY_BASIS_MODULUS = uint512_t(1) << (68 * 4); @@ -638,10 +615,10 @@ TEST(UltraCircuitConstructor, NonNativeFieldMultiplication) non_native_field_witnesses inputs{ a_indices, b_indices, q_indices, r_indices, modulus_limbs, fr(uint256_t(modulus)), }; - const auto [lo_1_idx, hi_1_idx] = circuit_constructor.evaluate_non_native_field_multiplication(inputs); - circuit_constructor.range_constrain_two_limbs(lo_1_idx, hi_1_idx, 70, 70); + const auto [lo_1_idx, hi_1_idx] = builder.evaluate_non_native_field_multiplication(inputs); + builder.range_constrain_two_limbs(lo_1_idx, hi_1_idx, 70, 70); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } @@ -649,9 +626,9 @@ TEST(UltraCircuitConstructor, NonNativeFieldMultiplication) * @brief Test that the aux block only contains aux gates. * */ -TEST(UltraCircuitConstructor, NonNativeFieldMultiplicationSortCheck) +TEST(UltraCircuitBuilder, NonNativeFieldMultiplicationSortCheck) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); fq a = fq::random_element(); fq b = fq::random_element(); @@ -679,10 +656,10 @@ TEST(UltraCircuitConstructor, NonNativeFieldMultiplicationSortCheck) const auto get_limb_witness_indices = [&](const std::array& limbs) { std::array limb_indices; - limb_indices[0] = circuit_constructor.add_variable(limbs[0]); - limb_indices[1] = circuit_constructor.add_variable(limbs[1]); - limb_indices[2] = circuit_constructor.add_variable(limbs[2]); - limb_indices[3] = circuit_constructor.add_variable(limbs[3]); + limb_indices[0] = builder.add_variable(limbs[0]); + limb_indices[1] = builder.add_variable(limbs[1]); + limb_indices[2] = builder.add_variable(limbs[2]); + limb_indices[3] = builder.add_variable(limbs[3]); return limb_indices; }; const uint512_t BINARY_BASIS_MODULUS = uint512_t(1) << (68 * 4); @@ -696,51 +673,50 @@ TEST(UltraCircuitConstructor, NonNativeFieldMultiplicationSortCheck) non_native_field_witnesses inputs{ a_indices, b_indices, q_indices, r_indices, modulus_limbs, fr(uint256_t(modulus)), }; - const auto [lo_1_idx, hi_1_idx] = circuit_constructor.evaluate_non_native_field_multiplication(inputs); - circuit_constructor.range_constrain_two_limbs(lo_1_idx, hi_1_idx, 70, 70); + const auto [lo_1_idx, hi_1_idx] = builder.evaluate_non_native_field_multiplication(inputs); + builder.range_constrain_two_limbs(lo_1_idx, hi_1_idx, 70, 70); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); // Everything above was copied from the previous test. // Check that in the aux blocks, the other selectors besides the aux selector are zero - for (size_t i = 0; i < circuit_constructor.blocks.aux.size(); ++i) { - EXPECT_EQ(circuit_constructor.blocks.aux.q_arith()[i], 0); - EXPECT_EQ(circuit_constructor.blocks.aux.q_delta_range()[i], 0); - EXPECT_EQ(circuit_constructor.blocks.aux.q_elliptic()[i], 0); - EXPECT_EQ(circuit_constructor.blocks.aux.q_lookup_type()[i], 0); - EXPECT_EQ(circuit_constructor.blocks.aux.q_poseidon2_external()[i], 0); - EXPECT_EQ(circuit_constructor.blocks.aux.q_poseidon2_internal()[i], 0); + for (size_t i = 0; i < builder.blocks.aux.size(); ++i) { + EXPECT_EQ(builder.blocks.aux.q_arith()[i], 0); + EXPECT_EQ(builder.blocks.aux.q_delta_range()[i], 0); + EXPECT_EQ(builder.blocks.aux.q_elliptic()[i], 0); + EXPECT_EQ(builder.blocks.aux.q_lookup_type()[i], 0); + EXPECT_EQ(builder.blocks.aux.q_poseidon2_external()[i], 0); + EXPECT_EQ(builder.blocks.aux.q_poseidon2_internal()[i], 0); } } -TEST(UltraCircuitConstructor, Rom) +TEST(UltraCircuitBuilder, Rom) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); uint32_t rom_values[8]{ - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), }; - size_t rom_id = circuit_constructor.create_ROM_array(8); + size_t rom_id = builder.create_ROM_array(8); for (size_t i = 0; i < 8; ++i) { - circuit_constructor.set_ROM_element(rom_id, i, rom_values[i]); + builder.set_ROM_element(rom_id, i, rom_values[i]); } - uint32_t a_idx = circuit_constructor.read_ROM_array(rom_id, circuit_constructor.add_variable(5)); + uint32_t a_idx = builder.read_ROM_array(rom_id, builder.add_variable(5)); EXPECT_EQ(a_idx != rom_values[5], true); - uint32_t b_idx = circuit_constructor.read_ROM_array(rom_id, circuit_constructor.add_variable(4)); - uint32_t c_idx = circuit_constructor.read_ROM_array(rom_id, circuit_constructor.add_variable(1)); + uint32_t b_idx = builder.read_ROM_array(rom_id, builder.add_variable(4)); + uint32_t c_idx = builder.read_ROM_array(rom_id, builder.add_variable(1)); - const auto d_value = circuit_constructor.get_variable(a_idx) + circuit_constructor.get_variable(b_idx) + - circuit_constructor.get_variable(c_idx); - uint32_t d_idx = circuit_constructor.add_variable(d_value); + const auto d_value = builder.get_variable(a_idx) + builder.get_variable(b_idx) + builder.get_variable(c_idx); + uint32_t d_idx = builder.add_variable(d_value); - circuit_constructor.create_big_add_gate({ + builder.create_big_add_gate({ a_idx, b_idx, c_idx, @@ -752,7 +728,7 @@ TEST(UltraCircuitConstructor, Rom) 0, }); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } @@ -760,7 +736,7 @@ TEST(UltraCircuitConstructor, Rom) * @brief A simple-as-possible RAM read test, for easier debugging * */ -TEST(UltraCircuitConstructor, RamSimple) +TEST(UltraCircuitBuilder, RamSimple) { UltraCircuitBuilder builder; @@ -790,41 +766,40 @@ TEST(UltraCircuitConstructor, RamSimple) EXPECT_TRUE(CircuitChecker::check(builder)); } -TEST(UltraCircuitConstructor, Ram) +TEST(UltraCircuitBuilder, Ram) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); uint32_t ram_values[8]{ - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), - circuit_constructor.add_variable(fr::random_element()), circuit_constructor.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), + builder.add_variable(fr::random_element()), builder.add_variable(fr::random_element()), }; - size_t ram_id = circuit_constructor.create_RAM_array(8); + size_t ram_id = builder.create_RAM_array(8); for (size_t i = 0; i < 8; ++i) { - circuit_constructor.init_RAM_element(ram_id, i, ram_values[i]); + builder.init_RAM_element(ram_id, i, ram_values[i]); } - uint32_t a_idx = circuit_constructor.read_RAM_array(ram_id, circuit_constructor.add_variable(5)); + uint32_t a_idx = builder.read_RAM_array(ram_id, builder.add_variable(5)); EXPECT_EQ(a_idx != ram_values[5], true); - uint32_t b_idx = circuit_constructor.read_RAM_array(ram_id, circuit_constructor.add_variable(4)); - uint32_t c_idx = circuit_constructor.read_RAM_array(ram_id, circuit_constructor.add_variable(1)); + uint32_t b_idx = builder.read_RAM_array(ram_id, builder.add_variable(4)); + uint32_t c_idx = builder.read_RAM_array(ram_id, builder.add_variable(1)); - circuit_constructor.write_RAM_array( - ram_id, circuit_constructor.add_variable(4), circuit_constructor.add_variable(500)); - uint32_t d_idx = circuit_constructor.read_RAM_array(ram_id, circuit_constructor.add_variable(4)); + builder.write_RAM_array(ram_id, builder.add_variable(4), builder.add_variable(500)); + uint32_t d_idx = builder.read_RAM_array(ram_id, builder.add_variable(4)); - EXPECT_EQ(circuit_constructor.get_variable(d_idx), 500); + EXPECT_EQ(builder.get_variable(d_idx), 500); // ensure these vars get used in another arithmetic gate - const auto e_value = circuit_constructor.get_variable(a_idx) + circuit_constructor.get_variable(b_idx) + - circuit_constructor.get_variable(c_idx) + circuit_constructor.get_variable(d_idx); - uint32_t e_idx = circuit_constructor.add_variable(e_value); + const auto e_value = builder.get_variable(a_idx) + builder.get_variable(b_idx) + builder.get_variable(c_idx) + + builder.get_variable(d_idx); + uint32_t e_idx = builder.add_variable(e_value); - circuit_constructor.create_big_add_gate( + builder.create_big_add_gate( { a_idx, b_idx, @@ -837,11 +812,11 @@ TEST(UltraCircuitConstructor, Ram) 0, }, true); - circuit_constructor.create_big_add_gate( + builder.create_big_add_gate( { - circuit_constructor.zero_idx, - circuit_constructor.zero_idx, - circuit_constructor.zero_idx, + builder.zero_idx, + builder.zero_idx, + builder.zero_idx, e_idx, 0, 0, @@ -851,36 +826,35 @@ TEST(UltraCircuitConstructor, Ram) }, false); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); // Test the builder copy constructor for a circuit with RAM gates - UltraCircuitBuilder duplicate_circuit_constructor{ circuit_constructor }; + UltraCircuitBuilder duplicate_builder{ builder }; - EXPECT_EQ(duplicate_circuit_constructor.get_estimated_num_finalized_gates(), - circuit_constructor.get_estimated_num_finalized_gates()); - EXPECT_TRUE(CircuitChecker::check(duplicate_circuit_constructor)); + EXPECT_EQ(duplicate_builder.get_estimated_num_finalized_gates(), builder.get_estimated_num_finalized_gates()); + EXPECT_TRUE(CircuitChecker::check(duplicate_builder)); } -TEST(UltraCircuitConstructor, RangeChecksOnDuplicates) +TEST(UltraCircuitBuilder, RangeChecksOnDuplicates) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); - uint32_t a = circuit_constructor.add_variable(100); - uint32_t b = circuit_constructor.add_variable(100); - uint32_t c = circuit_constructor.add_variable(100); - uint32_t d = circuit_constructor.add_variable(100); + uint32_t a = builder.add_variable(100); + uint32_t b = builder.add_variable(100); + uint32_t c = builder.add_variable(100); + uint32_t d = builder.add_variable(100); - circuit_constructor.assert_equal(a, b); - circuit_constructor.assert_equal(a, c); - circuit_constructor.assert_equal(a, d); + builder.assert_equal(a, b); + builder.assert_equal(a, c); + builder.assert_equal(a, d); - circuit_constructor.create_new_range_constraint(a, 1000); - circuit_constructor.create_new_range_constraint(b, 1001); - circuit_constructor.create_new_range_constraint(c, 999); - circuit_constructor.create_new_range_constraint(d, 1000); + builder.create_new_range_constraint(a, 1000); + builder.create_new_range_constraint(b, 1001); + builder.create_new_range_constraint(c, 999); + builder.create_new_range_constraint(d, 1000); - circuit_constructor.create_big_add_gate( + builder.create_big_add_gate( { a, b, @@ -893,44 +867,44 @@ TEST(UltraCircuitConstructor, RangeChecksOnDuplicates) 0, }, false); - bool result = CircuitChecker::check(circuit_constructor); + bool result = CircuitChecker::check(builder); EXPECT_EQ(result, true); } -TEST(UltraCircuitConstructor, CheckCircuitShowcase) +TEST(UltraCircuitBuilder, CheckCircuitShowcase) { - UltraCircuitBuilder circuit_constructor = UltraCircuitBuilder(); + UltraCircuitBuilder builder = UltraCircuitBuilder(); // check_circuit allows us to check correctness on the go - uint32_t a = circuit_constructor.add_variable(0xdead); - uint32_t b = circuit_constructor.add_variable(0xbeef); + uint32_t a = builder.add_variable(0xdead); + uint32_t b = builder.add_variable(0xbeef); // Let's create 2 gates that will bind these 2 variables to be one these two values - circuit_constructor.create_poly_gate( - { a, a, circuit_constructor.zero_idx, fr(1), -fr(0xdead) - fr(0xbeef), 0, 0, fr(0xdead) * fr(0xbeef) }); - circuit_constructor.create_poly_gate( - { b, b, circuit_constructor.zero_idx, fr(1), -fr(0xdead) - fr(0xbeef), 0, 0, fr(0xdead) * fr(0xbeef) }); + builder.create_poly_gate( + { a, a, builder.zero_idx, fr(1), -fr(0xdead) - fr(0xbeef), 0, 0, fr(0xdead) * fr(0xbeef) }); + builder.create_poly_gate( + { b, b, builder.zero_idx, fr(1), -fr(0xdead) - fr(0xbeef), 0, 0, fr(0xdead) * fr(0xbeef) }); // We can check if this works - EXPECT_EQ(CircuitChecker::check(circuit_constructor), true); + EXPECT_EQ(CircuitChecker::check(builder), true); // Now let's create a range constraint for b - circuit_constructor.create_new_range_constraint(b, 0xbeef); + builder.create_new_range_constraint(b, 0xbeef); // We can check if this works - EXPECT_EQ(CircuitChecker::check(circuit_constructor), true); + EXPECT_EQ(CircuitChecker::check(builder), true); // But what if we now assert b to be equal to a? - circuit_constructor.assert_equal(a, b, "Oh no"); + builder.assert_equal(a, b, "Oh no"); // It fails, because a is 0xdead and it can't fit in the range constraint - EXPECT_EQ(CircuitChecker::check(circuit_constructor), false); + EXPECT_EQ(CircuitChecker::check(builder), false); // But if we force them both back to be 0xbeef... - uint32_t c = circuit_constructor.add_variable(0xbeef); - circuit_constructor.assert_equal(c, b); + uint32_t c = builder.add_variable(0xbeef); + builder.assert_equal(c, b); // The circuit will magically pass again - EXPECT_EQ(CircuitChecker::check(circuit_constructor), true); + EXPECT_EQ(CircuitChecker::check(builder), true); } -} // namespace bb \ No newline at end of file +} // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/stdlib/translator_vm_verifier/translator_recursive_verifier.test.cpp b/barretenberg/cpp/src/barretenberg/stdlib/translator_vm_verifier/translator_recursive_verifier.test.cpp index 1b2afa2cd75f..dcf006cc286a 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib/translator_vm_verifier/translator_recursive_verifier.test.cpp +++ b/barretenberg/cpp/src/barretenberg/stdlib/translator_vm_verifier/translator_recursive_verifier.test.cpp @@ -1,4 +1,5 @@ #include "barretenberg/stdlib/translator_vm_verifier/translator_recursive_verifier.hpp" +#include "barretenberg/circuit_checker/translator_circuit_checker.hpp" #include "barretenberg/common/log.hpp" #include "barretenberg/stdlib/honk_verifier/ultra_verification_keys_comparator.hpp" #include "barretenberg/translator_vm/translator_verifier.hpp" @@ -74,7 +75,7 @@ template class TranslatorRecursiveTests : public ::te InnerBF evaluation_challenge_x = InnerBF::random_element(); auto circuit_builder = InnerBuilder(batching_challenge_v, evaluation_challenge_x, op_queue); - EXPECT_TRUE(circuit_builder.check_circuit()); + EXPECT_TRUE(TranslatorCircuitChecker::check(circuit_builder)); auto proving_key = std::make_shared(circuit_builder); InnerProver prover{ proving_key, prover_transcript }; auto proof = prover.construct_proof(); diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/translator.test.cpp b/barretenberg/cpp/src/barretenberg/translator_vm/translator.test.cpp index 36e163a47e7a..784c0469bb91 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator.test.cpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator.test.cpp @@ -1,3 +1,4 @@ +#include "barretenberg/circuit_checker/translator_circuit_checker.hpp" #include "barretenberg/common/log.hpp" #include "barretenberg/numeric/uint256/uint256.hpp" #include "barretenberg/relations/relation_parameters.hpp" @@ -63,7 +64,7 @@ TEST_F(TranslatorTests, Basic) // Generate a circuit and its verification key (computed at runtime from the proving key) CircuitBuilder circuit_builder = generate_test_circuit(batching_challenge_v, evaluation_challenge_x); - EXPECT_TRUE(circuit_builder.check_circuit()); + EXPECT_TRUE(TranslatorCircuitChecker::check(circuit_builder)); auto proving_key = std::make_shared(circuit_builder); TranslatorProver prover{ proving_key, prover_transcript }; auto proof = prover.construct_proof(); diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.cpp b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.cpp index f70ec92e9ea1..9f48ed062a32 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.cpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.cpp @@ -40,16 +40,16 @@ namespace bb { * @return TranslatorCircuitBuilder::AccumulationInput */ TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_witness_values( - const Fr op_code, - const Fr p_x_lo, - const Fr p_x_hi, - const Fr p_y_lo, - const Fr p_y_hi, - const Fr z1, - const Fr z2, - const Fq previous_accumulator, - const Fq batching_challenge_v, - const Fq evaluation_input_x) + const Fr& op_code, + const Fr& p_x_lo, + const Fr& p_x_hi, + const Fr& p_y_lo, + const Fr& p_y_hi, + const Fr& z1, + const Fr& z2, + const Fq& previous_accumulator, + const Fq& batching_challenge_v, + const Fq& evaluation_input_x) { // All parameters are well-described in the header, this is just for convenience constexpr size_t TOP_STANDARD_MICROLIMB_BITS = NUM_LAST_LIMB_BITS % MICRO_LIMB_BITS; @@ -57,21 +57,6 @@ TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_w constexpr size_t TOP_QUOTIENT_MICROLIMB_BITS = (TranslatorCircuitBuilder::NUM_QUOTIENT_BITS % NUM_LIMB_BITS) % MICRO_LIMB_BITS; - /** - * @brief A small function to transform a native element Fq into its bigfield representation in Fr scalars - * - * @details We transform Fq into an integer and then split it into 68-bit limbs, then convert them to Fr. - * - */ - auto base_element_to_limbs = [](const Fq& original) { - uint256_t original_uint = original; - return std::array({ - Fr(original_uint.slice(0, NUM_LIMB_BITS)), - Fr(original_uint.slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS)), - Fr(original_uint.slice(2 * NUM_LIMB_BITS, 3 * NUM_LIMB_BITS)), - Fr(original_uint.slice(3 * NUM_LIMB_BITS, 4 * NUM_LIMB_BITS)), - }); - }; /** * @brief A small function to transform a uint512_t element into its 4 68-bit limbs in Fr scalars * @@ -160,20 +145,17 @@ TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_w }; }; // x and powers of v are given to us in challenge form, so the verifier has to deal with this :) - Fq v_squared; - Fq v_cubed; - Fq v_quarted; - v_squared = batching_challenge_v * batching_challenge_v; - v_cubed = v_squared * batching_challenge_v; - v_quarted = v_cubed * batching_challenge_v; + Fq v_squared = batching_challenge_v * batching_challenge_v; + Fq v_cubed = v_squared * batching_challenge_v; + Fq v_quarted = v_cubed * batching_challenge_v; // Convert the accumulator, powers of v and x into "bigfield" form - auto previous_accumulator_limbs = base_element_to_limbs(previous_accumulator); - auto v_witnesses = base_element_to_limbs(batching_challenge_v); - auto v_squared_witnesses = base_element_to_limbs(v_squared); - auto v_cubed_witnesses = base_element_to_limbs(v_cubed); - auto v_quarted_witnesses = base_element_to_limbs(v_quarted); - auto x_witnesses = base_element_to_limbs(evaluation_input_x); + auto previous_accumulator_limbs = split_fq_into_limbs(previous_accumulator); + auto v_witnesses = split_fq_into_limbs(batching_challenge_v); + auto v_squared_witnesses = split_fq_into_limbs(v_squared); + auto v_cubed_witnesses = split_fq_into_limbs(v_cubed); + auto v_quarted_witnesses = split_fq_into_limbs(v_quarted); + auto x_witnesses = split_fq_into_limbs(evaluation_input_x); // To calculate the quotient, we need to evaluate the expression in integers. So we need uint512_t versions of all // elements involved @@ -211,8 +193,8 @@ TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_w // The formula is `accumulator = accumulator⋅x + (op + v⋅p.x + v²⋅p.y + v³⋅z₁ + v⁴z₂)`. We need to compute the // remainder (new accumulator value) - Fq remainder = previous_accumulator * evaluation_input_x + base_z_2 * v_quarted + base_z_1 * v_cubed + - base_p_y * v_squared + base_p_x * batching_challenge_v + base_op; + const Fq remainder = previous_accumulator * evaluation_input_x + base_z_2 * v_quarted + base_z_1 * v_cubed + + base_p_y * v_squared + base_p_x * batching_challenge_v + base_op; // We also need to compute the quotient uint512_t quotient_by_modulus = uint_previous_accumulator * uint_x + uint_z2 * uint_v_quarted + @@ -224,7 +206,7 @@ TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_w ASSERT(quotient_by_modulus == (quotient * uint512_t(Fq::modulus))); // Compute quotient and remainder bigfield representation - auto remainder_limbs = base_element_to_limbs(remainder); + auto remainder_limbs = split_fq_into_limbs(remainder); std::array quotient_limbs = uint512_t_to_limbs(quotient); // We will divide by shift_2 instantly in the relation itself, but first we need to compute the low part (0*0) and @@ -362,47 +344,25 @@ TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_w return input; } -/** - * @brief Create a single accumulation gate - * - * @param acc_step - */ -void TranslatorCircuitBuilder::create_accumulation_gate(const AccumulationInput acc_step) + +void TranslatorCircuitBuilder::assert_well_formed_accumulation_input(const AccumulationInput& acc_step) { // The first wires OpQueue/Transcript wires // Opcode should be {0,1,2,3,4,8} ASSERT(acc_step.op_code == 0 || acc_step.op_code == 1 || acc_step.op_code == 2 || acc_step.op_code == 3 || acc_step.op_code == 4 || acc_step.op_code == 8); - auto& op_wire = std::get(wires); - op_wire.push_back(add_variable(acc_step.op_code)); - // Every second op value in the transcript (indices 3, 5, etc) are not defined so let's just put zero there - op_wire.push_back(zero_idx); - - /** - * @brief Insert two values into the same wire sequentially - * - */ - auto insert_pair_into_wire = [this](WireIds wire_index, Fr first, Fr second) { - auto& current_wire = wires[wire_index]; - current_wire.push_back(add_variable(first)); - current_wire.push_back(add_variable(second)); - }; - // Check and insert P_x_lo and P_y_hi into wire 1 ASSERT(uint256_t(acc_step.P_x_lo) <= MAX_LOW_WIDE_LIMB_SIZE); ASSERT(uint256_t(acc_step.P_y_hi) <= MAX_HIGH_WIDE_LIMB_SIZE); - insert_pair_into_wire(WireIds::X_LOW_Y_HI, acc_step.P_x_lo, acc_step.P_y_hi); // Check and insert P_x_hi and z_1 into wire 2 ASSERT(uint256_t(acc_step.P_x_hi) <= MAX_HIGH_WIDE_LIMB_SIZE); ASSERT(uint256_t(acc_step.z_1) <= MAX_LOW_WIDE_LIMB_SIZE); - insert_pair_into_wire(WireIds::X_HIGH_Z_1, acc_step.P_x_hi, acc_step.z_1); // Check and insert P_y_lo and z_2 into wire 3 ASSERT(uint256_t(acc_step.P_y_lo) <= MAX_LOW_WIDE_LIMB_SIZE); ASSERT(uint256_t(acc_step.z_2) <= MAX_LOW_WIDE_LIMB_SIZE); - insert_pair_into_wire(WireIds::Y_LOW_Z_2, acc_step.P_y_lo, acc_step.z_2); // Check decomposition of values from the Queue into limbs used in bigfield evaluations ASSERT(acc_step.P_x_lo == (acc_step.P_x_limbs[0] + acc_step.P_x_limbs[1] * SHIFT_1)); @@ -424,19 +384,6 @@ void TranslatorCircuitBuilder::create_accumulation_gate(const AccumulationInput } ASSERT(uint256_t(limbs[total_limbs - 1]) < MAX_LAST_LIMB); }; - /** - * @brief Check correctness of values for range constraint limbs - * - */ - auto check_micro_limbs_maximum_values = - []( - const std::array, binary_limb_count>& limbs) { - for (size_t i = 0; i < binary_limb_count; i++) { - for (size_t j = 0; j < micro_limb_count; j++) { - ASSERT(uint256_t(limbs[i][j]) < MICRO_SHIFT); - } - } - }; const auto MAX_Z_LAST_LIMB = uint256_t(1) << (NUM_Z_BITS - NUM_LIMB_BITS); const auto MAX_QUOTIENT_LAST_LIMB = uint256_t(1) << (NUM_LAST_QUOTIENT_LIMB_BITS); @@ -449,20 +396,16 @@ void TranslatorCircuitBuilder::create_accumulation_gate(const AccumulationInput check_binary_limbs_maximum_values(acc_step.current_accumulator); check_binary_limbs_maximum_values(acc_step.quotient_binary_limbs, /*MAX_LAST_LIMB=*/MAX_QUOTIENT_LAST_LIMB); - // Insert limbs used in bigfield evaluations - insert_pair_into_wire(P_X_LOW_LIMBS, acc_step.P_x_limbs[0], acc_step.P_x_limbs[1]); - insert_pair_into_wire(P_X_HIGH_LIMBS, acc_step.P_x_limbs[2], acc_step.P_x_limbs[3]); - insert_pair_into_wire(P_Y_LOW_LIMBS, acc_step.P_y_limbs[0], acc_step.P_y_limbs[1]); - insert_pair_into_wire(P_Y_HIGH_LIMBS, acc_step.P_y_limbs[2], acc_step.P_y_limbs[3]); - insert_pair_into_wire(Z_LOW_LIMBS, acc_step.z_1_limbs[0], acc_step.z_2_limbs[0]); - insert_pair_into_wire(Z_HIGH_LIMBS, acc_step.z_1_limbs[1], acc_step.z_2_limbs[1]); - insert_pair_into_wire( - QUOTIENT_LOW_BINARY_LIMBS, acc_step.quotient_binary_limbs[0], acc_step.quotient_binary_limbs[1]); - insert_pair_into_wire( - QUOTIENT_HIGH_BINARY_LIMBS, acc_step.quotient_binary_limbs[2], acc_step.quotient_binary_limbs[3]); - insert_pair_into_wire(RELATION_WIDE_LIMBS, acc_step.relation_wide_limbs[0], acc_step.relation_wide_limbs[1]); - // Check limbs used in range constraints are in range + auto check_micro_limbs_maximum_values = + []( + const std::array, binary_limb_count>& limbs) { + for (size_t i = 0; i < binary_limb_count; i++) { + for (size_t j = 0; j < micro_limb_count; j++) { + ASSERT(uint256_t(limbs[i][j]) < MICRO_SHIFT); + } + } + }; check_micro_limbs_maximum_values(acc_step.P_x_microlimbs); check_micro_limbs_maximum_values(acc_step.P_y_microlimbs); check_micro_limbs_maximum_values(acc_step.z_1_microlimbs); @@ -472,18 +415,49 @@ void TranslatorCircuitBuilder::create_accumulation_gate(const AccumulationInput // Check that relation limbs are in range ASSERT(uint256_t(acc_step.relation_wide_limbs[0]) < MAX_RELATION_WIDE_LIMB_SIZE); ASSERT(uint256_t(acc_step.relation_wide_limbs[1]) < MAX_RELATION_WIDE_LIMB_SIZE); +} +/** + * @brief Create a single accumulation gate + * + * @param acc_step + */ +void TranslatorCircuitBuilder::create_accumulation_gate(const AccumulationInput& acc_step) +{ + assert_well_formed_accumulation_input(acc_step); + + auto& op_wire = std::get(wires); + op_wire.push_back(add_variable(acc_step.op_code)); + // Every second op value in the transcript (indices 3, 5, etc) are not defined so let's just put zero there + op_wire.push_back(zero_idx); /** - * @brief Put several values in sequential wires + * @brief Insert two values into the same wire sequentially * */ - auto lay_limbs_in_row = - [this](std::array input, WireIds starting_wire, size_t number_of_elements) { - ASSERT(number_of_elements <= array_size); - for (size_t i = 0; i < number_of_elements; i++) { - wires[starting_wire + i].push_back(add_variable(input[i])); - } - }; + auto insert_pair_into_wire = [this](WireIds wire_index, Fr first, Fr second) { + auto& current_wire = wires[wire_index]; + current_wire.push_back(add_variable(first)); + current_wire.push_back(add_variable(second)); + }; + + insert_pair_into_wire(WireIds::X_LOW_Y_HI, acc_step.P_x_lo, acc_step.P_y_hi); + + insert_pair_into_wire(WireIds::X_HIGH_Z_1, acc_step.P_x_hi, acc_step.z_1); + + insert_pair_into_wire(WireIds::Y_LOW_Z_2, acc_step.P_y_lo, acc_step.z_2); + + // Insert limbs used in bigfield evaluations + insert_pair_into_wire(P_X_LOW_LIMBS, acc_step.P_x_limbs[0], acc_step.P_x_limbs[1]); + insert_pair_into_wire(P_X_HIGH_LIMBS, acc_step.P_x_limbs[2], acc_step.P_x_limbs[3]); + insert_pair_into_wire(P_Y_LOW_LIMBS, acc_step.P_y_limbs[0], acc_step.P_y_limbs[1]); + insert_pair_into_wire(P_Y_HIGH_LIMBS, acc_step.P_y_limbs[2], acc_step.P_y_limbs[3]); + insert_pair_into_wire(Z_LOW_LIMBS, acc_step.z_1_limbs[0], acc_step.z_2_limbs[0]); + insert_pair_into_wire(Z_HIGH_LIMBS, acc_step.z_1_limbs[1], acc_step.z_2_limbs[1]); + insert_pair_into_wire( + QUOTIENT_LOW_BINARY_LIMBS, acc_step.quotient_binary_limbs[0], acc_step.quotient_binary_limbs[1]); + insert_pair_into_wire( + QUOTIENT_HIGH_BINARY_LIMBS, acc_step.quotient_binary_limbs[2], acc_step.quotient_binary_limbs[3]); + insert_pair_into_wire(RELATION_WIDE_LIMBS, acc_step.relation_wide_limbs[0], acc_step.relation_wide_limbs[1]); // We are using some leftover crevices for relation_wide_microlimbs auto low_relation_microlimbs = acc_step.relation_wide_microlimbs[0]; @@ -517,32 +491,41 @@ void TranslatorCircuitBuilder::create_accumulation_gate(const AccumulationInput auto top_quotient_microlimbs = acc_step.quotient_microlimbs[NUM_BINARY_LIMBS - 1]; top_quotient_microlimbs[NUM_MICRO_LIMBS - 1] = high_relation_microlimbs[NUM_MICRO_LIMBS - 1]; + /** + * @brief Put several values in sequential wires + * + */ + auto lay_limbs_in_row = [this](std::array input, WireIds starting_wire) { + size_t wire_index = starting_wire; + for (auto element : input) { + wires[wire_index].push_back(add_variable(element)); + wire_index++; + } + }; + // Now put all microlimbs into appropriate wires - lay_limbs_in_row(acc_step.P_x_microlimbs[0], P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.P_x_microlimbs[1], P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.P_x_microlimbs[2], P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(top_p_x_microlimbs, P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.P_y_microlimbs[0], P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.P_y_microlimbs[1], P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.P_y_microlimbs[2], P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(top_p_y_microlimbs, P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.z_1_microlimbs[0], Z_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.z_2_microlimbs[0], Z_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.z_1_microlimbs[1], Z_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.z_2_microlimbs[1], Z_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.current_accumulator, ACCUMULATORS_BINARY_LIMBS_0, NUM_BINARY_LIMBS); - lay_limbs_in_row(acc_step.previous_accumulator, ACCUMULATORS_BINARY_LIMBS_0, NUM_BINARY_LIMBS); - lay_limbs_in_row( - acc_step.current_accumulator_microlimbs[0], ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row( - acc_step.current_accumulator_microlimbs[1], ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row( - acc_step.current_accumulator_microlimbs[2], ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(top_current_accumulator_microlimbs, ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.quotient_microlimbs[0], QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.quotient_microlimbs[1], QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(acc_step.quotient_microlimbs[2], QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS); - lay_limbs_in_row(top_quotient_microlimbs, QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS); + lay_limbs_in_row(acc_step.P_x_microlimbs[0], P_X_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.P_x_microlimbs[1], P_X_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.P_x_microlimbs[2], P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(top_p_x_microlimbs, P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.P_y_microlimbs[0], P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.P_y_microlimbs[1], P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.P_y_microlimbs[2], P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(top_p_y_microlimbs, P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.z_1_microlimbs[0], Z_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.z_2_microlimbs[0], Z_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.z_1_microlimbs[1], Z_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.z_2_microlimbs[1], Z_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.current_accumulator, ACCUMULATORS_BINARY_LIMBS_0); + lay_limbs_in_row(acc_step.previous_accumulator, ACCUMULATORS_BINARY_LIMBS_0); + lay_limbs_in_row(acc_step.current_accumulator_microlimbs[0], ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.current_accumulator_microlimbs[1], ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.current_accumulator_microlimbs[2], ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(top_current_accumulator_microlimbs, ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0); + lay_limbs_in_row(acc_step.quotient_microlimbs[0], QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0); + lay_limbs_in_row(acc_step.quotient_microlimbs[1], QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0); + lay_limbs_in_row(acc_step.quotient_microlimbs[2], QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0); + lay_limbs_in_row(top_quotient_microlimbs, QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0); num_gates += 2; @@ -601,430 +584,4 @@ void TranslatorCircuitBuilder::feed_ecc_op_queue_into_circuit(const std::shared_ create_accumulation_gate(one_accumulation_step); } } -bool TranslatorCircuitBuilder::check_circuit() -{ - // Compute the limbs of evaluation_input_x and powers of batching_challenge_v (these go into the relation) - RelationInputs relation_inputs = compute_relation_inputs_limbs(batching_challenge_v, evaluation_input_x); - // Get the main wires (we will operate with range constraint wires mainly through indices, since this is easier) - auto& op_wire = std::get(wires); - auto& x_lo_y_hi_wire = std::get(wires); - auto& x_hi_z_1_wire = std::get(wires); - auto& y_lo_z_2_wire = std::get(wires); - auto& p_x_0_p_x_1_wire = std::get(wires); - auto& p_x_2_p_x_3_wire = std::get(wires); - auto& p_y_0_p_y_1_wire = std::get(wires); - auto& p_y_2_p_y_3_wire = std::get(wires); - auto& z_lo_wire = std::get(wires); - auto& z_hi_wire = std::get(wires); - auto& accumulators_binary_limbs_0_wire = std::get(wires); - auto& accumulators_binary_limbs_1_wire = std::get(wires); - auto& accumulators_binary_limbs_2_wire = std::get(wires); - auto& accumulators_binary_limbs_3_wire = std::get(wires); - auto& quotient_low_binary_limbs = std::get(wires); - auto& quotient_high_binary_limbs = std::get(wires); - auto& relation_wide_limbs_wire = std::get(wires); - auto reconstructed_evaluation_input_x = Fr(uint256_t(evaluation_input_x)); - auto reconstructed_batching_evaluation_v = Fr(uint256_t(batching_challenge_v)); - auto reconstructed_batching_evaluation_v2 = Fr(uint256_t(batching_challenge_v.pow(2))); - auto reconstructed_batching_evaluation_v3 = Fr(uint256_t(batching_challenge_v.pow(3))); - auto reconstructed_batching_evaluation_v4 = Fr(uint256_t(batching_challenge_v.pow(4))); - /** - * @brief Get elements at the same index from several sequential wires and put them into a vector - * - */ - auto get_sequential_micro_chunks = [this](size_t gate_index, WireIds starting_wire_index, size_t chunk_count) { - std::vector chunks; - for (size_t i = starting_wire_index; i < starting_wire_index + chunk_count; i++) { - chunks.push_back(get_variable(wires[i][gate_index])); - } - return chunks; - }; - - /** - * @brief Reconstruct the value of one regular limb used in relation computation from micro chunks used to - * create range constraints - * - * @details We might want to skip several items at the end, since those will be shifted or used - * for another decomposition - * - */ - auto accumulate_limb_from_micro_chunks = [](const std::vector& chunks, const int skipped_at_end = 1) { - Fr mini_accumulator(0); - auto end = chunks.end(); - std::advance(end, -skipped_at_end); - for (auto it = end; it != chunks.begin();) { - --it; - mini_accumulator = mini_accumulator * MICRO_SHIFT + *it; - } - return mini_accumulator; - }; - /** - * @brief Go through each gate - * - */ - for (size_t i = 1; i < num_gates - 1; i++) { - bool gate_is_odd = i & 1; - // The main relation is computed between odd and the next even indices. For example, 1 and 2 - if (gate_is_odd) { - // Get the values of P.x - Fr op_code = get_variable(op_wire[i]); - Fr p_x_lo = get_variable(x_lo_y_hi_wire[i]); - Fr p_x_hi = get_variable(x_hi_z_1_wire[i]); - Fr p_x_0 = get_variable(p_x_0_p_x_1_wire[i]); - Fr p_x_1 = get_variable(p_x_0_p_x_1_wire[i + 1]); - Fr p_x_2 = get_variable(p_x_2_p_x_3_wire[i]); - Fr p_x_3 = get_variable(p_x_2_p_x_3_wire[i + 1]); - const std::vector p_x_binary_limbs = { p_x_0, p_x_1, p_x_2, p_x_3 }; - - // P.y - Fr p_y_lo = get_variable(y_lo_z_2_wire[i]); - Fr p_y_hi = get_variable(x_lo_y_hi_wire[i + 1]); - Fr p_y_0 = get_variable(p_y_0_p_y_1_wire[i]); - Fr p_y_1 = get_variable(p_y_0_p_y_1_wire[i + 1]); - Fr p_y_2 = get_variable(p_y_2_p_y_3_wire[i]); - Fr p_y_3 = get_variable(p_y_2_p_y_3_wire[i + 1]); - const std::vector p_y_binary_limbs = { p_y_0, p_y_1, p_y_2, p_y_3 }; - // z1, z2 - Fr z_1 = get_variable(x_hi_z_1_wire[i + 1]); - Fr z_2 = get_variable(y_lo_z_2_wire[i + 1]); - - Fr z_1_lo = get_variable(z_lo_wire[i]); - Fr z_2_lo = get_variable(z_lo_wire[i + 1]); - Fr z_1_hi = get_variable(z_hi_wire[i]); - Fr z_2_hi = get_variable(z_hi_wire[i + 1]); - - const std::vector z_1_binary_limbs = { z_1_lo, z_1_hi }; - const std::vector z_2_binary_limbs = { z_2_lo, z_2_hi }; - // Relation limbs - Fr low_wide_relation_limb = get_variable(relation_wide_limbs_wire[i]); - Fr high_wide_relation_limb = get_variable(relation_wide_limbs_wire[i + 1]); - - // Current accumulator (updated value) - const std::vector current_accumulator_binary_limbs = { - get_variable(accumulators_binary_limbs_0_wire[i]), - get_variable(accumulators_binary_limbs_1_wire[i]), - get_variable(accumulators_binary_limbs_2_wire[i]), - get_variable(accumulators_binary_limbs_3_wire[i]), - }; - - // Previous accumulator - const std::vector previous_accumulator_binary_limbs = { - get_variable(accumulators_binary_limbs_0_wire[i + 1]), - get_variable(accumulators_binary_limbs_1_wire[i + 1]), - get_variable(accumulators_binary_limbs_2_wire[i + 1]), - get_variable(accumulators_binary_limbs_3_wire[i + 1]), - }; - - // Quotient - const std::vector quotient_binary_limbs = { - get_variable(quotient_low_binary_limbs[i]), - get_variable(quotient_low_binary_limbs[i + 1]), - get_variable(quotient_high_binary_limbs[i]), - get_variable(quotient_high_binary_limbs[i + 1]), - }; - - // Get micro chunks for checking decomposition and range - auto p_x_micro_chunks = { - get_sequential_micro_chunks(i, P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i, P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS) - }; - auto p_y_micro_chunks = { - get_sequential_micro_chunks(i, P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i, P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS) - }; - auto z_1_micro_chunks = { - get_sequential_micro_chunks(i, Z_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i, Z_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - }; - - auto z_2_micro_chunks = { - - get_sequential_micro_chunks(i + 1, Z_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, Z_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS) - }; - - auto current_accumulator_micro_chunks = { - get_sequential_micro_chunks(i, ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i, ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0, NUM_MICRO_LIMBS), - }; - auto quotient_micro_chunks = { - get_sequential_micro_chunks(i, QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i, QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), - get_sequential_micro_chunks(i + 1, QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0, NUM_MICRO_LIMBS), - }; - - // Lambda for checking the correctness of decomposition of values in the Queue into limbs for checking - // the relation - auto check_wide_limb_into_binary_limb_relation = [](const std::vector& wide_limbs, - const std::vector& binary_limbs) { - ASSERT(wide_limbs.size() * 2 == binary_limbs.size()); - for (size_t i = 0; i < wide_limbs.size(); i++) { - if ((binary_limbs[i * 2] + Fr(SHIFT_1) * binary_limbs[i * 2 + 1]) != wide_limbs[i]) { - return false; - } - } - return true; - }; - // Check that everything has been decomposed correctly - // P.xₗₒ = P.xₗₒ_0 + SHIFT_1 * P.xₗₒ_1 - // P.xₕᵢ = P.xₕᵢ_0 + SHIFT_1 * P.xₕᵢ_1 - // z_1 = z_1ₗₒ + SHIFT_1 * z_1ₕᵢ - // z_2 = z_2ₗₒ + SHIFT_2 * z_1ₕᵢ - if (!(check_wide_limb_into_binary_limb_relation({ p_x_lo, p_x_hi }, p_x_binary_limbs) && - check_wide_limb_into_binary_limb_relation({ p_y_lo, p_y_hi }, p_y_binary_limbs) && - check_wide_limb_into_binary_limb_relation({ z_1 }, z_1_binary_limbs) && - check_wide_limb_into_binary_limb_relation({ z_2 }, z_2_binary_limbs))) { - return false; - } - - enum LimbSeriesType { STANDARD_COORDINATE, Z_SCALAR, QUOTIENT }; - - // Check that limbs have been decomposed into microlimbs correctly - // value = ∑ (2ˡ)ⁱ⋅ chunkᵢ, where 2ˡ is the shift - auto check_micro_limb_decomposition_correctness = [&accumulate_limb_from_micro_chunks]( - const std::vector& binary_limbs, - const std::vector>& micro_limbs, - const LimbSeriesType limb_series_type) { - // Shifts for decompositions - constexpr auto SHIFT_12_TO_14 = Fr(4); - constexpr auto SHIFT_10_TO_14 = Fr(16); - constexpr auto SHIFT_8_TO_14 = Fr(64); - constexpr auto SHIFT_4_TO_14 = Fr(1024); - - ASSERT(binary_limbs.size() == micro_limbs.size()); - // First check that all the microlimbs are properly range constrained - for (auto& micro_limb_series : micro_limbs) { - for (auto& micro_limb : micro_limb_series) { - if (uint256_t(micro_limb) > MAX_MICRO_LIMB_SIZE) { - return false; - } - } - } - // For low limbs the last microlimb is used with the shift, so we skip it when reconstructing - // the limb - const size_t SKIPPED_FOR_LOW_LIMBS = 1; - for (size_t i = 0; i < binary_limbs.size() - 1; i++) { - if (binary_limbs[i] != accumulate_limb_from_micro_chunks(micro_limbs[i], SKIPPED_FOR_LOW_LIMBS)) { - return false; - } - // Check last additional constraint (68->70) - if (micro_limbs[i][NUM_MICRO_LIMBS - 1] != (SHIFT_12_TO_14 * micro_limbs[i][NUM_MICRO_LIMBS - 2])) { - return false; - } - } - - const size_t SKIPPED_FOR_STANDARD = 2; - const size_t SKIPPED_FOR_Z_SCALARS = 1; - const size_t SKIPPED_FOR_QUOTIENT = 2; - switch (limb_series_type) { - case STANDARD_COORDINATE: - // For standard Fq value the highest limb is 50 bits, so we skip the top 2 microlimbs - if (binary_limbs[binary_limbs.size() - 1] != - accumulate_limb_from_micro_chunks(micro_limbs[binary_limbs.size() - 1], SKIPPED_FOR_STANDARD)) { - return false; - } - // Check last additional constraint (50->56) - if (micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_STANDARD] != - (SHIFT_8_TO_14 * - micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_STANDARD - 1])) { - - return false; - } - break; - // For z top limbs we need as many microlimbs as for the low limbs - case Z_SCALAR: - if (binary_limbs[binary_limbs.size() - 1] != - accumulate_limb_from_micro_chunks(micro_limbs[binary_limbs.size() - 1], - SKIPPED_FOR_Z_SCALARS)) { - return false; - } - // Check last additional constraint (60->70) - if (micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_Z_SCALARS] != - (SHIFT_4_TO_14 * - micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_Z_SCALARS - 1])) { - return false; - } - break; - // Quotient also doesn't need the top 2 - case QUOTIENT: - if (binary_limbs[binary_limbs.size() - 1] != - accumulate_limb_from_micro_chunks(micro_limbs[binary_limbs.size() - 1], SKIPPED_FOR_QUOTIENT)) { - return false; - } - // Check last additional constraint (52->56) - if (micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_QUOTIENT] != - (SHIFT_10_TO_14 * - micro_limbs[binary_limbs.size() - 1][NUM_MICRO_LIMBS - SKIPPED_FOR_QUOTIENT - 1])) { - return false; - } - break; - default: - abort(); - } - - return true; - }; - // Check all micro limb decompositions - if (!check_micro_limb_decomposition_correctness(p_x_binary_limbs, p_x_micro_chunks, STANDARD_COORDINATE)) { - return false; - } - if (!check_micro_limb_decomposition_correctness(p_y_binary_limbs, p_y_micro_chunks, STANDARD_COORDINATE)) { - return false; - } - if (!check_micro_limb_decomposition_correctness(z_1_binary_limbs, z_1_micro_chunks, Z_SCALAR)) { - return false; - } - if (!check_micro_limb_decomposition_correctness(z_2_binary_limbs, z_2_micro_chunks, Z_SCALAR)) { - return false; - } - if (!check_micro_limb_decomposition_correctness( - current_accumulator_binary_limbs, current_accumulator_micro_chunks, STANDARD_COORDINATE)) { - return false; - } - if (!check_micro_limb_decomposition_correctness(quotient_binary_limbs, quotient_micro_chunks, QUOTIENT)) { - return false; - } - - // The logic we are trying to enforce is: - // current_accumulator = previous_accumulator ⋅ x + op_code + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ - // mod Fq To ensure this we transform the relation into the form: previous_accumulator ⋅ x + op + P.x ⋅ - // v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ - quotient ⋅ p - current_accumulator = 0 However, we don't have - // integers. Despite that, we can approximate integers for a certain range, if we know that there will - // not be any overflows. For now we set the range to 2²⁷² ⋅ r. We can evaluate the logic modulo 2²⁷² - // with range constraints and r is native. - // - // previous_accumulator ⋅ x + op + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ - quotient ⋅ p - - // current_accumulator = 0 => - // 1. previous_accumulator ⋅ x + op + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ + quotient ⋅ (-p mod - // 2²⁷²) - current_accumulator = 0 mod 2²⁷² - // 2. previous_accumulator ⋅ x + op + P.x ⋅ v + P.y ⋅ v² + z_1 ⋅ v³ + z_2 ⋅ v⁴ - quotient ⋅ p - - // current_accumulator = 0 mod r - // - // The second relation is straightforward and easy to check. The first, not so much. We have to evaluate - // certain bit chunks of the equation and ensure that they are zero. For example, for the lowest limb it - // would be (inclusive ranges): - // - // previous_accumulator[0:67] ⋅ x[0:67] + op + P.x[0:67] ⋅ v[0:67] + P.y[0:67] ⋅ v²[0:67] + z_1[0:67] ⋅ - // v³[0:67] + z_2[0:67] ⋅ v⁴[0:67] + quotient[0:67] ⋅ (-p mod 2²⁷²)[0:67] - current_accumulator[0:67] = - // intermediate_value; (we don't take parts of op, because it's supposed to be between 0 and 3) - // - // We could check that this intermediate_value is equal to 0 mod 2⁶⁸ by dividing it by 2⁶⁸ and - // constraining it. For efficiency, we actually compute wider evaluations for 136 bits, which require us - // to also obtain and shift products of [68:135] by [0:67] and [0:67] by [68:135] bits. - // The result of division goes into the next evaluation (the same as a carry flag would) - // So the lowest wide limb is : (∑everything[0:67]⋅everything[0:67] + - // 2⁶⁸⋅(∑everything[0:67]⋅everything[68:135]))/ 2¹³⁶ - // - // The high is: - // (low_limb + ∑everything[0:67]⋅everything[136:203] + ∑everything[68:135]⋅everything[68:135] + - // 2⁶⁸(∑everything[0:67]⋅everything[204:271] + ∑everything[68:135]⋅everything[136:203])) / 2¹³⁶ - // - // We also limit computation on limbs of op, z_1 and z_2, since we know that op has only the lowest limb - // and z_1 and z_2 have only the two lowest limbs - Fr low_wide_limb_relation_check = - - (previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[0] + op_code + - relation_inputs.v_limbs[0] * p_x_0 + relation_inputs.v_squared_limbs[0] * p_y_0 + - relation_inputs.v_cubed_limbs[0] * z_1_lo + relation_inputs.v_quarted_limbs[0] * z_2_lo + - quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[0] - current_accumulator_binary_limbs[0]) + - (previous_accumulator_binary_limbs[1] * relation_inputs.x_limbs[0] + - relation_inputs.v_limbs[1] * p_x_0 + relation_inputs.v_squared_limbs[1] * p_y_0 + - relation_inputs.v_cubed_limbs[1] * z_1_lo + relation_inputs.v_quarted_limbs[1] * z_2_lo + - quotient_binary_limbs[1] * NEGATIVE_MODULUS_LIMBS[0] + - previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[1] + - relation_inputs.v_limbs[0] * p_x_1 + relation_inputs.v_squared_limbs[0] * p_y_1 + - relation_inputs.v_cubed_limbs[0] * z_1_hi + relation_inputs.v_quarted_limbs[0] * z_2_hi + - quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[1] - current_accumulator_binary_limbs[1]) * - Fr(SHIFT_1); - if (low_wide_limb_relation_check != (low_wide_relation_limb * SHIFT_2)) { - return false; - } - Fr high_wide_relation_limb_check = - low_wide_relation_limb + previous_accumulator_binary_limbs[2] * relation_inputs.x_limbs[0] + - previous_accumulator_binary_limbs[1] * relation_inputs.x_limbs[1] + - previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[2] + relation_inputs.v_limbs[2] * p_x_0 + - relation_inputs.v_limbs[1] * p_x_1 + relation_inputs.v_limbs[0] * p_x_2 + - relation_inputs.v_squared_limbs[2] * p_y_0 + relation_inputs.v_squared_limbs[1] * p_y_1 + - relation_inputs.v_squared_limbs[0] * p_y_2 + relation_inputs.v_cubed_limbs[2] * z_1_lo + - relation_inputs.v_cubed_limbs[1] * z_1_hi + relation_inputs.v_quarted_limbs[2] * z_2_lo + - relation_inputs.v_quarted_limbs[1] * z_2_hi + quotient_binary_limbs[2] * NEGATIVE_MODULUS_LIMBS[0] + - quotient_binary_limbs[1] * NEGATIVE_MODULUS_LIMBS[1] + - quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[2] - current_accumulator_binary_limbs[2] + - (previous_accumulator_binary_limbs[3] * relation_inputs.x_limbs[0] + - previous_accumulator_binary_limbs[2] * relation_inputs.x_limbs[1] + - previous_accumulator_binary_limbs[1] * relation_inputs.x_limbs[2] + - previous_accumulator_binary_limbs[0] * relation_inputs.x_limbs[3] + - relation_inputs.v_limbs[3] * p_x_0 + relation_inputs.v_limbs[2] * p_x_1 + - relation_inputs.v_limbs[1] * p_x_2 + relation_inputs.v_limbs[0] * p_x_3 + - relation_inputs.v_squared_limbs[3] * p_y_0 + relation_inputs.v_squared_limbs[2] * p_y_1 + - relation_inputs.v_squared_limbs[1] * p_y_2 + relation_inputs.v_squared_limbs[0] * p_y_3 + - relation_inputs.v_cubed_limbs[3] * z_1_lo + relation_inputs.v_cubed_limbs[2] * z_1_hi + - relation_inputs.v_quarted_limbs[3] * z_2_lo + relation_inputs.v_quarted_limbs[2] * z_2_hi + - quotient_binary_limbs[3] * NEGATIVE_MODULUS_LIMBS[0] + - quotient_binary_limbs[2] * NEGATIVE_MODULUS_LIMBS[1] + - quotient_binary_limbs[1] * NEGATIVE_MODULUS_LIMBS[2] + - quotient_binary_limbs[0] * NEGATIVE_MODULUS_LIMBS[3] - current_accumulator_binary_limbs[3]) * - SHIFT_1; - if (high_wide_relation_limb_check != (high_wide_relation_limb * SHIFT_2)) { - return false; - } - // Apart from checking the correctness of the evaluation modulo 2²⁷² we also need to ensure that the - // logic works in our scalar field. For this we reconstruct the scalar field values from individual - // limbs - auto reconstructed_p_x = (p_x_0 + p_x_1 * SHIFT_1 + p_x_2 * SHIFT_2 + p_x_3 * SHIFT_3); - auto reconstructed_p_y = (p_y_0 + p_y_1 * SHIFT_1 + p_y_2 * SHIFT_2 + p_y_3 * SHIFT_3); - auto reconstructed_current_accumulator = - (current_accumulator_binary_limbs[0] + current_accumulator_binary_limbs[1] * SHIFT_1 + - current_accumulator_binary_limbs[2] * SHIFT_2 + current_accumulator_binary_limbs[3] * SHIFT_3); - auto reconstructed_previous_accumulator = - (previous_accumulator_binary_limbs[0] + previous_accumulator_binary_limbs[1] * SHIFT_1 + - previous_accumulator_binary_limbs[2] * SHIFT_2 + previous_accumulator_binary_limbs[3] * SHIFT_3); - - auto reconstructed_z1 = (z_1_lo + z_1_hi * SHIFT_1); - auto reconstructed_z2 = (z_2_lo + z_2_hi * SHIFT_1); - auto reconstructed_quotient = (quotient_binary_limbs[0] + quotient_binary_limbs[1] * SHIFT_1 + - quotient_binary_limbs[2] * SHIFT_2 + quotient_binary_limbs[3] * SHIFT_3); - - // Check the relation - if (!(reconstructed_previous_accumulator * reconstructed_evaluation_input_x + op_code + - reconstructed_p_x * reconstructed_batching_evaluation_v + - reconstructed_p_y * reconstructed_batching_evaluation_v2 + - reconstructed_z1 * reconstructed_batching_evaluation_v3 + - reconstructed_z2 * reconstructed_batching_evaluation_v4 + - reconstructed_quotient * NEGATIVE_MODULUS_LIMBS[4] - reconstructed_current_accumulator) - .is_zero()) { - return false; - }; - - } else { - // Check the accumulator is copied correctly - const std::vector current_accumulator_binary_limbs_copy = { - get_variable(accumulators_binary_limbs_0_wire[i]), - get_variable(accumulators_binary_limbs_1_wire[i]), - get_variable(accumulators_binary_limbs_2_wire[i]), - get_variable(accumulators_binary_limbs_3_wire[i]), - }; - const std::vector current_accumulator_binary_limbs = { - get_variable(accumulators_binary_limbs_0_wire[i + 1]), - get_variable(accumulators_binary_limbs_1_wire[i + 1]), - get_variable(accumulators_binary_limbs_2_wire[i + 1]), - get_variable(accumulators_binary_limbs_3_wire[i + 1]), - }; - - for (size_t j = 0; j < current_accumulator_binary_limbs.size(); j++) { - if (current_accumulator_binary_limbs_copy[j] != current_accumulator_binary_limbs[j]) { - return false; - } - } - } - } - return true; -}; } // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.fuzzer.cpp b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.fuzzer.cpp index 89e70b004df6..4e869e12971d 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.fuzzer.cpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.fuzzer.cpp @@ -4,7 +4,9 @@ // external_2: { status: not started, auditors: [], date: YYYY-MM-DD } // ===================== +#include "barretenberg/circuit_checker/translator_circuit_checker.hpp" #include "barretenberg/translator_vm/translator.fuzzer.hpp" + /** * @brief A very primitive fuzzing harness, no interesting mutations, just parse and throw at the circuit builder * @@ -40,15 +42,17 @@ extern "C" int LLVMFuzzerTestOneInput(const unsigned char* data, size_t size) Fq x_pow = x.pow(eccvm_ops.size() - 1); // Multiply by an appropriate power of x to get rid of the inverses - Fq result = ((((z_2_accumulator * batching_challenge + z_1_accumulator) * batching_challenge + p_y_accumulator) * - batching_challenge + - p_x_accumulator) * - batching_challenge + - op_accumulator) * - x_pow; + [[maybe_unused]] Fq result = + ((((z_2_accumulator * batching_challenge + z_1_accumulator) * batching_challenge + p_y_accumulator) * + batching_challenge + + p_x_accumulator) * + batching_challenge + + op_accumulator) * + x_pow; // The data is malformed, so just call check_circuit, but ignore the output - circuit_builder.check_circuit(); - (void)result; + if (!TranslatorCircuitChecker::check(circuit_builder)) { + return 1; + } return 0; } diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.hpp index ed5a3db771f9..d5cb7d1c2901 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.hpp @@ -76,8 +76,10 @@ namespace bb { * */ class TranslatorCircuitBuilder : public CircuitBuilderBase { - // We don't need templating for Goblin + + // The scalar field of BN254 using Fr = bb::fr; + // The base (coordinate) field of BN254 using Fq = bb::fq; public: @@ -223,10 +225,11 @@ class TranslatorCircuitBuilder : public CircuitBuilderBase { // highest to a more restrictive range (0 <= a < 2¹⁴ && 0 <= 4*a < 2¹⁴ ) ~ ( 0 <= a < 2¹² ) static constexpr size_t NUM_MICRO_LIMBS = 6; - // How many limbs we split the 254-bit value in + // Number of limbs used to decompose a 254-bit value for modular arithmetic. This will represent an Fq value as 4 Fr + // limbs to be representable inside a circuit defined overF r. static constexpr size_t NUM_BINARY_LIMBS = 4; - // How many limbs we use for computation of result modulo 2²⁷² + // Number of limbs used for computation of a result modulo 2²⁷² static constexpr size_t NUM_RELATION_WIDE_LIMBS = 2; // Range constraint of relation limbs @@ -316,13 +319,6 @@ class TranslatorCircuitBuilder : public CircuitBuilderBase { std::array v_cubed_limbs = { 0 }; std::array v_quarted_limbs = { 0 }; }; - struct RelationInputs { - std::array x_limbs; - std::array v_limbs; - std::array v_squared_limbs = { 0 }; - std::array v_cubed_limbs = { 0 }; - std::array v_quarted_limbs = { 0 }; - }; static constexpr std::string_view NAME_STRING = "TranslatorCircuitBuilder"; @@ -385,45 +381,32 @@ class TranslatorCircuitBuilder : public CircuitBuilderBase { ~TranslatorCircuitBuilder() override = default; /** - * @brief Create limb representations of x and powers of v that are needed to compute the witness or check - * circuit correctness + * @brief A small function to transform a native element Fq into its bigfield representation in Fr scalars + * + * @details We transform Fq into an integer and then split it into 68-bit limbs, then convert them to Fr. * - * @param evaluation_input_x The point at which the polynomials are being evaluated - * @param batching_challenge_v The batching challenge - * @return RelationInputs */ - static RelationInputs compute_relation_inputs_limbs(Fq batching_challenge_v, Fq evaluation_input_x) + static std::array split_fq_into_limbs(const Fq& base) { - /** - * @brief A small function to transform a native element Fq into its bigfield representation in Fr scalars - * - */ - auto base_element_to_limbs = [](Fq& original) { - uint256_t original_uint = original; - return std::array({ - Fr(original_uint.slice(0, NUM_LIMB_BITS)), - Fr(original_uint.slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS)), - Fr(original_uint.slice(2 * NUM_LIMB_BITS, 3 * NUM_LIMB_BITS)), - Fr(original_uint.slice(3 * NUM_LIMB_BITS, 4 * NUM_LIMB_BITS)), - }); - }; - Fq& v = batching_challenge_v; - Fq& x = evaluation_input_x; - Fq v_squared; - Fq v_cubed; - Fq v_quarted; - v_squared = v * v; - v_cubed = v_squared * v; - v_quarted = v_cubed * v; - RelationInputs result; - result.x_limbs = base_element_to_limbs(x); - result.v_limbs = base_element_to_limbs(v); - result.v_squared_limbs = base_element_to_limbs(v_squared); - result.v_cubed_limbs = base_element_to_limbs(v_cubed); - result.v_quarted_limbs = base_element_to_limbs(v_quarted); - return result; + uint256_t base_uint = base; + return std::array({ + Fr(base_uint.slice(0, NUM_LIMB_BITS)), + Fr(base_uint.slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS)), + Fr(base_uint.slice(2 * NUM_LIMB_BITS, 3 * NUM_LIMB_BITS)), + Fr(base_uint.slice(3 * NUM_LIMB_BITS, 4 * NUM_LIMB_BITS)), + }); } + /** + * @brief Ensures the accumulation input is well-formed and can be used to create a gate. + * @details There are two main types of checks: that members of the AccumulationInput are within the appropriate + * ranges and that the members containing `*limbs` have been constructed appropriately from the original values, + * also present in the input. + * + * @param acc_step + */ + static void assert_well_formed_accumulation_input(const AccumulationInput& acc_step); + /** * @brief Create a single accumulation gate * @@ -432,22 +415,8 @@ class TranslatorCircuitBuilder : public CircuitBuilderBase { * * @param acc_step */ - void create_accumulation_gate(AccumulationInput acc_step); + void create_accumulation_gate(const AccumulationInput& acc_step); - /** - * @brief Get the result of accumulation - * - * @return bb::fq - */ - bb::fq get_computation_result() - { - const size_t RESULT_ROW = 1; - ASSERT(num_gates > RESULT_ROW); - return (uint256_t(get_variable(wires[WireIds::ACCUMULATORS_BINARY_LIMBS_0][RESULT_ROW])) + - uint256_t(get_variable(wires[WireIds::ACCUMULATORS_BINARY_LIMBS_1][RESULT_ROW])) * SHIFT_1 + - uint256_t(get_variable(wires[WireIds::ACCUMULATORS_BINARY_LIMBS_2][RESULT_ROW])) * SHIFT_2 + - uint256_t(get_variable(wires[WireIds::ACCUMULATORS_BINARY_LIMBS_3][RESULT_ROW])) * SHIFT_3); - } /** * @brief Generate all the gates required to prove the correctness of batched evalution of polynomials representing * commitments to ECCOpQueue @@ -456,25 +425,16 @@ class TranslatorCircuitBuilder : public CircuitBuilderBase { */ void feed_ecc_op_queue_into_circuit(const std::shared_ptr ecc_op_queue); - /** - * @brief Check the witness satisifies the circuit - * - * @details Goes through each gate and checks the correctness of accumulation - * - * @return true - * @return false - */ - bool check_circuit(); - static AccumulationInput generate_witness_values(const Fr op_code, - const Fr p_x_lo, - const Fr p_x_hi, - const Fr p_y_lo, - const Fr p_y_hi, - const Fr z1, - const Fr z2, - const Fq previous_accumulator, - const Fq batching_challenge_v, - const Fq evaluation_input_x); + static AccumulationInput generate_witness_values(const Fr& op_code, + const Fr& p_x_lo, + const Fr& p_x_hi, + const Fr& p_y_lo, + const Fr& p_y_hi, + const Fr& z1, + const Fr& z2, + const Fq& previous_accumulator, + const Fq& batching_challenge_v, + const Fq& evaluation_input_x); }; } // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.test.cpp b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.test.cpp index 77a8fdb122a7..50755278aab5 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.test.cpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.test.cpp @@ -1,4 +1,5 @@ #include "translator_circuit_builder.hpp" +#include "barretenberg/circuit_checker/translator_circuit_checker.hpp" #include "barretenberg/ecc/curves/bn254/bn254.hpp" #include "barretenberg/op_queue/ecc_op_queue.hpp" #include @@ -9,6 +10,7 @@ using namespace bb; namespace { auto& engine = numeric::get_debug_randomness(); } +using CircuitChecker = TranslatorCircuitChecker; /** * @brief Check that a single accumulation gate is created correctly * @@ -69,7 +71,7 @@ TEST(TranslatorCircuitBuilder, CircuitBuilderBaseCase) // Submit one accumulation step in the builder circuit_builder.create_accumulation_gate(single_accumulation_step); // Check if the circuit fails - EXPECT_TRUE(circuit_builder.check_circuit()); + EXPECT_TRUE(TranslatorCircuitChecker::check(circuit_builder)); } /** @@ -127,7 +129,8 @@ TEST(TranslatorCircuitBuilder, SeveralOperationCorrectness) // Create circuit builder and feed the queue inside auto circuit_builder = TranslatorCircuitBuilder(batching_challenge, x, op_queue); // Check that the circuit passes - EXPECT_TRUE(circuit_builder.check_circuit()); - // Check the computation result is in line with what we've computed - EXPECT_EQ(result, circuit_builder.get_computation_result()); + EXPECT_TRUE(CircuitChecker::check(circuit_builder)); + // Check the accumulation result stored as 4 limbs in the circuit and then reconstructed is consistent with the + // value computed by hand. + EXPECT_EQ(result, CircuitChecker::get_computation_result(circuit_builder)); } diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/translator_composer.fuzzer.cpp b/barretenberg/cpp/src/barretenberg/translator_vm/translator_composer.fuzzer.cpp index 8de48a775448..0417096830ac 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_composer.fuzzer.cpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_composer.fuzzer.cpp @@ -4,6 +4,7 @@ // external_2: { status: not started, auditors: [], date: YYYY-MM-DD } // ===================== +#include "barretenberg/circuit_checker/translator_circuit_checker.hpp" #include "barretenberg/translator_vm/translator.fuzzer.hpp" #include "barretenberg/translator_vm/translator_prover.hpp" #include "barretenberg/translator_vm/translator_verifier.hpp" @@ -35,8 +36,7 @@ extern "C" int LLVMFuzzerTestOneInput(const unsigned char* data, size_t size) auto circuit_builder = TranslatorCircuitBuilder(translation_batching_challenge, x, op_queue); // Check that the circuit passes - bool checked = circuit_builder.check_circuit(); - + bool checked = TranslatorCircuitChecker::check(circuit_builder); // Construct proof auto proving_key = std::make_shared(circuit_builder); TranslatorProver prover(proving_key, prover_transcript); diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/translator_mini.fuzzer.cpp b/barretenberg/cpp/src/barretenberg/translator_vm/translator_mini.fuzzer.cpp index ae0071da2241..80269533d456 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_mini.fuzzer.cpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_mini.fuzzer.cpp @@ -4,6 +4,7 @@ // external_2: { status: not started, auditors: [], date: YYYY-MM-DD } // ===================== +#include "barretenberg/circuit_checker/translator_circuit_checker.hpp" #include "barretenberg/numeric/uint256/uint256.hpp" #include "translator_circuit_builder.hpp" @@ -47,7 +48,7 @@ extern "C" int LLVMFuzzerTestOneInput(const unsigned char* data, size_t size) auto circuit_builder = bb::TranslatorCircuitBuilder(v, x); circuit_builder.create_accumulation_gate(single_accumulation_step); - if (!circuit_builder.check_circuit()) { + if (!TranslatorCircuitChecker::check(circuit_builder)) { return 1; } return 0;