feat(prover): chunk the accelerator tables and project them for storage

[Oppen]

What

The six data-proportional accelerator chips — KECCAK, KECCAK_RND, ECSM, ECDAS, HINT,
COMMIT — get max_rows limits and chunking, and all of them are projected in
auto_storage.

Why

Split out of the #874 review, where the DMA table was flagged for having no max_rows
entry. The gap is the whole accelerator family, not DMA:

• All six padded their entire op list into one table (n.next_power_of_two().max(4)),
  so table height is proportional to guest data with no ceiling. At epoch_size_log2 = 23
  a keccak- or ECSM-heavy epoch is a single multi-GB table — and a single table is the one
  thing no storage mode can stream: disk-spill bounds memory per chunk, and there was
  only ever one chunk.
• KECCAK, KECCAK_RND, ECSM and ECDAS did not appear in auto_storage::table_specs at
  all, so the Ram/Disk estimate under-projected precisely the programs most likely to
  need Disk. (COMMIT was already projected.)

Why chunking is sound here

Every one of these ConstraintSets is row-local — none references main(1, ..) — so no
constraint spans a chunk boundary, and the buses they drive are a LogUp multiset argument
that is indifferent to which table a row sits in. KECCAK_RND splits on whole permutations:
one call is 24 contiguous rows (ROUNDS_PER_OP), and its limit divides by that.

Limits

Same effective-width model as the core chips (main_cols + 3 × buses, MEMW's 127 @ 2^19 as
the baseline):

Table	Main	Bus	Eff.width	Max rows
KECCAK	511	134	913	2^16
KECCAK_RND	1480	1031	4573	2^14
ECSM	667	579	2404	2^15
ECDAS	521	388	1685	2^15
HINT	41	27	122	2^19
COMMIT	19	18	73	2^20

accelerator_max_rows_track_effective_width pins each width to the AIR, so adding a column
or a bus to one of these chips fails a test instead of silently leaving its limit stale.

MaxRowsConfig::small() deliberately keeps the production values for these six: shrinking
them to 2^5 splits a committed output or one ECSM ladder into dozens of sub-proofs and
slows every test that uses it. The chunking test shrinks them itself.

Projection

TableLengths gains keccak/keccak_rnd/ecsm/ecdas/hint padded-row counts;
count_table_lengths counts the ecalls and table_specs includes all of them plus
KECCAK_RC. ECDAS is an upper bound (ecdas::MAX_STEPS_PER_ECSM, ≤2 ladder steps per scalar
bit), in the same spirit as the existing LT/MUL/DVRM/BRANCH bounds — the drift test asserts
>= for it and exact equality for the other four.

Breaking

The six tables move out of FIXED_TABLE_COUNT (11 → 5) into TableCounts. That changes
the sub-proof layout and the statement absorbed into the transcript, so the domain tags are
bumped (STATEMENT_V3 → V4, continuation epoch/global V2 → V3). Prover and verifier
must ship together; earlier binaries cannot verify these proofs. #874 and #876 also touch
FIXED_TABLE_COUNT, so whichever lands second rebases.

Validation

• make test-prover: 560 passed, 0 failed, 24 ignored.
• make lint: clean (all four clippy passes, including debug-checks, disk-spill, cuda).
• New accelerator_chunking_tests: effective widths pinned; a 3-call keccak guest at one
  call per chunk produces one KECCAK and one KECCAK_RND chunk per call, each padded to 32
  rows; default limits keep a small program at one chunk per accelerator.
• make test additionally fails on this machine in -p executor --lib with
  dyld: symbol not found in flat namespace '__end' — a link/env failure in a crate this
  PR does not touch (running the prebuilt executor test binary directly reproduces it,
  and the binary contains no prover code). Not investigated here.

Not in scope

Epoch sizing is still cycle-count-only (resume_with_limit), so an epoch's row budget can
still be blown with no cycle-count change. Bounding that needs the executor to stop an
epoch on a weighted row budget, which breaks the "intermediate epoch = exactly 2^k cycles"
invariant (continuation.rs:1327) — deliberately left out.

[jotabulacios]

Automated review pass, with measurements. Run on vm-benchmarks-1 against this PR's own
merge-base (58160b6f); FIXED_TABLE_COUNT and all three domain tags are identical in current
main, and the seven prover-touching commits in between are six GPU paths plus the guest
allocator, so the numbers transfer. Same guest ELF on both arms throughout (the change is
prover-only, so one ELF isolates it).

The description undersells this: it's a prove-time win, not just a memory bound.

Real ethrex block, --continuations --epoch-size-log2 22, 3 runs per cell, all six pairs have
disjoint ranges:

	ram	disk (FORCE_DISK_SPILL=1)
prove time	−3.17%	−3.72%
peak heap	−5.45%	−6.86%
peak RSS	−4.51%	−4.80%

Recursion step (blowup2 preset, 250 epochs, 2 runs per arm):

	base	PR	Δ
prove time	3,284.5 / 3,343.6 s	2,969.3 / 2,978.2 s	−10.27% (disjoint, 306 s of air)
proof size	20,146,413,296 B	25,572,649,808 B	+26.93%
peak heap	102,975 / 105,415 MB	99,437 / 100,585 MB	−4.02% (disjoint)
peak RSS	96,137,108 / 99,179,620 kB	98,672,988 / 99,301,580 kB	+1.36% (ranges overlap)

The time win is 3× bigger in recursion than on a block, and the keccak count is why: the block
makes 10,478 accelerator calls, the recursion verifier 4,311,131.

• risk: the +26.93% proof size is not in the description, and the recursion step is the worst
  place to pay it — its output gets verified again, now carrying ~500 more sub-proofs from
  chunking KECCAK_RND across 250 epochs. Both arms produced their size byte-identically on both
  runs, so this is deterministic, not a noisy read. max_rows is not a neutral ceiling, it is a
  knob trading prove time for proof size, and KECCAK_RND's 2^14 looks too tight. Worth sweeping
  that one value before merge: a larger ceiling means fewer chunks, and most of the −10% should
  survive.
• risk: that +27% is worth checking against the recursion guest's 512 MiB
  MAX_PRIVATE_INPUT_SIZE headroom. Not measured — on a 20-tx block the dumped blob barely moved
  (203 → 202 MB) because chunking never triggers there, but it does in a keccak-heavy regime.
• note: heap drops but RSS does not (−4.02% vs +1.36% with overlapping ranges), so in the
  recursion regime the jemalloc saving does not reach the OS — and RSS is what OOMs a box. That is
  the one regime the motivation leans on.
• note: DMA and DMA_SET stay outside the family fix. Once feat/dma memcpy #874/Perf/dma tail wide memset #896 land they would be the only
  accelerator tables with no max_rows and no auto_storage spec, and DMA is 1,581,885 rows on a
  real block. Both are row-local, so extending the chunking to them is sound — worth a follow-up
  rather than leaving the family half-covered.
• nit: ops_per_chunk = (max_rows.keccak_rnd / ROUNDS_PER_OP).max(1) breaks the rows ≤ max_rows
  invariant for any limit below 24 — deliberate, since a permutation cannot be split, but the
  effective floor of 24 is not stated. A debug_assert! would pin it.
• nit: air_trace_pairs pairs AIRs to traces with .zip(), which truncates silently on a length
  mismatch; the proof then fails the expected_proof_count check at verify time instead of at
  prove time. A debug_assert_eq! on the lengths moves the error to where the bug is.

Chunking soundness checked and came back clean: none of the six ConstraintSets references
main(1, ..) or any nonzero offset, an empty op list still yields one padded chunk so
validate()'s ≥1 holds for every table, padded_chunked_rows reproduces ops.chunks() exactly
including the empty case, FIXED_TABLE_COUNT - 1 stays correct with HALT still among the fixed
five, and leaving CONTINUATION_GLOBAL_TAG at V2 is right — the global statement absorbs the ELF
digest, epoch count, private pages, FRI degree and touched page bases, but not the table counts.