logderiv_lookup_relation.hpp

Go to the documentation of this file.

// === AUDIT STATUS ===
// internal:    { status: Complete, auditors: [Luke, Raju], commit: }
// external_1:  { status: not started, auditors: [], commit: }
// external_2:  { status: not started, auditors: [], commit: }
// =====================
 
#pragma once
#include <array>
#include <tuple>
 
#include "barretenberg/common/constexpr_utils.hpp"
#include "barretenberg/common/thread.hpp"
#include "barretenberg/honk/proof_system/logderivative_library.hpp"
#include "barretenberg/polynomials/univariate.hpp"
#include "barretenberg/relations/relation_types.hpp"
 
namespace bb {
 
template <typename FF_> class LogDerivLookupRelationImpl {
  public:
    using FF = FF_;
    static constexpr bool HAS_LOGDERIVATIVE_INVERSE_COMPUTATION = true;
    static constexpr size_t TABLE_TERMS = 1; // the number of table terms in the lookup relation
    // 1 + polynomial degree of this relation
    static constexpr size_t INVERSE_SUBRELATION_LENGTH = 5; // both subrelations are degree 4
    static constexpr size_t LOOKUP_SUBRELATION_LENGTH = 5;  // both subrelations are degree 4
    static constexpr size_t BOOLEAN_CHECK_SUBRELATION_LENGTH =
        3; // deg + 1 of the relation checking that read_tag_m is a boolean value
 
    static constexpr std::array<size_t, 3> SUBRELATION_PARTIAL_LENGTHS{
        INVERSE_SUBRELATION_LENGTH,      // inverse construction sub-relation
        LOOKUP_SUBRELATION_LENGTH,       // log derivative lookup argument sub-relation
        BOOLEAN_CHECK_SUBRELATION_LENGTH // boolean check sub-relation
    };
 
    static constexpr std::array<bool, 3>
        SUBRELATION_LINEARLY_INDEPENDENT = { true /*Inverse subrelation*/,
                                             false /*Lookup subrelation*/,
                                             true /*read_tag boolean check subrelation*/ };
 
    template <typename AllEntities> inline static bool skip(const AllEntities& in)
    {
        // Ensure the input does not contain a lookup gate or data that is being read
        return in[AllEntities::EntityId::q_lookup].is_zero() && in[AllEntities::EntityId::lookup_read_counts].is_zero();
    }
 
    template <typename AllValues> static bool operation_exists_at_row(const AllValues& row)
    {
        // is the row a lookup gate or does it contain table data that has been read at some point in this circuit
        return (row.q_lookup == 1) || (row.lookup_read_tags == 1);
    }
 
    // Get the inverse polynomial for this relation
    template <typename AllEntities> static auto& get_inverse_polynomial(AllEntities& in)
    {
        return in[AllEntities::EntityId::lookup_inverses];
    }
 
    template <typename Accumulator, typename AllEntities>
    static Accumulator compute_inverse_exists(const AllEntities& in)
    {
        using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
 
        const auto row_has_write = CoefficientAccumulator(in[AllEntities::EntityId::lookup_read_tags]);
        const auto row_has_read = CoefficientAccumulator(in[AllEntities::EntityId::q_lookup]);
        // Relation checking: is_read_gate == 1 || read_tag == 1
        // Important note: the relation written below assumes that is_read_gate and read_tag are boolean values, which
        // is guaranteed by the boolean_check subrelation. If not, fixing one of the two, the return value is a linear
        // function in the other variable and can be set to an arbitrary value independent of the fixed value. See the
        // boolean_check subrelation for more explanation.
        // 1 - (1 - row_has_write) * (1- row_has_read)
        //  degree                1             1                1                 1     =    2
        return Accumulator(-(row_has_write * row_has_read) + row_has_write + row_has_read);
    }
 
    // Compute table_1 + gamma + table_2 * eta + table_3 * eta_2 + table_4 * eta_3
    // table_1,2,3 correspond to the (maximum) three columns of the lookup table and table_4 is the unique identifier
    // of the lookup table table_index
    template <typename Accumulator, typename AllEntities, typename Parameters>
    static Accumulator compute_table_term(const AllEntities& in, const Parameters& params)
    {
        using ParameterCoefficientAccumulator = typename Parameters::DataType::CoefficientAccumulator;
        using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
 
        const auto gamma = ParameterCoefficientAccumulator(params.gamma);
        const auto beta = ParameterCoefficientAccumulator(params.beta);
        const auto beta_sqr = ParameterCoefficientAccumulator(params.beta_sqr);
        const auto beta_cube = ParameterCoefficientAccumulator(params.beta_cube);
 
        auto table_1 = CoefficientAccumulator(in[AllEntities::EntityId::table_1]);
        auto table_2 = CoefficientAccumulator(in[AllEntities::EntityId::table_2]);
        auto table_3 = CoefficientAccumulator(in[AllEntities::EntityId::table_3]);
        auto table_4 = CoefficientAccumulator(in[AllEntities::EntityId::table_4]);
 
        // degree          1     0           1         0          1         0        =   1
        auto result = (table_2 * beta) + (table_3 * beta_sqr) + (table_4 * beta_cube);
        result += table_1;
        result += gamma;
        return Accumulator(result);
    }
 
    template <typename Accumulator, typename AllEntities, typename Parameters>
    static Accumulator compute_lookup_term(const AllEntities& in, const Parameters& params)
    {
        using ParameterCoefficientAccumulator = typename Parameters::DataType::CoefficientAccumulator;
        using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
 
        const auto gamma = ParameterCoefficientAccumulator(params.gamma);
        const auto beta = ParameterCoefficientAccumulator(params.beta);
        const auto beta_sqr = ParameterCoefficientAccumulator(params.beta_sqr);
        const auto beta_cube = ParameterCoefficientAccumulator(params.beta_cube);
 
        auto w_1 = CoefficientAccumulator(in[AllEntities::EntityId::w_l]);
        auto w_2 = CoefficientAccumulator(in[AllEntities::EntityId::w_r]);
        auto w_3 = CoefficientAccumulator(in[AllEntities::EntityId::w_o]);
 
        auto w_1_shift = CoefficientAccumulator(in[AllEntities::EntityId::w_l_shift]);
        auto w_2_shift = CoefficientAccumulator(in[AllEntities::EntityId::w_r_shift]);
        auto w_3_shift = CoefficientAccumulator(in[AllEntities::EntityId::w_o_shift]);
 
        auto table_index = CoefficientAccumulator(in[AllEntities::EntityId::q_o]);
        auto negative_column_1_step_size = CoefficientAccumulator(in[AllEntities::EntityId::q_r]);
        auto negative_column_2_step_size = CoefficientAccumulator(in[AllEntities::EntityId::q_m]);
        auto negative_column_3_step_size = CoefficientAccumulator(in[AllEntities::EntityId::q_c]);
 
        // The wire values for lookup gates are accumulators structured in such a way that the differences w_i -
        // step_size*w_i_shift result in values present in column i of a corresponding table. See the documentation in
        // method bb::plookup::get_lookup_accumulators() in  for a detailed explanation.
        // degree                                      1                 1         1       0 = 2
        auto derived_table_entry_1 = (negative_column_1_step_size * w_1_shift) + (w_1 + gamma);
        // degree                                        1             1          1 =    2
        auto derived_table_entry_2 = (negative_column_2_step_size * w_2_shift) + w_2;
        // degree                                         1              1          1 = 2
        auto derived_table_entry_3 = (negative_column_3_step_size * w_3_shift) + w_3;
        //                              1           0    = 1
        auto table_index_entry = table_index * beta_cube;
 
        // (w_1 + γ + q_2*w_1_shift) + β(w_2 + q_m*w_2_shift) + β²(w_3 + q_c*w_3_shift) + β³*q_index.
        // deg 2 or 3
        // degree                            2              0                      2                    0   =   2
        auto result = Accumulator(derived_table_entry_2) * beta + Accumulator(derived_table_entry_3) * beta_sqr;
        result += Accumulator(derived_table_entry_1 + table_index_entry);
        return result;
    }
 
    template <typename Polynomials>
    static void compute_logderivative_inverse(Polynomials& polynomials,
                                              auto& relation_parameters,
                                              const size_t circuit_size,
                                              const size_t start_index = 0)
    {
        BB_BENCH_NAME("Lookup::compute_logderivative_inverse");
        auto& inverse_polynomial = get_inverse_polynomial(polynomials);
 
        const size_t num_rows = circuit_size - start_index;
        size_t min_iterations_per_thread = 1 << 6; // min number of iterations for which we'll spin up a unique thread
        size_t num_threads = bb::calculate_num_threads(num_rows, min_iterations_per_thread);
 
        parallel_for(num_threads, [&](ThreadChunk chunk) {
            BB_BENCH_TRACY_NAME("Lookup::compute_inverses/chunk");
            for (size_t j : chunk.range(num_rows)) {
                size_t i = j + start_index;
                // We only compute the inverse if this row contains a lookup gate or data that has been looked up
                if (polynomials.q_lookup().get(i) == 1 || polynomials.lookup_read_tags().get(i) == 1) {
                    // TODO(https://github.com/AztecProtocol/barretenberg/issues/940): avoid get_row if possible.
                    auto row = polynomials.get_row(i); // Note: this is a copy. use sparingly!
                    auto value = compute_lookup_term<FF>(row, relation_parameters) *
                                 compute_table_term<FF>(row, relation_parameters);
                    inverse_polynomial.at(i) = value;
                }
            }
        });
 
        // Compute inverse polynomial I in place by inverting the product at each row
        FF::batch_invert(inverse_polynomial.coeffs());
    };
 
    template <typename ContainerOverSubrelations, typename AllEntities, typename Parameters>
    static void accumulate(ContainerOverSubrelations& accumulator,
                           const AllEntities& in,
                           const Parameters& params,
                           const FF& scaling_factor)
    {
        // declare the accumulator of the maximum length, in non-ZK Flavors, they are of the same length,
        // whereas in ZK Flavors, the accumulator corresponding log derivative lookup argument sub-relation is the
        // longest
        using ShortAccumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>;
        using BooleanCheckerAccumulator = typename std::tuple_element_t<2, ContainerOverSubrelations>;
        using ShortView = typename ShortAccumulator::View;
 
        using Accumulator = typename std::tuple_element_t<1, ContainerOverSubrelations>;
        using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
 
        // allows to re-use the values accumulated by the accumulator of the size smaller than
        // the size of Accumulator declared above
 
        const auto inverses_m = CoefficientAccumulator(in[AllEntities::EntityId::lookup_inverses]); // Degree 1
        const Accumulator inverses(inverses_m);
        const auto read_counts_m = CoefficientAccumulator(in[AllEntities::EntityId::lookup_read_counts]); // Degree 1
        const auto read_selector_m = CoefficientAccumulator(in[AllEntities::EntityId::q_lookup]);         // Degree 1
 
        const auto inverse_exists = compute_inverse_exists<Accumulator>(in);   // Degree 2
        const auto lookup_term = compute_lookup_term<Accumulator>(in, params); // Degree 2
        const auto table_term = compute_table_term<Accumulator>(in, params);   // Degree 1
 
        // Establish the correctness of the polynomial of inverses I. Note: inverses is computed so that the value is 0
        // if !inverse_exists.
        // Degrees:                 5                 2           1           1                          0
        const Accumulator logderiv_first_term = (lookup_term * table_term * inverses - inverse_exists) * scaling_factor;
        std::get<0>(accumulator) += ShortView(logderiv_first_term); // Deg 5
 
        // Establish validity of the read. Note: no scaling factor here since this constraint is 'linearly dependent,
        // i.e. enforced across the entire trace, not on a per-row basis.
        // Degrees:                         1                  2          =       3
        Accumulator tmp = Accumulator(read_selector_m) * table_term;
        tmp -= (Accumulator(read_counts_m) * lookup_term);
        tmp *= inverses;                 // degree 4(5)
        std::get<1>(accumulator) += tmp; // Deg 4 (5)
 
        // We should make sure that the read_tag is a boolean value
        const auto read_tag_m = CoefficientAccumulator(in[AllEntities::EntityId::lookup_read_tags]);
        const auto read_tag = BooleanCheckerAccumulator(read_tag_m);
        // degree                          1         1                       0(1) =  2
        std::get<2>(accumulator) += (read_tag * read_tag - read_tag) * scaling_factor;
    }
};
 
template <typename FF> using LogDerivLookupRelation = Relation<LogDerivLookupRelationImpl<FF>>;
 
} // namespace bb