translator_circuit_builder.hpp

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: }
// =====================
 
#pragma once
#include "barretenberg/common/constexpr_utils.hpp"
#include "barretenberg/ecc/curves/bn254/fq.hpp"
#include "barretenberg/honk/execution_trace/execution_trace_block.hpp"
#include "barretenberg/numeric/uint256/uint256.hpp"
#include "barretenberg/op_queue/ecc_op_queue.hpp"
#include "barretenberg/stdlib_circuit_builders/circuit_builder_base.hpp"
 
namespace bb {
class TranslatorCircuitBuilder : public CircuitBuilderBase<bb::fr> {
 
    // The scalar field of BN254
    using Fr = bb::fr;
    // The base (coordinate) field of BN254
    using Fq = bb::fq;
 
  public:
    static constexpr size_t NUM_WIRES = 81;
    static constexpr size_t NUM_SELECTORS = 0;
 
    [[nodiscard]] size_t get_num_constant_gates() const override { return 0; };
 
    enum WireIds : uint8_t {
        OP, // The first 4 wires contain the standard values from the EccQueue wire
        X_LOW_Y_HI,
        X_HIGH_Z_1,
        Y_LOW_Z_2,
        P_X_LOW_LIMBS,               // P.xₗₒ split into 2 68 bit limbs
        P_X_HIGH_LIMBS,              // P.xₕᵢ split into a 68 and a 50 bit limb
        P_Y_LOW_LIMBS,               // P.yₗₒ split into 2 68 bit limbs
        P_Y_HIGH_LIMBS,              // P.yₕᵢ split into a 68 and a 50 bit limb
        Z_LOW_LIMBS,                 // Low limbs of z_1 and z_2 (68 bits each)
        Z_HIGH_LIMBS,                // High Limbs of z_1 and z_2 (60 bits each)
        ACCUMULATORS_BINARY_LIMBS_0, // Contain 68-bit limbs of current and previous accumulator (previous at higher
                                     // indices because of the nuances of KZG commitment).
        ACCUMULATORS_BINARY_LIMBS_1,
        ACCUMULATORS_BINARY_LIMBS_2,
        ACCUMULATORS_BINARY_LIMBS_3, // Highest limb is 50 bits (254 mod 68)    P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, // Low
                                     // limbs split further into smaller chunks for range constraints
        QUOTIENT_LOW_BINARY_LIMBS,   // Quotient limbs
        QUOTIENT_HIGH_BINARY_LIMBS,
        RELATION_WIDE_LIMBS,              // Limbs for checking the correctness of  mod 2²⁷² relations.
        P_X_LOW_LIMBS_RANGE_CONSTRAINT_0, // Low limbs split further into smaller chunks for range constraints
        P_X_LOW_LIMBS_RANGE_CONSTRAINT_1,
        P_X_LOW_LIMBS_RANGE_CONSTRAINT_2,
        P_X_LOW_LIMBS_RANGE_CONSTRAINT_3,
        P_X_LOW_LIMBS_RANGE_CONSTRAINT_4,
        P_X_LOW_LIMBS_RANGE_CONSTRAINT_TAIL,
        P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0, // High limbs split into chunks for range constraints
        P_X_HIGH_LIMBS_RANGE_CONSTRAINT_1,
        P_X_HIGH_LIMBS_RANGE_CONSTRAINT_2,
        P_X_HIGH_LIMBS_RANGE_CONSTRAINT_3,
        P_X_HIGH_LIMBS_RANGE_CONSTRAINT_4,
        P_X_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL,
        P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0, // Low limbs split into chunks for range constraints
        P_Y_LOW_LIMBS_RANGE_CONSTRAINT_1,
        P_Y_LOW_LIMBS_RANGE_CONSTRAINT_2,
        P_Y_LOW_LIMBS_RANGE_CONSTRAINT_3,
        P_Y_LOW_LIMBS_RANGE_CONSTRAINT_4,
        P_Y_LOW_LIMBS_RANGE_CONSTRAINT_TAIL,
        P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0, // High limbs split into chunks for range constraints
        P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_1,
        P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_2,
        P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_3,
        P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_4,
        P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL,
        Z_LOW_LIMBS_RANGE_CONSTRAINT_0, // Range constraints for low limbs of z_1 and z_2
        Z_LOW_LIMBS_RANGE_CONSTRAINT_1,
        Z_LOW_LIMBS_RANGE_CONSTRAINT_2,
        Z_LOW_LIMBS_RANGE_CONSTRAINT_3,
        Z_LOW_LIMBS_RANGE_CONSTRAINT_4,
        Z_LOW_LIMBS_RANGE_CONSTRAINT_TAIL,
        Z_HIGH_LIMBS_RANGE_CONSTRAINT_0, // Range constraints for high limbs of z_1 and z_2
        Z_HIGH_LIMBS_RANGE_CONSTRAINT_1,
        Z_HIGH_LIMBS_RANGE_CONSTRAINT_2,
        Z_HIGH_LIMBS_RANGE_CONSTRAINT_3,
        Z_HIGH_LIMBS_RANGE_CONSTRAINT_4,
        Z_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL,
 
        ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0, // Range constraints for the current accumulator limbs (no need to
                                                  // redo previous accumulator)
        ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_1,
        ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_2,
        ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_3,
        ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_4,
        ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_TAIL,
        ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0,
        ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_1,
        ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_2,
        ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_3,
        ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_4,
        ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL,
 
        QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_0, // Range constraints for quotient
        QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_1,
        QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_2,
        QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_3,
        QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_4,
        QUOTIENT_LOW_LIMBS_RANGE_CONSTRAIN_TAIL,
        QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_0,
        QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_1,
        QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_2,
        QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_3,
        QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_4,
        QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAIN_TAIL,
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_0,
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_1,
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_2,
        RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_3,
 
        TOTAL_COUNT
 
    };
 
    // Basic goblin translator has the minimum minicircuit size of 2048, so optimize for that case
    // For context, minicircuit is the part of the final polynomials fed into the proving system, where we have all the
    // arithmetic logic. However, the full circuit is several times larger (we use a trick to bring down the degree of
    // the permutation argument)
    static constexpr size_t DEFAULT_TRANSLATOR_VM_LENGTH = 2048;
 
    // Maximum size of a single limb is 68 bits
    static constexpr size_t NUM_LIMB_BITS = 68;
 
    // For soundness we need to constrain the highest limb so that the whole value is at most 50 bits
    static constexpr size_t NUM_LAST_LIMB_BITS = Fq::modulus.get_msb() + 1 - (3 * NUM_LIMB_BITS);
 
    // 128-bit z_1 and z_2 are split into 2 limbs each
    static constexpr size_t NUM_Z_LIMBS = 2;
 
    // Number of bits in the quotient representation
    static constexpr size_t NUM_QUOTIENT_BITS = 256;
 
    // Number of bits in the quotient highest limb
    static constexpr size_t NUM_LAST_QUOTIENT_LIMB_BITS = 256 - (3 * NUM_LIMB_BITS);
 
    // Number of bits in Z scalars
    static constexpr size_t NUM_Z_BITS = 128;
    // The circuit builder has a default range constraint mechanism that is used throughout. It range cosntrains the
    // values to < 2¹⁴
    static constexpr size_t MICRO_LIMB_BITS = 14;
 
    // Maximum size of a micro limb used for range constraints
    static constexpr auto MAX_MICRO_LIMB_SIZE = (uint256_t(1) << MICRO_LIMB_BITS) - 1;
 
    // To range constrain a limb to 68 bits we need 6 limbs: 5 for 14-bit windowed chunks and 1 to range constrain the
    // highest to a more restrictive range (0 <= a < 2¹⁴ && 0 <= 4*a < 2¹⁴ ) ~ ( 0 <= a < 2¹² )
    static constexpr size_t NUM_MICRO_LIMBS = 6;
 
    // Number of limbs used to decompose a 254-bit value for modular arithmetic. This will represent an Fq value as 4 Fr
    // limbs to be representable inside a circuit defined overF r.
    static constexpr size_t NUM_BINARY_LIMBS = 4;
 
    // Number of limbs used for computation of a result modulo 2²⁷²
    static constexpr size_t NUM_RELATION_WIDE_LIMBS = 2;
 
    // Range constraint of relation limbs
    static constexpr size_t RELATION_WIDE_LIMB_BITS = 84;
 
    // Maximum size of each relation limb (in accordance with range constraints)
    static constexpr uint256_t MAX_RELATION_WIDE_LIMB_SIZE = uint256_t(1) << RELATION_WIDE_LIMB_BITS;
 
    // Shift of a single micro (range constraint) limb
    static constexpr auto MICRO_SHIFT = uint256_t(1) << MICRO_LIMB_BITS;
 
    // Maximum size of 2 lower limbs concatenated
    static constexpr auto MAX_LOW_WIDE_LIMB_SIZE = (uint256_t(1) << (NUM_LIMB_BITS * 2)) - 1;
 
    // Maximum size of 2 higher limbs concatenated
    static constexpr auto MAX_HIGH_WIDE_LIMB_SIZE = (uint256_t(1) << (NUM_LIMB_BITS + NUM_LAST_LIMB_BITS)) - 1;
 
    // Maximum size of z limbs
    static constexpr auto MAX_Z_LIMB_SIZE = (uint256_t(1) << NUM_Z_BITS) - 1;
 
    // Index at which the accumulation result is stored in the circuit, preceded by 2 shiftability zeros
    // and three random ops that contribute to ensuring the Translator proof does not leak
    // information about the op queue content linked to the circuits being proven
    static constexpr size_t RESULT_ROW = 8;
 
    // Number of no-ops at the beginning of Translator trace (provides the 2 leading zero rows required for
    // polynomial shiftability of op queue wires). Contributed by the tail kernel's queue_ecc_no_op().
    static constexpr size_t NUM_NO_OPS_START = 1;
    static_assert(NUM_NO_OPS_START == 1);
 
    // Number of random ops at the beginning of Translator trace
    static constexpr size_t NUM_RANDOM_OPS_START = 3;
    static_assert(NUM_RANDOM_OPS_START == 3);
    static_assert(NUM_RANDOM_OPS_START == ECC_NUM_RANDOM_OPS_START);
 
    // Number of random ops at the end of Translator trace
    static constexpr size_t NUM_RANDOM_OPS_END = 2;
    static_assert(NUM_RANDOM_OPS_END == 2);
 
    // How much you'd need to multiply a value by to perform a shift to a higher binary limb
    static constexpr auto SHIFT_1 = uint256_t(1) << NUM_LIMB_BITS;
 
    // Shift by 2 binary limbs
    static constexpr auto SHIFT_2 = uint256_t(1) << (NUM_LIMB_BITS << 1);
 
    // Precomputed inverse to easily divide by the shift by 2 limbs
    static constexpr auto SHIFT_2_INVERSE = Fr(SHIFT_2).invert();
 
    // Shift by 3 binary limbs
    static constexpr auto SHIFT_3 = uint256_t(1) << (NUM_LIMB_BITS * 3);
 
    // The modulus of the target emulated field as a 512-bit integer
    static constexpr uint512_t MODULUS_U512 = uint512_t(Fq::modulus);
 
    // The binary modulus used in the CRT computation (2²⁷²)
    static constexpr uint512_t BINARY_BASIS_MODULUS = uint512_t(1) << (NUM_LIMB_BITS << 2);
 
    // Negated modulus of the target emulated field in the binary modulus (2²⁷² - q)
    static constexpr uint512_t NEGATIVE_PRIME_MODULUS = BINARY_BASIS_MODULUS - MODULUS_U512;
 
    // Negated modulus of the target emulated field in the binary modulus split into 4 binary limbs + the final limb is
    // the negated modulus of the target emulated field in the scalar field.
    static constexpr std::array<Fr, 5> NEGATIVE_MODULUS_LIMBS = {
        Fr(NEGATIVE_PRIME_MODULUS.slice(0, NUM_LIMB_BITS).lo),
        Fr(NEGATIVE_PRIME_MODULUS.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo),
        Fr(NEGATIVE_PRIME_MODULUS.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo),
        Fr(NEGATIVE_PRIME_MODULUS.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo),
        -Fr(Fq::modulus)
    };
 
    template <typename FF> static std::array<FF, 5> compute_negative_modulus_limbs()
    {
        return { FF(NEGATIVE_PRIME_MODULUS.slice(0, NUM_LIMB_BITS).lo),
                 FF(NEGATIVE_PRIME_MODULUS.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo),
                 FF(NEGATIVE_PRIME_MODULUS.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo),
                 FF(NEGATIVE_PRIME_MODULUS.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo),
                 -FF(Fq::modulus) };
    }
 
    struct AccumulationInput {
        // Members necessary for the gate creation
        UltraOp ultra_op;
        std::array<Fr, NUM_BINARY_LIMBS> P_x_limbs;
        std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> P_x_microlimbs;
        std::array<Fr, NUM_BINARY_LIMBS> P_y_limbs;
        std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> P_y_microlimbs;
 
        std::array<Fr, NUM_Z_LIMBS> z_1_limbs;
        std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_Z_LIMBS> z_1_microlimbs;
        std::array<Fr, NUM_Z_LIMBS> z_2_limbs;
        std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_Z_LIMBS> z_2_microlimbs;
 
        std::array<Fr, NUM_BINARY_LIMBS> previous_accumulator;
        std::array<Fr, NUM_BINARY_LIMBS> current_accumulator;
        std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> current_accumulator_microlimbs;
        std::array<Fr, NUM_BINARY_LIMBS> quotient_binary_limbs;
        std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_BINARY_LIMBS> quotient_microlimbs;
        std::array<Fr, NUM_RELATION_WIDE_LIMBS> relation_wide_limbs;
        std::array<std::array<Fr, NUM_MICRO_LIMBS>, NUM_RELATION_WIDE_LIMBS> relation_wide_microlimbs;
    };
 
    static constexpr std::string_view NAME_STRING = "TranslatorCircuitBuilder";
 
    // The challenge that is used for batching together evaluations of several polynomials
    Fq batching_challenge_v;
 
    // The input we evaluate polynomials on
    Fq evaluation_input_x;
 
    bool avm_mode = false;
 
    std::array<std::vector<uint32_t>, NUM_WIRES> wires;
 
    TranslatorCircuitBuilder(Fq batching_challenge_v_, Fq evaluation_input_x_, bool avm_mode_ = false)
        : batching_challenge_v(batching_challenge_v_)
        , evaluation_input_x(evaluation_input_x_)
        , avm_mode(avm_mode_)
    {
        this->set_zero_idx(add_variable(Fr::zero()));
    };
 
    TranslatorCircuitBuilder(Fq batching_challenge_v_,
                             Fq evaluation_input_x_,
                             std::shared_ptr<ECCOpQueue> op_queue,
                             bool avm_mode = false)
        : TranslatorCircuitBuilder(batching_challenge_v_, evaluation_input_x_, avm_mode)
 
    {
        BB_BENCH_NAME("TranslatorCircuitBuilder::constructor");
        feed_ecc_op_queue_into_circuit(std::move(op_queue));
    }
 
    TranslatorCircuitBuilder() = default;
    TranslatorCircuitBuilder(const TranslatorCircuitBuilder& other) = delete;
    TranslatorCircuitBuilder(TranslatorCircuitBuilder&& other) = delete;
    TranslatorCircuitBuilder& operator=(const TranslatorCircuitBuilder& other) = delete;
    TranslatorCircuitBuilder& operator=(TranslatorCircuitBuilder&& other) = delete;
    ~TranslatorCircuitBuilder() override = default;
 
    static std::array<Fr, NUM_BINARY_LIMBS> split_fq_into_limbs(const Fq& base)
    {
        uint256_t base_uint = base;
        return std::array<Fr, NUM_BINARY_LIMBS>({
            Fr(base_uint.slice(0, NUM_LIMB_BITS)),
            Fr(base_uint.slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS)),
            Fr(base_uint.slice(2 * NUM_LIMB_BITS, 3 * NUM_LIMB_BITS)),
            Fr(base_uint.slice(3 * NUM_LIMB_BITS, 4 * NUM_LIMB_BITS)),
        });
    }
 
    static void assert_well_formed_ultra_op(const UltraOp& ultra_op);
 
    static void assert_well_formed_accumulation_input(const AccumulationInput& acc_step);
 
    void create_accumulation_gate(const AccumulationInput& acc_step);
 
    void populate_wires_from_ultra_op(const UltraOp& ultra_op);
 
    void insert_pair_into_wire(WireIds wire_index, Fr first, Fr second)
    {
        auto& current_wire = wires[wire_index];
        current_wire.push_back(add_variable(first));
        current_wire.push_back(add_variable(second));
    }
 
    void feed_ecc_op_queue_into_circuit(const std::shared_ptr<ECCOpQueue>& ecc_op_queue);
 
    static AccumulationInput generate_witness_values(const UltraOp& ultra_op,
                                                     const Fq& previous_accumulator,
                                                     const Fq& batching_challenge_v,
                                                     const Fq& evaluation_input_x);
 
  private:
    static std::array<Fr, NUM_BINARY_LIMBS> 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) };
    }
 
    static std::array<Fr, NUM_Z_LIMBS> 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)) };
    }
 
    static std::array<Fr, NUM_MICRO_LIMBS> split_limb_into_microlimbs(const Fr& limb, size_t num_bits);
 
    template <size_t total_limbs>
    static void check_binary_limbs_maximum_values(const std::array<Fr, total_limbs>& 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);
    }
 
    template <size_t binary_limb_count, size_t micro_limb_count>
    static void check_micro_limbs_maximum_values(
        const std::array<std::array<Fr, micro_limb_count>, 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);
            }
        }
    }
 
    template <size_t array_size> void lay_limbs_in_row(std::array<Fr, array_size> input, WireIds starting_wire)
    {
        size_t wire_index = starting_wire;
        for (auto element : input) {
            wires[wire_index].push_back(add_variable(element));
            wire_index++;
        }
    }
 
    void process_random_op(const UltraOp& ultra_op);
};
 
} // namespace bb