From fe3a0b8230225a16144a152a1096753077b2ba40 Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 2 Jul 2026 12:32:38 -0300 Subject: [PATCH 1/4] Stream per-epoch proof verification --- docs/continuations_design.md | 21 +- prover/src/continuation.rs | 410 +++++++++++++++++++++++++++-------- 2 files changed, 340 insertions(+), 91 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 9c3f54747..4e722dca1 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -458,9 +458,19 @@ binding holds there too — not just on the integrated path. The continuation can be proved and verified by separate parties. `prove_continuation` emits a self-contained `ContinuationProof` bundle; `verify_continuation(elf, &bundle)` checks it using **only the bundle and the ELF** — nothing from the prover's memory. -The integrated `prove_and_verify_continuation` is now a thin wrapper -(`prove_continuation` then `verify_continuation`), and `prove_verify_epoch` is -likewise split into `prove_epoch` + `verify_epoch`. +The integrated `prove_and_verify_continuation` proves and verifies in one +**streaming** pass: it proves each epoch, verifies it inline with `verify_epoch`, +and drops that epoch's `MultiProof` — retaining only the small +`boundary`/`l2g_root`/`public_output` — before building and verifying the one +global proof. This bounds its retained-proof memory to a single epoch at a time +instead of holding all *N*. It is a faithful in-process mirror of +`verify_continuation` (it derives `is_final`/`label` **positionally** — a one-epoch +lookahead for `is_final` — and chains `register_init` from each verified epoch's +`reg_fini`, never trusting the prover), but it is **not** a substitute for verifying +an untrusted serialized bundle — `verify_continuation` remains that. The epoch loop +it shares with `prove_continuation` lives in an internal `EpochDriver`, so the +bundle producer and the streaming path cannot diverge in how epochs are produced. +`prove_verify_epoch` is likewise split into `prove_epoch` + `verify_epoch`. The bundle is prover-supplied and therefore **untrusted**. Per epoch it carries the `MultiProof`, the `public_output` slice, `table_counts`, @@ -554,8 +564,9 @@ recursion/aggregation layer (deferred). `prove_epoch` / `verify_epoch` with the shared `build_epoch_airs` helper; the global proof (`prove_global` / `verify_global`); the per-epoch AIRs (`l2g_memory_air` / `l2g_global_air`); the power-of-two epoch sizing from - `epoch_size_log2`; the register-FINI preprocessing; the transcript seeding; and - `prove_and_verify_continuation` (the thin integrated wrapper). + `epoch_size_log2`; the register-FINI preprocessing; the transcript seeding; the + shared `EpochDriver` epoch loop; and `prove_and_verify_continuation` (the + streaming integrated prove→verify→drop path). - `prover/src/lib.rs` — `verify_l2g_commitment_binding` (epoch L2G root ↔ global sub-table root) and the commit-bus offset/balance helpers (`compute_commit_bus_offset`, `compute_expected_commit_bus_balance`) that take the diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index ccdd5a6f9..af3f12a5c 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -50,6 +50,7 @@ use stark::trace::TraceTable; use stark::traits::AIR; use stark::verifier::{IsStarkVerifier, Verifier}; +use crate::paged_mem::PagedMem; use crate::statement::{StatementKind, absorb_continuation_global_statement, absorb_statement}; use crate::tables::local_to_global::{self, CellBoundary}; use crate::tables::page::{self, PageConfig}; @@ -619,75 +620,101 @@ fn verify_global( ) } -/// Prove a full continuation and return a self-contained [`ContinuationProof`] -/// (prove half only — no verification). Splits the execution into `2^epoch_size_log2` -/// cycle epochs, proves each, and proves the one cross-epoch global-memory linkage. +/// Streaming driver over the epochs of one execution: owns the executor and the +/// carried cross-epoch state (`image`, `provenance`, `prev_fini`) and proves one epoch +/// per [`next`](EpochDriver::next) call. It is the single source of truth for the epoch +/// loop, so the bundle path ([`prove_continuation`], which keeps every proof) and the +/// streaming self-verify path ([`prove_and_verify_continuation`], which verifies and +/// drops each proof) cannot diverge in how epochs are produced. /// -/// Intermediate epochs run exactly `2^epoch_size_log2` cycles, so their CPU tables -/// have power-of-two row counts and therefore zero padding rows — important because -/// CPU padding rows participate in the inline-PC `memory` chain (carrying pc=1) -/// which is only anchored by the HALT chip's emit_pc/consume_pc, and intermediate -/// epochs exclude HALT. With padding rows present and no HALT their pc=1 tokens -/// dangle and the Memory bus fails to balance; zero padding rows sidestep that. The -/// final epoch keeps its remainder and its HALT, so its padding chain is anchored as -/// usual. A program that fits in one epoch runs as a single final (monolithic-style) -/// epoch. -pub fn prove_continuation( - elf_bytes: &[u8], - private_inputs: &[u8], - epoch_size_log2: u32, - opts: &ProofOptions, -) -> Result { - if epoch_size_log2 < 2 { - return Err(Error::InvalidContinuationEpochSize( - "epoch_size_log2 must be at least 2 (4 cycles)".to_string(), - )); - } - let epoch_size = 1usize.checked_shl(epoch_size_log2).ok_or_else(|| { - Error::InvalidContinuationEpochSize(format!( - "epoch_size_log2 {epoch_size_log2} is too large for this platform" - )) - })?; - - let elf = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; - let mut executor = Executor::new(&elf, private_inputs.to_vec()) - .map_err(|e| Error::Execution(format!("{e}")))?; - - // The cross-epoch memory image, carried forward: epoch i+1's init is epoch i's - // fini, updated in place with each epoch's touched-cell final values. - let mut image = build_initial_image_paged(&elf, private_inputs); - let init_page_data = build_init_page_data(&image); - let mut provenance = - local_to_global::genesis_provenance(image.iter().map(|(a, v)| (a, v as u64))); +/// `init_page_data` is snapshotted from the INITIAL image in [`new`](EpochDriver::new) +/// and never recomputed from the carried (mutated) image, so the global proof's genesis +/// matches the ELF the verifier rebuilds. +struct EpochDriver<'a> { + elf: Elf, + elf_bytes: &'a [u8], + private_inputs: &'a [u8], + opts: &'a ProofOptions, + epoch_size: usize, + executor: Executor, + /// Cross-epoch memory image, carried forward: epoch i+1's init is epoch i's fini. + image: PagedMem, + provenance: PagedMem<(u64, u64, u64)>, + /// Genesis page data snapshotted from the initial image (fed to `prove_global`). + init_page_data: HashMap>, + /// The previous epoch's bound final register file `R_{i+1}` (next epoch's init). + prev_fini: Option>, + index: u64, +} - let mut epochs: Vec = Vec::new(); - // The previous epoch's bound final register file R_{i+1}; epoch i+1's init is - // derived from it (the cross-epoch register binding). - let mut prev_fini: Option> = None; +impl<'a> EpochDriver<'a> { + fn new( + elf_bytes: &'a [u8], + private_inputs: &'a [u8], + epoch_size_log2: u32, + opts: &'a ProofOptions, + ) -> Result { + if epoch_size_log2 < 2 { + return Err(Error::InvalidContinuationEpochSize( + "epoch_size_log2 must be at least 2 (4 cycles)".to_string(), + )); + } + let epoch_size = 1usize.checked_shl(epoch_size_log2).ok_or_else(|| { + Error::InvalidContinuationEpochSize(format!( + "epoch_size_log2 {epoch_size_log2} is too large for this platform" + )) + })?; + + let elf = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; + let executor = Executor::new(&elf, private_inputs.to_vec()) + .map_err(|e| Error::Execution(format!("{e}")))?; + + let image = build_initial_image_paged(&elf, private_inputs); + let init_page_data = build_init_page_data(&image); + let provenance = + local_to_global::genesis_provenance(image.iter().map(|(a, v)| (a, v as u64))); + + Ok(Self { + elf, + elf_bytes, + private_inputs, + opts, + epoch_size, + executor, + image, + provenance, + init_page_data, + prev_fini: None, + index: 0, + }) + } - let mut index: u64 = 0; - loop { - if executor.pc() == 0 { - break; + /// Prove the next epoch, or `Ok(None)` once the execution has halted. Advances the + /// carried image/provenance/register state. This epoch's `is_final` is decided here + /// by whether the program halted inside it (`executor.pc() == 0`) and baked into its + /// AIRs (HALT is present only on the final epoch); the verifier re-derives `is_final` + /// independently rather than trusting this. + fn next(&mut self) -> Result, Error> { + if self.executor.pc() == 0 { + return Ok(None); } - // The cross-epoch ordering check (IsB20 on `fini_epoch - 1 - init_epoch`) - // only spans `local_to_global::MAX_EPOCHS` epochs. Beyond that the IsB20 bus - // cannot balance, so an honest proof is impossible — fail fast with a clear - // error instead of building an unprovable trace. The verifier already - // rejects any such proof; this is a prover-side guard for a clean message. - if index >= local_to_global::MAX_EPOCHS { + // The cross-epoch ordering check (IsB20 on `fini_epoch - 1 - init_epoch`) only + // spans `local_to_global::MAX_EPOCHS` epochs. Beyond that an honest proof is + // impossible — fail fast instead of building an unprovable trace. + if self.index >= local_to_global::MAX_EPOCHS { return Err(Error::InvalidContinuationEpochSize(format!( "execution needs more than {} continuation epochs (the IsB20 cross-epoch \ ordering range); use a larger epoch size", local_to_global::MAX_EPOCHS ))); } - let register_init: Vec = if index == 0 { - register::register_init_from_entry_point(elf.entry_point) + + let register_init: Vec = if self.index == 0 { + register::register_init_from_entry_point(self.elf.entry_point) } else { - // Epoch i+1's init is epoch i's bound fini, reused directly (same - // `register_word_address_list` order) — the cross-epoch register binding. - prev_fini.clone().ok_or_else(|| { + // Epoch i+1's init is epoch i's bound fini, reused directly — the + // cross-epoch register binding. + self.prev_fini.clone().ok_or_else(|| { Error::ContinuationInvariant( "previous epoch final registers are missing after the first epoch".to_string(), ) @@ -695,63 +722,100 @@ pub fn prove_continuation( }; // Run one epoch; `logs` is this epoch's chunk only (the executor clears it). - let logs = match executor - .resume_with_limit(epoch_size) + let logs = match self + .executor + .resume_with_limit(self.epoch_size) .map_err(|e| Error::Execution(format!("{e}")))? { Some(logs) => logs.to_vec(), - None => break, + None => return Ok(None), }; - let is_final = executor.pc() == 0; + let is_final = self.executor.pc() == 0; - // Invariant: a non-final epoch ran the full `epoch_size` (a power of two), - // so its CPU table has no padding rows. - if !is_final && logs.len() != epoch_size { + // Invariant: a non-final epoch ran the full `epoch_size` (a power of two), so + // its CPU table has no padding rows. + if !is_final && logs.len() != self.epoch_size { return Err(Error::ContinuationInvariant(format!( - "intermediate epoch ran {} cycles, expected {epoch_size}", - logs.len() + "intermediate epoch ran {} cycles, expected {}", + logs.len(), + self.epoch_size ))); } - let label = local_to_global::epoch_label(index); + let label = local_to_global::epoch_label(self.index); let traces = Traces::from_image_and_logs( - &elf, - &image, + &self.elf, + &self.image, ®ister_init, &logs, &MaxRowsConfig::default(), - private_inputs, + self.private_inputs, is_final, true, #[cfg(feature = "disk-spill")] stark::storage_mode::StorageMode::Ram, )?; - let boundary = - local_to_global::epoch_boundary(&mut provenance, label, &traces.touched_memory_cells); + let boundary = local_to_global::epoch_boundary( + &mut self.provenance, + label, + &traces.touched_memory_cells, + ); let start = EpochStart { register_init: ®ister_init, label, }; - let epoch = prove_epoch(&elf, elf_bytes, &start, traces, is_final, &boundary, opts)?; - prev_fini = Some(epoch.reg_fini.clone()); + let epoch = prove_epoch( + &self.elf, + self.elf_bytes, + &start, + traces, + is_final, + &boundary, + self.opts, + )?; + self.prev_fini = Some(epoch.reg_fini.clone()); // Carry the image forward: this epoch's fini is the next epoch's init. for cell in &boundary { - image.set(cell.address, (cell.fini.value & 0xFF) as u8); + self.image.set(cell.address, (cell.fini.value & 0xFF) as u8); } - epochs.push(epoch); + self.index += 1; - if is_final { - break; - } - index += 1; + Ok(Some(epoch)) + } +} + +/// Prove a full continuation and return a self-contained [`ContinuationProof`] +/// (prove half only — no verification). Splits the execution into `2^epoch_size_log2` +/// cycle epochs, proves each, and proves the one cross-epoch global-memory linkage. +/// +/// Intermediate epochs run exactly `2^epoch_size_log2` cycles, so their CPU tables +/// have power-of-two row counts and therefore zero padding rows — important because +/// CPU padding rows participate in the inline-PC `memory` chain (carrying pc=1) +/// which is only anchored by the HALT chip's emit_pc/consume_pc, and intermediate +/// epochs exclude HALT. With padding rows present and no HALT their pc=1 tokens +/// dangle and the Memory bus fails to balance; zero padding rows sidestep that. The +/// final epoch keeps its remainder and its HALT, so its padding chain is anchored as +/// usual. A program that fits in one epoch runs as a single final (monolithic-style) +/// epoch. +pub fn prove_continuation( + elf_bytes: &[u8], + private_inputs: &[u8], + epoch_size_log2: u32, + opts: &ProofOptions, +) -> Result { + let mut driver = EpochDriver::new(elf_bytes, private_inputs, epoch_size_log2, opts)?; + + let mut epochs: Vec = Vec::new(); + while let Some(epoch) = driver.next()? { + epochs.push(epoch); } // One global LogUp over all the (kept) local-to-global tables. let all_boundaries: Vec> = epochs.iter().map(|e| e.boundary.clone()).collect(); - let global = prove_global(&all_boundaries, elf_bytes, &init_page_data, opts)?; + let global = prove_global(&all_boundaries, elf_bytes, &driver.init_page_data, opts)?; Ok(ContinuationProof { epochs, @@ -859,16 +923,101 @@ pub fn verify_continuation( Ok(Some(public_output)) } -/// Convenience wrapper: prove then verify in one call (the original integrated API). -/// Returns `Ok(Some(public_output))` iff the continuation proves and verifies. +/// Prove and verify a full continuation in one streaming pass: each epoch is proved, +/// verified inline, and its proof dropped — only `boundary`, `l2g_root`, and +/// `public_output` are retained — then the one cross-epoch global proof is built and +/// verified. This bounds the retained-proof memory to O(1) epochs instead of collecting +/// every epoch proof up front (as [`prove_continuation`] + [`verify_continuation`] do). +/// +/// The verification is a faithful mirror of [`verify_continuation`]: `register_init` is +/// chained from each verified epoch's `reg_fini`, and `label`/`is_final` are derived +/// positionally here (one-epoch lookahead for `is_final`), never taken from the prover. +/// It is NOT a substitute for verifying an untrusted serialized `ContinuationProof` — +/// [`verify_continuation`] remains that. Returns `Ok(Some(public_output))` iff the +/// continuation proves and verifies. pub fn prove_and_verify_continuation( elf_bytes: &[u8], private_inputs: &[u8], epoch_size_log2: u32, opts: &ProofOptions, ) -> Result>, Error> { - let bundle = prove_continuation(elf_bytes, private_inputs, epoch_size_log2, opts)?; - verify_continuation(elf_bytes, &bundle, opts) + let mut driver = EpochDriver::new(elf_bytes, private_inputs, epoch_size_log2, opts)?; + + // Verify-side state, rebuilt independently of the prover: `register_init` chains + // from each verified epoch's bound `reg_fini` (epoch 0 from the ELF entry point). + let mut register_init = register::register_init_from_entry_point(driver.elf.entry_point); + let mut all_boundaries: Vec> = Vec::new(); + let mut epoch_roots: Vec = Vec::new(); + let mut public_output: Vec = Vec::new(); + let mut index: u64 = 0; + + // One-epoch lookahead: `is_final` is derived from whether another epoch actually + // follows (positional), not from a flag the prover stored, so a driver enumeration + // bug cannot be silently self-consistent between the prove and verify halves. + let mut pending = driver.next()?; + while let Some(epoch) = pending { + let next = driver.next()?; + let is_final = next.is_none(); + let label = local_to_global::epoch_label(index); + + // Ordering is load-bearing: verify_epoch must pass BEFORE `l2g_root` is trusted + // and the proof dropped. The global L2G air is constraint-free, so the epoch + // proof (checked here) is the sole enforcer of the L2G column constraints, and + // `l2g_root` is only bound to a verified trace once verify_epoch returns true. + if !verify_epoch( + &driver.elf, + elf_bytes, + &epoch, + ®ister_init, + is_final, + label, + opts, + ) { + return Ok(None); + } + + // Keep only what the global step + final checks need; the MultiProof drops here. + // `epoch` is owned, so `reg_fini` moves out (no clone) into the next epoch's + // derived init — the cross-epoch register chain, checked independently here. + let EpochProof { + boundary, + l2g_root, + public_output: out, + reg_fini, + .. + } = epoch; + register_init = reg_fini; + public_output.extend_from_slice(&out); + epoch_roots.push(l2g_root); + all_boundaries.push(boundary); + index += 1; + + pending = next; + } + + // Mirror verify_continuation's n == 0 early-return (reachable via an `e_entry == 0` + // ELF, which yields zero epochs): without it the empty global prove/verify would + // trivially pass and accept a run the standalone verifier rejects. + if all_boundaries.is_empty() { + return Ok(None); + } + + let global = prove_global(&all_boundaries, elf_bytes, &driver.init_page_data, opts)?; + if !verify_global( + &all_boundaries, + &global, + &driver.elf, + elf_bytes, + private_inputs, + opts, + ) { + return Ok(None); + } + if !verify_l2g_commitment_binding(&epoch_roots, &global) { + return Ok(None); + } + + Ok(Some(public_output)) } #[cfg(test)] @@ -958,6 +1107,95 @@ mod tests { ); } + // Anti-drift guard: the streaming self-verify path (`prove_and_verify_continuation`) + // must accept/reject and aggregate output IDENTICALLY to the authoritative two-phase + // path (`prove_continuation` + the untouched `verify_continuation`). The streaming + // path derives `is_final`/`label` positionally and chains `register_init` itself, so + // it must agree with the standalone verifier on both the single-epoch + // (immediately-final) and multi-epoch (enumeration-boundary) shapes. + #[test] + fn test_streaming_matches_two_phase() { + let _ = env_logger::builder().is_test(true).try_init(); + + // `expected` pins an independent known-good output where we know it, so the + // test is not purely differential over one shared prover (a shared-prover or + // aggregation bug affecting both halves identically would otherwise pass). + let commit_output: &[u8] = &[0xAA, 0xBB, 0xCC, 0xDD]; + for (name, log2, want_multi, expected) in [ + ("test_commit_split", 6u32, false, Some(commit_output)), // one final epoch + ("test_commit_split", 4, true, Some(commit_output)), // splits across epochs + ("all_loadstore_32", 3, true, None), // several intermediate epochs + ] { + let elf_bytes = asm_elf_bytes(name); + + let bundle = + prove_continuation(&elf_bytes, &[], log2, &ProofOptions::default_test_options()) + .unwrap(); + if want_multi { + assert!( + bundle.num_epochs() > 1, + "{name} @ log2={log2} must split into multiple epochs" + ); + } else { + assert_eq!( + bundle.num_epochs(), + 1, + "{name} @ log2={log2} must be a single final epoch" + ); + } + let two_phase = + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap(); + assert!(two_phase.is_some(), "{name} @ log2={log2} must verify"); + + let streaming = prove_and_verify_continuation( + &elf_bytes, + &[], + log2, + &ProofOptions::default_test_options(), + ) + .unwrap(); + + assert_eq!( + streaming, two_phase, + "{name} @ log2={log2}: streaming self-verify diverged from prove+verify_continuation" + ); + if let Some(expected) = expected { + assert_eq!( + streaming.as_deref(), + Some(expected), + "{name} @ log2={log2}: streaming output must match the known-good value" + ); + } + } + } + + // An ELF whose entry point is 0 yields zero epochs (the executor starts halted). + // The streaming path must mirror `verify_continuation`'s `n == 0` early-return and + // reject it with `Ok(None)` rather than trivially "verifying" an empty run. + #[test] + fn test_streaming_zero_epoch_returns_none() { + let _ = env_logger::builder().is_test(true).try_init(); + let mut elf_bytes = asm_elf_bytes("all_loadstore_32"); + // ELF64 `e_entry` is an 8-byte little-endian field at offset 24; zero it so the + // executor starts with pc == 0 and the driver produces no epochs. + for b in &mut elf_bytes[24..32] { + *b = 0; + } + assert_eq!(Elf::load(&elf_bytes).unwrap().entry_point, 0); + assert!( + prove_and_verify_continuation( + &elf_bytes, + &[], + 4, + &ProofOptions::default_test_options() + ) + .unwrap() + .is_none(), + "a zero-entry ELF (zero epochs) must be rejected, not accepted as empty" + ); + } + // Regression for touched-cell prediction from carried registers. A syscall // whose operand pointers live in registers (ECSM reads a0/a1/a2) can have those // registers set in an EARLIER epoch than the call. `test_ecsm_split` sets From 135474c92c892bd1be51fde062eb0ecabcff08e0 Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 2 Jul 2026 14:25:45 -0300 Subject: [PATCH 2/4] Add a private-input-size parity guard and a regression tests --- prover/src/continuation.rs | 72 +++++++++++++++++++++++++++++++++++++- 1 file changed, 71 insertions(+), 1 deletion(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index af3f12a5c..fbcff5c36 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -32,7 +32,9 @@ //! //! The prover and verifier are split: `prove_continuation` emits a self-contained //! `ContinuationProof` bundle and `verify_continuation` checks it from the bundle -//! and ELF alone (`prove_and_verify_continuation` is a thin wrapper over both). +//! and ELF alone; `prove_and_verify_continuation` proves and verifies in one +//! streaming pass, verifying and dropping each epoch proof so its retained-proof +//! memory stays bounded to a single epoch. use std::collections::HashMap; @@ -728,6 +730,12 @@ impl<'a> EpochDriver<'a> { .map_err(|e| Error::Execution(format!("{e}")))? { Some(logs) => logs.to_vec(), + // `resume_with_limit` returns `None` only when `pc == 0` at entry, which the + // guard above already handles — so this arm is effectively unreachable today. + // Kept as a graceful terminator (not `unreachable!`) so that if a future + // change makes the executor stop for another reason, the driver ends cleanly + // rather than panicking; a resulting `is_final` disagreement would be caught + // by `verify_epoch` on the streaming path, never silently accepted. None => return Ok(None), }; let is_final = self.executor.pc() == 0; @@ -941,6 +949,16 @@ pub fn prove_and_verify_continuation( epoch_size_log2: u32, opts: &ProofOptions, ) -> Result>, Error> { + // Match `verify_continuation`'s up-front bound so the two paths surface the same + // error on an oversized input (the executor also rejects it, but with a different + // variant). + if private_inputs.len() as u64 > MAX_PRIVATE_INPUT_SIZE { + return Err(Error::InvalidTableCounts(format!( + "private input size ({}) exceeds max ({MAX_PRIVATE_INPUT_SIZE})", + private_inputs.len() + ))); + } + let mut driver = EpochDriver::new(elf_bytes, private_inputs, epoch_size_log2, opts)?; // Verify-side state, rebuilt independently of the prover: `register_init` chains @@ -1196,6 +1214,58 @@ mod tests { ); } + // Exactly-2-epoch discriminator for the `is_final` lookahead: the minimal case that + // exercises the false→true transition exactly once. `epoch_size_log2` is derived from + // the measured cycle count as the largest power of two strictly below `total`, so + // `2^L < total <= 2^(L+1)` ⟹ exactly 2 epochs — pinning `num_epochs() == 2` (not just + // `> 1`) and confirming the streaming path still equals the two-phase path. Guards + // against a lookahead/label off-by-one at the tightest enumeration boundary. + #[test] + fn test_streaming_exactly_two_epochs() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let total = Executor::new(&Elf::load(&elf_bytes).unwrap(), vec![]) + .unwrap() + .run() + .unwrap() + .logs + .len(); + let epoch_size_log2 = (total as u64 - 1).ilog2(); + assert!( + epoch_size_log2 >= 2, + "program ({total} cycles) too short to derive a valid 2-epoch split" + ); + + let bundle = prove_continuation( + &elf_bytes, + &[], + epoch_size_log2, + &ProofOptions::default_test_options(), + ) + .unwrap(); + assert_eq!( + bundle.num_epochs(), + 2, + "epoch_size_log2={epoch_size_log2} over {total} cycles must yield exactly 2 epochs" + ); + let two_phase = + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap(); + assert!(two_phase.is_some()); + + let streaming = prove_and_verify_continuation( + &elf_bytes, + &[], + epoch_size_log2, + &ProofOptions::default_test_options(), + ) + .unwrap(); + assert_eq!( + streaming, two_phase, + "streaming self-verify diverged from prove+verify_continuation at exactly 2 epochs" + ); + } + // Regression for touched-cell prediction from carried registers. A syscall // whose operand pointers live in registers (ECSM reads a0/a1/a2) can have those // registers set in an EARLIER epoch than the call. `test_ecsm_split` sets From 73fe0f882aae2284302a268f2165eb70b1e195ba Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 3 Jul 2026 11:30:11 -0300 Subject: [PATCH 3/4] fix docs and test --- docs/continuations_design.md | 4 ++-- prover/src/continuation.rs | 9 ++++++++- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 4e722dca1..d428970d8 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -462,8 +462,8 @@ The integrated `prove_and_verify_continuation` proves and verifies in one **streaming** pass: it proves each epoch, verifies it inline with `verify_epoch`, and drops that epoch's `MultiProof` — retaining only the small `boundary`/`l2g_root`/`public_output` — before building and verifying the one -global proof. This bounds its retained-proof memory to a single epoch at a time -instead of holding all *N*. It is a faithful in-process mirror of +global proof. This bounds its retained-proof memory to O(1) epochs (at most two are +live across the one-epoch `is_final` lookahead) instead of holding all *N*. It is a faithful in-process mirror of `verify_continuation` (it derives `is_final`/`label` **positionally** — a one-epoch lookahead for `is_final` — and chains `register_init` from each verified epoch's `reg_fini`, never trusting the prover), but it is **not** a substitute for verifying diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index fbcff5c36..7b532690e 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -34,7 +34,8 @@ //! `ContinuationProof` bundle and `verify_continuation` checks it from the bundle //! and ELF alone; `prove_and_verify_continuation` proves and verifies in one //! streaming pass, verifying and dropping each epoch proof so its retained-proof -//! memory stays bounded to a single epoch. +//! memory stays bounded to O(1) epochs (at most two are live across the one-epoch +//! `is_final` lookahead) instead of collecting all of them. use std::collections::HashMap; @@ -1230,6 +1231,12 @@ mod tests { .unwrap() .logs .len(); + // Guard before the arithmetic: `total - 1` underflows and `ilog2(0)` panics + // for total <= 1, so check the precondition first rather than after. + assert!( + total >= 2, + "program ({total} cycles) too short to derive a valid 2-epoch split" + ); let epoch_size_log2 = (total as u64 - 1).ilog2(); assert!( epoch_size_log2 >= 2, From c20cbdff504bf28076bd7b06a7c22bd8f6d6c32f Mon Sep 17 00:00:00 2001 From: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com> Date: Fri, 3 Jul 2026 18:24:57 -0300 Subject: [PATCH 4/4] fix(continuations): review follow-ups for the streaming verify path (#778) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Clarify the private-input guard comment: the parity it buys is with verify_continuation (the standalone verifier); the two-phase composition prove_continuation + verify_continuation instead fails inside Executor::new with Error::Execution before that bound is reached. Add the missing regression test pinning the guard's InvalidTableCounts variant. - Fail loudly (ContinuationInvariant) if resume_with_limit ever returns None mid-run instead of ending the driver cleanly: a clean end would let prove_continuation emit a bundle whose last epoch lacks HALT — never verifiable, with no diagnostic at the cause. Unreachable today (None only occurs with pc == 0 at entry, already guarded), so no behavior change. - Add reciprocal sync notes between verify_continuation's epoch loop and its inline mirror in prove_and_verify_continuation: the differential test only exercises honest proofs, so it cannot catch a rejection check dropped from one of the two copies. - Document the deliberate reg_fini length-guard asymmetry (in-process fini is trusted; a wrong length is an invariant bug that should fail loudly, not be reported as a rejected proof). - Qualify the lookahead comment (positional is_final buys mirror fidelity, not independence from the in-process executor) and the design doc's 'small boundary' claim (boundaries grow with total touched memory; the O(1) bound is on retained proof data). --- docs/continuations_design.md | 9 +++-- prover/src/continuation.rs | 69 ++++++++++++++++++++++++++++++------ 2 files changed, 64 insertions(+), 14 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index d428970d8..3ff49c78d 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -460,9 +460,12 @@ emits a self-contained `ContinuationProof` bundle; `verify_continuation(elf, &bu checks it using **only the bundle and the ELF** — nothing from the prover's memory. The integrated `prove_and_verify_continuation` proves and verifies in one **streaming** pass: it proves each epoch, verifies it inline with `verify_epoch`, -and drops that epoch's `MultiProof` — retaining only the small -`boundary`/`l2g_root`/`public_output` — before building and verifying the one -global proof. This bounds its retained-proof memory to O(1) epochs (at most two are +and drops that epoch's `MultiProof` — retaining only the +`boundary`/`l2g_root`/`public_output` (small next to a `MultiProof` for typical +epochs, though the accumulated per-epoch `boundary` lists still grow with the run's +total touched memory — the O(1) bound below is on retained *proof* data) — before +building and verifying the one global proof. This bounds its retained-proof memory +to O(1) epochs (at most two are live across the one-epoch `is_final` lookahead) instead of holding all *N*. It is a faithful in-process mirror of `verify_continuation` (it derives `is_final`/`label` **positionally** — a one-epoch lookahead for `is_final` — and chains `register_init` from each verified epoch's diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 7b532690e..516ed5d7f 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -731,13 +731,20 @@ impl<'a> EpochDriver<'a> { .map_err(|e| Error::Execution(format!("{e}")))? { Some(logs) => logs.to_vec(), - // `resume_with_limit` returns `None` only when `pc == 0` at entry, which the - // guard above already handles — so this arm is effectively unreachable today. - // Kept as a graceful terminator (not `unreachable!`) so that if a future - // change makes the executor stop for another reason, the driver ends cleanly - // rather than panicking; a resulting `is_final` disagreement would be caught - // by `verify_epoch` on the streaming path, never silently accepted. - None => return Ok(None), + // Unreachable today: `resume_with_limit` returns `None` only when `pc == 0` + // at entry, which the guard above already handles. If a future executor + // change makes it stop mid-run for another reason, fail loudly at the cause + // (still no panic) rather than ending the driver cleanly: a clean end here + // would make `prove_continuation` emit a bundle whose last epoch lacks HALT + // — never verifiable, with no diagnostic linking the later rejection back + // to the early stop. + None => { + return Err(Error::ContinuationInvariant( + "executor stopped mid-run without halting (resume_with_limit \ + returned None with pc != 0 at epoch entry)" + .to_string(), + )); + } }; let is_final = self.executor.pc() == 0; @@ -886,6 +893,10 @@ pub fn verify_continuation( let mut epoch_roots: Vec = Vec::with_capacity(n); let mut public_output: Vec = Vec::new(); + // NOTE: `prove_and_verify_continuation` mirrors this loop and the tail checks below + // inline over streamed epochs. Any check added or changed here MUST be mirrored + // there — the differential test only exercises honest proofs, so it cannot catch a + // rejection check missing from one of the two copies. for (index, epoch) in bundle.epochs.iter().enumerate() { let is_final = index == n - 1; let label = local_to_global::epoch_label(index as u64); @@ -950,9 +961,12 @@ pub fn prove_and_verify_continuation( epoch_size_log2: u32, opts: &ProofOptions, ) -> Result>, Error> { - // Match `verify_continuation`'s up-front bound so the two paths surface the same - // error on an oversized input (the executor also rejects it, but with a different - // variant). + // Match `verify_continuation`'s up-front bound so this function and the standalone + // verifier surface the same error variant for an oversized input, and fail fast + // before the executor copies it. (The two-phase composition `prove_continuation` + + // `verify_continuation` instead fails inside `Executor::new` with + // `Error::Execution` — `prove_continuation` runs first, so the verifier's bound is + // never reached on that path.) if private_inputs.len() as u64 > MAX_PRIVATE_INPUT_SIZE { return Err(Error::InvalidTableCounts(format!( "private input size ({}) exceeds max ({MAX_PRIVATE_INPUT_SIZE})", @@ -964,6 +978,9 @@ pub fn prove_and_verify_continuation( // Verify-side state, rebuilt independently of the prover: `register_init` chains // from each verified epoch's bound `reg_fini` (epoch 0 from the ELF entry point). + // NOTE: this loop and the tail checks below are an inline mirror of + // `verify_continuation`'s — any check added or changed there MUST be mirrored here + // (see the matching note on its epoch loop). let mut register_init = register::register_init_from_entry_point(driver.elf.entry_point); let mut all_boundaries: Vec> = Vec::new(); let mut epoch_roots: Vec = Vec::new(); @@ -972,7 +989,10 @@ pub fn prove_and_verify_continuation( // One-epoch lookahead: `is_final` is derived from whether another epoch actually // follows (positional), not from a flag the prover stored, so a driver enumeration - // bug cannot be silently self-consistent between the prove and verify halves. + // bug (an off-by-one or reorder) cannot be silently self-consistent between the + // prove and verify halves. Both halves ultimately observe the same in-process + // executor, so this buys mirror fidelity with `verify_continuation`'s positional + // derivation, not independence from the prover. let mut pending = driver.next()?; while let Some(epoch) = pending { let next = driver.next()?; @@ -998,6 +1018,12 @@ pub fn prove_and_verify_continuation( // Keep only what the global step + final checks need; the MultiProof drops here. // `epoch` is owned, so `reg_fini` moves out (no clone) into the next epoch's // derived init — the cross-epoch register chain, checked independently here. + // Unlike `verify_continuation` there is deliberately no `reg_fini` length guard: + // there it is deserialized and untrusted, while here it comes from in-process + // `prove_epoch` (`fini_from_trace` always yields exactly NUM_REGISTER_ADDRESSES + // entries). A wrong length would be an internal invariant bug and should fail + // loudly (the debug_assert in `compute_precomputed_commitment_with_fini`) + // rather than be reported as a rejected proof. let EpochProof { boundary, l2g_root, @@ -1501,6 +1527,27 @@ mod tests { )); } + // Negative: the streaming path's up-front private-input bound must reject an + // oversized input with the same variant as `verify_continuation` (its documented + // mirror). Pins the guard itself: without it the executor rejects the same input + // later, but with `Error::Execution`. Fires before any proving, so the test only + // costs the one oversized allocation. + #[test] + fn test_streaming_rejects_oversized_private_inputs() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let oversized = vec![0; MAX_PRIVATE_INPUT_SIZE as usize + 1]; + assert!(matches!( + prove_and_verify_continuation( + &elf_bytes, + &oversized, + 4, + &ProofOptions::default_test_options() + ), + Err(Error::InvalidTableCounts(_)) + )); + } + // The bundle's `boundary` field is used only to rebuild the global AIRs' touched- // PAGE set (genesis is recomputed from the ELF). The cross-epoch memory values // live in the committed L2G traces, tied to the epoch proofs by