translator_circuit_builder.cpp

Go to the documentation of this file.

// === AUDIT STATUS ===
// internal:    { status: Planned, auditors: [], commit: }
// external_1:  { status: not started, auditors: [], commit: }
// external_2:  { status: not started, auditors: [], commit: }
// =====================
 
#include "translator_circuit_builder.hpp"
#include "barretenberg/common/assert.hpp"
#include "barretenberg/common/bb_bench.hpp"
#include "barretenberg/ecc/curves/bn254/fr.hpp"
#include "barretenberg/numeric/uint256/uint256.hpp"
#include "barretenberg/op_queue/ecc_op_queue.hpp"
 
#include <cstddef>
namespace bb {
 
TranslatorCircuitBuilder::AccumulationInput TranslatorCircuitBuilder::generate_witness_values(
    const UltraOp& ultra_op,
    const Fq& previous_accumulator,
    const Fq& batching_challenge_v,
    const Fq& evaluation_input_x)
{
 
    // 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;
    Fq v_quarted = v_cubed * batching_challenge_v;
 
    // Convert the accumulator, powers of v and x into "bigfield" form
    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
    size_t op_code = ultra_op.op_code.value();
    auto uint_previous_accumulator = uint512_t(previous_accumulator);
    auto uint_x = uint512_t(evaluation_input_x);
    auto uint_op = uint512_t(op_code);
    // Use get_base_point_standard_form() so infinity points are consistently mapped to (0,0)
    const auto [base_p_x, base_p_y] = ultra_op.get_base_point_standard_form();
    auto uint_p_x = uint512_t(base_p_x);
    auto uint_p_y = uint512_t(base_p_y);
    auto uint_z1 = uint512_t(ultra_op.z_1);
    auto uint_z2 = uint512_t(ultra_op.z_2);
    auto uint_v = uint512_t(batching_challenge_v);
    auto uint_v_squared = uint512_t(v_squared);
    auto uint_v_cubed = uint512_t(v_cubed);
    auto uint_v_quarted = uint512_t(v_quarted);
 
    Fq base_op = Fq(uint256_t(op_code));
    Fq base_z_1 = Fq(uint256_t(ultra_op.z_1));
    Fq base_z_2 = Fq(uint256_t(ultra_op.z_2));
 
    // Construct bigfield representations of P.x and P.y from the infinity-safe coordinates
    auto p_x_limbs = split_fq_into_limbs(base_p_x);
    auto p_y_limbs = split_fq_into_limbs(base_p_y);
 
    // Construct bigfield representations of ultra_op.z_1 and ultra_op.z_2 only using 2 limbs each
    auto z_1_limbs = split_wide_limb_into_2_limbs(ultra_op.z_1);
    auto z_2_limbs = split_wide_limb_into_2_limbs(ultra_op.z_2);
 
    // 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)
    // clang-format off
    const Fq remainder = previous_accumulator * evaluation_input_x +
                         base_op                                   +
                         base_p_x * batching_challenge_v           +
                         base_p_y * v_squared                      +
                         base_z_1 * v_cubed                        +
                         base_z_2 * v_quarted;
 
    // We also need to compute the quotient
    uint512_t quotient_by_modulus = uint_previous_accumulator * uint_x +
                                    uint_op                            +
                                    uint_p_x * uint_v                  +
                                    uint_p_y * uint_v_squared          +
                                    uint_z1  * uint_v_cubed            +
                                    uint_z2  * uint_v_quarted          -
                                    uint512_t(remainder);
    // clang-format on
 
    uint512_t quotient = quotient_by_modulus / uint512_t(Fq::modulus);
 
    BB_ASSERT_EQ(quotient_by_modulus, quotient * uint512_t(Fq::modulus));
 
    // Compute quotient and remainder bigfield representation
    auto remainder_limbs = split_fq_into_limbs(remainder);
    std::array<Fr, NUM_BINARY_LIMBS> 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
    // the high part (0*1, 1*0) multiplied by a single limb shift
    // clang-format off
    Fr low_wide_relation_limb_part_1 =
        previous_accumulator_limbs[0] * x_witnesses[0]            +
        op_code                                                   +
        p_x_limbs[0]                  * v_witnesses[0]            +
        p_y_limbs[0]                  * v_squared_witnesses[0]    +
        z_1_limbs[0]                  * v_cubed_witnesses[0]      +
        z_2_limbs[0]                  * v_quarted_witnesses[0]    +
        quotient_limbs[0]             * NEGATIVE_MODULUS_LIMBS[0] -
        remainder_limbs[0];
 
    Fr low_wide_relation_limb =
        low_wide_relation_limb_part_1 +
        (previous_accumulator_limbs[1] * x_witnesses[0]            +
         previous_accumulator_limbs[0] * x_witnesses[1]            +
         p_x_limbs[0]                  * v_witnesses[1]            +
         p_x_limbs[1]                  * v_witnesses[0]            +
         p_y_limbs[0]                  * v_squared_witnesses[1]    +
         p_y_limbs[1]                  * v_squared_witnesses[0]    +
         z_1_limbs[0]                  * v_cubed_witnesses[1]      +
         z_1_limbs[1]                  * v_cubed_witnesses[0]      +
         z_2_limbs[0]                  * v_quarted_witnesses[1]    +
         z_2_limbs[1]                  * v_quarted_witnesses[0]    +
         quotient_limbs[0]             * NEGATIVE_MODULUS_LIMBS[1] +
         quotient_limbs[1]             * NEGATIVE_MODULUS_LIMBS[0] -
         remainder_limbs[1]) * SHIFT_1;
    // clang-format on
 
    // Low bits have to be zero
    BB_ASSERT_EQ(uint256_t(low_wide_relation_limb).slice(0, 2 * NUM_LIMB_BITS), 0U);
 
    Fr low_wide_relation_limb_divided = low_wide_relation_limb * SHIFT_2_INVERSE;
 
    // The high relation limb is the accumulation of the low limb divided by 2¹³⁶ and the combination of limbs with
    // indices (0*2,1*1,2*0) with limbs with indices (0*3,1*2,2*1,3*0) multiplied by 2⁶⁸
    // clang-format off
    Fr high_wide_relation_limb_part_1 =
        low_wide_relation_limb_divided                            +
        previous_accumulator_limbs[2] * x_witnesses[0]            +
        previous_accumulator_limbs[1] * x_witnesses[1]            +
        previous_accumulator_limbs[0] * x_witnesses[2]            +
        p_x_limbs[0]                  * v_witnesses[2]            +
        p_x_limbs[1]                  * v_witnesses[1]            +
        p_x_limbs[2]                  * v_witnesses[0]            +
        p_y_limbs[0]                  * v_squared_witnesses[2]    +
        p_y_limbs[1]                  * v_squared_witnesses[1]    +
        p_y_limbs[2]                  * v_squared_witnesses[0]    +
        z_1_limbs[0]                  * v_cubed_witnesses[2]      +
        z_1_limbs[1]                  * v_cubed_witnesses[1]      +
        z_2_limbs[0]                  * v_quarted_witnesses[2]    +
        z_2_limbs[1]                  * v_quarted_witnesses[1]    +
        quotient_limbs[2]             * NEGATIVE_MODULUS_LIMBS[0] +
        quotient_limbs[1]             * NEGATIVE_MODULUS_LIMBS[1] +
        quotient_limbs[0]             * NEGATIVE_MODULUS_LIMBS[2] -
        remainder_limbs[2];
 
    Fr high_wide_relation_limb =
        high_wide_relation_limb_part_1 +
        (previous_accumulator_limbs[3] * x_witnesses[0]            +
         previous_accumulator_limbs[2] * x_witnesses[1]            +
         previous_accumulator_limbs[1] * x_witnesses[2]            +
         previous_accumulator_limbs[0] * x_witnesses[3]            +
         p_x_limbs[0]                  * v_witnesses[3]            +
         p_x_limbs[1]                  * v_witnesses[2]            +
         p_x_limbs[2]                  * v_witnesses[1]            +
         p_x_limbs[3]                  * v_witnesses[0]            +
         p_y_limbs[0]                  * v_squared_witnesses[3]    +
         p_y_limbs[1]                  * v_squared_witnesses[2]    +
         p_y_limbs[2]                  * v_squared_witnesses[1]    +
         p_y_limbs[3]                  * v_squared_witnesses[0]    +
         z_1_limbs[0]                  * v_cubed_witnesses[3]      +
         z_1_limbs[1]                  * v_cubed_witnesses[2]      +
         z_2_limbs[0]                  * v_quarted_witnesses[3]    +
         z_2_limbs[1]                  * v_quarted_witnesses[2]    +
         quotient_limbs[3]             * NEGATIVE_MODULUS_LIMBS[0] +
         quotient_limbs[2]             * NEGATIVE_MODULUS_LIMBS[1] +
         quotient_limbs[1]             * NEGATIVE_MODULUS_LIMBS[2] +
         quotient_limbs[0]             * NEGATIVE_MODULUS_LIMBS[3] -
         remainder_limbs[3]) * SHIFT_1;
    // clang-format on
 
    // Check that the results lower 136 bits are zero
    BB_ASSERT_EQ(uint256_t(high_wide_relation_limb).slice(0, 2 * NUM_LIMB_BITS), 0U);
 
    // Get divided version
    auto high_wide_relation_limb_divided = high_wide_relation_limb * SHIFT_2_INVERSE;
 
    const auto last_limb_index = NUM_BINARY_LIMBS - 1;
 
    std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> P_x_microlimbs;
    std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> P_y_microlimbs;
    std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_Z_LIMBS> z_1_microlimbs;
    std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_Z_LIMBS> z_2_microlimbs;
    std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> current_accumulator_microlimbs;
    std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> quotient_microlimbs;
 
    // Split all standard limbs (68-bit) into microlimbs for range constraining
    for (size_t i = 0; i < last_limb_index; i++) {
        P_x_microlimbs[i] = split_limb_into_microlimbs(p_x_limbs[i], NUM_LIMB_BITS);
        P_y_microlimbs[i] = split_limb_into_microlimbs(p_y_limbs[i], NUM_LIMB_BITS);
        current_accumulator_microlimbs[i] = split_limb_into_microlimbs(remainder_limbs[i], NUM_LIMB_BITS);
        quotient_microlimbs[i] = split_limb_into_microlimbs(quotient_limbs[i], NUM_LIMB_BITS);
    }
 
    // Split top limbs (varying bit sizes) into microlimbs
    P_x_microlimbs[last_limb_index] = split_limb_into_microlimbs(p_x_limbs[last_limb_index], NUM_LAST_LIMB_BITS);
    P_y_microlimbs[last_limb_index] = split_limb_into_microlimbs(p_y_limbs[last_limb_index], NUM_LAST_LIMB_BITS);
    current_accumulator_microlimbs[last_limb_index] =
        split_limb_into_microlimbs(remainder_limbs[last_limb_index], NUM_LAST_LIMB_BITS);
    quotient_microlimbs[last_limb_index] =
        split_limb_into_microlimbs(quotient_limbs[last_limb_index], NUM_LAST_QUOTIENT_LIMB_BITS);
 
    // Split z scalars into microlimbs (handled separately due to different limb count)
    for (size_t i = 0; i < NUM_Z_LIMBS - 1; i++) {
        z_1_microlimbs[i] = split_limb_into_microlimbs(z_1_limbs[i], NUM_LIMB_BITS);
        z_2_microlimbs[i] = split_limb_into_microlimbs(z_2_limbs[i], NUM_LIMB_BITS);
    }
    z_1_microlimbs[NUM_Z_LIMBS - 1] =
        split_limb_into_microlimbs(z_1_limbs[NUM_Z_LIMBS - 1], NUM_Z_BITS - NUM_LIMB_BITS);
    z_2_microlimbs[NUM_Z_LIMBS - 1] =
        split_limb_into_microlimbs(z_2_limbs[NUM_Z_LIMBS - 1], NUM_Z_BITS - NUM_LIMB_BITS);
 
    // Start filling the witness container
    AccumulationInput input{
        .ultra_op = ultra_op,
        .P_x_limbs = p_x_limbs,
        .P_x_microlimbs = P_x_microlimbs,
        .P_y_limbs = p_y_limbs,
        .P_y_microlimbs = P_y_microlimbs,
        .z_1_limbs = z_1_limbs,
        .z_1_microlimbs = z_1_microlimbs,
        .z_2_limbs = z_2_limbs,
        .z_2_microlimbs = z_2_microlimbs,
        .previous_accumulator = previous_accumulator_limbs,
        .current_accumulator = remainder_limbs,
        .current_accumulator_microlimbs = current_accumulator_microlimbs,
        .quotient_binary_limbs = quotient_limbs,
        .quotient_microlimbs = quotient_microlimbs,
        .relation_wide_limbs = { low_wide_relation_limb_divided, high_wide_relation_limb_divided },
        .relation_wide_microlimbs = { split_limb_into_microlimbs(low_wide_relation_limb_divided,
                                                                 RELATION_WIDE_LIMB_BITS),
                                      split_limb_into_microlimbs(high_wide_relation_limb_divided,
                                                                 RELATION_WIDE_LIMB_BITS) },
 
    };
 
    return input;
}
 
void TranslatorCircuitBuilder::assert_well_formed_ultra_op(const UltraOp& ultra_op)
{
    // Opcode should be {0,3,4,8}
    size_t op_code = ultra_op.op_code.value();
    BB_ASSERT(op_code == 0 || op_code == 3 || op_code == 4 || op_code == 8);
 
    // Check and insert x_lo and y_hi into wire 1
    BB_ASSERT_LTE(uint256_t(ultra_op.x_lo), MAX_LOW_WIDE_LIMB_SIZE);
    BB_ASSERT_LTE(uint256_t(ultra_op.y_hi), MAX_HIGH_WIDE_LIMB_SIZE);
 
    // Check and insert x_hi and z_1 into wire 2
    BB_ASSERT_LTE(uint256_t(ultra_op.x_hi), MAX_HIGH_WIDE_LIMB_SIZE);
    BB_ASSERT_LTE(uint256_t(ultra_op.z_1), MAX_Z_LIMB_SIZE);
 
    // Check and insert y_lo and z_2 into wire 3
    BB_ASSERT_LTE(uint256_t(ultra_op.y_lo), MAX_LOW_WIDE_LIMB_SIZE);
    BB_ASSERT_LTE(uint256_t(ultra_op.z_2), MAX_Z_LIMB_SIZE);
}
 
void TranslatorCircuitBuilder::assert_well_formed_accumulation_input(const AccumulationInput& acc_step)
{
    // The first wires OpQueue/Transcript wires
    assert_well_formed_ultra_op(acc_step.ultra_op);
 
    // Check decomposition of values from the Queue into limbs used in bigfield evaluations
    BB_ASSERT_EQ(acc_step.ultra_op.x_lo, acc_step.P_x_limbs[0] + acc_step.P_x_limbs[1] * SHIFT_1);
    BB_ASSERT_EQ(acc_step.ultra_op.x_hi, acc_step.P_x_limbs[2] + acc_step.P_x_limbs[3] * SHIFT_1);
    BB_ASSERT_EQ(acc_step.ultra_op.y_lo, acc_step.P_y_limbs[0] + acc_step.P_y_limbs[1] * SHIFT_1);
    BB_ASSERT_EQ(acc_step.ultra_op.y_hi, acc_step.P_y_limbs[2] + acc_step.P_y_limbs[3] * SHIFT_1);
    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);
 
    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
    check_binary_limbs_maximum_values(acc_step.P_x_limbs);
    check_binary_limbs_maximum_values(acc_step.P_y_limbs);
    check_binary_limbs_maximum_values(acc_step.z_1_limbs, /*MAX_LAST_LIMB=*/MAX_Z_LAST_LIMB);
    check_binary_limbs_maximum_values(acc_step.z_2_limbs, /*MAX_LAST_LIMB=*/MAX_Z_LAST_LIMB);
    check_binary_limbs_maximum_values(acc_step.previous_accumulator);
    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);
 
    // Check limbs used in range constraints are in range
    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);
    check_micro_limbs_maximum_values(acc_step.z_2_microlimbs);
    check_micro_limbs_maximum_values(acc_step.current_accumulator_microlimbs);
 
    // Check that relation limbs are in range
    BB_ASSERT_LT(uint256_t(acc_step.relation_wide_limbs[0]), MAX_RELATION_WIDE_LIMB_SIZE);
    BB_ASSERT_LT(uint256_t(acc_step.relation_wide_limbs[1]), MAX_RELATION_WIDE_LIMB_SIZE);
}
 
void TranslatorCircuitBuilder::populate_wires_from_ultra_op(const UltraOp& ultra_op)
{
    auto& op_wire = std::get<WireIds::OP>(wires);
    if (ultra_op.op_code.is_random_op) {
        op_wire.push_back(add_variable(fr(ultra_op.op_code.random_value_1)));
        op_wire.push_back(add_variable(fr(ultra_op.op_code.random_value_2)));
    } else {
        op_wire.push_back(add_variable(fr(ultra_op.op_code.value())));
        // Similarly to the ColumnPolynomials in the merge protocol, the op_wire is 0 at every second index for a
        // genuine op
        op_wire.push_back(zero_idx());
    }
    insert_pair_into_wire(WireIds::X_LOW_Y_HI, ultra_op.x_lo, ultra_op.y_hi);
 
    insert_pair_into_wire(WireIds::X_HIGH_Z_1, ultra_op.x_hi, ultra_op.z_1);
 
    insert_pair_into_wire(WireIds::Y_LOW_Z_2, ultra_op.y_lo, ultra_op.z_2);
}
 
void TranslatorCircuitBuilder::create_accumulation_gate(const AccumulationInput& acc_step)
{
    assert_well_formed_accumulation_input(acc_step);
 
    populate_wires_from_ultra_op(acc_step.ultra_op);
 
    // 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];
    auto high_relation_microlimbs = acc_step.relation_wide_microlimbs[1];
 
    // We have 4 wires specifically for the relation microlimbs
    insert_pair_into_wire(
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_0, low_relation_microlimbs[0], high_relation_microlimbs[0]);
    insert_pair_into_wire(
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_1, low_relation_microlimbs[1], high_relation_microlimbs[1]);
    insert_pair_into_wire(
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_2, low_relation_microlimbs[2], high_relation_microlimbs[2]);
    insert_pair_into_wire(
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_3, low_relation_microlimbs[3], high_relation_microlimbs[3]);
 
    // Next ones go into top P_x and P_y, current accumulator and quotient unused microlimbs
 
    // Insert the second highest low relation microlimb into the space left in P_x range constraints highest wire
    auto top_p_x_microlimbs = acc_step.P_x_microlimbs[NUM_BINARY_LIMBS - 1];
    top_p_x_microlimbs[NUM_MICRO_LIMBS - 1] = low_relation_microlimbs[NUM_MICRO_LIMBS - 2];
 
    // Insert the second highest high relation microlimb into the space left in P_y range constraints highest wire
    auto top_p_y_microlimbs = acc_step.P_y_microlimbs[NUM_BINARY_LIMBS - 1];
    top_p_y_microlimbs[NUM_MICRO_LIMBS - 1] = high_relation_microlimbs[NUM_MICRO_LIMBS - 2];
 
    // The highest low relation microlimb goes into the crevice left in current accumulator microlimbs
    auto top_current_accumulator_microlimbs = acc_step.current_accumulator_microlimbs[NUM_BINARY_LIMBS - 1];
    top_current_accumulator_microlimbs[NUM_MICRO_LIMBS - 1] = low_relation_microlimbs[NUM_MICRO_LIMBS - 1];
 
    // The highest high relation microlimb goes into the quotient crevice
    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];
 
    // 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);
    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);
 
    increment_num_gates(2);
 
    // Check that all the wires are filled equally
    bb::constexpr_for<0, TOTAL_COUNT, 1>([&]<size_t i>() { BB_ASSERT_EQ(std::get<i>(wires).size(), num_gates()); });
}
 
void TranslatorCircuitBuilder::feed_ecc_op_queue_into_circuit(const std::shared_ptr<ECCOpQueue>& ecc_op_queue)
{
    BB_BENCH_NAME("TranslatorCircuitBuilder::feed_ecc_op_queue_into_circuit");
    using Fq = bb::fq;
    // If in AVM mode, we use the non-zk reconstructed ultra ops as the structure required by Translator is added by the
    // GoblinAVM constructor. In Chonk, this structure is given by the zk columns, so we use the zk reconstructed
    // ultra ops.
    const auto& ultra_ops =
        avm_mode ? ecc_op_queue->get_no_zk_reconstructed_ultra_ops() : ecc_op_queue->get_zk_reconstructed_ultra_ops();
    std::vector<Fq> accumulator_trace;
    Fq current_accumulator(0);
    if (ultra_ops.empty()) {
        return;
    }
 
    // Handle the initial UltraOp (a no-op) by filling the start of all wire polynomials with zeros. This ensures
    // all translator wire polynomials begin with 0, which is necessary for shifted polynomials in the proving system.
    // Although only the first index needs to be zero, we add two zeros to maintain consistency since each actual
    // UltraOp populates two polynomial indices.
    for (auto& wire : wires) {
        wire.push_back(zero_idx());
        wire.push_back(zero_idx());
    }
    increment_num_gates(2);
 
    for (size_t i = 0; i < NUM_NO_OPS_START; i++) {
        BB_ASSERT(ultra_ops[i].op_code.value() == 0, "Expected no-op at the start of the op queue");
    }
 
    // Process random operations at the start of the op queue (after the initial no-op), no accumulation gates needed.
    // These ensure commitments and evaluations do not reveal information about op queue content.
    for (size_t i = NUM_NO_OPS_START; i < NUM_NO_OPS_START + NUM_RANDOM_OPS_START; ++i) {
        process_random_op(ultra_ops[i]);
    }
 
    // Guard against unsigned wraparound when computing ops_end below
    const size_t min_ops = NUM_NO_OPS_START + NUM_RANDOM_OPS_START + (avm_mode ? 0 : NUM_RANDOM_OPS_END);
    BB_ASSERT(ultra_ops.size() >= min_ops, "Op queue too small for Translator circuit construction");
 
    const size_t ops_end = avm_mode ? ultra_ops.size() : ultra_ops.size() - NUM_RANDOM_OPS_END;
    // Range of UltraOps for which we should construct accumulation gates
    std::span ultra_ops_span(ultra_ops.begin() + static_cast<std::ptrdiff_t>(NUM_NO_OPS_START + NUM_RANDOM_OPS_START),
                             ultra_ops.begin() + static_cast<std::ptrdiff_t>(ops_end));
 
    // Pre-compute accumulator values for each step since the circuit processes values in reverse order
    // and requires knowledge of the previous accumulator to construct each gate. Both accumulator computation
    // and gate creation skip the random operations at the beginning and end of the op queue and any zero-opcode
    // padding ops, as these should not influence the final accumulation result (located at index RESULT_ROW).
    // The accumulation result is sent as part of the Chonk proof, and so we add a genuine operation with
    // randomly generated values during Chonk execution to ensure no information about the rest of the ops is
    // leaked. Accumulator pre-computation is achieved by processing the queue in reverse order.
    for (const auto& ultra_op : std::ranges::reverse_view(ultra_ops_span)) {
        if (ultra_op.op_code.value() == 0) {
            //  Skip no-ops as they should not affect the computation of the accumulator
            continue;
        }
        current_accumulator *= evaluation_input_x;
        const auto [x_fq, y_fq] = ultra_op.get_base_point_standard_form();
        current_accumulator +=
            Fq(ultra_op.op_code.value()) +
            batching_challenge_v *
                (x_fq + batching_challenge_v *
                            (y_fq + batching_challenge_v *
                                        (uint256_t(ultra_op.z_1) + batching_challenge_v * uint256_t(ultra_op.z_2))));
        accumulator_trace.push_back(current_accumulator);
    }
 
    // Accumulator final value, recomputed during witness generation and expected at RESULT_ROW
    Fq final_accumulator_state = accumulator_trace.back();
    accumulator_trace.pop_back();
 
    std::array<Fr, NUM_BINARY_LIMBS> previous_accumulator_binary_limbs = split_fq_into_limbs(final_accumulator_state);
    // Generate witness values and accumulation gates from all the actual UltraOps, starting from beginning
    for (const auto& ultra_op : ultra_ops_span) {
        if (ultra_op.op_code.value() == 0) {
            // For no-op operations, the translator trace remains empty except for accumulator binary limbs,
            // which are copied from the previous row where a real operation occurred (i.e., where the op wire
            // at an even index contains a non-zero value). During proving, we verify that the wires at that
            // previous row are well-formed and that the accumulator value is correctly propagated throughout
            // the entire no-op range for both even and odd indices.
            for (size_t j = 0; j < ACCUMULATORS_BINARY_LIMBS_0; j++) {
                wires[j].push_back(zero_idx());
                wires[j].push_back(zero_idx());
            }
            size_t idx = 0;
            for (size_t j = ACCUMULATORS_BINARY_LIMBS_0; j <= ACCUMULATORS_BINARY_LIMBS_3; j++) {
                wires[j].push_back(add_variable(previous_accumulator_binary_limbs[idx]));
                wires[j].push_back(add_variable(previous_accumulator_binary_limbs[idx]));
                idx++;
            }
            for (size_t j = ACCUMULATORS_BINARY_LIMBS_3 + 1; j < TOTAL_COUNT; j++) {
                wires[j].push_back(zero_idx());
                wires[j].push_back(zero_idx());
            }
            increment_num_gates(2);
            continue;
        }
 
        Fq previous_accumulator{ 0 };
        // Pop the last value from accumulator trace and use it as previous accumulator
        if (!accumulator_trace.empty()) {
            previous_accumulator = accumulator_trace.back();
            accumulator_trace.pop_back();
        }
        // Compute witness values
        AccumulationInput one_accumulation_step =
            generate_witness_values(ultra_op, previous_accumulator, batching_challenge_v, evaluation_input_x);
 
        // Save the state of accumulator in case the next operation encountered is a no-op
        previous_accumulator_binary_limbs = one_accumulation_step.previous_accumulator;
        // And put them into the wires
        create_accumulation_gate(one_accumulation_step);
    }
 
    // Also process the last two random ops present at the end of the op queue to hide the ecc ops of the last circuit
    // whose ops are added to the op queue
    for (size_t i = ops_end; i < ultra_ops.size(); ++i) {
        process_random_op(ultra_ops[i]);
    }
 
    // The Translator uses a strict 2-row trace structure (even=computation, odd=transfer).
    // An odd gate count would shift the entire witness layout, corrupting all relations.
    BB_ASSERT(num_gates() % 2 == 0, "Translator circuit gate count must be even for 2-row trace structure");
}
std::array<TranslatorCircuitBuilder::Fr, TranslatorCircuitBuilder::NUM_MICRO_LIMBS> 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<Fr, NUM_MICRO_LIMBS> 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