fix(continuations): review follow-ups for the streaming verify path#778
Merged
MauroToscano merged 1 commit intoJul 3, 2026
Conversation
- 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).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Review follow-ups for #766 (targets its branch, so the diff stays scoped to the streaming path).
Motivation
An adversarial multi-agent review of #766 surfaced a handful of low-severity items — all comment/diagnosability/test-level; no correctness or soundness issues. This PR lands the ones that are cheap and don't touch design decisions.
Description
prove_continuation+verify_continuation) fails earlier, insideExecutor::new, withError::Execution— the verifier's bound is never reached on that path. The comment now states exactly which parity the guard buys (with the standalone verifier, plus fail-fast before the executor copies the input), and a regression test pins the guard'sInvalidTableCountsvariant (previously nothing exercised it; the bundle-path test only coversverify_continuation).EpochDriver::next: fail loudly if the executor ever stops mid-run. TheNone => Ok(None)arm is unreachable today, and its comment's safety argument ("caught byverify_epochon the streaming path") only covers one of the driver's two callers: on theprove_continuationpath a future mid-run stop would silently emit a bundle whose last epoch lacks HALT — never verifiable, with no diagnostic at the cause. Now returnsErr(ContinuationInvariant)— still no panic, no behavior change today (the whole continuation suite passes unchanged).prove_and_verify_continuationinline-mirrorsverify_continuation's loop and tail; the differential test only exercises honest proofs, so it cannot catch a rejection check dropped from one copy. Both loops now carry a note that changes must be mirrored.reg_finilength-guard asymmetry (in-process fini is trusted, a wrong length is an internal invariant bug that should fail loudly rather than read as a rejected proof) so it doesn't look like drift.is_finalactually buys (mirror fidelity — both halves observe the same in-process executor), and the design doc qualifies "small" (accumulatedboundarylists grow with total touched memory; the O(1) bound is on retained proof data — 56 B per touched byte-address per epoch, so memory-heavy runs retain GBs of boundaries either way).Deliberately NOT done here (author's call, happy to discuss): extracting a shared per-epoch verify-state helper consumed by both
verify_continuationand the streaming loop. It would make check-set drift impossible by construction (and make rejection checks unit-testable with corruptedEpochProofs) at the cost of a ~268 Breg_finiclone + a transientboundaryclone per epoch on the streaming side — but it refactors the soundness boundary, which shouldn't happen in a drive-by PR.Testing
cargo fmt,cargo clippy -p lambda-vm-prover --all-targetsclean;test_streaming_rejects_oversized_private_inputs(new),test_streaming_zero_epoch_returns_none,test_streaming_exactly_two_epochs, andtest_streaming_matches_two_phaseall pass in release.