clarify some point counter stuff, add the skew constraint implicitly for round == 32

Author: notnotraju

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

@@ -220,7 +220,7 @@ $\fq$, the column must be range constrained, either with an explicit range check
 | transcript_eq                              | q_eq                            | $\{0, 1\}$    |                                                                                                                                      | is opcode                                                                                                                                                                                                          |
 | transcript_reset_accumulator               | q_reset_accumulator             | $\{0, 1 \}$   |                                                                                                                                      | does opcode reset accumulator?                                                                                                                                                                                     |
 | transcript_msm_transition                  | msm_transition                  | $\{0, 1\}$    | `msm_transition = is_mul && next_not_msm && (state.count + num_muls > 0);`                                                           | are we at the end of an msm? i.e., is current transcript row the final `mul` opcode of a MSM                                                                                                                       |
-| transcript_pc                              | pc                              | $\fq$         | `updated_state.pc = state.pc - num_muls;`                                                                                            | _decreasing_ program counter. Only takes into count `mul` operations, not `add` operations.                                                                                                                        |
+| transcript_pc                              | pc                              | $\fq$         | `updated_state.pc = state.pc - num_muls;`                                                                                            | _decreasing_ point counter. Only takes into count `mul` operations, not `add` operations.                                                                                                                          |
 | transcript_msm_count                       | msm_count                       | $\fq$         | `updated_state.count = current_ongoing_msm ? state.count + num_muls : 0;`                                                            | Number of muls so far in the \*current\* MSM (NOT INCLUDING the current step)                                                                                                                                      |
 | transcript_msm_count_zero_at_transition    | msm_count_zero_at_transition    | $\{0, 1\}$    | `((state.count + num_muls) == 0) && entry.op_code.mul && next_not_msm;`                                                              | is the number of scalar muls we have completed at the end of our "MSM block" zero? (note that from the definition, if this variable is non-zero, then `msm_transition == 0`.)                                      |
 | transcript_Px                              | base_x                          | $\fq$         |                                                                                                                                      | (input trace) $x$-coordinate of base point $P$                                                                                                                                                                     |
@@ -304,13 +304,13 @@ If our `op` is a `mul`, with scalars `z1` and `z2`, the situation is more compli
 
 - $\transcriptmsmcount$ counts the number of active short-scalar multiplications _up to and not including_ the current `mul` op. The value of this column at the _next_ row increments by $2 - \transcriptzonezero - \transcriptztwozero$.
 - In other words, we simply avoid (our deferred) computations if $\transcriptzonezero = 1$ and/or $\transcriptztwozero = 1$.
-- Similarly, $\transcriptpc$ _decrements_ by $2 - \transcriptzonezero - \transcriptztwozero$. We use a decreasing program counter (only counting short `mul`s) for efficiency reasons, as it allows for cheaper commitments.
+- Similarly, $\transcriptpc$ _decrements_ by $2 - \transcriptzonezero - \transcriptztwozero$. We use a decreasing point counter (only counting short `mul`s) for efficiency reasons, as it allows for cheaper commitments.
 - If the next `op` is not a `mul`, and the total number of active `mul` operations (which is $\transcriptmsmcount + (2 - \transcriptzonezero - \transcriptztwozero)$) is non-zero, set the $\transcriptmsmtransition = 1$. Else, set $\transcriptmsmcountzeroattransition = 1$. Either way, the current `mul` then represents the end of an MSM. This is where $\transcriptmsmcountattransitioninverse$ is used.
 - If $\transcriptmsmtransition = 0$, then $\transcriptmsmx$, $\transcriptmsmy$, $\transcriptmsmintermediatex$, and $\transcriptmsmintermediatey$ are all $0$. (In particular, this holds when we are in the middle of an MSM.) Otherwise, we call $\transcriptmsmx$ and $\transcriptmsmy$ from the multiset argument, i.e., from the MSM table. Then the values of $\transcriptmsmintermediatex$ and $\transcriptmsmintermediatey$ are obtained by subtracting off the `OFFSET`.
 
 #### Transcript size
 
-The size of the _non-zero_ part of the table is the length of the `OpQueue` + 1 (we have shiftable columns). We have organized our wire values so that zero-padding is compatible with the polynomial constraints. (See e.g. the _decreasing_ program counter.)
+The size of the _non-zero_ part of the table is the length of the `OpQueue` + 1 (we have shiftable columns). We have organized our wire values so that zero-padding is compatible with the polynomial constraints. (See e.g. the _decreasing_ point counter.)
 
 ### Precomputed Columns
 
@@ -364,7 +364,7 @@ The following is one row in the Precomputed table; there are `NUM_WNAF_DIGITS_PE
 | precompute_s4lo | s8 | $[0, 4)$ | | second two bits of $\text{compress}(a*{31 - (4i + 3)})$ |
 | precompute_skew | skew | $\{0,1\}$ | | skew bit |
 | precompute_point_transition | point_transition | $\{0,1\}$ | | are we at the last row corresponding to this scalar? |
-| precompute_pc | pc | $\fq$ | | value of the program counter of this EC operation |
+| precompute_pc | pc | $\fq$ | | value of the point counter of this EC operation |
 | precompute_round | round | $\fq$ | | "row" of the computation, i.e., `i`. |
 | precompute_scalar_sum | scalar_sum | $\fq$ | | sum up-to-now of the digits |
 | precompute_tx, precompute_ty | precompute_accumulator | $E(\fq)\subset \fq\times \fq$ | | $(15-2i)P$ |

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

@@ -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_flavor.hpp

@@ -546,6 +546,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/msm_builder.hpp

@@ -27,8 +27,10 @@ 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 pc = 0;        // decreasing counter over all half-length (128 bit) scalar muls used to compute
+                                // the required MSMs
+        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.
@@ -148,7 +150,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);

barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation_impl.hpp

@@ -130,7 +130,14 @@ void ECCVMMSMRelationImpl<FF>::accumulate(ContainerOverSubrelations& accumulator
      * @brief Constraining addition rounds
      *
      * The boolean column q_add describes whether a round is an ADDITION round.
-     * The values of q_add are Prover-defined. We need to ensure they set q_add correctly.
+     * The values of q_add are Prover-defined. We need to ensure they set q_add correctly. We will do this via a
+     * multiset-equality check (formerly called a "strict lookup"), which allows the various tables to "communicate".
+     * On a high level, we ensure that this table "reads" (pc, round, wnaf_slice), another table (PointTable) "writes" a
+     * potentially different set of (pc, round, wnaf_slice), and we demand that the reads match the writes.
+     * Alternatively said, the MSM columns spawn a multiset of tuples of the form (pc, round, wnaf_slice), the
+     * PointTable columns span a potentially different multiset of tuples of the form (pc, round, wnaf_slice), and we
+     * _check_ that these two multisets match.
+     *
      * We rely on the following statements that we assume are constrained to be true (from other relations):
      *      1. The set of reads into (pc, round, wnaf_slice) is constructed when q_add = 1
      *      2. The set of reads into (pc, round, wnaf_slice) must match the set of writes from the point_table columns
@@ -365,7 +372,8 @@ void ECCVMMSMRelationImpl<FF>::accumulate(ContainerOverSubrelations& accumulator
     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
+    // 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;
 
     // ROUND TRANSITION LOGIC
@@ -392,26 +400,35 @@ void ECCVMMSMRelationImpl<FF>::accumulate(ContainerOverSubrelations& accumulator
     //      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).
     // 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 `skew_shift == 1`, which then forces `round == 31`.
-    //
-    // NOTE(@notnotraju): we must also constrain q_skew == 1 when round == 32. As far as I can tell, this is not done
-    // anywhere. Here is the potential bad thing that could happen: we could set q_skew to be 0 after the only place
-    // where it is forced (at round transition). Or worse, we could alternative q_skew and double in this round 32. As
-    // far as I can tell, this requires adding an extra column, which bears witness to the fact that the round is 32.
+    // conversely, if round tx and double_shift == 0, then `skew_shift == 1` (which then forces `round == 31`).
+
     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;
 
     // 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 is 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, not 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;
 
     // UPDATING THE COUNT
 
-    // if we are changing the "round" (i.e. starting to process a new wNAF digit), the count_shift must be 0.
+    // if we are changing the `round` (i.e. starting to process a new wNAF digit), 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

barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation_impl.hpp

@@ -18,17 +18,18 @@ namespace bb {
  * by the ECCVM.
  *
  * First term: tuple of (pc, round, wnaf_slice), computed when slicing scalar multipliers into slices,
- *             as part of ECCVMWnafRelation
+ *             as part of ECCVMWnafRelation. (Recall that pc stands for "point counter". Here, round corresponds to
+ *             `msm_round`.)
  * Input source: ECCVMWnafRelation
  * Output source: ECCVMMSMRelation
  *
  *
- * Second term: tuple of (point-counter, P.x, P.y, scalar-multiplier), used in ECCVMWnafRelation and
- *              ECCVMPointTableRelation
+ * Second term: tuple of (pc, P.x, P.y, scalar-multiplier), used in ECCVMWnafRelation and
+ *              ECCVMPointTableRelation. (Recall that pc stands for "point counter".)
  * Input source: ECCVMPointTableRelation
  * Output source: ECCVMMSMRelation
  *
- * Third term: tuple of (point-counter, P.x, P.y, msm-size) from ECCVMMSMRelation
+ * Third term: tuple of (pc, P.x, P.y, msm-size) from ECCVMMSMRelation. (Recall that pc stands for "point counter".)
  * Input source: ECCVMMSMRelation
  * Output source: ECCVMTranscriptRelation
  *
@@ -59,8 +60,9 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_numerator(const AllE
     /**
      * @brief First term: tuple of (pc, round, wnaf_slice), computed when slicing scalar multipliers into slices,
      *        as part of ECCVMWnafRelation.
-     *        If precompute_select = 1, tuple entry = (wnaf-slice + point-counter * beta + msm-round * beta_sqr).
-     *                       There are 4 tuple entries per row.
+     *        If precompute_select = 1, tuple entry = (wnaf-slice + pc * beta + msm-round * beta_sqr).
+     *        There are 4 tuple entries per row of the Precompute table. Moreover, the element that "increments" is
+     *        4 * `precompute_round`, due to the fact that the Precompute columns contain four "digits"/slices per row.
      */
     Accumulator numerator(1); // degree-0
     {
@@ -125,8 +127,8 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_numerator(const AllE
     }
 
     /**
-     * @brief Second term: tuple of (point-counter, P.x, P.y, scalar-multiplier), used in ECCVMWnafRelation and
-     * ECCVMPointTableRelation. ECCVMWnafRelation validates the sum of the wnaf slices associated with point-counter
+     * @brief Second term: tuple of (pc, P.x, P.y, scalar-multiplier), used in ECCVMWnafRelation and
+     * ECCVMPointTableRelation. ECCVMWnafRelation validates the sum of the wnaf slices associated with pc
      * equals scalar-multiplier. ECCVMPointTableRelation computes a table of muliples of [P]: { -15[P], -13[P], ...,
      * 15[P] }. We need to validate that scalar-multiplier and [P] = (P.x, P.y) come from MUL opcodes in the transcript
      * columns.
@@ -200,10 +202,10 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_numerator(const AllE
         numerator *= point_table_init_read; // degree-9
     }
     /**
-     * @brief Third term: tuple of (point-counter, P.x, P.y, msm-size) from ECCVMMSMRelation.
+     * @brief Third term: tuple of (pc, P.x, P.y, msm-size) from ECCVMMSMRelation.
      *        (P.x, P.y) is the output of a multi-scalar-multiplication evaluated in ECCVMMSMRelation.
      *        We need to validate that the same values (P.x, P.y) are present in the Transcript columns and describe a
-     *        multi-scalar multiplication of size `msm-size`, starting at `point-counter`.
+     *        multi-scalar multiplication of size `msm-size`, starting at `pc`.
      *
      *        If msm_transition_shift = 1, this indicates the current row is the last row of a multiscalar
      * multiplication evaluation. The output of the MSM will be present on `(msm_accumulator_x_shift,
@@ -345,7 +347,7 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_denominator(const Al
         denominator *= point_table_init_write; // degree 17
     }
     /**
-     * @brief Third term: tuple of (point-counter, P.x, P.y, msm-size) from ECCVMTranscriptRelation.
+     * @brief Third term: tuple of (pc, P.x, P.y, msm-size) from ECCVMTranscriptRelation.
      *        (P.x, P.y) is the *claimed* output of a multi-scalar-multiplication evaluated in ECCVMMSMRelation.
      *        We need to validate that the msm output produced in ECCVMMSMRelation is equivalent to the output present
      * in `transcript_msm_output_x, transcript_msm_output_y`, for a given multi-scalar multiplication starting at