Say what the new checks actually do

[MauroToscano]

Targets feat/skip-empty-tables (#977), not main — every text below only exists on that branch.

Comments and docs only. No code changes: git diff -U0 -- '*.rs' has zero non-comment lines.

Came out of a review of #977. The change itself holds up — I could not construct a witness the verifier accepts via a declared-away table, and the bus argument closes: bus_id is the α⁰ term so no cross-bus cancellation, every Alu receiver pins a disjoint alu_flags set, every droppable table has a mandatory anchor, and the CPU's dispatch flags are pinned to the ELF through packed_decode → preprocessed DECODE at multiplicity 1 − WORD_INSTR. What needed fixing was the prose around it.

The three that are security claims

is_final is defense in depth, not a plugged hole. statement.rs said the only thing separating a final from a non-final epoch's AIR set was the sub-proof count arithmetic. It was not the only thing, and it is worth being precise because someone will eventually lean on this. A role flip was already rejected three ways: the expected count moves by one; deleting HALT's sub-proof to compensate drops its main Merkle root from the Phase A absorption and re-randomizes every downstream challenge; and HALT's 36 bus interactions are hardcoded Multiplicity::One (1 Ecall receive, 31 Memw sends, 4 Memory), so its contribution cannot be absent from a balanced sum. That last one is also what makes "the last epoch really halted" a constraint rather than a convention. Binding the role explicitly is still the right call — it just should not be described as closing a live gap, in case a future reader weakens one of the three that actually hold it down.

The accelerator <= 1 cap is a shape restriction. Its comment said it beat a cross-check that "would only catch it once the counts had already sized the AIR set". Both verifiers run the cross-check first — verify_proof_parts: validate → total-vs-proofs.len() → VmAirs::new, and verify_epoch the same. What the cap actually buys is the per-field shape, which the cross-check misses because it constrains only the total: inflate keccak, lower another count by the same amount, and the sum still matches. Worth keeping, worth stating correctly. The usize::MAX wrap story in the test docstring belongs to total() and to counts_that_wrap_have_no_total, so it moved there.

verify_proof_parts still warned that a zero count removes constraint sets — now the legitimate, expected shape for eighteen of the twenty counts, and in direct contradiction of validate's own rewritten doc.

The rest

• ECSM/ECDAS and HINT are absent, not "empty/all-padding" — those two comments sit directly above the generate_optional calls that made them false.
• Traces: every Vec field can be empty except cpus and memw_registers. Only the six accelerators said so, which reads as a distinction that isn't there — this PR's own traces.memws[0] → memw_chunk_rows fixes exist because it isn't. Stated once at the struct level.
• FIXED_TABLE_COUNT: HALT is why it isn't simply "always" — non-final epochs size with FIXED_TABLE_COUNT - 1, and it's pub.
• TableCounts: no longer "number of chunks for each split table" — six fields aren't chunk counts.
• MUL/DVRM dedup mirrors chunk_and_generate_optional now (4 sites).
• table_specs never did match air_trace_pairs order and doesn't need to — all three consumers sum or sort. Noted instead that it models 11 of 20 tables, so a keccak- or ecdas-dominated run is under-estimated.
• prove_and_verify_vm_minimal no longer proves "all VM tables".
• docs/continuations_design.md §7 is the only place enumerating the epoch statement encoding, so it has to list is_final — someone reproducing it for an independent verifier would reject every honest proof. §8's bullet gets the fuller argument.

Separately, not fixed here

Two pre-existing bugs found in the same area, both worth their own PR:

• count_table_lengths drops every word (*W) instruction from the SHIFT/MUL/DVRM/LT counters (trace_builder.rs sizing pass vs. the cpu32_chip_op routing). A 32-bit-arithmetic Rust guest builds full-size tables while the sizing pass reports zero rows, so auto_storage::decide returns Ram on a run that needed Disk. Byte-identical on main; no current fixture reaches it.
• auto_storage_tests.rs runs in no CI job — #[cfg(all(test, feature = "disk-spill"))], and the Disk-spill job's filter doesn't match the names. It's the direct consumer of this PR's padded_chunked_rows_optional change. Appending auto_storage to that job's filter would cover it.