memory_relation.hpp

Go to the documentation of this file.

// === AUDIT STATUS ===
// internal:    { status: not started, auditors: [], date: YYYY-MM-DD }
// external_1:  { status: not started, auditors: [], date: YYYY-MM-DD }
// external_2:  { status: not started, auditors: [], date: YYYY-MM-DD }
// =====================
 
#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, 6> 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
    };
 
    template <typename AllEntities> inline static bool skip(const AllEntities& in) { return in.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);
 
        auto w_1_m = CoefficientAccumulator(in.w_l);
        auto w_2_m = CoefficientAccumulator(in.w_r);
        auto w_3_m = CoefficientAccumulator(in.w_o);
        auto w_4_m = CoefficientAccumulator(in.w_4);
        auto w_1_shift_m = CoefficientAccumulator(in.w_l_shift);
        auto w_2_shift_m = CoefficientAccumulator(in.w_r_shift);
        auto w_3_shift_m = CoefficientAccumulator(in.w_o_shift);
        auto w_4_shift_m = CoefficientAccumulator(in.w_4_shift);
 
        auto q_1_m = CoefficientAccumulator(in.q_l);
        auto q_2_m = CoefficientAccumulator(in.q_r);
        auto q_3_m = CoefficientAccumulator(in.q_o);
        auto q_4_m = CoefficientAccumulator(in.q_4);
        auto q_m_m = CoefficientAccumulator(in.q_m);
        auto q_c_m = CoefficientAccumulator(in.q_c);
 
        auto q_memory_m = CoefficientAccumulator(in.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
    };
};
 
template <typename FF> using MemoryRelation = Relation<MemoryRelationImpl<FF>>;
} // namespace bb