ecc_msm_relation_impl.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/ecc/curves/bn254/g1.hpp"
#include "barretenberg/ecc/groups/precomputed_generators_bn254_impl.hpp"
#include "ecc_msm_relation.hpp"
 
namespace bb {
 
template <typename FF>
template <typename ContainerOverSubrelations, typename AllEntities, typename Parameters>
void ECCVMMSMRelationImpl<FF>::accumulate(ContainerOverSubrelations& accumulator,
                                          const AllEntities& in,
                                          const Parameters& /*unused*/,
                                          const FF& scaling_factor)
{
    using Accumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>;
    using View = typename Accumulator::View;
 
    const auto& x1 = View(in.msm_x1);
    const auto& y1 = View(in.msm_y1);
    const auto& x2 = View(in.msm_x2);
    const auto& y2 = View(in.msm_y2);
    const auto& x3 = View(in.msm_x3);
    const auto& y3 = View(in.msm_y3);
    const auto& x4 = View(in.msm_x4);
    const auto& y4 = View(in.msm_y4);
    const auto& collision_inverse1 = View(in.msm_collision_x1);
    const auto& collision_inverse2 = View(in.msm_collision_x2);
    const auto& collision_inverse3 = View(in.msm_collision_x3);
    const auto& collision_inverse4 = View(in.msm_collision_x4);
    const auto& lambda1 = View(in.msm_lambda1);
    const auto& lambda2 = View(in.msm_lambda2);
    const auto& lambda3 = View(in.msm_lambda3);
    const auto& lambda4 = View(in.msm_lambda4);
    const auto& lagrange_first = View(in.lagrange_first);
    const auto& add1 = View(in.msm_add1);
    const auto& add1_shift = View(in.msm_add1_shift);
    const auto& add2 = View(in.msm_add2);
    const auto& add3 = View(in.msm_add3);
    const auto& add4 = View(in.msm_add4);
    const auto& acc_x = View(in.msm_accumulator_x);
    const auto& acc_y = View(in.msm_accumulator_y);
    const auto& acc_x_shift = View(in.msm_accumulator_x_shift);
    const auto& acc_y_shift = View(in.msm_accumulator_y_shift);
    const auto& slice1 = View(in.msm_slice1);
    const auto& slice2 = View(in.msm_slice2);
    const auto& slice3 = View(in.msm_slice3);
    const auto& slice4 = View(in.msm_slice4);
    const auto& msm_transition = View(in.msm_transition);
    const auto& msm_transition_shift = View(in.msm_transition_shift);
    const auto& round = View(in.msm_round);
    const auto& round_shift = View(in.msm_round_shift);
    const auto& q_add = View(in.msm_add); // is 1 iff we are at an ADD row in Straus algorithm
    const auto& q_add_shift = View(in.msm_add_shift);
    const auto& q_skew = View(in.msm_skew);
    const auto& q_skew_shift = View(in.msm_skew_shift);
    const auto& q_double = View(in.msm_double); // is 1 iff we are at an DOUBLE row in Straus algorithm
    const auto& q_double_shift = View(in.msm_double_shift);
    const auto& msm_size = View(in.msm_size_of_msm);
    const auto& pc = View(in.msm_pc); // pc stands for `point-counter`.
    const auto& pc_shift = View(in.msm_pc_shift);
    const auto& count = View(in.msm_count);
    const auto& count_shift = View(in.msm_count_shift);
    auto is_not_first_row = (-lagrange_first + 1);
 
    auto add = [&](auto& xb,
                   auto& yb,
                   auto& xa,
                   auto& ya,
                   auto& lambda,
                   auto& selector,
                   auto& relation,
                   auto& collision_relation) {
        // computation of lambda is valid: if q == 1, then L == (yb - ya) / (xb - xa)
        // if q == 0, then L == 0. combining these into a single constraint yields:
        // q * (L * (xb - xa - 1) - (yb - ya)) + L = 0
        relation += selector * (lambda * (xb - xa - 1) - (yb - ya)) + lambda;
        collision_relation += selector * (xb - xa);
        // x_out = L.L + (-xb - xa) * q + (1 - q) xa
        // deg L = 1, deg q = 1, min(deg(xa), deg(xb))≥ 1.
        // hence deg(x_out) = 1 + max(deg(xa, xb))
        auto x_out = lambda.sqr() + (-xb - xa - xa) * selector + xa;
 
        // y_out = L . (xa - x_out) - ya * q + (1 - q) ya
        // hence deg(y_out) = max(1 + deg(x_out), 1 + deg(ya))
        auto y_out = lambda * (xa - x_out) + (-ya - ya) * selector + ya;
        return std::array<Accumulator, 2>{ x_out, y_out };
    };
 
    auto first_add = [&](auto& xb,
                         auto& yb,
                         auto& xa,
                         auto& ya,
                         auto& lambda,
                         auto& selector,
                         auto& relation,
                         auto& collision_relation) {
        // N.B. this is brittle - should be curve agnostic but we don't propagate the curve parameter into relations!
        constexpr auto offset_generator = get_precomputed_generators<g1, "ECCVM_OFFSET_GENERATOR", 1>()[0];
        constexpr uint256_t oxu = offset_generator.x;
        constexpr uint256_t oyu = offset_generator.y;
        const Accumulator xo(oxu);
        const Accumulator yo(oyu);
        // set (x, y) to be either accumulator if `selector == 0` or OFFSET if `selector == 1`.
        auto x = xo * selector + xb * (-selector + 1);
        auto y = yo * selector + yb * (-selector + 1);
        relation += lambda * (x - xa) - (y - ya); // degree 3
        collision_relation += (xa - x);
        auto x_out = lambda * lambda + (-x - xa);
        auto y_out = lambda * (xa - x_out) - ya;
        return std::array<Accumulator, 2>{ x_out, y_out };
    };
 
    // ADD operations (if row represents ADD round, not SKEW or DOUBLE)
    Accumulator add_relation(0); // validates the correctness of all elliptic curve additions.
    Accumulator x1_collision_relation(0);
    Accumulator x2_collision_relation(0);
    Accumulator x3_collision_relation(0);
    Accumulator x4_collision_relation(0);
    // If `msm_transition == 1`, we have started a new MSM. We need to treat the current value of [Acc] as the point at
    // infinity!
    auto [x_t1, y_t1] =
        first_add(acc_x, acc_y, x1, y1, lambda1, msm_transition, add_relation, x1_collision_relation); // [deg 2, deg 3]
    auto [x_t2, y_t2] = add(x2, y2, x_t1, y_t1, lambda2, add2, add_relation, x2_collision_relation);   // [deg 3, deg 4]
    auto [x_t3, y_t3] = add(x3, y3, x_t2, y_t2, lambda3, add3, add_relation, x3_collision_relation);   // [deg 4, deg 5]
    auto [x_t4, y_t4] = add(x4, y4, x_t3, y_t3, lambda4, add4, add_relation, x4_collision_relation);   // [deg 5, deg 6]
 
    // Validate accumulator output matches ADD output if q_add = 1
    std::get<0>(accumulator) += q_add * (acc_x_shift - x_t4) * scaling_factor;
    std::get<1>(accumulator) += q_add * (acc_y_shift - y_t4) * scaling_factor;
    std::get<2>(accumulator) += q_add * add_relation * scaling_factor;
 
    auto dbl = [&](auto& x, auto& y, auto& lambda, auto& relation) {
        auto two_x = x + x;
        relation += lambda * (y + y) - (two_x + x) * x;
        auto x_out = lambda.sqr() - two_x;
        auto y_out = lambda * (x - x_out) - y;
        return std::array<Accumulator, 2>{ x_out, y_out };
    };
 
    Accumulator double_relation(0);
    auto [x_d1, y_d1] = dbl(acc_x, acc_y, lambda1, double_relation);
    auto [x_d2, y_d2] = dbl(x_d1, y_d1, lambda2, double_relation);
    auto [x_d3, y_d3] = dbl(x_d2, y_d2, lambda3, double_relation);
    auto [x_d4, y_d4] = dbl(x_d3, y_d3, lambda4, double_relation);
    std::get<10>(accumulator) += q_double * (acc_x_shift - x_d4) * scaling_factor;
    std::get<11>(accumulator) += q_double * (acc_y_shift - y_d4) * scaling_factor;
    std::get<12>(accumulator) += q_double * double_relation * scaling_factor;
 
    Accumulator skew_relation(0);
    static FF inverse_seven = FF(7).invert();
    auto skew1_select = slice1 * inverse_seven;
    auto skew2_select = slice2 * inverse_seven;
    auto skew3_select = slice3 * inverse_seven;
    auto skew4_select = slice4 * inverse_seven;
    Accumulator x1_skew_collision_relation(0);
    Accumulator x2_skew_collision_relation(0);
    Accumulator x3_skew_collision_relation(0);
    Accumulator x4_skew_collision_relation(0);
    // add skew points iff row is a SKEW row AND slice = 7 (point_table[7] maps to -[P])
    // N.B. while it would be nice to have one `add` relation for both ADD and SKEW rounds,
    // this would increase degree of sumcheck identity vs evaluating them separately.
    // This is because, for add rounds, the result of adding [P1], [Acc] is [P1 + Acc] or [P1]
    //             but for skew rounds, the result of adding [P1], [Acc] is [P1 + Acc] or [Acc]
    auto [x_s1, y_s1] = add(x1, y1, acc_x, acc_y, lambda1, skew1_select, skew_relation, x1_skew_collision_relation);
    auto [x_s2, y_s2] = add(x2, y2, x_s1, y_s1, lambda2, skew2_select, skew_relation, x2_skew_collision_relation);
    auto [x_s3, y_s3] = add(x3, y3, x_s2, y_s2, lambda3, skew3_select, skew_relation, x3_skew_collision_relation);
    auto [x_s4, y_s4] = add(x4, y4, x_s3, y_s3, lambda4, skew4_select, skew_relation, x4_skew_collision_relation);
 
    // Validate accumulator output matches SKEW output if q_skew = 1
    std::get<3>(accumulator) += q_skew * (acc_x_shift - x_s4) * scaling_factor;
    std::get<4>(accumulator) += q_skew * (acc_y_shift - y_s4) * scaling_factor;
    std::get<5>(accumulator) += q_skew * skew_relation * scaling_factor;
 
    // Check x-coordinates do not collide if row is an ADD row or a SKEW row
    // if either q_add or q_skew = 1, an inverse should exist for each computed relation
    // Step 1: construct boolean selectors that describe whether we added a point at the current row
    const auto add_first_point = add1 * q_add + q_skew * skew1_select;
    const auto add_second_point = add2 * q_add + q_skew * skew2_select;
    const auto add_third_point = add3 * q_add + q_skew * skew3_select;
    const auto add_fourth_point = add4 * q_add + q_skew * skew4_select;
    // Step 2: construct the difference a.k.a. delta between x-coordinates for each point add (depending on if row is
    // ADD or SKEW)
    const auto x1_delta = x1_skew_collision_relation * q_skew + x1_collision_relation * q_add;
    const auto x2_delta = x2_skew_collision_relation * q_skew + x2_collision_relation * q_add;
    const auto x3_delta = x3_skew_collision_relation * q_skew + x3_collision_relation * q_add;
    const auto x4_delta = x4_skew_collision_relation * q_skew + x4_collision_relation * q_add;
    // Step 3: x_delta * inverse - 1 = 0 if we performed a point addition (else x_delta * inverse = 0)
    std::get<6>(accumulator) += (x1_delta * collision_inverse1 - add_first_point) * scaling_factor;
    std::get<7>(accumulator) += (x2_delta * collision_inverse2 - add_second_point) * scaling_factor;
    std::get<8>(accumulator) += (x3_delta * collision_inverse3 - add_third_point) * scaling_factor;
    std::get<9>(accumulator) += (x4_delta * collision_inverse4 - add_fourth_point) * scaling_factor;
 
    // When add_i = 0, force slice_i to ALSO be 0
    std::get<13>(accumulator) += (-add1 + 1) * slice1 * scaling_factor;
    std::get<14>(accumulator) += (-add2 + 1) * slice2 * scaling_factor;
    std::get<15>(accumulator) += (-add3 + 1) * slice3 * scaling_factor;
    std::get<16>(accumulator) += (-add4 + 1) * slice4 * scaling_factor;
 
    // SELECTORS ARE MUTUALLY EXCLUSIVE
    // at most one of q_skew, q_double, q_add can be nonzero.
    // note that as we can expect our table to be zero padded, we _do not_ insist that q_add + q_double + q_skew == 1.
    std::get<17>(accumulator) += (q_add * q_double + q_add * q_skew + q_double * q_skew) * scaling_factor;
 
    // Validate that if q_add = 1 or q_skew = 1, add1 also is 1
    // NOTE(#2222): could just get rid of add1 as a column, as it is a linear combination.
    std::get<32>(accumulator) += (add1 - q_add - q_skew) * scaling_factor;
 
    // ROUND TRANSITION LOGIC
    // `round_transition` describes whether we are transitioning between "rounds" of the MSM according to the Straus
    // algorithm. In particular, the `round` corresponds to the wNAF digit we are currently processing.
 
    const auto round_delta = round_shift - round;
    // If `msm_transition == 0` (next row) then `round_delta` is boolean; the round is internal to a given MSM and
    // represents the wNAF digit currently being processed. `round_delta == 0` means that the current and next steps of
    // the Straus algorithm are processing the same wNAF digit place.
 
    // `round_transition == 0` if `round_delta == 0` or the next row is an MSM transition.
    // if `round_transition != 1`, then `round_transition == round_delta == 1` by the following constraint.
    // in particular, `round_transition` is boolean. (`round_delta` is not boolean precisely one step before an MSM
    // transition, but that does not concern us here.)
    const auto round_transition = round_delta * (-msm_transition_shift + 1);
    std::get<18>(accumulator) += round_transition * (round_delta - 1) * scaling_factor;
 
    // If `round_transition == 1`, then `round_delta == 1` and `msm_transition_shift == 0`. Therefore, we wish to
    // constrain next row in the VM to either be a double (if `round != 31`) or skew (if `round == 31`). In either case,
    // the point is that we have finished processing a wNAF digit place and need to either perform the doublings to move
    // on to the next place _or_ we are at the last place and need to perform the skew computation to finish. These are
    // equationally represented as:
    //      round_transition * skew_shift * (round - 31) = 0 (if round tx and skew, then round == 31);
    //      round_transition * (skew_shift + double_shift - 1) = 0 (if round tx, then skew XOR double = 1).
    //      (-round_delta + 1) * q_double_shift = 1 (if q_double_shift == 1, then round_transition = 1)
    // together, these have the following implications: if round tx and round != 31, then double_shift = 1.
    // conversely, if round tx and double_shift == 0, then `q_skew_shift == 1` (which then forces `round == 31`).
    // similarly, if q_double_shift == 1, then round_transition == 0,
    // the fact that a round_transition occurs at the first time skew_shift == 1 follows from the fact that skew == 1
    // implies round == 32 and the above three relations, together with the _definition_ of round_transition.
    std::get<19>(accumulator) += round_transition * q_skew_shift * (round - 31) * scaling_factor;
    std::get<20>(accumulator) += round_transition * (q_skew_shift + q_double_shift - 1) * scaling_factor;
    std::get<35>(accumulator) += (-round_delta + 1) * q_double_shift * scaling_factor;
    // if the next is neither double nor skew, and we are not at an msm_transition, then round_delta = 0 and the next
    // "row" of our VM is processing the same wNAF digit place.
    std::get<21>(accumulator) += round_transition * (-q_double_shift + 1) * (-q_skew_shift + 1) * scaling_factor;
 
    // CONSTRAINING Q_DOUBLE AND Q_SKEW
    // NOTE: we have already constrained q_add, q_skew, and q_double to be mutually exclusive.
 
    // if double, next add = 1. As q_double, q_add, and q_skew are mutually exclusive, this suffices to force
    // q_double_shift == q_skew_shift == 0.
    std::get<22>(accumulator) += q_double * (-q_add_shift + 1) * scaling_factor;
    // if the current row has q_skew == 1 and the next row is _not_ an MSM transition, then q_skew_shift = 1.
    // this forces q_skew to precisely correspond to the rows where `round == 32`. Indeed, note that the first q_skew
    // bit is set correctly:
    //      round == 31, round_transition == 1 ==> q_skew_shift == 1. (if, to the contrary, q_double_shift == 1, then
    //      the q_add_shift_shift == 1, but we assume that we have correctly constrained the q_adds via the multiset
    //      argument. this means that q_double_shift == 0, which forces q_skew_shift == 1 because round_transition
    //      == 1.)
    // this means that the first row with `round == 32` has q_skew == 1. then all subsequent q_skew entries must be 1,
    // _until_ we start our new MSM.
    std::get<33>(accumulator) += (-msm_transition_shift + 1) * q_skew * (-q_skew_shift + 1) * scaling_factor;
    // if q_skew == 1, then round == 32. This is almost certainly redundant but psychologically useful to "constrain
    // both ends".
    std::get<34>(accumulator) += q_skew * (-round + 32) * scaling_factor;
 
    // UPDATING THE COUNT
 
    // if we are changing the `round` (i.e., starting to process a new wNAF digit or at an msm transition), the
    // count_shift must be 0.
    std::get<23>(accumulator) += round_delta * count_shift * scaling_factor;
    // if msm_transition = 0 and round_transition = 0, then the next "row" of the VM is processing the same wNAF digit.
    // this means that the count must increase: count_shift = count + add1 + add2 + add3 + add4
    std::get<24>(accumulator) += (-msm_transition_shift + 1) * (-round_delta + 1) *
                                 (count_shift - count - add1 - add2 - add3 - add4) * scaling_factor;
 
    // at least one of the following must be true:
    //      the next step is an MSM transition;
    //      the next count is zero (meaning we are starting the processing of a new wNAF digit)
    //      the next step is processing the same wNAF digit (i.e., round_delta == 0)
    // (note that at the start of a new MSM, the count is also zero, so the above are not mutually exclusive.)
    std::get<25>(accumulator) +=
        is_not_first_row * (-msm_transition_shift + 1) * round_delta * count_shift * scaling_factor;
 
    // if msm_transition = 1, then round = 0.
    std::get<26>(accumulator) += msm_transition * round * scaling_factor;
 
    // if msm_transition_shift = 1, pc = pc_shift + msm_size
    // NB: `ecc_set_relation` ensures `msm_size` maps to `transcript.msm_count` for the current value of `pc`
    std::get<27>(accumulator) += is_not_first_row * msm_transition_shift * (msm_size + pc_shift - pc) * scaling_factor;
 
    // Addition continuity checks
    // We want to RULE OUT the following scenarios:
    // Case 1: add2 = 1, add1 = 0
    // Case 2: add3 = 1, add2 = 0
    // Case 3: add4 = 1, add3 = 0
    // These checks ensure that the current row does not skip points (for both ADD and SKEW ops)
    // This is part of a wider set of checks we use to ensure that all point data is used in the assigned
    // multiscalar multiplication operation (and not in a different MSM operation).
    std::get<28>(accumulator) += add2 * (-add1 + 1) * scaling_factor;
    std::get<29>(accumulator) += add3 * (-add2 + 1) * scaling_factor;
    std::get<30>(accumulator) += add4 * (-add3 + 1) * scaling_factor;
 
    // Final continuity check.
    // If an addition spans two rows, we need to make sure that the following scenario is RULED OUT:
    //   add4 = 0 on the CURRENT row, add1 = 1 on the NEXT row
    // We must apply the above for the two cases:
    // Case 1: q_add = 1 on the CURRENT row, q_add = 1 on the NEXT row
    // Case 2: q_skew = 1 on the CURRENT row, q_skew = 1 on the NEXT row
    // (i.e. if q_skew = 1, q_add_shift = 1 this implies an MSM transition so we skip this continuity check)
    std::get<31>(accumulator) +=
        (q_add * q_add_shift + q_skew * q_skew_shift) * (-add4 + 1) * add1_shift * scaling_factor;
 
    // remaining checks (done in ecc_set_relation.hpp, ecc_lookup_relation.hpp)
    // when transition occurs, perform set membership lookup on (accumulator / pc / msm_size)
    // perform set membership lookups on add_i * (pc / round / slice_i)
    // perform lookups on (pc / slice_i / x / y)
 
    // We look up wnaf slices by mapping round + pc -> slice
    // We use an exact set membership check to validate that
    // wnafs written in wnaf_relation == wnafs read in msm relation
    // We use `add1/add2/add3/add4` to flag whether we are performing a wnaf read op
    // We can set these to be Prover-defined as the set membership check implicitly ensures that the correct reads
    // have occurred.
}
 
} // namespace bb