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