fix(continuation): prove the global memory argument AFTER the epochs, not beside them

[MauroToscano]

fix(continuation): prove the global memory argument AFTER the epochs, not beside them

pt/serialise-global @ 111ca721 → per-table-gpu. One file, prover/src/continuation.rs,
+43 / −55. One signed commit. make lint exit 0 over all three feature sets; make fmt a
no-op.

Measured, one RTX 5090 (31.40 GiB driver-visible), 2^21 / blowup 4, TABLE_PARALLELISM=4,
10 Hz VRAM sampling, census 525,932,288 cells identical in every arm:

arm	GPU peak	of card
no serialisation, LAMBDA_VM_VRAM_BUDGET_MB=16000	31,864 MiB	97.7 %
this change, same budget	24,536 MiB	75.2 %
no serialisation, default budget	32,056 MiB	98.3 %

The 7.3 GiB is this change's. The budget did nothing to the peak — that is what the first row is
for, and it is why this lands on its own rather than behind a scheduler rewrite.

---

What changes

The global prove ran on its own scoped thread so it would overlap the tail epochs. That
scope.spawn is deleted. boundary_rx now stays outside the epoch scope and is drained once with
try_iter() after the scope joins and after the existing first_err check; prove_global runs
inline there. The global_result mutex and the GlobalResult alias go with it — the error
propagates with a plain ? instead of through a slot, and the "an epoch already failed, skip the
global prove" guard is subsumed by the first_err early return that was already there. The
comment at the channel declaration, which asserted the overlap, is rewritten so the two ends of
the mechanism cannot drift apart again.

★ This is a revert of a schedule optimisation, not a redesign. The safety argument is the
overlap's own comment:

the global proof consumes only execution artifacts (boundaries, ELF, genesis pages) — never an
epoch proof — so this is pure schedule. Proof bytes are unchanged.

Both halves still hold, in the other direction. Nothing about the argument moved: the same
boundaries, the same touched_page_bases, the same global_transcript, the same
multi_prove call with the same inputs in the same order.

Two mechanical notes. The boundary channel is unbounded, so the producer never blocked on it
before and does not now — the epoch pipeline's capacity-1 build and prove channels remain the only
backpressure. And the boundaries were always Arc shares of the ones the epoch prover holds, so
buffering them in the channel instead of in a thread-local Vec costs nothing: same allocations,
same lifetimes, one fewer copy of the pointer.

The mechanism

Every multi_prove builds its own VramGate::new(vram_budget) (crypto/stark/src/prover.rs,
the R1 pre-pass), and vram_budget is detect_vram_budget_bytes — 80 % of total device memory.
An epoch prove and the global prove are two multi_prove calls. Overlapped, they put

2 × 25.12 GiB = 50.24 GiB of admission budget on a 31.40 GiB card

with nothing summing the two. Neither gate can see the other, and neither is wrong about anything
it was asked.

⚠ And each additionally holds a working set no gate counts at all. The R1 main commit's handle
keeps the column-major LDE, the trace-domain snapshot and the full Merkle node buffer resident
(math-cuda/src/lde.rs::coset_lde_row_major_with_merkle_tree_keep — tree: Some(tree),
retain_trace_col_major hard-coded true) from the commit until that table's own rounds task ends.
Round 1 is a hard barrier — every root must be in the transcript before the LogUp challenges are
sampled — so at the R1/R2 transition the card holds

Σ_t n_t · (40·m_t + 128)     bytes, at blowup 4

while the gate's used has fallen back to zero. Measured at this posture: 11.86 GiB for an
epoch prove, 6.0 GiB for the global prove. Two proves, two barriers, two budgets, one card.

The abort set identified both proves, which is why this is a mechanism and not a story. Eight
threads aborted in the same instant through gpu_lde::refuse_host_recovery, and their shapes
partition cleanly:

shape	table	lives only in
main 9 / aux 1 ×6	l2g_global_air	prove_global
main 21 / aux 5 @ LDE 2^22	BITWISE (fixed 2^20 height)	an epoch prove
main 18 / aux 3 @ LDE 2^21	LOAD	an epoch prove

local_to_global::cols::NUM_COLUMNS is 9 and bus_interactions is 2 interactions, so
aux = ⌈2/2⌉ = 1. The epoch-local l2g_memory_air carries memory_bus_interactions (2) plus
range_check_interactions (1 + |RANGE_CHECKED_HALFWORDS| + 1 = 4) = six, so aux 3, never 1.
Nothing else in the registry is 9 wide. BITWISE and LOAD are absent from prove_global's table
set entirely, which is l2g_global_air × epochs plus global_memory_air × touched pages.

The overlapped run's VRAM trace says the same thing in one shape: a single 31 s hump spanning 58
tables in one monotone ladder — one prove's worth of tables laddering down on top of another
prove's tooth.

⇒ The window opens about builders + 2 epochs before the end, and never earlier. The producer
cannot run further ahead than the capacity-1 build channel, two builders and the capacity-1 prove
channel allow, and the global thread blocks on boundary_rx until boundary_tx drops with the
producer. That is why the same configuration was a coin flip: it aborted twice and succeeded once,
because whether the hump lands on a tooth's peak is a race whose width varies run to run.

The measurement

Base 19 epochs in 251.8 s, PROVED AND VERIFIED, total 459.72 s.

Seven quantities were pre-registered before the run, with falsifiers.

	pre-registered	measured
P0	bundle-loaded control unmoved	+1.1 %	✓ the change does not reach outside prove_continuation
P1	peak 26,000–31,100, < 31,500	24,536	✓ under, and below the band — see below
P2	a distinct final global tooth appears	238–247 s, 14,456 MiB, monotone ladder, ~10 s	✓
P3	floor unchanged, 4.5–6.7 GiB	4,440–5,560 MiB	✓
P4	epoch teeth unchanged, max ≈25,900	23,960	lower — see below
P5	base wall +5–15 %	total 474.59 → 459.72 s, −15 s	reconciled, see below
P6	k=4 survives	yes	✓

★ P1 and P4 came in low for one reason, and it was an error of mine that two mistakes had been
hiding. The prediction priced the co-resident set as "fill the byte budget", but
VramGate::acquire blocks; it does not skip ahead — run_admitted workers pull indices in
heaviest-first walk order and queue behind each other. At 15.625 GiB the two heaviest 2^21 tables
are est 9.80 + 9.56 = 19.36 GiB, so the second blocks and one heavy table proves at a
time. That is a 34 % over-estimate of the incremental set (9.84 predicted against 6.54 actual),
and it was cancelling a 15 % under-estimate of the barrier (10.3 predicted against the 11.86
the tooth implies). Net +1.90 GiB, which is exactly the gap. The two errors agreeing is the
failure mode this campaign has on the record, and the count matching was what concealed it: fix
both, and do not quote a tooth match as corroboration of either input.

★ P5 is reconciled rather than falsified, and the honest verdict is "not detectable". The
quantity was mis-named — the added work lands after the epoch loop, so it cannot appear in a
timer around the epoch loop. In the total it appears as −15 s, not +31. The overlapped 31 s was
a lock-queue artefact: gpu_lde::r2_serialize_guard is a process-wide static Mutex serialising
every table's R2 submission window across proves, not just across tables, and the two proves
were also sharing one rayon pool. Alone, the global prove ran ~10 s — 3.1× faster — and the
epoch tail got the lock back. ⇒ The cost of serialising is not 31 s of margin bought with wall
time; removing the contention paid for the serialisation.

Two independent readings of the global prove's working set, which is the number the whole account
turns on:

route	value
standalone tooth 14,456 − between-epoch floor 4,984	9.25 GiB
unserialised spike 31,864 − that run's other teeth ≤22,104	9.53 GiB

They agree to 288 MiB (3 %) — the increment the overlap adds to a tooth is the global
prove's entire working set, which is what "no gate subtracts it" predicts and nothing else does.

The caveat, stated rather than buried

⚠ Serialising can convert a shared overflow into a solo one. Alone, the global prove's tooth is
floor + B_global + Σ live increments, and B_global grows with the touched-page count P at
2^18 × 288 B = 0.0703 GiB per global_memory_air. At the default budget it admits ~17 tables
concurrently, and:

P	global tooth alone	of card
0	27,504 MiB	85.5 %
50	31,104	96.7 %
63	32,040	99.6 %

⇒ Run this with LAMBDA_VM_VRAM_BUDGET_MB=16000 until the gate is process-wide and its
scheduler budget is decoupled from admit's per-table ceiling. At 16000 the same tooth is
21,904 MiB at P = 0 and 29,104 at P = 100, and the constant still clears the largest single
dispatch (≈6.7 GiB for a 2^21 main commit) with room, so no transient is declined — which
matters, because a declined transient on a device-only table is refuse_host_recovery, the
abort this PR exists to remove.

⚠ P for this block is unmeasured. It is ContinuationProof::touched_page_bases.len(), or the
count of main 4 / aux 1 entries in the global prove's [prover] table walk R1 line. Read it
before running at the default budget.

What this does not fix

• The epoch prove is still ungoverned. B_epoch is invisible to the gate whether or not the
  global prove overlaps, and at this posture it is 11.86 GiB of the 24,536 MiB peak. The durable
  form is one process-wide VramGate, seeded with the barrier and charging tasks only their
  increment, with its budget decoupled from admit's ceiling. This PR is what makes that
  gate's budget satisfiable: it turns B_epoch + B_global into max(B_epoch, B_global), which
  at 2^21 is 15.8 GiB of headroom against 6.3.
• 2^22 at blowup 4 remains out of reach, and this PR does not change that.
  B_epoch(2^22) ≈ 23.7 GiB against 27.7 GiB of usable working set, with a single MEMW
  incremental at 11.3 GiB — no k, no budget and no schedule fits that. It needs the barrier
  levers (free the trace snapshot at R1 exit, −8·C_main; download the main Merkle tree after the
  root, −128·R_tot; together −29…39 %) and a row cap on the tables MaxRowsConfig does not
  cover.
• A ~5 GiB standing floor persists between proves and belongs to no prove. It is unattributed
  here and is measured separately.

Gate — MEASURED

--lib     1090 passed / 9 failed / 46 ignored     against a pre-registered 1091 / 8 / 46
--list    1145                                     (independent, one invocation) ✓
stark / math-cuda                                  untouched, as predicted ✓

The ninth is continuation::tests::test_prover_panic_mid_pipeline_returns_err, and it is the one
exception this gate reserved in advance. Every other name matches the eight below, byte for byte.

⚠ Stated precisely, because the looser version would overclaim in this PR's favour: that red neither
implicates nor exonerates this change. The bound it failed is a 300 s whole-call timeout —
to-panic + shutdown > 300 — which has two summands and isolates neither. This change deletes a
scope.spawn on the shutdown path, so it could only ever move the shutdown half, and a whole-call
bound does not measure that half. ⇒ The failing summand is unknown, and this PR is not gated on it.

That the failure is not this change's is established separately: it appears on branches without this
commit — #975 read the same ninth name at fdd2e0d1, and passed on a re-run at the same sha, so it is
intermittent under suite load. Its diagnosis is in flight on a separate branch and does not belong here.

ⓘ For the record on what a split bound shows: an instrumented run measured
total 490.19 s = to-panic 489.10 s + shutdown 1.09 s — a healthy 1.09 s shutdown inside a run this
300 s bound would have failed. That is why the summand matters and why the count alone does not settle it.

Gate — as pre-registered

Pre-registered before the run as a name set, not a count — a count is invariant under both a
regression and a substitution, which is how three runs of #975 read 1090 / 9 / 46 twice with a
different failure the second time., not a count — a count is invariant under both a
regression and a substitution, which is how three runs of #975 read 1090 / 9 / 46 twice with a
different failure the second time.

--lib counts    1091 passed / 8 failed / 46 ignored = 1145
--list          1145                                        (independent, one invocation)
failure NAMES   byte-identical to the eight                 (extract and diff, do not eyeball)

The eight, byte-identical across #973, #974 and #975 (seven are the RPX pin's, one — the_closure… —
pre-dates the pin; the pin registered ten and the format deletion removed the two batched census tests):

lfm::epoch_tests::the_closure_rejects_a_moved_index_or_output
lfm::fri_tests::the_emitted_permutation_count_meets_the_pinned_prediction
lfm::fri_tests::the_fri_join_adds_no_second_point_derivation
lfm::machine_tests::register_derivation_cost
lfm::machine_tests::the_register_derivation_matches_production
lfm::machine_tests::the_register_derivation_proves_and_verifies
lfm::machine_tests::transcript_replay_cell_counts
lfm::per_table_census_tests::the_blake3_tenant_socket_matches_the_record

Extracted mechanically, never read off the screen:

cargo test --release -p lambda-vm-prover --lib 2>&1 | tee lib.log
sed -n '/^failures:$/,/^test result:/p' lib.log | grep -E '^    [a-z]' | sort > names.new
diff names.new names.expected      # must be empty

⚠ A ninth red is acceptable in exactly one case: if it is
continuation::tests::test_prover_panic_mid_pipeline_returns_err. That test bounds an honest
prove at 300 s, which binds under load rather than measuring the wedge it was written for; the
mechanism is named and the fix is separate, on pt/panic-timer. Any other ninth name is a
regression in this change and blocks it — the point of a set is that a substitution cannot pass.

stark and math-cuda are untouched by a change confined to prover/src/continuation.rs, so
their counts must be unmoved.