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.