memory_relation.hpp

Go to the documentation of this file.

// === AUDIT STATUS ===
// internal:    { status: Complete, auditors: [Luke, Raju], commit: 05a381f8b31ae4648e480f1369e911b148216e8b}
// external_1:  { status: not started, auditors: [], commit: }
// external_2:  { status: not started, auditors: [], commit: }
// =====================
 
#pragma once
#include "barretenberg/numeric/uint256/uint256.hpp"
#include "barretenberg/relations/relation_types.hpp"
 
namespace bb {
 
template <typename FF_> class MemoryRelationImpl {
  public:
    using FF = FF_;
 
    static constexpr std::array<size_t, 8> SUBRELATION_PARTIAL_LENGTHS{
        6, // memory sub-relation;
        6, // ROM consistency sub-relation 1
        6, // ROM consistency sub-relation 2
        6, // RAM consistency sub-relation 1
        6, // RAM consistency sub-relation 2
        6, // RAM consistency sub-relation 3
        6, // ROM-LogUp inverse correctness (per-row vanishing)
        6  // ROM-LogUp sum identity (linearly dependent: summed across the trace)
    };
 
    // Subrelation 7 (ROM-LogUp sum) is linearly dependent: it asserts that a sum across all rows is zero rather
    // than a per-row identity, so it must not be multiplied by `scaling_factor` in the accumulation step.
    static constexpr std::array<bool, 8> SUBRELATION_LINEARLY_INDEPENDENT{ true, true, true, true,
                                                                           true, true, true, false };
 
    template <typename AllEntities> inline static bool skip(const AllEntities& in)
    {
        return in[AllEntities::EntityId::q_memory].is_zero();
    }
 
    template <typename ContainerOverSubrelations, typename AllEntities, typename Parameters>
    inline static void accumulate(ContainerOverSubrelations& accumulators,
                                  const AllEntities& in,
                                  const Parameters& params,
                                  const FF& scaling_factor)
    {
        // all accumulators are of the same length, so we set our accumulator type to (arbitrarily) be the first one.
        // if there were one that were shorter, we could also profitably use a `ShortAccumulator` type. however,
        // that is not the case here.
        using Accumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>;
        using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
 
        using ParameterCoefficientAccumulator = typename Parameters::DataType::CoefficientAccumulator;
 
        const auto& eta_m = ParameterCoefficientAccumulator(params.eta);
        const auto& eta_two_m = ParameterCoefficientAccumulator(params.eta_two);
        const auto& eta_three_m = ParameterCoefficientAccumulator(params.eta_three);
        const auto& rom_logup_gamma_m = ParameterCoefficientAccumulator(params.rom_logup_gamma);
 
        auto w_1_m = CoefficientAccumulator(in[AllEntities::EntityId::w_l]);
        auto w_2_m = CoefficientAccumulator(in[AllEntities::EntityId::w_r]);
        auto w_3_m = CoefficientAccumulator(in[AllEntities::EntityId::w_o]);
        auto w_4_m = CoefficientAccumulator(in[AllEntities::EntityId::w_4]);
        auto w_1_shift_m = CoefficientAccumulator(in[AllEntities::EntityId::w_l_shift]);
        auto w_2_shift_m = CoefficientAccumulator(in[AllEntities::EntityId::w_r_shift]);
        auto w_3_shift_m = CoefficientAccumulator(in[AllEntities::EntityId::w_o_shift]);
        auto w_4_shift_m = CoefficientAccumulator(in[AllEntities::EntityId::w_4_shift]);
 
        auto q_1_m = CoefficientAccumulator(in[AllEntities::EntityId::q_l]);
        auto q_2_m = CoefficientAccumulator(in[AllEntities::EntityId::q_r]);
        auto q_3_m = CoefficientAccumulator(in[AllEntities::EntityId::q_o]);
        auto q_4_m = CoefficientAccumulator(in[AllEntities::EntityId::q_4]);
        auto q_m_m = CoefficientAccumulator(in[AllEntities::EntityId::q_m]);
        auto q_c_m = CoefficientAccumulator(in[AllEntities::EntityId::q_c]);
 
        auto q_memory_m = CoefficientAccumulator(in[AllEntities::EntityId::q_memory]);
 
        auto memory_record_check_m = w_3_m * eta_three_m; // degree 1
        memory_record_check_m += w_2_m * eta_two_m;
        memory_record_check_m += w_1_m * eta_m;
        memory_record_check_m += q_c_m;
        auto partial_record_check_m = memory_record_check_m; // degree 1. used later in RAM consistency check
        memory_record_check_m = memory_record_check_m - w_4_m;
        auto memory_record_check = Accumulator(memory_record_check_m);
        auto neg_index_delta_m = w_1_m - w_1_shift_m;
        auto index_delta_is_zero_m = neg_index_delta_m + FF(1); // deg 1
        auto record_delta_m = w_4_shift_m - w_4_m;
 
        Accumulator index_increases_by_zero_or_one(neg_index_delta_m.sqr() +
                                                   neg_index_delta_m); // check if next index minus current index is
                                                                       // boolean. applies to both ROM and RAM. deg 2
 
        auto adjacent_values_match_if_adjacent_indices_match =
            Accumulator(index_delta_is_zero_m * record_delta_m); // deg 2
 
        auto q_memory_by_scaling_m = q_memory_m * scaling_factor; // deg 1
        auto q_memory_by_scaling = Accumulator(q_memory_by_scaling_m);
        auto q_one_by_two_m = q_1_m * q_2_m; // deg 2
        auto q_one_by_two = Accumulator(q_one_by_two_m);
        auto q_one_by_two_by_memory_by_scaling = q_one_by_two * q_memory_by_scaling; // deg 3
        // witnesses that for consecutive ROM gates, values match if indices match.
        std::get<1>(accumulators) +=
            adjacent_values_match_if_adjacent_indices_match * q_one_by_two_by_memory_by_scaling; // deg 5
        // witnesses that index increases by {0, 1} for sorted ROM gates.
        std::get<2>(accumulators) += index_increases_by_zero_or_one * q_one_by_two_by_memory_by_scaling; // deg 5
 
        auto ROM_consistency_check_identity = memory_record_check * q_one_by_two; // deg 3
 
        auto neg_access_type_m = (partial_record_check_m - w_4_m); // will be boolean for honest Prover; degree 1.
        Accumulator neg_access_type(neg_access_type_m);
        auto access_check = neg_access_type.sqr() + neg_access_type; // check value is boolean; degree 2.
 
        auto neg_next_gate_access_type_m = w_3_shift_m * eta_three_m; // degree 1
        neg_next_gate_access_type_m += w_2_shift_m * eta_two_m;
        neg_next_gate_access_type_m += w_1_shift_m * eta_m;
        neg_next_gate_access_type_m = neg_next_gate_access_type_m - w_4_shift_m;
        Accumulator neg_next_gate_access_type(neg_next_gate_access_type_m); // degree 1
        auto value_delta_m = w_3_shift_m - w_3_m;                           // degree 1
        auto adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation =
            Accumulator(index_delta_is_zero_m * value_delta_m) *
            Accumulator(neg_next_gate_access_type_m + FF(1)); // deg 3
 
        // We can't apply the RAM consistency check identity on the final entry in the sorted list: the wires in the
        // next gate would make the identity fail.  We need to validate that its 'access type' bool is correct. Can't
        // do with an arithmetic gate because of the  `eta` factors.
        // Our solution is that we have the final sorted RAM record be unconstrained (i.e., none of the
        // `MEMORY_SELECTORS` are turned on); then, we may _uniformly_ check that the *next* gate's access type is
        // correct, to cover this edge case.
        auto next_gate_access_type_is_boolean = neg_next_gate_access_type.sqr() + neg_next_gate_access_type; // deg 2
 
        auto q_3_by_memory_and_scaling = Accumulator(q_3_m * q_memory_by_scaling_m);
        // For RAM entries, if adjacent indices match and the next access is a read, then
        // values must be equal.
        std::get<3>(accumulators) +=
            adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation *
            q_3_by_memory_and_scaling;                                                             // deg 5
        std::get<4>(accumulators) += index_increases_by_zero_or_one * q_3_by_memory_and_scaling;   // deg 4
        std::get<5>(accumulators) += next_gate_access_type_is_boolean * q_3_by_memory_and_scaling; // deg 4
 
        auto RAM_consistency_check_identity = access_check * q_3_by_memory_and_scaling; // deg 4
 
        auto timestamp_delta_m = w_2_shift_m - w_2_m;                                            // deg 1
        auto RAM_timestamp_check_identity_m = index_delta_is_zero_m * timestamp_delta_m - w_3_m; // deg 2
        Accumulator RAM_timestamp_check_identity(RAM_timestamp_check_identity_m);
        // degree 5
        auto memory_identity = ROM_consistency_check_identity;
        memory_identity += RAM_timestamp_check_identity * Accumulator(q_4_m * q_1_m); // deg 4
        memory_identity += memory_record_check * Accumulator(q_m_m * q_1_m);          // deg 4
 
        memory_identity *= q_memory_by_scaling;            // deg 5
        memory_identity += RAM_consistency_check_identity; // deg 5
        std::get<0>(accumulators) += memory_identity;      // deg 5
 
        auto one_minus_q_1_m = -q_1_m + FF(1);              // deg 1
        Accumulator q_logup_table(q_2_m * one_minus_q_1_m); // deg 2
        Accumulator q_logup_read(q_4_m * one_minus_q_1_m);  // deg 2
        Accumulator q_logup_any = q_logup_table + q_logup_read;
 
        // Fingerprint denominator: w_l + eta * w_r + eta_two * q_c + rom_logup_gamma. Degree 1.
        Accumulator denom(w_1_m + w_2_m * eta_m + q_c_m * eta_two_m + rom_logup_gamma_m);
 
        Accumulator w_4_acc(w_4_m);
 
        // Subrelation 6: q_memory * q_logup_any * (w_4 * denom - 1) = 0. Per-row vanishing; deg 5.
        std::get<6>(accumulators) += q_memory_by_scaling * q_logup_any * (w_4_acc * denom - FF(1));
 
        // Subrelation 7: sum over the trace of q_memory * (q_logup_read - q_logup_table * w_o) * w_4 = 0.
        // Linearly dependent, hence no scaling_factor; deg 5.
        Accumulator logup_sum_contribution = q_logup_read - q_logup_table * Accumulator(w_3_m);
        logup_sum_contribution *= w_4_acc;
        logup_sum_contribution *= Accumulator(q_memory_m);
        std::get<7>(accumulators) += logup_sum_contribution;
    };
};
 
template <typename FF> using MemoryRelation = Relation<MemoryRelationImpl<FF>>;
} // namespace bb