Continuations (Approach 2): prove executions epoch-by-epoch

[nicole-graus]

Motivation

Monolithic proving holds the whole execution trace in memory, so program size is bounded by RAM. Continuations split a long execution into fixed-size epochs that are proven independently, keeping peak memory flat as the program grows. Only memory consistency has to cross epoch boundaries.

What this does

• Splits execution into N-cycle epochs, each proven on its own; tables are dropped from memory after each epoch.
• Introduces the local-to-global (L2G) table: one row per memory cell an epoch touches. Inside an epoch it bookends the Memory bus (replacing PAGE, which is switched off in continuation epochs); across epochs it carries each cell's init/fini claims.
• Links epochs with one global proof over a GlobalMemory LogUp plus a global_memory table that anchors genesis (initial memory, recomputed from the ELF by the verifier — not prover-supplied) and finalization (final values).
• Per-epoch perf: skip PAGE where the L2G bookend covers it, carry the memory image forward instead of re-snapshotting, and store memory in dense per-page arrays.

Soundness mechanisms

• Range checks on L2G columns — only what isn't already pinned by MEMW (cross-epoch-only fields via IsHalfword halfwords; values via AreBytes).
• fini_epoch as a verifier-supplied per-table constant (1-based labels, genesis = 0) — the prover can't choose it.
• Cross-epoch ordering init_epoch < fini_epoch, checked via IsB20[fini_epoch − 1 − init_epoch], preventing a row from referencing a future/own epoch to inject an unjustified value.
• MU selector gating the GlobalMemory bus so padding rows are inert; the Memory bus and range/ordering checks stay unconditional, so the ordering check can never be skipped via MU.

Full write-up, including both MU-wiring designs and the adversarial-review reasoning, in docs/continuations_l2g_design.md.

Status — draft

Known soundness gap, deferred: cross-epoch register continuity (epoch i's register init is a prover-supplied snapshot, not yet bound to epoch i-1's fini). Memory continuity is complete.

How to test

cargo test --release -p lambda-vm-prover continuation