Say what the new checks actually do

docs/continuations_design.md

@@ -502,7 +502,10 @@ weaken soundness — and it pins every proof to its program and position, so a p
 can't be replayed elsewhere:
 
 - Each **epoch** absorbs: a domain tag, the ELF digest, the public output, the
-  table layout, and the **epoch label** (its position).
+  table layout, the **epoch label** (its position), and **`is_final`** (whether it
+  carries HALT). The table layout is every `TableCounts` field individually, so a
+  layout that moves a count from one chip to another diverges here even when the
+  total is unchanged.
 - The **global** proof absorbs: a (distinct) domain tag, the ELF digest, the
   **epoch count**, the **private-input page count** (§3.6), and the **touched page-base
   set** — so the whole genesis AIR layout (which GLOBAL_MEMORY tables exist and which are
@@ -544,9 +547,16 @@ becomes an **explicit verifier action**:
 
 - **Enumerate, don't trust.** The verifier assigns each epoch's `label` and the
   `is_final` flag **by position** (`0..N-1`; the last is final), so the prover can't
-  relabel, reorder, truncate, or append epochs — a wrong label diverges that epoch's
-  Fiat-Shamir challenges, and a wrong `is_final` builds the HALT table in/out and
-  mismatches the committed proof.
+  relabel, reorder, truncate, or append epochs. Both are absorbed into the epoch
+  statement, so either one wrong diverges that epoch's Fiat-Shamir challenges.
+  `is_final` is additionally load-bearing three more times: it moves the expected
+  sub-proof count by one (`FIXED_TABLE_COUNT - 1` for non-final epochs); 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 bus
+  interactions are hardcoded `Multiplicity::One`, so its contribution cannot be
+  missing from a balanced sum. That last one is what makes "the last epoch really
+  halted" a constraint rather than a convention — a truncated run's non-halting
+  last epoch is built *with* HALT and fails the balance.
 - **Derive the register / x254 chain.** Epoch 0's register INIT is derived from the
   ELF entry point; epoch *i+1*'s INIT is derived from epoch *i*'s bundle `reg_fini`
   (incl. x254 @ 508). So `init(i+1) == fini(i)` is now *enforced by the verifier

prover/src/auto_storage.rs

@@ -104,7 +104,12 @@ fn aux_cols(bus_count: usize) -> u64 {
     bus_count.div_ceil(2) as u64
 }
 
-/// Per-table specs in the same order as `air_trace_pairs` in `prove`.
+/// Per-table specs for the heap estimate. The order is not meaningful — every
+/// consumer sums or sorts — and it does not track `air_trace_pairs`.
+///
+/// Note this list models only the tables `TableLengths` carries: there is no
+/// entry for eq, bytewise, store, cpu32, keccak, keccak_rnd, ecsm, ecdas or
+/// hint, so a run dominated by one of those is under-estimated.
 fn table_specs(lengths: &TableLengths) -> Vec<TableSpec> {
     let bitwise_rows = BITWISE_ROWS as u64;
     let register_rows = NUM_REGISTER_ADDRESSES.next_power_of_two() as u64;

prover/src/lib.rs

@@ -80,14 +80,20 @@ pub struct RuntimePageRange {
     pub count: u64,
 }
 
-/// Number of tables that always contribute exactly one sub-proof, regardless
-/// of `TableCounts`: bitwise, decode, halt, keccak_rc, register. The
-/// accelerator chips are counted instead — a run that never calls one carries
-/// no table for it.
+/// Number of tables that contribute exactly one sub-proof regardless of
+/// `TableCounts`: bitwise, decode, halt, keccak_rc, register. The accelerator
+/// chips are counted instead — a run that never calls one carries no table for
+/// it.
+///
+/// HALT is the exception, and the reason this is not simply "always": a
+/// continuation epoch carries it only when it is the final one, so `verify_epoch`
+/// sizes non-final epochs with `FIXED_TABLE_COUNT - 1`. Any caller computing an
+/// expected sub-proof count for a continuation epoch must do the same.
 pub const FIXED_TABLE_COUNT: usize = 5;
 
-/// Number of chunks for each split table.
-/// The verifier needs this to reconstruct matching AIRs.
+/// How many sub-proofs each counted table contributes. Chunked chips report
+/// their chunk count; the six accelerators are not chunked and report 0 or 1
+/// (see `validate`). The verifier needs this to reconstruct matching AIRs.
 #[derive(Debug, Clone, rkyv::Archive, rkyv::Serialize, rkyv::Deserialize)]
 pub struct TableCounts {
     pub cpu: usize,
@@ -178,10 +184,13 @@ impl TableCounts {
             }
         }
         // The accelerators are not chunked: `generate_optional` emits one table
-        // or none, so a count above 1 is a shape no prover can produce. Rejected
-        // here rather than left to the sub-proof cross-check, which would only
-        // catch it once the counts had already sized the AIR set. If one of them
-        // ever becomes chunked, this list is what changes.
+        // or none, so a count above 1 is a shape no prover can produce. The
+        // sub-proof cross-check constrains only the *total*, so on its own it
+        // lets an inflated accelerator count through whenever another count is
+        // lowered to match; this pins the per-field shape instead. It is not
+        // load-bearing for memory safety — both verifiers run the cross-check
+        // before any count sizes an AIR set — and if one of them ever becomes
+        // chunked, this list is what changes.
         let at_most_one = [
             ("keccak", self.keccak),
             ("keccak_rnd", self.keccak_rnd),
@@ -1510,8 +1519,11 @@ fn verify_proof_parts(
     decode_commitment: Option<Commitment>,
     page_commitments: Option<&[(u64, Commitment)]>,
 ) -> Result<bool, Error> {
-    // Validate table_counts before constructing AIRs.
-    // A malicious prover could set counts to 0, removing entire constraint sets.
+    // Validate table_counts before constructing AIRs. A zero count is legitimate
+    // for every chip but CPU and MEMW_R — what keeps it honest is the LogUp bus,
+    // not this call (see `TableCounts::validate`). This rejects the two counts
+    // whose absence describes no execution at all, and the accelerator shapes no
+    // prover can produce.
     table_counts.validate()?;
 
     // Bound num_private_input_pages before allocating PageConfigs — the tight honest

prover/src/statement.rs

@@ -162,12 +162,21 @@ pub(crate) fn absorb_statement_with_digest(
     // Continuation epochs additionally bind their position (replay protection)
     // and whether they are the final one. `is_final` decides whether HALT is in
     // the epoch's AIR set, so without it the transcripts of a final and a
-    // non-final epoch carrying the same counts are identical, and the only thing
-    // separating the two AIR sets is the sub-proof count arithmetic in
-    // `verify_epoch`. The verifier derives `is_final` from the epoch's position
-    // in the bundle, so a spliced bundle re-reads an epoch under the other role
-    // and diverges here. Monolithic proofs append nothing, so their encoding is
-    // unchanged.
+    // non-final epoch carrying the same counts are identical. The verifier
+    // derives `is_final` from the epoch's position in the bundle, so a spliced
+    // bundle re-reads an epoch under the other role and diverges here.
+    //
+    // Defense in depth, not a plugged hole: a role flip is already rejected
+    // without this byte, and by more than one check. Re-reading an epoch under
+    // the other role moves the expected sub-proof count by one (`verify_epoch`'s
+    // `FIXED_TABLE_COUNT - 1` arm); 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 own bus interactions are hardcoded
+    // `Multiplicity::One`, so its contribution cannot be absent from a balanced
+    // sum. Binding the role here makes it an explicit statement field instead of
+    // an emergent consequence of those three — do not weaken any of them on the
+    // strength of this byte. Monolithic proofs append nothing, so their encoding
+    // is unchanged.
     if let StatementKind::ContinuationEpoch {
         epoch_label,
         is_final,

prover/src/tables/trace_builder.rs

@@ -1735,8 +1735,8 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec<BitwiseOperation> {
 /// and IS_B20 lookups for carry range checks.
 ///
 /// IS_HALF and IS_B20 are emitted once per raw op. MSB16 is deduplicated
-/// per `max_rows_mul` chunk, mirroring `chunk_and_generate` — a unique signed
-/// op that spans two instances is sent twice and must be tallied twice.
+/// per `max_rows_mul` chunk, mirroring `chunk_and_generate_optional` — a unique
+/// signed op that spans two instances is sent twice and must be tallied twice.
 ///
 /// Returns: Vec of bitwise lookups
 pub(crate) fn collect_bitwise_from_mul(
@@ -1833,7 +1833,7 @@ pub(crate) fn collect_bitwise_from_mul(
 ///
 /// IS_HALF and ZERO (C8/C20) are emitted once per raw op. MSB16 and the
 /// NEG-template ZERO lookups (C3/C5) are deduplicated per `max_rows_dvrm`
-/// chunk, mirroring `chunk_and_generate`.
+/// chunk, mirroring `chunk_and_generate_optional`.
 ///
 /// Returns: Vec of bitwise lookups
 pub(crate) fn collect_bitwise_from_dvrm(
@@ -2803,6 +2803,14 @@ impl CollectedEpoch {
 }
 
 /// All generated trace tables.
+///
+/// Every `Vec` field here may be **empty**: a chip the run never reaches carries
+/// no table at all, so indexing one without checking panics on a program that
+/// happens not to use it. The only exceptions are `cpus` and `memw_registers`,
+/// which are built through `chunk_and_generate` and always carry at least one
+/// (padded) chunk — the same two `TableCounts::validate` requires. Several
+/// fields below spell this out individually; the rule is the struct's, not
+/// theirs.
 pub struct Traces {
     /// CPU execution traces (split into chunks of max_rows::CPU)
     pub cpus: Vec<TraceTable<GoldilocksField, GoldilocksExtension>>,
@@ -3619,7 +3627,8 @@ fn build_traces<I: ImageSource + Sync>(
     };
     let gen_register = || register::generate_register_trace(&register_final_state, register_init);
     let gen_halt = || halt::generate_halt_trace(halt_timestamp, halt_next_pc);
-    // ECSM accelerator traces (empty/all-padding for programs that do not use ECSM).
+    // ECSM accelerator traces. A program that does not use ECSM carries no ECSM
+    // and no ECDAS table at all — not a padded one.
     let gen_ecsms = || {
         generate_optional(
             &ecsm_ops,
@@ -3636,7 +3645,7 @@ fn build_traces<I: ImageSource + Sync>(
             storage_mode,
         )
     };
-    // HINT table (all-padding for programs that make no hint ecalls).
+    // HINT table. Absent entirely for programs that make no hint ecalls.
     let gen_hints = || {
         generate_optional(
             &hint_ops,

prover/src/tests/dvrm_tests.rs

@@ -467,7 +467,8 @@ fn test_dvrm_air_wires_in_chip_constraints() {
 
 /// Regression test for the `Msb16` LogUp over-send bug.
 ///
-/// DVRM is split into chip instances of `max_rows.dvrm` raw ops (`chunk_and_generate`)
+/// DVRM is split into chip instances of `max_rows.dvrm` raw ops
+/// (`chunk_and_generate_optional`)
 /// and each instance deduplicates only its own chunk, sending its three MSB16 sign
 /// lookups once per unique signed op *per instance* (multiplicity = the `SIGNED` bit).
 /// So `collect_bitwise_from_dvrm`, which feeds the BITWISE MSB16 multiplicity, must use

prover/src/tests/mul_tests.rs

@@ -371,7 +371,8 @@ fn test_mul_range_checks_input_halves() {
 
 /// Regression test for the `Msb16` LogUp over-send bug.
 ///
-/// MUL is split into chip instances of `max_rows.mul` raw ops (`chunk_and_generate`)
+/// MUL is split into chip instances of `max_rows.mul` raw ops
+/// (`chunk_and_generate_optional`)
 /// and each instance deduplicates only its own chunk, sending the MSB16 sign lookup
 /// once per unique signed op *per instance* (multiplicity = the `SIGNED` bit). So
 /// `collect_bitwise_from_mul`, which feeds the BITWISE MSB16 multiplicity, must use

prover/src/tests/prove_elfs_tests.rs

@@ -59,9 +59,10 @@ fn memw_chunk_rows(
         .flat_map(|t| (0..t.num_rows()).map(move |row| (t, row)))
 }
 
-/// Run multi_prove and multi_verify for all VM tables.
+/// Run multi_prove and multi_verify over the tables this run actually carries.
 ///
-/// Includes: CPU + Bitwise + LT + MEMW + LOAD + DECODE + MUL + BRANCH + HALT + REGISTER + PAGEs
+/// The AIR set comes from `traces.table_counts()`, so a chip the program never
+/// reaches is absent from both sides rather than proved as a padded table.
 ///
 /// Uses minimal bitwise (no full 2^20 preprocessed table) but DECODE is always preprocessed.
 pub(crate) fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool {

prover/src/tests/skip_empty_tables_tests.rs

@@ -361,15 +361,18 @@ fn validate_still_requires_cpu_and_the_register_file() {
 }
 
 /// The counts ride in the proof, so they are the prover's to choose, and the
-/// sub-proof cross-check compares only their sum. A plain `+` wraps silently in
-/// release (the workspace sets no `overflow-checks`), so an attacker can park
-/// one field near `usize::MAX`, pick a second to carry the sum around to
-/// whatever `proofs.len()` is, and pass that check with the huge field intact —
-/// straight into `VmAirs::new`, which sizes a `Vec` from it.
-/// The six accelerators are not chunked — `generate_optional` emits one table or
-/// none — so any count above 1 describes a table set no prover can build. Both
-/// verifiers call `validate` before the counts size anything (`verify_proof_parts`
-/// and `verify_epoch`), so rejecting it here is rejecting it on every path.
+/// sub-proof cross-check constrains only their *sum*. The six accelerators are
+/// not chunked — `generate_optional` emits one table or none — so any count
+/// above 1 describes a table set no prover can build, and the sum alone does not
+/// catch it: lower another count by the same amount and the total still matches.
+/// This pins the per-field shape.
+///
+/// It is a shape restriction, not a memory-safety guard. Both verifiers run the
+/// cross-check *before* any count sizes an AIR set (`verify_proof_parts`:
+/// `validate` → total-vs-`proofs.len()` → `VmAirs::new`; `verify_epoch` the
+/// same), and `total()` is checked, so an astronomical count cannot reach
+/// `VmAirs::new` by wrapping the sum either — that is
+/// [`counts_that_wrap_have_no_total`]'s property, not this one's.
 #[test]
 fn an_accelerator_count_above_one_is_rejected() {
     let (elf, logs, _instructions) = run_asm_elf("test_keccak");