diff --git a/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.cpp b/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.cpp index bd71d7ce7472..e6433f598aec 100644 --- a/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.cpp +++ b/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.cpp @@ -1,515 +1,140 @@ +// === AUDIT STATUS === +// internal: { status: Planned, auditors: [], commit: } +// external_1: { status: not started, auditors: [], commit: } +// external_2: { status: not started, auditors: [], commit: } +// ===================== + #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) +TranslatorCircuitChecker::Params TranslatorCircuitChecker::compute_relation_params(const Builder& circuit) { - - auto wires = circuit.wires; - - auto report_fail = [&](const char* message, size_t row_idx) { - info(message, row_idx); - return false; + Params params; + + const Fq v = circuit.batching_challenge_v; + const Fq v2 = v * v; + const Fq v3 = v2 * v; + const Fq v4 = v3 * v; + + const auto x_limbs = Builder::split_fq_into_limbs(circuit.evaluation_input_x); + const auto v_limbs = Builder::split_fq_into_limbs(v); + const auto v2_limbs = Builder::split_fq_into_limbs(v2); + const auto v3_limbs = Builder::split_fq_into_limbs(v3); + const auto v4_limbs = Builder::split_fq_into_limbs(v4); + + // evaluation_input_x: 4 binary limbs + 1 native Fr representation + params.evaluation_input_x = { + x_limbs[0], x_limbs[1], x_limbs[2], x_limbs[3], Fr(uint256_t(circuit.evaluation_input_x)) }; - // 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; + // batching_challenge_v^1 through v^4: each has 4 binary limbs + 1 native Fr + params.batching_challenge_v[0] = { v_limbs[0], v_limbs[1], v_limbs[2], v_limbs[3], Fr(uint256_t(v)) }; + params.batching_challenge_v[1] = { v2_limbs[0], v2_limbs[1], v2_limbs[2], v2_limbs[3], Fr(uint256_t(v2)) }; + params.batching_challenge_v[2] = { v3_limbs[0], v3_limbs[1], v3_limbs[2], v3_limbs[3], Fr(uint256_t(v3)) }; + params.batching_challenge_v[3] = { v4_limbs[0], v4_limbs[1], v4_limbs[2], v4_limbs[3], Fr(uint256_t(v4)) }; + + // accumulated_result: the 4 binary limbs stored at RESULT_ROW. + // The AccumulatorTransferRelation verifies this matches the accumulator at the result row. + BB_ASSERT_GT(circuit.num_gates(), RESULT_ROW); + params.accumulated_result = { + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_0][RESULT_ROW]), + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_1][RESULT_ROW]), + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_2][RESULT_ROW]), + circuit.get_variable(circuit.wires[WireIds::ACCUMULATORS_BINARY_LIMBS_3][RESULT_ROW]), }; - /** - * @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; - }; - - auto check_binary_limbs_equality = [&](const std::vector& first, const std::vector& second, size_t gate) { - for (const auto [first_limb, second_limb] : zip_view(first, second)) { - if (first_limb != second_limb) { - return report_fail("Binary limbs are not equal = ", gate); - } - } - return true; - }; - - auto check_accumulator_transfer = [&](const std::vector& previous_accumulator, size_t gate) { - if (gate % 2 != 1) { - return report_fail("accumulator transfer should only be checked at odd gates = ", gate); - } - if (gate + 1 < circuit.num_gates() - 1) { - // Check that the next gate's current accumulator equals this gate's previous accumulator - const std::vector next_gate_current_accumulator = { - circuit.get_variable(accumulators_binary_limbs_0_wire[gate + 1]), - circuit.get_variable(accumulators_binary_limbs_1_wire[gate + 1]), - circuit.get_variable(accumulators_binary_limbs_2_wire[gate + 1]), - circuit.get_variable(accumulators_binary_limbs_3_wire[gate + 1]), - }; - if (!check_binary_limbs_equality(next_gate_current_accumulator, previous_accumulator, gate + 1)) { - return false; - } - } else { - // Check accumulator starts at zero - for (const auto& limb : previous_accumulator) { - if (limb != Fr(0)) { - return report_fail("accumulator doesn't start with 0 = ", gate + 1); - } - } - } - return true; - }; - - auto check_no_op = - [&](const std::vector& current_accumulator, const std::vector& previous_accumulator, size_t gate) { - if (!check_binary_limbs_equality(current_accumulator, previous_accumulator, gate)) { - return false; - } - return check_accumulator_transfer(previous_accumulator, gate + 1); - }; - - auto check_random_op_code = [&](const Fr op_code, size_t gate) { - if (gate % 2 == 0) { - if (op_code == Fr(0) || op_code == Fr(3) || op_code == Fr(4) || op_code == Fr(8)) { - return report_fail("Opcode should be random value at even gate = ", gate); - } - } else { - if (op_code == Fr(0)) { - return report_fail("Opcode should be 0 at odd gate = ", gate); - } - } - return true; - }; - - // TODO(https: // github.com/AztecProtocol/barretenberg/issues/1367): Report all failures more explicitly and - // consider making use of relations. - auto in_random_range = [&](size_t i) { - return (i >= 2 * Builder::NUM_NO_OPS_START && i < RESULT_ROW) || - (i >= circuit.num_gates() - (circuit.avm_mode ? 0 : 2 * Builder::NUM_RANDOM_OPS_END) && - i < circuit.num_gates()); - }; - for (size_t i = 2; i < circuit.num_gates() - 1; i += 2) { - - // Ensure random op is present in expected ranges - Fr op_code = circuit.get_variable(op_wire[i]); - if (in_random_range(i)) { - check_random_op_code(op_code, i); - Fr op_code_next = circuit.get_variable(op_wire[i + 1]); - check_random_op_code(op_code_next, i + 1); - continue; - } - - // 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]), - }; - - if (op_code == 0) { - if (!check_no_op(current_accumulator_binary_limbs, previous_accumulator_binary_limbs, i)) { - return false; - }; - continue; - } - - 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]); - - // 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) { - BB_ASSERT_EQ(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 report_fail("wide limb decomposition failied at row = ", i); - } - - enum LimbSeriesType { STANDARD_COORDINATE, Z_SCALAR, QUOTIENT }; + return params; +} - // 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); +void TranslatorCircuitChecker::populate_values(const Builder& circuit, AllValues& values, size_t row_idx) +{ + const size_t num_gates = circuit.num_gates(); + BB_ASSERT_LT(row_idx, num_gates); + + // ----------------------------------------------------------------------- + // Wire values at current row + // get_wires() returns 81 refs in WireIds order: [op, x_lo_y_hi, ..., range_constraints] + // This matches circuit.wires[0..80] exactly. + // ----------------------------------------------------------------------- + auto wire_refs = values.get_wires(); + for (size_t j = 0; j < Builder::WireIds::TOTAL_COUNT; j++) { + wire_refs[j] = circuit.get_variable(circuit.wires[j][row_idx]); + } + + // ----------------------------------------------------------------------- + // Shifted wire values (= values at next row, or zero at boundary). + // ShiftedEntities::get_all() returns 86 refs: + // [0..79] : shifts of circuit.wires[1..80] (x_lo_y_hi through last range constraint) + // [80..85] : shifts of ordered range constraints (0..4) and z_perm (not from circuit wires) + // ----------------------------------------------------------------------- + auto& shifted_base = static_cast&>(values); + auto shifted_refs = shifted_base.get_all(); + if (row_idx + 1 < num_gates) { + // circuit.wires[j+1] holds the wire that shifts to shifted_refs[j] + for (size_t j = 0; j < 80; j++) { + shifted_refs[j] = circuit.get_variable(circuit.wires[j + 1][row_idx + 1]); + } + } + // shifted_refs[80..85] (ordered range constraints + z_perm) remain zero; + // the relations that use them (Permutation, DeltaRange) are not checked here. + + // ----------------------------------------------------------------------- + // Lagrange selector values — computed analytically from the row index. + // + // Translator processes the trace in two regions per mini-circuit: + // [0, RANDOMNESS_START) : initialisation rows (rows 0..1) + // [RANDOMNESS_START, RESULT_ROW) : random no-op rows (lagrange_mini_masking) + // [RESULT_ROW, num_without_mask) : actual accumulation rows (even/odd processing) + // [num_without_mask, num_gates) : end-masking rows (lagrange_mini_masking, unless AVM mode) + // ----------------------------------------------------------------------- + const size_t end_masking_rows = circuit.avm_mode ? 0 : Flavor::NUM_MASKED_ROWS_END; + const size_t num_without_mask = (num_gates > end_masking_rows) ? (num_gates - end_masking_rows) : num_gates; + + const bool in_start_random_range = (row_idx >= Flavor::RANDOMNESS_START && row_idx < RESULT_ROW); + const bool in_end_random_range = (row_idx >= num_without_mask); + const bool in_processing_range = (row_idx >= RESULT_ROW && row_idx < num_without_mask); + const bool is_even = (row_idx % 2 == 0); + + values.lagrange_mini_masking = Fr(in_start_random_range || in_end_random_range ? 1 : 0); + values.lagrange_even_in_minicircuit = Fr(in_processing_range && is_even ? 1 : 0); + values.lagrange_odd_in_minicircuit = Fr(in_processing_range && !is_even ? 1 : 0); + values.lagrange_result_row = Fr(row_idx == RESULT_ROW ? 1 : 0); + values.lagrange_last_in_minicircuit = Fr(num_without_mask > 0 && row_idx == num_without_mask - 1 ? 1 : 0); +} - BB_ASSERT_EQ(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; - } - } +bool TranslatorCircuitChecker::check(const Builder& circuit) +{ + using OpcodeConstraint = TranslatorOpcodeConstraintRelation; + using AccumulatorTransfer = TranslatorAccumulatorTransferRelation; + using Decomposition = TranslatorDecompositionRelation; + using NonNativeField = TranslatorNonNativeFieldRelation; - 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])) { + const Params params = compute_relation_params(circuit); + AllValues values{}; - 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(); - } + for (size_t i = 0; i < circuit.num_gates(); ++i) { + populate_values(circuit, values, i); - 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)) { + if (!check_relation(values, params)) { + info("TranslatorCircuitChecker: Failed TranslatorOpcodeConstraintRelation at row = ", i); return false; } - if (!check_micro_limb_decomposition_correctness(z_1_binary_limbs, z_1_micro_chunks, Z_SCALAR)) { + if (!check_relation(values, params)) { + info("TranslatorCircuitChecker: Failed TranslatorAccumulatorTransferRelation at row = ", i); return false; } - if (!check_micro_limb_decomposition_correctness(z_2_binary_limbs, z_2_micro_chunks, Z_SCALAR)) { + if (!check_relation(values, params)) { + info("TranslatorCircuitChecker: Failed TranslatorDecompositionRelation at row = ", i); return false; } - if (!check_micro_limb_decomposition_correctness( - current_accumulator_binary_limbs, current_accumulator_micro_chunks, STANDARD_COORDINATE)) { + if (!check_relation(values, params)) { + info("TranslatorCircuitChecker: Failed TranslatorNonNativeFieldRelation at row = ", i); 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 - constexpr 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; - }; - - if (!check_accumulator_transfer(previous_accumulator_binary_limbs, i + 1)) { - return false; - } - }; + } return true; } -}; // namespace bb + +} // 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 index f128b4555bab..14956be5e94f 100644 --- a/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.hpp +++ b/barretenberg/cpp/src/barretenberg/circuit_checker/translator_circuit_checker.hpp @@ -1,11 +1,19 @@ #pragma once +#include "barretenberg/relations/relation_parameters.hpp" +#include "barretenberg/relations/translator_vm/translator_decomposition_relation.hpp" +#include "barretenberg/relations/translator_vm/translator_extra_relations.hpp" +#include "barretenberg/relations/translator_vm/translator_non_native_field_relation.hpp" #include "barretenberg/translator_vm/translator_circuit_builder.hpp" +#include "barretenberg/translator_vm/translator_flavor.hpp" namespace bb { class TranslatorCircuitChecker { - using Fr = bb::fr; - using Fq = bb::fq; using Builder = TranslatorCircuitBuilder; + using Flavor = TranslatorFlavor; + using Fr = Flavor::FF; + using Fq = Flavor::BF; using WireIds = Builder::WireIds; + using AllValues = Flavor::AllValues; + using Params = RelationParameters; // Number of limbs used to decompose a 254-bit value for modular arithmetic static constexpr size_t NUM_BINARY_LIMBS = Builder::NUM_BINARY_LIMBS; @@ -13,13 +21,6 @@ class TranslatorCircuitChecker { static constexpr size_t RESULT_ROW = Builder::RESULT_ROW; 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; /** @@ -37,24 +38,55 @@ class TranslatorCircuitChecker { } /** - * @brief Create limb representations of x and powers of v that are needed to compute the witness or check - * circuit correctness + * @brief Check the witness satisifies the circuit + * + * @details Goes through each gate and checks the correctness of accumulation using the Translator relations. + * Checks TranslatorOpcodeConstraintRelation, TranslatorAccumulatorTransferRelation, + * TranslatorDecompositionRelation, and TranslatorNonNativeFieldRelation for each row. * - * @param evaluation_input_x The point at which the polynomials are being evaluated - * @param batching_challenge_v The batching challenge - * @return RelationInputs + * Note: TranslatorPermutationRelation and TranslatorDeltaRangeConstraintRelation are not checked here + * because they require grand product polynomials (z_perm) and sorted range constraint polynomials + * that are only available at the prover level, not from the circuit builder directly. + * + * @return true if all relation constraints are satisfied, false otherwise */ - static RelationInputs compute_relation_inputs_limbs(const Fq& batching_challenge_v, const Fq& evaluation_input_x); + static bool check(const Builder& circuit); + private: /** - * @brief Check the witness satisifies the circuit + * @brief Build the RelationParameters from the circuit's public inputs. * - * @details Goes through each gate and checks the correctness of accumulation + * @details Populates evaluation_input_x (4 binary limbs + 1 native Fr), + * batching_challenge_v powers (4 sets of 5 limbs), and accumulated_result (4 limbs). + */ + static Params compute_relation_params(const Builder& circuit); + + /** + * @brief Populate an AllValues struct for a single row of the circuit. * - * @return true - * @return false + * @details Sets wire values from the circuit at row_idx, shifted wire values from row_idx+1 + * (or zero at the last row), and computes Lagrange selector values analytically. */ + static void populate_values(const Builder& circuit, AllValues& values, size_t row_idx); - static bool check(const Builder& circuit); + /** + * @brief Check that a given relation evaluates to zero for the provided row values. + * + * @tparam Relation The relation type to check + */ + template static bool check_relation(const AllValues& values, const Params& params) + { + typename Relation::SumcheckArrayOfValuesOverSubrelations evals; + for (auto& e : evals) { + e = Fr(0); + } + Relation::accumulate(evals, values, params, Fr(1)); + for (auto& e : evals) { + if (e != Fr(0)) { + return false; + } + } + return true; + } }; } // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/honk/relation_checker.hpp b/barretenberg/cpp/src/barretenberg/honk/relation_checker.hpp index a4b9096abe9c..a184c0fe635a 100644 --- a/barretenberg/cpp/src/barretenberg/honk/relation_checker.hpp +++ b/barretenberg/cpp/src/barretenberg/honk/relation_checker.hpp @@ -4,6 +4,10 @@ #include "barretenberg/common/log.hpp" #include "barretenberg/flavor/mega_flavor.hpp" #include "barretenberg/flavor/ultra_flavor.hpp" +#include "barretenberg/relations/translator_vm/translator_decomposition_relation.hpp" +#include "barretenberg/relations/translator_vm/translator_extra_relations.hpp" +#include "barretenberg/relations/translator_vm/translator_non_native_field_relation.hpp" +#include "barretenberg/translator_vm/translator_flavor.hpp" namespace bb { @@ -183,6 +187,33 @@ template <> class RelationChecker : public RelationChecker { return all_subrelation_failures; } }; -} // namespace bb -// namespace bb +// Specialization for TranslatorFlavor: checks the four row-by-row relations that do not require +// grand product polynomials (Permutation and DeltaRangeConstraint are excluded as they need z_perm +// and sorted ordered_range_constraints polynomials computed during proving). +template <> class RelationChecker : public RelationChecker { + using Base = RelationChecker; + + public: + static AllSubrelationFailures check_all(const auto& polynomials, const auto& params) + { + using FF = TranslatorFlavor::FF; + AllSubrelationFailures all_subrelation_failures; + + auto try_check = [&](const char* name) { + auto failures = Base::check(polynomials, params, name); + if (!failures.empty()) { + all_subrelation_failures[name] = failures; + } + }; + + try_check.template operator()>("TranslatorOpcodeConstraint"); + try_check.template operator()>("TranslatorAccumulatorTransfer"); + try_check.template operator()>("TranslatorDecomposition"); + try_check.template operator()>("TranslatorNonNativeField"); + + return all_subrelation_failures; + } +}; + +} // namespace bb 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 b4c2c510650a..931550a9c878 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.cpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.cpp @@ -41,58 +41,6 @@ TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_w const Fq& evaluation_input_x) { - /** - * @brief A small function to transform a uint512_t element into its 4 68-bit limbs in Fr scalars - * - * @details Split and integer stored in uint512_T into 4 68-bit chunks (we assume that it is lower than 2²⁷²), - * convert to Fr - */ - auto uint512_t_to_limbs = [](const uint512_t& original) { - return std::array{ Fr(original.slice(0, NUM_LIMB_BITS).lo), - Fr(original.slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS).lo), - Fr(original.slice(2 * NUM_LIMB_BITS, 3 * NUM_LIMB_BITS).lo), - Fr(original.slice(3 * NUM_LIMB_BITS, 4 * NUM_LIMB_BITS).lo) }; - }; - - /** - * @brief A function for splitting wide limbs (P_x_lo, P_y_hi, etc) into two limbs - */ - auto split_wide_limb_into_2_limbs = [](const Fr& wide_limb) { - return std::array{ Fr(uint256_t(wide_limb).slice(0, NUM_LIMB_BITS)), - Fr(uint256_t(wide_limb).slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS)) }; - }; - - /** - * @brief A function to split a limb into microlimbs for range constraints - * - * @details Splits a limb of arbitrary bit size into 14-bit microlimbs. For partial microlimbs, - * stores both the actual value and its shifted version for proper range constraint handling. - * Always returns NUM_MICRO_LIMBS (6) elements, padding with zeros if needed. - */ - auto split_limb_into_microlimbs = [](const Fr& limb, const size_t num_bits) { - static_assert(MICRO_LIMB_BITS == 14); - size_t num_full_micro_limbs = num_bits / MICRO_LIMB_BITS; - size_t last_limb_bits = num_bits % MICRO_LIMB_BITS; - std::array microlimbs{}; - - // Fill in the full 14-bit microlimbs - for (size_t i = 0; i < num_full_micro_limbs; ++i) { - microlimbs[i] = uint256_t(limb).slice(i * MICRO_LIMB_BITS, (i + 1) * MICRO_LIMB_BITS); - } - - // If there's a partial microlimb at the end, store both actual microlimb and its tail - if (last_limb_bits > 0) { - // Extract up to the next 14-bit boundary (actual) - microlimbs[num_full_micro_limbs] = uint256_t(limb).slice(num_full_micro_limbs * MICRO_LIMB_BITS, - (num_full_micro_limbs + 1) * MICRO_LIMB_BITS); - - // Store the shifted version in the next slot (tail microlimb) - microlimbs[num_full_micro_limbs + 1] = uint256_t(microlimbs[num_full_micro_limbs]) - << (MICRO_LIMB_BITS - last_limb_bits); - } - return microlimbs; - }; - // x and v are challenges: random values unknown at compile time, treated as witnesses. Fq v_squared = batching_challenge_v * batching_challenge_v; Fq v_cubed = v_squared * batching_challenge_v; @@ -351,19 +299,6 @@ void TranslatorCircuitBuilder::assert_well_formed_accumulation_input(const Accum BB_ASSERT_EQ(acc_step.ultra_op.z_1, acc_step.z_1_limbs[0] + acc_step.z_1_limbs[1] * SHIFT_1); BB_ASSERT_EQ(acc_step.ultra_op.z_2, acc_step.z_2_limbs[0] + acc_step.z_2_limbs[1] * SHIFT_1); - /** - * @brief Check correctness of limbs values - * - */ - auto check_binary_limbs_maximum_values = [](const std::array& limbs, - const uint256_t& MAX_LAST_LIMB = - (uint256_t(1) << NUM_LAST_LIMB_BITS)) { - for (size_t i = 0; i < total_limbs - 1; i++) { - BB_ASSERT_LT(uint256_t(limbs[i]), SHIFT_1); - } - BB_ASSERT_LT(uint256_t(limbs[total_limbs - 1]), MAX_LAST_LIMB); - }; - 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); // Check limb values are in 68-bit range @@ -376,15 +311,6 @@ void TranslatorCircuitBuilder::assert_well_formed_accumulation_input(const Accum check_binary_limbs_maximum_values(acc_step.quotient_binary_limbs, /*MAX_LAST_LIMB=*/MAX_QUOTIENT_LAST_LIMB); // 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++) { - BB_ASSERT_LT(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); @@ -471,17 +397,6 @@ 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 A function to place an array of values into sequential wires starting from a given wire ID - */ - 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); lay_limbs_in_row(acc_step.P_x_microlimbs[1], P_X_LOW_LIMBS_RANGE_CONSTRAINT_0); @@ -532,17 +447,6 @@ void TranslatorCircuitBuilder::feed_ecc_op_queue_into_circuit(const std::shared_ } increment_num_gates(2); - auto process_random_op = [&](const UltraOp& ultra_op) { - BB_ASSERT(ultra_op.op_code.is_random_op, "function should only be called to process a random op"); - populate_wires_from_ultra_op(ultra_op); - // Populate the other wires with zeros - for (size_t i = WireIds::P_X_LOW_LIMBS; i < wires.size(); i++) { - wires[i].push_back(zero_idx()); - wires[i].push_back(zero_idx()); - } - increment_num_gates(2); - }; - // When encountering the random operations in the op queue, populate the op wire without creating accumulation gates // These are present in the op queue at the beginning and end to ensure commitments and evaluations to op queue // polynomials do not reveal information about data in the op queue @@ -633,4 +537,39 @@ void TranslatorCircuitBuilder::feed_ecc_op_queue_into_circuit(const std::shared_ process_random_op(ultra_ops[i]); } } +std::array TranslatorCircuitBuilder:: + split_limb_into_microlimbs(const Fr& limb, size_t num_bits) +{ + static_assert(MICRO_LIMB_BITS == 14); + const size_t num_full_micro_limbs = num_bits / MICRO_LIMB_BITS; + const size_t last_limb_bits = num_bits % MICRO_LIMB_BITS; + std::array microlimbs{}; + + // Fill in the full 14-bit microlimbs + for (size_t i = 0; i < num_full_micro_limbs; ++i) { + microlimbs[i] = uint256_t(limb).slice(i * MICRO_LIMB_BITS, (i + 1) * MICRO_LIMB_BITS); + } + + // If there's a partial microlimb at the end, store both actual microlimb and its tail + if (last_limb_bits > 0) { + microlimbs[num_full_micro_limbs] = + uint256_t(limb).slice(num_full_micro_limbs * MICRO_LIMB_BITS, (num_full_micro_limbs + 1) * MICRO_LIMB_BITS); + microlimbs[num_full_micro_limbs + 1] = uint256_t(microlimbs[num_full_micro_limbs]) + << (MICRO_LIMB_BITS - last_limb_bits); + } + return microlimbs; +} + +void TranslatorCircuitBuilder::process_random_op(const UltraOp& ultra_op) +{ + BB_ASSERT(ultra_op.op_code.is_random_op, "function should only be called to process a random op"); + populate_wires_from_ultra_op(ultra_op); + // Populate the other wires with zeros + for (size_t i = WireIds::P_X_LOW_LIMBS; i < wires.size(); i++) { + wires[i].push_back(zero_idx()); + wires[i].push_back(zero_idx()); + } + increment_num_gates(2); +} + } // namespace bb 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 e1be80d48ab7..56d8b7109fe8 100644 --- a/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/translator_vm/translator_circuit_builder.hpp @@ -438,6 +438,76 @@ class TranslatorCircuitBuilder : public CircuitBuilderBase { const Fq& previous_accumulator, const Fq& batching_challenge_v, const Fq& evaluation_input_x); + + private: + /** + * @brief Convert a uint512_t value into its 4 68-bit limbs as Fr scalars. + */ + static std::array uint512_t_to_limbs(const uint512_t& original) + { + return { Fr(original.slice(0, NUM_LIMB_BITS).lo), + Fr(original.slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS).lo), + Fr(original.slice(2 * NUM_LIMB_BITS, 3 * NUM_LIMB_BITS).lo), + Fr(original.slice(3 * NUM_LIMB_BITS, 4 * NUM_LIMB_BITS).lo) }; + } + + /** + * @brief Split a 136-bit Fr value (wide limb) into two 68-bit limbs. + */ + static std::array split_wide_limb_into_2_limbs(const Fr& wide_limb) + { + return { Fr(uint256_t(wide_limb).slice(0, NUM_LIMB_BITS)), + Fr(uint256_t(wide_limb).slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS)) }; + } + + /** + * @brief Split a limb of arbitrary bit size into 14-bit micro-limbs for range constraints. + */ + static std::array split_limb_into_microlimbs(const Fr& limb, size_t num_bits); + + /** + * @brief Assert that all standard limbs are < 2^68 and the last limb is < MAX_LAST_LIMB. + */ + template + static void check_binary_limbs_maximum_values(const std::array& limbs, + const uint256_t& MAX_LAST_LIMB = (uint256_t(1) << NUM_LAST_LIMB_BITS)) + { + for (size_t i = 0; i < total_limbs - 1; i++) { + BB_ASSERT_LT(uint256_t(limbs[i]), SHIFT_1); + } + BB_ASSERT_LT(uint256_t(limbs[total_limbs - 1]), MAX_LAST_LIMB); + } + + /** + * @brief Assert that all micro-limbs are < 2^14. + */ + template + static void 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++) { + BB_ASSERT_LT(uint256_t(limbs[i][j]), MICRO_SHIFT); + } + } + } + + /** + * @brief Place array_size Fr values into consecutive wire slots starting at starting_wire. + */ + template void lay_limbs_in_row(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++; + } + } + + /** + * @brief Populate wires for a random op (op wire filled, all other wires zero-filled). + */ + void process_random_op(const UltraOp& ultra_op); }; } // namespace bb