translator_circuit_checker.cpp

Go to the documentation of this file.

#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;
 
    auto report_fail = [&](const char* message, size_t row_idx) {
        info(message, row_idx);
        return false;
    };
 
    // 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<WireIds::OP>(circuit.wires);
    auto& x_lo_y_hi_wire = std::get<WireIds::X_LOW_Y_HI>(circuit.wires);
    auto& x_hi_z_1_wire = std::get<WireIds::X_HIGH_Z_1>(circuit.wires);
    auto& y_lo_z_2_wire = std::get<WireIds::Y_LOW_Z_2>(circuit.wires);
    auto& p_x_0_p_x_1_wire = std::get<WireIds::P_X_LOW_LIMBS>(circuit.wires);
    auto& p_x_2_p_x_3_wire = std::get<WireIds::P_X_HIGH_LIMBS>(circuit.wires);
    auto& p_y_0_p_y_1_wire = std::get<WireIds::P_Y_LOW_LIMBS>(circuit.wires);
    auto& p_y_2_p_y_3_wire = std::get<WireIds::P_Y_HIGH_LIMBS>(circuit.wires);
    auto& z_lo_wire = std::get<WireIds::Z_LOW_LIMBS>(circuit.wires);
    auto& z_hi_wire = std::get<WireIds::Z_HIGH_LIMBS>(circuit.wires);
    auto& accumulators_binary_limbs_0_wire = std::get<WireIds::ACCUMULATORS_BINARY_LIMBS_0>(circuit.wires);
    auto& accumulators_binary_limbs_1_wire = std::get<WireIds::ACCUMULATORS_BINARY_LIMBS_1>(circuit.wires);
    auto& accumulators_binary_limbs_2_wire = std::get<WireIds::ACCUMULATORS_BINARY_LIMBS_2>(circuit.wires);
    auto& accumulators_binary_limbs_3_wire = std::get<WireIds::ACCUMULATORS_BINARY_LIMBS_3>(circuit.wires);
    auto& quotient_low_binary_limbs = std::get<WireIds::QUOTIENT_LOW_BINARY_LIMBS>(circuit.wires);
    auto& quotient_high_binary_limbs = std::get<WireIds::QUOTIENT_HIGH_BINARY_LIMBS>(circuit.wires);
    auto& relation_wide_limbs_wire = std::get<WireIds::RELATION_WIDE_LIMBS>(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)));
    auto get_sequential_micro_chunks = [&](size_t gate_index, WireIds starting_wire_index, size_t chunk_count) {
        std::vector<Fr> 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;
    };
 
    auto accumulate_limb_from_micro_chunks = [](const std::vector<Fr>& 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<Fr>& first, const std::vector<Fr>& 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<Fr>& 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<Fr>& current_accumulator, const std::vector<Fr>& 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<Fr>& wide_limbs,
                                                            const std::vector<Fr>& 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 };
 
        // 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<Fr>& binary_limbs,
                                                              const std::vector<std::vector<Fr>>& 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);
 
            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;
                }
            }
 
            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
        constexpr std::array<Fr, 5> 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