Feat/skip empty tables

prover/src/continuation.rs

@@ -490,6 +490,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
@@ -803,7 +810,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);
     }
@@ -1991,6 +2006,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 +2444,65 @@ mod tests {
         );
     }
 
+    /// 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