Commit 38feb15
Continuations (Approach 2): prove executions epoch-by-epoch (#685)
* split execution into epochs
* Add an initial-memory image
* build a single epoch's traces
* Add an is_final flag for halt
* Make the HALT table optional
* Add a register_init parameter to VmAirs::new for the REGISTER preprocessed commitment
* reject a non-final epoch that contains the program-terminating instruction
* Add local-to-global boundary and process epochs to emit the boundary set
* Add local-to-global air table
* Add cross-epoch local-to-global memory linkage
* Add memory_bus_interactions to emit epoch init/fini tokens
* Wire the local-to-global table as the epoch-local Memory-bus bookend
* Add prove_and_verify_continuation
* stream epochs one at a time and drop traces after proving
* add bench_continuation
* Add multi-pass array asm program (1 MiB footprint, ~20M steps) as a worst-case local-to-global
memory stress benchmark
* Add a count mode to bench_continuation that reports a program's cycle count by running the executor only, as a no-proving proxy for monolithic proving memory
* l2g val to a single byte column
* Thread private inputs so we can bench ethrex program
* Use the static preprocessed bitwise commitment
* Avoid redundant per-epoch work (skip page and carry the memory)
* add global_memory for init-elf binding
* add clasification into stack vs data/heap in bench_continuation
* store memory in dense per-page arrays instead of per-cell HashMaps
* update doc
* Range-check the local-to-global continuation table columns
* slim range-check since memw already does it
* make fini_epoch constant, add MU selector for padding rows, add epoch ordering constraint
* Gate the local-to-global MU selector on the GlobalMemory bus only and constrain it boolean, leaving the epoch-local Memory bus and the range/ordering checks on unconditional multiplicity so the cross-epoch init_epoch < fini_epoch ordering check can never be skipped via MU; padding rows stay harmless because they self-cancel on the Memory bus and send only valid range/ordering lookups. Also add a design doc describing the continuation local-to-global memory protocol, both MU-wiring designs, and the soundness reasoning.
* Revert the local-to-global MU wiring to Design X (MU gates every L2G interaction, including the epoch-local Memory-bus bookend), because the Design Y variant that gated only the GlobalMemory bus is unsound: with the Memory bookend on unconditional multiplicity, a prover can set MU=0 on a non-first-touch row to orphan a touched epoch from the cross-epoch chain while its epoch proof still passes, and point the prover-controlled finalization at the truncation, silently dropping a real memory write. Gating the Memory bookend with MU forces MU=1 on every touched cell, which forces every touching epoch into the telescoping chain, making the chain complete and the finalization trustworthy. Update the design doc to record both designs, the chain-truncation attack, and the anchoring reasoning that makes Design X sound.
* Bind cross-epoch register
* Bind continuation epoch and global proofs to their statement in Fiat-Shamir (ELF, epoch label, epoch, count)
* update md
* carry the x254 commit index across epochs
* Force continuation epoch size to a power of two
* Use a power-of-two epoch size in tests
* Add a test with a non-power-of-two epoch size
* Split the integrated continuation prove+verify
* CLI continuation flag
* Remove dead-code allow and update doc
* Thread ProofOptions through prove_continuation/verify_continuation
* Seed the per-epoch touched-cell prediction from the carried register file instead of a fresh one
* Validate each epoch's reg_fini length
* Assert test_commit_across_epochs_verifies actually produces more than one epoch
* Continuations cleanup: docs, comments, and regression tests (#714)
Keep the follow-up scoped to non-performance cleanup while preserving the soundness regression coverage.
- Add L2G/global-memory regression tests for MU selector behavior, chain truncation, l2g-root binding, and private-input continuations.
- Fix stale continuation/global-memory docs and comments.
- Replace bare x254 byte address literals with register_base_address(254).
- Remove the unused DEFAULT_EPOCH_SIZE constant and document run_epochs as a test/bench helper.
* Use log2 epoch size for continuation CLI (#717)
Replace the continuation CLI's raw --epoch-size / --num-epochs controls with --epoch-size-log2.
The CLI now computes an exact power-of-two epoch size directly, defaults to 2^20, rejects tiny log2 values below 18, and no longer runs a cycle-count pre-pass to split into a target epoch count.
Update the continuation design doc and help text with the ethrex 10-transfer memory sweep as guidance.
* Delete init_ts column and drop ts from GlobalMemory bus
* Replace the always-zero global_memory init_epoch column with a verifier-fixed GENESIS_EPOCH constant
* Represent init state with dense representation instead of intermediate HashMaps
* Avoid duplicate L2G trace work in continuations (#719)
* Reuse genesis page data for continuation global proof (#720)
* Polish continuation verification and CLI (#728)
* Make continuation API take epoch size log2 (#730)
* Return continuation invariant errors instead of panicking (#731)
* Simplify continuation L2G trace construction (#732)
* Clean up continuation AIR setup (#733)
* Reject continuations exceeding the IsB20 cross-epoch ordering range (#734)
The cross-epoch ordering check proves `init_epoch < fini_epoch` via an IsB20
(20-bit) lookup on `fini_epoch - 1 - init_epoch`, so a run can have at most
2^20 epochs. Beyond that the IsB20 bus cannot balance and no honest proof
exists. Previously this was guarded only by a debug_assert in the prover's
bitwise emission, so a release build would build an unprovable trace and fail
cryptically — reachable via the library API with a small epoch size (the CLI's
min epoch size keeps it out of reach there).
Add a hard check in `prove_continuation`'s epoch loop returning
`Error::InvalidContinuationEpochSize` with a clear message once the epoch count
would exceed the range. This is a prover-side guard only: the verifier already
rejects any such proof (the IsB20 table is preprocessed and the ordering sender
is rebuilt verifier-side from a positional epoch label), so soundness is
unchanged — it just turns a confusing failure into a clean error.
Introduce `local_to_global::MAX_EPOCHS` as the single source of truth, used by
both the new check and the existing debug_assert (replacing the `1 << 20`
literal).
* add doc and debug_assert
---------
Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>1 parent ae858b8 commit 38feb15
31 files changed
Lines changed: 6560 additions & 227 deletions
File tree
- .github/workflows
- bin/cli
- src
- docs
- executor
- programs/asm
- src/vm
- tests
- prover
- benches
- src
- tables
- tests
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
102 | 102 | | |
103 | 103 | | |
104 | 104 | | |
| 105 | + | |
| 106 | + | |
| 107 | + | |
| 108 | + | |
| 109 | + | |
| 110 | + | |
| 111 | + | |
| 112 | + | |
| 113 | + | |
| 114 | + | |
| 115 | + | |
| 116 | + | |
| 117 | + | |
| 118 | + | |
| 119 | + | |
| 120 | + | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
105 | 125 | | |
106 | | - | |
| 126 | + | |
107 | 127 | | |
108 | 128 | | |
109 | 129 | | |
110 | | - | |
| 130 | + | |
111 | 131 | | |
112 | 132 | | |
113 | 133 | | |
114 | 134 | | |
115 | 135 | | |
| 136 | + | |
116 | 137 | | |
117 | 138 | | |
118 | 139 | | |
119 | 140 | | |
| 141 | + | |
120 | 142 | | |
121 | 143 | | |
122 | 144 | | |
123 | 145 | | |
124 | 146 | | |
125 | 147 | | |
126 | 148 | | |
| 149 | + | |
| 150 | + | |
| 151 | + | |
127 | 152 | | |
128 | 153 | | |
129 | 154 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
57 | 57 | | |
58 | 58 | | |
59 | 59 | | |
60 | | - | |
61 | | - | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
62 | 64 | | |
63 | 65 | | |
64 | 66 | | |
| |||
72 | 74 | | |
73 | 75 | | |
74 | 76 | | |
| 77 | + | |
75 | 78 | | |
76 | | - | |
| 79 | + | |
| 80 | + | |
77 | 81 | | |
78 | 82 | | |
79 | 83 | | |
| |||
96 | 100 | | |
97 | 101 | | |
98 | 102 | | |
| 103 | + | |
| 104 | + | |
| 105 | + | |
| 106 | + | |
| 107 | + | |
| 108 | + | |
| 109 | + | |
99 | 110 | | |
100 | 111 | | |
101 | 112 | | |
102 | 113 | | |
| 114 | + | |
| 115 | + | |
| 116 | + | |
| 117 | + | |
| 118 | + | |
| 119 | + | |
| 120 | + | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
| 125 | + | |
103 | 126 | | |
104 | 127 | | |
105 | 128 | | |
| |||
0 commit comments