chore: audit ECCVM msm relation (#16532)

Audit of the MSM relation.

There were a couple of columns that I think were underconstrained. I have made the MSM relations more
robust/clear as to why they are correct.

Aside from a few changes to the relations, this PR mostly involves a lot of documentation. The most important part of this is re: the multiset equality check. The description of _why_ this suffices to correctly constrain the q_add columns is more transparent now.

---------

Co-authored-by: notnotraju <[email protected]>

Author: notnotraju

barretenberg/cpp/src/barretenberg/eccvm/README.md

@@ -28,7 +28,7 @@ template <typename CycleGroup> struct ScalarMul {
     typename CycleGroup::affine_element base_point;
     std::array<int, NUM_WNAF_DIGITS_PER_SCALAR>
         wnaf_digits; // [a_{n-1}, a_{n-1}, ..., a_{0}], where each a_i ∈ {-2ʷ⁻¹ + 1, -2ʷ⁻¹ + 3, ..., 2ʷ⁻¹ - 3, 2ʷ⁻¹ -
-                     // 1} ∪ {0}. (here, w = `NUM_WNAF_DIGIT_BITS`). in particular, a_i is an odd integer with
+                     // 1}. (here, w = `NUM_WNAF_DIGIT_BITS`). in particular, a_i is an odd integer with
                      // absolute value less than 2ʷ. Represents the number `scalar` = ∑ᵢ aᵢ 2⁴ⁱ - `wnaf_skew`.
     bool wnaf_skew;  // necessary to represent _even_ integers
     // size bumped by 1 to record base_point.dbl()

barretenberg/cpp/src/barretenberg/eccvm/eccvm_builder_types.hpp

@@ -182,7 +182,7 @@ class ECCVMCircuitBuilder {
             msm.resize(msm_sizes[i]);
         }
         // populate result using the auxiliary vectors `msm_opqueue_index` and `msm_mul_index`, together with
-        // `eccvm_ops`. this first pass will *not* get the pc (program counter) correct. we explain why when we set it
+        // `eccvm_ops`. this first pass will *not* get the pc (point counter) correct. we explain why when we set it
         // correctly.
         parallel_for_range(msm_opqueue_index.size(), [&](size_t start, size_t end) {
             for (size_t i = start; i < end; i++) {

barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.hpp

@@ -549,6 +549,10 @@ class ECCVMFlavor {
          *          msm_lambda2: temp variable used for ecc point addition algorithm if msm_add2 = 1
          *          msm_lambda3: temp variable used for ecc point addition algorithm if msm_add3 = 1
          *          msm_lambda4: temp variable used for ecc point addition algorithm if msm_add4 = 1
+         *          msm_slice1: wNAF digit/slice for first add
+         *          msm_slice2: wNAF digit/slice for second add
+         *          msm_slice3: wNAF digit/slice for third add
+         *          msm_slice4: wNAF digit/slice for fourth add
          *          msm_collision_x1: used to ensure incomplete ecc addition exceptions not triggered if msm_add1 = 1
          *          msm_collision_x2: used to ensure incomplete ecc addition exceptions not triggered if msm_add2 = 1
          *          msm_collision_x3: used to ensure incomplete ecc addition exceptions not triggered if msm_add3 = 1

barretenberg/cpp/src/barretenberg/eccvm/eccvm_flavor.hpp

@@ -27,9 +27,15 @@ class ECCVMMSMMBuilder {
     static constexpr size_t NUM_WNAF_DIGITS_PER_SCALAR = bb::eccvm::NUM_WNAF_DIGITS_PER_SCALAR;
 
     struct alignas(64) MSMRow {
-        uint32_t pc = 0;        // counter over all half-length (128 bit) scalar muls used to compute the required MSMs
-        uint32_t msm_size = 0;  // the number of points that will be scaled and summed
-        uint32_t msm_count = 0; // number of multiplications processed so far in current MSM round
+        uint32_t pc = 0;       // decreasing point-counter, over all half-length (128 bit) scalar muls used to compute
+                               // the required MSMs. however, this value is _constant_ on a given MSM and more precisely
+                               //  refers to the number of half-length scalar muls completed up until we have started
+                               // the current MSM.
+        uint32_t msm_size = 0; // the number of points in (a.k.a. the length of) the MSM in whose computation
+                               // this VM row participates
+        uint32_t msm_count = 0; // number of multiplications processed so far (not including this row) in current MSM
+                                // round (a.k.a. wNAF digit slot). this specifically refers to the number of wNAF-digit
+                                // * point scalar products we have looked up and accumulated.
         uint32_t msm_round = 0; // current "round" of MSM, in {0, ..., 32 = `NUM_WNAF_DIGITS_PER_SCALAR`}. With the
                                 // Straus algorithm, we proceed wNAF digit by wNAF digit, from left to right. (final
                                 // round deals with the `skew` bit.)
@@ -73,7 +79,7 @@ class ECCVMMSMMBuilder {
      * @brief Computes the row values for the Straus MSM columns of the ECCVM.
      *
      * For a detailed description of the Straus algorithm and its relation to the ECCVM, please see
-     * https://hackmd.io/@aztec-network/rJ5xhuCsn
+     * https://hackmd.io/@aztec-network/rJ5xhuCsn or, alternatively, the [ECCVM readme](README.md).
      *
      * @param msms A vector of vectors of `ScalarMul`s, a.k.a. a vector of `MSM`s.
      * @param point_table_read_counts Table of read counts to be populated.
@@ -96,17 +102,23 @@ class ECCVMMSMMBuilder {
         //   row      = point_idx * rows_per_point_table + (some function of the slice value)
         //
         // Illustration:
-        //   Block Structure   Table structure:
-        //      | 0 | 1 |        | Block_{0}                      | <-- pc = total_number_of_muls
-        //      | - | - |        | Block_{1}                      | <-- pc = total_number_of_muls-(num muls in msm 0)
-        //    1 | # | # | -1     |   ...                          | ...
-        //    3 | # | # | -3     | Block_{total_number_of_muls-1} | <-- pc = num muls in last msm
+        //   Block Structure:
+        //      | 0 | 1 |
+        //      | - | - |
+        //    1 | # | # | -1
+        //    3 | # | # | -3
         //    5 | # | # | -5
         //    7 | # | # | -7
         //    9 | # | # | -9
         //   11 | # | # | -11
         //   13 | # | # | -13
         //   15 | # | # | -15
+        //
+        //   Table structure:
+        //    | Block_{0}                      | <-- pc = total_number_of_muls
+        //    | Block_{1}                      | <-- pc = total_number_of_muls-(num muls in msm 0)
+        //    |   ...                          | ...
+        //    | Block_{total_number_of_muls-1} | <-- pc = num muls in last msm
 
         const size_t num_rows_in_read_counts_table =
             static_cast<size_t>(total_number_of_muls) *
@@ -146,7 +158,7 @@ class ECCVMMSMMBuilder {
         std::vector<size_t> msm_row_counts;
         msm_row_counts.reserve(msms.size() + 1);
         msm_row_counts.push_back(1);
-        // compute the program counter (i.e. the index among all single scalar muls) that each multiscalar
+        // compute the point counter (i.e. the index among all single scalar muls) that each multiscalar
         // multiplication will start at.
         std::vector<size_t> pc_values;
         pc_values.reserve(msms.size() + 1);
@@ -203,7 +215,7 @@ class ECCVMMSMMBuilder {
                             bool add = num_points_in_row > relative_point_idx;
                             const size_t point_idx = offset + relative_point_idx;
                             if (add) {
-                                // pc starts at total_number_of_muls and decreases non-uniformly to 0
+                                // `pc` starts at total_number_of_muls and decreases non-uniformly to 0.
                                 // -15 maps to the 1st point in the lookup table (array element 0)
                                 // -1 maps to the point in the lookup table that corresponds to the negation of the
                                 // original input point (i.e. the point we need to add into the accumulator if wnaf_skew

barretenberg/cpp/src/barretenberg/eccvm/msm_builder.hpp

@@ -109,8 +109,8 @@ class ECCVMTranscriptBuilder {
 
     // maintains the state of the VM at any given "time" (i.e., at any given value of pc).
     struct VMState {
-        uint32_t pc = 0; // decreasing program counter that tracks the total number of multiplications that our virtual
-                         // machine has left to compute.
+        uint32_t pc = 0;    // decreasing point counter that tracks the total number of multiplications that our virtual
+                            // machine has left to compute.
         uint32_t count = 0; // Number of muls in the current MSM _excluding the current row_.
         Element accumulator = CycleGroup::affine_point_at_infinity; // accumulator for all group operations.
         Element msm_accumulator =