fix(lfm,tests): the eleven pins the main-sync port left behind, each against its mover

crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp

@@ -1097,7 +1097,31 @@ void permute_probe_matches_the_oracle_table() {
 // ---------------------------------------------------------------------------
 uint64_t run_grind(const uint64_t inner[4], uint8_t factor, uint64_t base, uint64_t count) {
     const uint64_t limit = (uint64_t)1 << (64 - factor);
-    uint64_t result = UINT64_MAX;
+    // ⛔⛔ `unsigned long long`, NOT `uint64_t`, AND THAT DIFFERENCE WAS THE BUG.
+    // The kernel takes `volatile unsigned long long *` because that is the type
+    // CUDA's `atomicMin` overload wants, so this object's address is handed out
+    // under it. `uint64_t` is `unsigned long long` on Darwin/arm64 and
+    // `unsigned long` on LP64 glibc — a DIFFERENT type of the same width — so on
+    // Linux the cast type-punned, and with `#include "rpx.cu"` putting the whole
+    // kernel in this translation unit, GCC 13.3 at -O2 was free under TBAA to
+    // assume a write through `unsigned long long *` could not touch an
+    // `unsigned long`, and to keep `result` in a register across the inlined call.
+    //
+    // It did. `run_grind` returned `UINT64_MAX` for every input on the box, so
+    // every check below that expects the SENTINEL passed vacuously while every
+    // check that expects a FOUND nonce failed — six rows, at every sha back to
+    // the gated base `c00342c1f`, while the same source passed on a clang/arm64
+    // laptop where the two types coincide. Measured on the box 2026-09-20:
+    // `-O2` → 6 failures; `-O2 -fno-strict-aliasing` → all pass; `-O0` → all pass.
+    //
+    // ⚠ NONE OF THAT WAS EVER A STATEMENT ABOUT THE DEVICE GRIND. This file is a
+    // HOST replay of the kernel source through `cuda_host_shim.h`; the defect
+    // was in the harness holding the result, not in the kernel it was testing.
+    // ⛔ Do not "tidy" this back to `uint64_t`: matching the pointer type the
+    // kernel is given is what makes the access well-defined, and the box gate
+    // carries a mutation that restores `uint64_t` and requires those six rows
+    // back — so the tidy-up would be caught, loudly, by a red nobody wants again.
+    unsigned long long result = UINT64_MAX;
     CUDA_HOST_SINGLE_THREAD();
     rpx_grind_search(inner, limit, base, count, (volatile unsigned long long *)&result);
     return result;

others/lfm-migration-riders.md

@@ -19,11 +19,23 @@ draw counts. Acceptable — hence a rider, not a fix.
 
 ## 2. One-byte pad at the end of the statement encoding
 
+**★ RESOLVED — the pad arrived, and nobody aimed it here.** #977 took the six
+accelerator chips out of `FIXED_TABLE_COUNT` (11 → 5) and made them counted, so
+the statement absorbs six more `u64` counts (`NUM_TABLE_COUNTS` 15 → 21, `+48`,
+which moves no shift), and the same PR appended `is_final` as the statement's
+last byte (`+1`). `215 + 49 = 264 ≡ 0 (mod 4)`. The constant term's own shift is
+gone; the cursor Phase A inherits is now `L mod 4` alone, so the splice is free
+whenever `L ≡ 0 (mod 4)` instead of `L ≡ 1`. The domain tag went to
+`LAMBDAVM_CONTINUATION_EPOCH_V5` along the way, so the tag bump the note at the
+bottom asks for was paid too. Everything below is the analysis as it stood, kept
+for the arithmetic; the numbers in it are the pre-#977 encoding.
+
 **What:** pad the continuation-epoch statement so its length is `≡ 0 (mod 4)`.
 
-**Why:** the encoding is `207 + L + 16R` bytes (not 223 — an arithmetic slip in
-the first report, now machine-checked by
-`epoch_statement_cursor_is_three_plus_output_len`). Every subsequent absorb
+**Why:** the encoding is `264 + L + 16R` bytes (207 when this was written, then
+215 with `TableCounts::blake3`; not 223 — an arithmetic slip in the first
+report, now machine-checked by
+`epoch_statement_cursor_is_the_output_len_alone`). Every subsequent absorb
 inherits the resulting cursor — including all of Phase A, whose roots are
 individually 32-byte-aligned but land misaligned because they inherit the
 statement's cursor. (Alignment is a property of the CURSOR, not of the field:

prover/src/lfm/SOUNDNESS.md

@@ -193,10 +193,28 @@ is what keeps `E` small. At `T = 24` with tables at their row cap (`L_t = 12`),
 `3E = 1,092` base candidates and `P ≈ 2.5·10^−7`. At a larger `T ≈ 60`, `E = 904` and
 `P ≈ 6.3·10^−7`.
 
-`T = 24` is **measured, not assumed**: reading a real two-epoch continuation proof
-(`machine_tests::arena_filler_reads_real_committed_roots`) gives 24 sub-proofs for an
-intermediate epoch and 25 for the final one, the extra being HALT. It was an honest hedge when
-this section was written; it no longer needs to be.
+`T = 24` was the epoch shape when this section was written: a real two-epoch continuation proof
+gave 24 sub-proofs for an intermediate epoch and 25 for the final one, the extra being HALT.
+
+⚠ TWO CORRECTIONS, and the bound survives both.
+
+**`T` is now SMALLER, and the bound is monotone in `T`.** #977 (`892c7d1bc` on this lineage) took
+`FIXED_TABLE_COUNT` 11 → 5 and made COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS and HINT counted, so
+an epoch that never reaches one carries no sub-proof for it — `epoch_verify_tests`'
+`SUB_PROOFS` measures 16 on the fibonacci fixture, down from 25. `E = 4 + Σ_t (3 + L_t)` is
+increasing in `T`, and `P ≤ 3E · 2^−32` is increasing in `E`, so a smaller `T` only lowers `P`:
+the `P ≈ 2.5·10^−7` quoted at `T = 24` remains a valid upper bound, now a conservative one. The
+`T ≈ 60` figure is the side that matters for a real block and is untouched.
+
+**The cited test does not pin the number.** `machine_tests::arena_filler_reads_real_committed_roots`
+asserts `tables > 0`, one main root per sub-proof, and that no root is all-zero — never a count.
+So "measured, not assumed" was true of the run that was done and false of the suite: nothing
+would have failed when `T` moved, and nothing did. The count that IS asserted is
+`epoch_verify_tests`' `SUB_PROOFS`, on a different fixture (`epoch_tests::real_epoch`) than the
+two-epoch continuation this paragraph describes. `T` for THAT fixture is unmeasured since #977;
+it is bounded above by the 25/26 ceiling in
+`tests::constraint_artifact_tests::continuation_epoch_constraint_leg`, which is what the bound
+above should be read against until someone runs it.
 
 **State it as `< 10^−6` per proof at production shapes**, growing by `≈ 1.05·10^−8` per additional
 table — each table contributes `3 + L_t ≈ 15` extension draws, so the per-table increment is 15×

prover/src/lfm/blake3_chip_tests.rs

@@ -1215,8 +1215,29 @@ fn the_flip_inventory_of_registered_programs_is_pinned() {
     /// takes a 64-byte block where the keccak sponge takes a 136-byte rate, so
     /// the same message divides into more compressions — which is the in-machine
     /// half of the cost the campaign priced, visible here as a row count.
+    ///
+    /// ★ StatementReplayV0 moved 9 → 10 on the main-sync port, and the mover is
+    /// NAMED rather than absorbed.
+    ///
+    /// MOVER: `892c7d1bc` (main's `c2ac5d546`, #977) — arm (ii), the STATEMENT
+    /// ENCODING. That merge's two arms are (i) the table set shrank, empty
+    /// tables now being elided rather than padded, and (ii) the absorbed epoch
+    /// statement grew. This pin is on (ii); `epoch_verify_tests`' SUB_PROOFS is
+    /// on (i).
+    ///
+    /// #977 took the six accelerator chips out of
+    /// `FIXED_TABLE_COUNT` (11 → 5) and made them counted, so the epoch
+    /// statement absorbs six more `u64` counts, and the same PR appended
+    /// `is_final` as the statement's last byte. `NUM_TABLE_COUNTS` went 15 → 21
+    /// and `EpochStatementShape::byte_len` gained a trailing `+ 1`: the
+    /// statement is **+49 bytes**, which is under one 64-byte `Blake3Chain`
+    /// block and therefore worth exactly one more compression.
+    ///
+    /// TranscriptReplayV0 stays at 8, and that is what keeps this a pair rather
+    /// than two literals: it replays no statement, so a change that moved BOTH
+    /// counts would not be this one and would have to name itself.
     const TRANSCRIPT_REPLAY_BLAKE3_ROWS: usize = 8;
-    const STATEMENT_REPLAY_BLAKE3_ROWS: usize = 9;
+    const STATEMENT_REPLAY_BLAKE3_ROWS: usize = 10;
 
     use super::instr::Instr;
     use super::programs::{

prover/src/lfm/constraint_tests.rs

@@ -1477,10 +1477,19 @@ fn quotient_rows(artifact: &ConstraintArtifact, log2_trace_length: u32) -> usize
 ///
 /// The composition is `others/lfm-constraint-lowering-design.md` §8.2.2's, which
 /// `tests::constraint_artifact_tests::continuation_epoch_constraint_leg` derives
-/// from the real epoch shape and pins against a measured 24/25 sub-proof count:
-/// 14 split-table families at one chunk each, plus the nine fixed tables an
-/// intermediate epoch carries (all ten on the final one), plus one L2G_MEMORY.
-/// PAGE does not appear — epochs pass `page_configs = &[]`.
+/// from the real epoch shape and pins against a measured 25/26 sub-proof
+/// CEILING: 14 split-table families at one chunk each, plus the nine
+/// always-on-or-accelerator tables an intermediate epoch can carry (all ten on
+/// the final one), plus one L2G_MEMORY. PAGE does not appear — epochs pass
+/// `page_configs = &[]`.
+///
+/// ⚠ THE FIXED TERM IS A CEILING SINCE #977, not a floor. That PR took
+/// `FIXED_TABLE_COUNT` 11 → 5, moving COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS
+/// and HINT into `TableCounts` — a run that never reaches one carries no
+/// sub-proof for it. So the sums below are what a workload that calls every
+/// accelerator pays, which is the right figure for a budget and the wrong one
+/// for a specific epoch: `epoch_verify_tests` measures 16 on the fibonacci
+/// fixture, which reaches none of the six.
 ///
 /// ### What this instrument cannot see
 ///
@@ -1499,8 +1508,16 @@ fn continuation_epoch_constraint_leg_cost() {
         "CPU", "LT", "SHIFT", "EQ", "BYTEWISE", "STORE", "CPU32", "MEMW", "MEMW_A", "MEMW_R",
         "LOAD", "MUL", "DVRM", "BRANCH",
     ];
-    /// `FIXED_TABLE_COUNT`'s ten, which contribute exactly one sub-proof each
-    /// regardless of `TableCounts`. HALT is last: an intermediate epoch drops it.
+    /// The ten an epoch can carry outside the split families: `FIXED_TABLE_COUNT`'s
+    /// five (BITWISE, DECODE, KECCAK_RC, REGISTER, HALT), which contribute one
+    /// sub-proof each regardless of `TableCounts`, plus five of the six
+    /// accelerators #977 moved into `TableCounts`. HALT is last: an intermediate
+    /// epoch drops it.
+    ///
+    /// ⚠ HINT is the sixth accelerator and is absent from this list, which is
+    /// why the enumeration is ten where the pre-#977 constant said eleven. The
+    /// omission is inherited, not deliberate, and it makes these sums a LOWER
+    /// bound on the accelerator-inclusive ceiling.
     const FIXED: &[&str] = &[
         "BITWISE",
         "DECODE",
@@ -1554,16 +1571,16 @@ fn continuation_epoch_constraint_leg_cost() {
     let design_intermediate = families_unfused + fixed_unfused + l2g_unfused;
 
     println!(
-        "\ncontinuation epoch, constraint leg (minimum shape, 25 sub-proofs)\n\
+        "\ncontinuation epoch, constraint leg (minimum shape, 25-sub-proof ceiling)\n\
          \x20 14 split families        {families:>7}  (unfused {families_unfused})\n\
          \x20  9 fixed, no HALT        {fixed_no_halt:>7}  (unfused {fixed_unfused})\n\
          \x20  1 L2G_MEMORY            {l2g:>7}  (unfused {l2g_unfused})\n\
          \x20 INTERMEDIATE leg         {intermediate:>7}  vs the design's {design_intermediate}\n\
          \x20 + recombination @ log2(N) = {LOG2_TRACE_LENGTH}  {recombination:>7}  \
          (zerofier, beta-fold, one division, claimed-parts Horner, assert)\n\
-         \x20 INTERMEDIATE total       {:>7}  over 25 sub-proofs\n\
+         \x20 INTERMEDIATE total       {:>7}  over <=25 sub-proofs\n\
          \x20 FINAL epoch (+HALT)      {final_leg:>7} leg, {final_total} total, \
-         over 25 sub-proofs",
+         over <=26 sub-proofs",
         intermediate + recombination
     );
 

prover/src/lfm/epoch_tests.rs

@@ -23,7 +23,8 @@
 //!
 //! It stops at the challenges. That the legs then CONSUME these cells is
 //! [`the_legs_consume_the_replayed_challenges`]'s job, and the whole-epoch
-//! composition (25 sub-proofs behind one statement) is not built here.
+//! composition (16 sub-proofs behind one statement on this fixture, 25 at the
+//! post-#977 ceiling) is not built here.
 
 use stark::config::Commitment;
 use stark::proof::stark::MultiProof;