Feat/skip empty tables

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
@@ -565,7 +575,9 @@ becomes an **explicit verifier action**:
   while any different set is rejected.
 - **Reconstruct the output** by concatenating the per-epoch commit slices (each
   commit-bus-bound, contiguous via the x254 chain).
-- The verifier also `validate()`s `table_counts` and never trusts a prover-supplied
+- The verifier also `validate()`s `table_counts` — which since per-epoch table skipping
+  means *only* that CPU and MEMW_R are present and that no accelerator claims more than
+  one table, not that every table is there — and never trusts a prover-supplied
   page config (continuation epochs have none — PAGE is skipped under the L2G
   bookend, so `page_configs` is always empty).
 

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/continuation.rs

@@ -84,21 +84,26 @@ type E = GoldilocksExtension;
 type AirRef<'a> = &'a dyn AIR<Field = F, FieldExtension = E, PublicInputs = ()>;
 
 /// Fresh transcript seeded with the epoch's statement (ELF, public output, table
-/// layout) and `epoch_label` (its position). The epoch's prove, verify, and
-/// bus-balance replay all seed via this so their challenges match; the seeding
-/// pins each epoch proof to its program and position (replay protection).
+/// layout), `epoch_label` (its position) and `is_final` (whether it carries
+/// HALT). The epoch's prove, verify, and bus-balance replay all seed via this so
+/// their challenges match; the seeding pins each epoch proof to its program,
+/// position and role (replay protection).
 fn epoch_transcript(
     elf_bytes: &[u8],
     public_output: &[u8],
     table_counts: &TableCounts,
     runtime_page_ranges: &[RuntimePageRange],
     epoch_label: u64,
+    is_final: bool,
     fri_final_poly_log_degree: u8,
 ) -> DefaultTranscript<E> {
     let mut transcript = DefaultTranscript::<E>::new(&[]);
     absorb_statement(
         &mut transcript,
-        StatementKind::ContinuationEpoch { epoch_label },
+        StatementKind::ContinuationEpoch {
+            epoch_label,
+            is_final,
+        },
         elf_bytes,
         public_output,
         table_counts,
@@ -490,6 +495,13 @@ impl ContinuationProof {
     pub fn num_epochs(&self) -> usize {
         self.epochs.len()
     }
+
+    /// What each epoch declared it carries, for tests that have to show the
+    /// epochs disagree. `epochs` itself stays private.
+    #[cfg(test)]
+    pub(crate) fn epoch_table_counts(&self) -> Vec<&TableCounts> {
+        self.epochs.iter().map(|e| &e.table_counts).collect()
+    }
 }
 
 /// Borrowed view over an [`EpochProof`] (owned or archived-in-place). Lets
@@ -727,6 +739,7 @@ fn prove_epoch(
             &table_counts,
             &runtime_page_ranges,
             label,
+            is_final,
             opts.fri_final_poly_log_degree,
         )
     };
@@ -803,7 +816,15 @@ fn verify_epoch(
         FIXED_TABLE_COUNT - 1
     };
     let proof = epoch.proof();
-    let expected_proof_count = table_counts.total() + fixed_tables + 1;
+    // Checked: the counts are prover-supplied and a wrapped sum would let one
+    // field stay huge and still match `proof.len()`.
+    let Some(expected_proof_count) = table_counts
+        .total()
+        .and_then(|t| t.checked_add(fixed_tables))
+        .and_then(|t| t.checked_add(1))
+    else {
+        return Ok(false);
+    };
     if expected_proof_count != proof.len() {
         return Ok(false);
     }
@@ -833,6 +854,7 @@ fn verify_epoch(
             &table_counts,
             &runtime_page_ranges,
             label,
+            is_final,
             opts.fri_final_poly_log_degree,
         )
     };
@@ -1991,6 +2013,146 @@ mod tests {
         );
     }
 
+    /// Each epoch drops the chips it never reaches, and it decides that on its
+    /// own: a table missing from one epoch still shows up in another that does
+    /// use it. The skip is not a property of the run, it is a property of the
+    /// epoch — computing it over the whole run instead would drag every table
+    /// used anywhere into every epoch.
+    #[test]
+    fn table_presence_is_decided_per_epoch() {
+        let _ = env_logger::builder().is_test(true).try_init();
+        let elf_bytes = asm_elf_bytes("all_loadstore_32");
+        let epoch_size_log2 = 3;
+        let opts = ProofOptions::default_test_options();
+
+        let bundle = prove_continuation(&elf_bytes, &[], epoch_size_log2, &opts).unwrap();
+        // Guard against silent degradation: one epoch cannot disagree with another.
+        assert!(
+            bundle.epochs.len() >= 2,
+            "need at least two epochs, got {}",
+            bundle.epochs.len()
+        );
+
+        // `(name, count)` per epoch, in a fixed order so the rows line up.
+        let per_epoch: Vec<Vec<(&str, usize)>> = bundle
+            .epochs
+            .iter()
+            .map(|e| {
+                let c = &e.table_counts;
+                vec![
+                    ("lt", c.lt),
+                    ("memw", c.memw),
+                    ("memw_aligned", c.memw_aligned),
+                    ("load", c.load),
+                    ("mul", c.mul),
+                    ("dvrm", c.dvrm),
+                    ("shift", c.shift),
+                    ("branch", c.branch),
+                    ("eq", c.eq),
+                    ("bytewise", c.bytewise),
+                    ("store", c.store),
+                    ("cpu32", c.cpu32),
+                    ("keccak", c.keccak),
+                    ("keccak_rnd", c.keccak_rnd),
+                    ("ecsm", c.ecsm),
+                    ("ecdas", c.ecdas),
+                    ("hint", c.hint),
+                    ("commit", c.commit),
+                ]
+            })
+            .collect();
+        let layout = || {
+            per_epoch
+                .iter()
+                .enumerate()
+                .map(|(i, row)| {
+                    let present: Vec<&str> = row
+                        .iter()
+                        .filter(|(_, n)| *n > 0)
+                        .map(|(t, _)| *t)
+                        .collect();
+                    format!("epoch {i}: {present:?}")
+                })
+                .collect::<Vec<_>>()
+                .join("\n  ")
+        };
+
+        // Something is actually being skipped, or the rest proves nothing.
+        assert!(
+            per_epoch.iter().any(|row| row.iter().any(|(_, n)| *n == 0)),
+            "no epoch skipped any table:\n  {}",
+            layout()
+        );
+
+        // And the epochs disagree: some table is in one and out of another.
+        //
+        // Among the *non-final* epochs only. The final epoch is the one that
+        // carries HALT and the one where a program's output is committed, so a
+        // difference that involves it can be structural — a whole-run table set
+        // would still produce it, and this assertion would pass while measuring
+        // nothing about per-epoch granularity.
+        assert!(
+            per_epoch.len() >= 3,
+            "need at least two non-final epochs to compare, got {} epochs",
+            per_epoch.len()
+        );
+        let non_final = &per_epoch[..per_epoch.len() - 1];
+        let disagreeing: Vec<&str> = non_final[0]
+            .iter()
+            .enumerate()
+            .filter(|(i, (_, first))| {
+                non_final
+                    .iter()
+                    .any(|row| (row[*i].1 == 0) != (*first == 0))
+            })
+            .map(|(_, (name, _))| *name)
+            .collect();
+        assert!(
+            !disagreeing.is_empty(),
+            "the non-final epochs all carry the same tables, so per-epoch \
+             granularity is untested here — pick a program or epoch size that \
+             varies:\n  {}",
+            layout()
+        );
+
+        // Sharper: a table that is present, goes away, and comes back cannot be
+        // produced by any scheme that computes one set over the run or over a
+        // prefix of it. Counting the blocks of consecutive epochs a table
+        // appears in, more than one block is exactly that shape.
+        let blocks = |i: usize| {
+            let present: Vec<bool> = per_epoch.iter().map(|row| row[i].1 > 0).collect();
+            present
+                .iter()
+                .enumerate()
+                .filter(|(k, p)| **p && (*k == 0 || !present[k - 1]))
+                .count()
+        };
+        let reappearing: Vec<&str> = per_epoch[0]
+            .iter()
+            .enumerate()
+            .filter(|(i, _)| blocks(*i) > 1)
+            .map(|(_, (name, _))| *name)
+            .collect();
+        assert!(
+            !reappearing.is_empty(),
+            "no table leaves and comes back, so a union or prefix scheme would \
+             produce this same layout — the test cannot tell them apart:\n  {}",
+            layout()
+        );
+
+        println!("tables present in some non-final epochs but not others: {disagreeing:?}");
+        println!("tables that leave and come back: {reappearing:?}");
+        println!("  {}", layout());
+
+        // The mixed-shape bundle has to verify end to end.
+        assert!(
+            verify_continuation(&elf_bytes, &bundle, &opts)
+                .unwrap()
+                .is_some(),
+            "a bundle whose epochs carry different table sets must still verify"
+        );
+    }
+
     // Supplied genesis roots must verify identically to the trustless recompute,
     // and a tampered root (DECODE or a page) must be rejected. `data_page_touch`
     // touches a real ELF `.data` page, unlike this file's stack-only fixtures.
@@ -2289,6 +2451,89 @@ mod tests {
         );
     }
 
+    /// The epoch counterpart of the overflow branch: `verify_epoch` swallows a
+    /// total that wraps as `Ok(false)` where the monolithic verifier returns
+    /// `Err`, so a regression there is silent. Nothing reached that arm before.
+    #[test]
+    fn test_split_verify_rejects_an_epoch_whose_counts_overflow() {
+        let _ = env_logger::builder().is_test(true).try_init();
+        let elf_bytes = asm_elf_bytes("all_loadstore_32");
+        let opts = ProofOptions::default_test_options();
+        let mut bundle = prove_continuation(&elf_bytes, &[], 3, &opts).unwrap();
+        assert!(!bundle.epochs.is_empty());
+
+        bundle.epochs[0].table_counts.lt = usize::MAX;
+        assert!(
+            bundle.epochs[0].table_counts.total().is_none(),
+            "the tampered counts must actually wrap, or this tests the wrong branch"
+        );
+        assert!(
+            verify_continuation(&elf_bytes, &bundle, &opts)
+                .unwrap()
+                .is_none(),
+            "an epoch whose declared counts have no total must be rejected"
+        );
+    }
+
+    /// The continuation counterpart of the monolithic
+    /// `test_verify_rejects_undercounted_table_count`: an epoch that declares
+    /// away a table it actually carries. Both branches of the cross-check are
+    /// exercised, because the fixed-table term differs between a non-final
+    /// epoch (`FIXED_TABLE_COUNT - 1`, no HALT) and the final one — and
+    /// `verify_epoch` swallows the mismatch as `Ok(false)` rather than an
+    /// error, so a regression in that arithmetic would be silent.
+    #[test]
+    fn test_split_verify_rejects_undercounted_epoch_table_count() {
+        let _ = env_logger::builder().is_test(true).try_init();
+        let elf_bytes = asm_elf_bytes("all_loadstore_32");
+        let opts = ProofOptions::default_test_options();
+        let mut bundle = prove_continuation(&elf_bytes, &[], 3, &opts).unwrap();
+        assert!(
+            bundle.epochs.len() >= 2,
+            "need a non-final and a final epoch, got {}",
+            bundle.epochs.len()
+        );
+        let last = bundle.epochs.len() - 1;
+        for epoch in [0, last] {
+            // Whatever this epoch does carry: the point is declaring one of its
+            // own tables away, not which one.
+            let counts = &mut bundle.epochs[epoch].table_counts;
+            let (name, restore) = if counts.load > 0 {
+                ("load", std::mem::replace(&mut counts.load, 0))
+            } else if counts.store > 0 {
+                ("store", std::mem::replace(&mut counts.store, 0))
+            } else {
+                ("lt", std::mem::replace(&mut counts.lt, 0))
+            };
+            assert!(
+                restore > 0,
+                "epoch {epoch} carries no optional table to declare away"
+            );
+            assert!(
+                verify_continuation(&elf_bytes, &bundle, &opts)
+                    .unwrap()
+                    .is_none(),
+                "epoch {epoch} declaring away its {name} table must be rejected"
+            );
+            let counts = &mut bundle.epochs[epoch].table_counts;
+            match name {
+                "load" => counts.load = restore,
+                "store" => counts.store = restore,
+                _ => counts.lt = restore,
+            }
+        }
+
+        // The control, and the reason the rejections above mean something: put
+        // the counts back and the same bundle verifies. One verify, at the end,
+        // rather than one before and one after — each costs a full pass.
+        assert!(
+            verify_continuation(&elf_bytes, &bundle, &opts)
+                .unwrap()
+                .is_some(),
+            "restoring the counts must bring the bundle back"
+        );
+    }
+
     // The raw private input must not be bundled under continuations. The bundle carries no
     // raw private bytes (only `num_private_input_pages`), yet a multi-epoch continuation of
     // a program that reads private input verifies from the bundle + ELF ALONE and