chore: ECCVM shiftable column audit at lagrange_first row

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

@@ -362,6 +362,90 @@ class ECCVMFlavor {
 
     /**
      * @brief Represents polynomials shifted by 1 or their evaluations, defined relative to WitnessEntities.
+     *
+     * @details
+     * ## Shiftable columns and the lagrange_first row
+     *
+     * The PCS enforces P[0] = 0 for shiftable columns. With masking at the top of the circuit,
+     * `lagrange_first` activates at row k = NUM_DISABLED_ROWS_IN_SUMCHECK, not row 0. The value P[k] is
+     * NOT constrained by the PCS — a malicious prover can freely choose it.
+     *
+     * For soundness, every shiftable column must either:
+     *   (a) be explicitly constrained to zero at the lagrange_first row, or
+     *   (b) have its unconstrained value be unable to pollute subsequent computation.
+     *
+     * The builder sets all shiftable columns to 0 at the lagrange_first row (it is the empty first row of
+     * each subtable). Relations enforce this in three ways:
+     *
+     * ### Explicitly constrained at lagrange_first (relations force P[k] or P[k+1] = 0)
+     *
+     *   - z_perm (col 25): Z_PERM_INIT enforces `lagrange_first * z_perm = 0`.
+     *   - precompute_round (col 20): ROUND_SHIFT_ZERO forces round_shift = 0 at lagrange_first.
+     *   - precompute_scalar_sum (col 2): SCALAR_SUM_SHIFT_ZERO forces scalar_sum_shift = 0.
+     *   - precompute_s1hi (col 3): FIRST_SLICE_POSITIVE constrains s1hi_shift ∈ {2, 3}.
+     *   - transcript_accumulator_not_empty (col 22): **UNCONSTRAINED — needs fix.** See TODO in
+     *     eccvm_relation_corruption.test.cpp. Without `lagrange_first * accumulator_not_empty = 0`, a
+     *     malicious prover can disable INFINITY_ACC_X/Y and inject arbitrary accumulator coordinates.
+     *
+     * ### Dead: P[k] is not read by any relation at any active row
+     *
+     * These columns are not referenced by any non-trivially-active subrelation at row k. A malicious
+     * prover can set P[k] to anything and no per-row relation fires. This is safe because:
+     *   - P[k] as an unshifted value at row k: every relation term vanishes (gated by
+     *     `is_not_first_row = 0` or by selectors that are zero at the empty first row).
+     *   - P[k] as a shifted value at row k-1: row k-1 is in the masking region where sumcheck does not
+     *     evaluate relations.
+     *   - P[k+1] = P_shift(k) is unconstrained by row k's relations (same gating), but IS constrained
+     *     at row k+1 by that row's own relations (hiding row, etc.).
+     *
+     * These columns also do not appear in the set relation's numerator/denominator at row k.
+     * Verified by `HarmlessColumnsUnconstrainedAtLagrangeFirst` (checks all 6 relation families
+     * including SetRelation at row k).
+     *
+     *   - precompute_dx/dy (cols 4-5), precompute_tx/ty (cols 6-7): gated by (-lagrange_first + 1).
+     *   - msm_accumulator_x/y (cols 12-13): gated by (-lagrange_first + 1) in IDLE_ROW_PRESERVES_ACC
+     *     and by operation selectors elsewhere. Set relation reads msm_accumulator_x/y_shift (not
+     *     unshifted), gated by (-lagrange_first + 1) * msm_transition_shift.
+     *
+     * ### Multiset-constrained: not caught per-row, but caught by global multiset balance
+     *
+     * These columns appear in the set relation's numerator or denominator at row k. Corrupting P[k]
+     * changes the multiset entry at row k, which requires a matching entry in the precompute/MSM
+     * subtables that doesn't exist in the honest trace. The set relation catches this via its terminal
+     * condition (z_perm_shift = 0 at lagrange_last), not per-row.
+     *
+     * Note: our single-row test (`HarmlessColumnsUnconstrainedAtLagrangeFirst`) evaluates SetRelation
+     * at row k but does NOT detect this, because the test recomputes z_perm from the corrupted trace.
+     * The global multiset mismatch only manifests at lagrange_last.
+     *
+     *   - msm_count (col 14), msm_round (col 15), msm_pc (col 17): appear in set relation denominator
+     *     (first term: wnaf slice tuples). Not referenced by MSM/transcript/wnaf/point-table relations
+     *     at row k (gated by is_not_first_row or operation selectors).
+     *   - transcript_pc (col 19): appears in set relation denominator (second and third terms). Not
+     *     referenced by transcript relation at row k (gated by is_not_first_row in PC_UPDATE; gated by
+     *     transcript_mul = 0 and transcript_msm_transition = 0 in the set relation terms).
+     *
+     * ### Self-consistency: corruption is caught by existing relations
+     *
+     * These columns participate in relations that are NOT gated off at the lagrange_first row.
+     * Corrupting them produces a non-zero relation contribution, so sumcheck catches it. Some of these
+     * are operation selectors — setting them to non-zero activates subrelations that require consistency
+     * with non-shiftable columns (e.g., `op = 0` at the empty first row).
+     *
+     *   - transcript_mul (col 0): OPCODE_WELL_FORMED catches mismatch with non-shiftable `op`.
+     *   - msm_transition (col 8): BoolsRelation catches non-boolean values.
+     *   - transcript_msm_count (col 1): MSM_COUNT_ZERO_WHEN_NOT_MUL forces msm_count = 0 when q_mul = 0.
+     *   - msm_add (col 9): activates ADD_ACC_X/Y, ADD1_DECOMPOSITION — all require consistent data.
+     *   - msm_double (col 10): activates DOUBLE_ACC_X/Y.
+     *   - msm_skew (col 11): activates SKEW_ACC_X/Y, SKEW_IMPLIES_ROUND_32.
+     *   - msm_add1 (col 16): ADD1_DECOMPOSITION (add1 - q_add - q_skew = 0).
+     *   - precompute_pc (col 18): INACTIVE_PC forces pc = 0 when precompute_select = 0.
+     *   - precompute_select (col 21): activates SCALAR_SUM_CHECK, ROUND_CHECK, PC_CHECK.
+     *   - transcript_accumulator_x/y (cols 23-24): INFINITY_ACC_X/Y forces acc = 0 when
+     *     accumulator_not_empty = 0. **WARNING**: this safety depends on transcript_accumulator_not_empty
+     *     being constrained to 0 at the lagrange_first row. If a malicious prover sets
+     *     accumulator_not_empty = 1, INFINITY_ACC_X/Y is disabled and acc_x/y become unconstrained.
+     *     Fixing the transcript_accumulator_not_empty gap (above) also fixes acc_x/y.
      */
     template <typename DataType> class ShiftedEntities {
       public: