diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 9c3f54747..8b30e57fc 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -3,7 +3,8 @@ This is the single design document for the "continuations" prover (Approach 2, "prove-epoch" from the streaming spec). It covers the things a continuation must carry across epoch boundaries — **memory** (the bulk of the doc: §1–§5, including -the cross-epoch local-to-global table and the Design X vs Design Y decision), +the cross-epoch local-to-global table and its selector-free chain-completeness +argument), **registers** including the commit index x254 (§6), and the **Fiat-Shamir statement binding** (§7) that ties each epoch proof to its program and position — plus the soundness mechanisms that make each safe. §8 describes the **standalone (split) @@ -76,9 +77,11 @@ makes the proof fail. which epoch wrote it access timestamp) ``` -Column layout (9 columns): `address_lo/hi` (32-bit), `init_value` (byte), +Column layout (8 columns): `address_lo/hi` (32-bit), `init_value` (byte), `init_epoch` (two 16-bit halfwords), `fini_value` (byte), -`fini_timestamp_lo/hi` (32-bit), `MU` (selector). +`fini_timestamp_lo/hi` (32-bit). There is **no selector column** — every row is +real (a touched cell or a brought-forward filler) and every interaction fires with +multiplicity 1 (see §3.4). Note: **`fini_epoch` is NOT a column** — it is supplied as a per-table constant (see §4.2). @@ -182,29 +185,56 @@ Unreachable in practice (optimal epochs are millions of cycles → thousands of epochs even for a billion-cycle run) and fails closed. If ever needed, widen the gap check to 32-bit or switch to the LT table. -### 3.4 The `MU` selector - -Traces are padded with blank rows to a power of two (an FFT requirement). Those -padding rows must not disturb any bus. - -Originally padding was harmless because a blank row's `init` and `fini` tokens -were identical and self-cancelled. **Two** of the changes above broke that, each -on its own: - -- §3.2 (constant `fini_epoch`): a padding row's `fini` now carries - `epoch = the constant` while its `init` carries `epoch = 0`, so the tokens - differ and no longer cancel. -- §3.3 (the ordering check): a padding row has `init_epoch == fini_epoch` (both - `0`), which fails the strict `<` check. - -So `MU` is required by *either* change. - -Fix: a selector column `MU` (1 on real rows, 0 on padding). Interactions gated by -`Multiplicity::Column(MU)` contribute nothing on padding rows. - -`MU` is itself constrained boolean (`MU·(1−MU)=0`), and pinned to the right -rows by bus balance (a real row with `MU=0` drops its telescoping link → -imbalance). +### 3.4 Padding via brought-forward (filler) rows + +Traces are padded to a power of two (an FFT requirement). Those padding rows must +not disturb any bus. + +Blank (all-zero) padding rows do **not** work here. Two of the changes above break +their self-cancellation, each on its own: + +- §3.2 (constant `fini_epoch`): a blank row's `fini` carries `epoch = the constant` + while its `init` carries `epoch = 0`, so on the **GlobalMemory** bus the two + tokens differ and no longer cancel. +- §3.3 (the ordering check): a blank row has `init_epoch == fini_epoch` (both `0`), + which fails the strict `<` check. + +An earlier design fixed this with a boolean **`MU` selector column** (1 on real +rows, 0 on padding) gating every interaction. That column has since been +**removed**. Instead the table has **no selector**: every interaction fires with +multiplicity 1 (exactly like PAGE), and the power-of-two padding rows are **real +"brought-forward" rows** for genuinely-untouched memory cells, carried forward +unchanged from their previous owner to the current epoch: + +- `init_value == fini_value` (value unchanged), +- `fini_timestamp = 0`, +- `init_epoch = the cell's previous owner` (`GENESIS_EPOCH = 0` if never written), +- `fini_epoch = the current epoch` (the same per-table constant as real rows). + +Such a filler is a provable no-op on both buses: + +- **Epoch-local Memory bus:** its init-receive `[0, addr, 0, 0, value]` and + fini-send `[0, addr, 0, 0, value]` are the *identical* token (`fini_ts = 0`, + `init_value = fini_value`), so they self-cancel — exactly as PAGE's init/fini + bookend cancels for a never-accessed cell. An untouched cell has **no MEMW + partner** to balance any non-cancelling token, so this self-cancellation is the + *only* shape a filler can take without dangling a Memory-bus token; the memory + argument therefore **forces** both `fini_ts = 0` and `init_value = fini_value`. +- **GlobalMemory bus:** it consumes the cell's current head token + `(addr, value, prev_owner)` and produces `(addr, value, current_epoch)` — a + value-preserving telescoping link, grounded (like every chain) at genesis and + ordered by the strict `init_epoch < fini_epoch` check (`prev_owner < current`). + The constant `fini_epoch` is fine here precisely because a filler is a *real + link*, not a self-cancel. + +The prover sources filler cells from each epoch's own touched pages first (which +never enlarge the global touched-page set) and from genesis pages as a fallback +(needed when an epoch touched no cell of its own); it updates each brought-forward +cell's provenance to the current epoch so the next epoch to touch it sees the right +owner. This relies on `#total live cells ≥ next_pow2(#touched per epoch)`; the +prover **fails closed** (`Error::ContinuationFillerShortage`) if that pool is ever +too small — a completeness limit, never an unsound proof. Because paged memory +gives each touched page `2^18` cells, this holds for every realistic program. ### 3.5 CPU padding and the power-of-two epoch size @@ -233,48 +263,47 @@ accepts — only how the driver slices cycles. A debug-assert enforces the --- -## 4. Design X vs Design Y — *where* `MU` is applied +## 4. Chain completeness — why the design is selector-free (and safe) -`MU` is needed to neutralize padding, but **which** interactions should it gate? +The soundness backbone is **chain completeness**: every touched epoch must be +forced into each cell's cross-epoch chain, so the prover-controlled finalization is +pinned. This section explains why completeness holds with **no selector column**, +and preserves — as the guiding lesson — the chain-truncation attack that an earlier +selector-based design (Design Y) opened. -``` - GlobalMemory Memory range + - (telescoping) (bookend) ordering - Design X (SOUND): MU MU MU ← MU gates everything - Design Y (UNSOUND): MU One One ← MU only on GlobalMemory -``` - -**Conclusion up front: Design X is sound; Design Y is *not*.** We initially -believed Y was a cleaner equivalent (and two adversarial reviews agreed). They -were wrong — Y opens a chain-truncation attack. Below is X, then Y, then the -attack and why X blocks it. +### Why completeness holds without a selector (Statement S) -### Design X +The load-bearing fact is **Statement S**: -`MU` gates **every** L2G interaction (matches the standard table pattern — -LT/MUL/MEMW each gate all their interactions with one multiplicity column). +> In a continuation epoch, the only table that provides a RAM cell's seed (its +> value at timestamp 0) on the Memory bus is L2G (PAGE is off). If a cell is +> accessed by MEMW during the epoch, the memory argument requires that seed; if the +> L2G seed/fini bookend does not fire, the Memory bus cannot balance. Therefore any +> accessed cell is forced to have a firing L2G bookend. -The crucial consequence — which we first mistook for redundancy — is that gating -the **Memory bus bookend** with `MU` forces `MU = 1` on every *touched* cell: -a touched cell's MEMW accesses need the L2G seed/fini on the Memory bus (PAGE is -off), so `MU = 0` would dangle them → the epoch proof fails. This is **Statement -S** below. Forcing `MU = 1` on every touched cell forces every touching epoch -**into the global chain** — so the chain is **complete**, and cannot be truncated. +S rests on three checkable facts: (1) PAGE is off in continuation epochs; +(2) MEMW enforces timestamp ordering, so a cell's access chain must bottom out at +the seed; (3) no other table provides a RAM seed (REGISTER is registers only, a +disjoint token subspace). -### Design Y (rejected — unsound) +With **no selector column**, every L2G row's Memory bookend fires unconditionally +(`Multiplicity::One`). So a touched cell's bookend *always* fires — there is no +selector to set to 0 — which is a strictly stronger form of S than any gated +design: every touching epoch is **unconditionally** in the global chain, so the +chain is complete and the finalization is pinned. Fillers add only extra +value-preserving links (§3.4) and never remove one. -`MU` gates **only the GlobalMemory bus**; the Memory bus and range/ordering checks -use `Multiplicity::One`. The intended win was that the ordering check then fires -unconditionally so `MU` can't skip it. But decoupling the Memory bookend from `MU` -**broke Statement S**: a touched cell's bookend now fires regardless of `MU` -(`Multiplicity::One`), so the epoch proof passes even with `MU = 0`. Nothing then -forces `MU = 1` on a *non-first-touch* row — and that is exploitable. +### The lesson we keep: the Design-Y chain-truncation attack -### The attack Design Y allows: orphan a touched epoch +An earlier design ("Design Y") gated **only** the GlobalMemory bus with a selector +`MU`, leaving the Memory bookend and range/ordering checks at `Multiplicity::One`. +Two adversarial reviews called it sound; they were wrong. Because the Memory +bookend fired regardless of `MU`, a touched epoch's proof passed even with `MU = 0`, +and nothing forced `MU = 1` on a *non-first-touch* row: Cell A, touched by epochs e1 then e2. Honest: genesis `v0` → e1 writes `f1` → -e2 writes `f2` → final `f2`. A cheating prover sets **`MU = 0` on e2's L2G row** -and sets `global_memory`'s finalization for A to `f1`: +e2 writes `f2` → final `f2`. A cheat sets `MU = 0` on e2's L2G row and points +`global_memory`'s finalization for A at `f1`: ``` genesis(v0) ──► e1.init ✓ (genesis must be consumed — forces e1 only) @@ -282,45 +311,21 @@ and sets `global_memory`'s finalization for A to `f1`: e2.init / e2.fini ✗ MU=0 — orphaned, don't fire ``` -- The GlobalMemory bus **balances** (every fired token matched). -- e2's **epoch proof still passes** — in Design Y its Memory bookend is - `Multiplicity::One`, so it fires regardless of `MU`; e2 ran internally-consistently. -- **Nothing forces `MU_e2 = 1`:** e2 isn't first-touch (genesis went to e1), and - the finalization is a *prover column*, so it just absorbs whatever the last fired - fini was. - -Result: e2's write to A is silently dropped — A's final value is claimed `f1` -when it's really `f2`. A false statement, proven. (For a *middle* epoch, reroute -the later init to consume the earlier fini, skipping the middle one.) - -The root cause is the **input/output asymmetry** of the anchors: genesis is the -*input* and is ELF-bound (fixed), but the finalization is the *output* — a prover -column. The finalization is only trustworthy if the chain is **complete** so that -the last fini is *forced* to be consumed by it. A complete chain pins the -finalization; a truncatable chain leaves it free. Design X forces completeness -(via `MU=1` on every touched cell); Design Y does not. - -### Statement S (why Design X is sound, and what Y broke) - -> In a continuation epoch, the only table that provides a RAM cell's seed (its -> value at timestamp 0) on the Memory bus is L2G (PAGE is off). If a cell is -> accessed by MEMW during the epoch, the memory argument requires that seed; with -> `MU = 0` the seed is absent and the Memory bus cannot balance. Therefore any -> accessed cell is forced to `MU = 1`. - -S rests on three checkable facts: (1) PAGE is off in continuation epochs; -(2) MEMW enforces timestamp ordering, so a cell's access chain must bottom out at -the seed; (3) no other table provides a RAM seed (REGISTER is registers only, a -disjoint token subspace). +The GlobalMemory bus balances, e2's epoch proof still passes, and e2's write to A +is silently dropped — A's final value is claimed `f1` when it is really `f2`. A +false statement, proven. The root cause is the **input/output asymmetry** of the +anchors: genesis is the *input* and is ELF-bound (fixed), but the finalization is +the *output* — a prover column, trustworthy only if the chain is **complete** so +the last fini is *forced* to be consumed by it. -**S requires the Memory bookend to be `MU`-gated** — that is exactly what Design X -has and Design Y removed. So the "redundant" `MU` on the Memory bus in Design X is -in fact load-bearing: it's what forces every touched epoch into the chain, making -the chain complete and the finalization trustworthy. +**How the current design forecloses this:** there is no `MU` column to zero, so no +row can be silenced — the attack is structurally impossible. Removing the selector +did not weaken S; it removed the very lever the attack needed. (This is why we do +**not** reintroduce any selector-gated Memory bookend.) ### The anchoring chain (why a real access cannot be dropped at all) -`MU = 1` being forced bottoms out at the program itself: +A forced-firing L2G bookend bottoms out at the program itself: ``` ELF ─DECODE(preprocessed)─► each row's instruction (LOAD/STORE flags) is fixed @@ -328,13 +333,14 @@ the chain complete and the finalization trustworthy. │ ▼ a real load/store row has its flag = 1 (DECODE match + IsBit) ⟹ CPU sends Memw req ▼ MEMW must receive it (MU_READ/MU_WRITE) — dropping it ⟹ Memw-bus imbalance - ▼ MEMW's bookend pairing needs the L2G seed/fini — in Design X (MU-gated) ⟹ MU=1 - ▼ MU=1 ⟹ the cell is in the global chain ⟹ chain complete ⟹ finalization pinned + ▼ MEMW's bookend pairing needs the L2G seed/fini, which fires unconditionally + ▼ ⟹ the cell is in the global chain ⟹ chain complete ⟹ finalization pinned ``` This is the VM's core execution soundness (DECODE + PC-continuity + IsBit flags, verified in `cpu.rs` / `constraints/cpu.rs`), extended one link at a time up to -cross-epoch memory. Design X keeps every link; Design Y cut the MEMW→L2G link. +cross-epoch memory. Every link is kept; the selector-free bookend is what makes the +MEMW→L2G link unconditional. ### How `global_memory`'s finalization is constrained — and the parallel with `main` @@ -343,28 +349,33 @@ output, not a known input). It is pinned **internally** by the bus: it must cons the last fini of each cell's chain, which (with a complete chain) is the cell's real last-written value. This is exactly how **PAGE** works in the monolithic prover — PAGE's `fini` is pinned by the (single, complete) Memory bus to the last -MEMW write. Design X is the faithful cross-epoch extension; Design Y silently -dropped the "chain is complete" property both rely on. +MEMW write. The selector-free L2G is the faithful cross-epoch extension; Design Y +silently dropped the "chain is complete" property both rely on. --- ## 5. Adversarial review summary -1. **`MU` safety (Design X).** Could `MU=0` on a real row, or a non-boolean `MU`, - skip the ordering or forge a balance? No — caught by the Memory bus (Statement - S) and the boolean constraint. **Holds.** -2. **Design Y.** Two adversarial reviews concluded Y was sound (padding harmless, - ordering unconditional, "ghost row" attack defeated). **They were wrong.** Both - only tested *first-touch* `MU=0` (genesis dangles → caught) and added/forged +1. **Selector-free padding (brought-forward fillers).** Can a filler row be a + non-no-op — inject/change a value, or forge a timestamp? No — an untouched cell + has no MEMW partner, so on the Memory bus its init/fini must be the identical + token (`fini_ts = 0`, `init_value = fini_value`) or a token dangles; any other + shape is rejected. On the GlobalMemory bus a filler is forced to consume its + cell's real head token, so its value telescopes from genesis. **Holds** (see the + negative tests in `local_to_global_bus_tests.rs`). +2. **The Design-Y lesson (chain truncation).** An earlier selector design gated only + the GlobalMemory bus; two adversarial reviews called it sound and were wrong — + they only tested *first-touch* `MU=0` (genesis dangles → caught) and added/forged rows; neither tested **truncating the chain at a non-first-touch row** while - pointing the prover-controlled finalization at the truncation. That attack (§4) - makes Y unsound. Lesson: a review that misses an attack class proves nothing - about it — the truncation/orphan class was the gap. + pointing the prover-controlled finalization at the truncation (§4). Removing the + selector entirely makes that attack structurally impossible (no row can be + silenced). Lesson kept: a review that misses an attack class proves nothing about + it — the truncation/orphan class was the gap. 3. **`fini_epoch` as a constant.** Sound — strictly more so than a column. Labels are verifier-computed from epoch position (unforgeable); prove/verify use identical labels (no off-by-one); the free `init_epoch` column and - `global_memory`'s `FINI_EPOCH` column are pinned by bus balance **when the chain - is complete** (Design X). Independent of the X/Y choice. + `global_memory`'s `FINI_EPOCH` column are pinned by bus balance because the chain + is complete (§4 — every touched cell's bookend fires unconditionally). --- @@ -518,15 +529,16 @@ recursion/aggregation layer (deferred). ## 9. Status and open items - Implemented and tested: range checks (§3.1), `fini_epoch` constant (§3.2), - ordering check (§3.3), the `MU` selector (§3.4), the **power-of-two epoch size** - (§3.5), **cross-epoch registers** (§6), the **commit index x254** across epochs - (§6), the **Fiat-Shamir statement binding** (§7), and the **standalone split - prover/verifier** (§8) — bundle serialized with `bincode` and driven from the CLI - (`prove`/`verify --continuations`). -- **The committed code implements Design X** (`MU` gates every L2G interaction), - which is the sound design. Design Y was implemented briefly, then found unsound - (§4, the chain-truncation attack) and **reverted**. Do not re-introduce the - Design Y wiring: gating only the GlobalMemory bus reopens the orphan attack. + ordering check (§3.3), **selector-free brought-forward filler padding** (§3.4), + the **power-of-two epoch size** (§3.5), **cross-epoch registers** (§6), the + **commit index x254** across epochs (§6), the **Fiat-Shamir statement binding** + (§7), and the **standalone split prover/verifier** (§8) — bundle serialized with + `bincode` and driven from the CLI (`prove`/`verify --continuations`). +- **The L2G table has no selector column.** An earlier `MU`-gated design (and the + briefly-implemented, unsound Design Y that gated only the GlobalMemory bus) were + both replaced by the selector-free filler design (§3.4). Do **not** reintroduce a + selector-gated Memory bookend: it would recreate the lever the chain-truncation + attack (§4) needs. - Deferred: - **Succinctness.** The split verifier is non-succinct (N+1 proofs, §8). A single small proof needs a recursion/aggregation layer — a separate, larger effort. @@ -541,7 +553,7 @@ recursion/aggregation layer (deferred). - `prover/src/tables/local_to_global.rs` — L2G columns, trace generation, the Memory/GlobalMemory bus interactions, range checks, the ordering lookup, and - the per-row selector. + `append_bring_forward_fillers` (the selector-free power-of-two padding). - `prover/src/tables/global_memory.rs` — the genesis (ELF-bound) and finalization anchors. - `prover/src/tables/register.rs` — the REGISTER table: REG-C1/REG-C2 Memory-bus diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index ccdd5a6f9..52d327b89 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -104,33 +104,19 @@ fn global_transcript(elf_bytes: &[u8], num_epochs: usize) -> DefaultTranscript Vec>> { - use crate::constraints::templates::IsBitConstraint; - use stark::constraints::transition::TransitionConstraint; - vec![IsBitConstraint::unconditional(local_to_global::cols::MU, 0).boxed()] -} - /// Local-to-global AIR on the cross-epoch GlobalMemory bus (used in the global proof). /// /// `epoch_label` is this epoch's 1-based label; it is the `fini_epoch` constant /// the fini token carries (not a trace column, since it's the same for every row). /// -/// Uses `empty_constraints()` deliberately: the MU boolean (`MU·(1-MU)=0`), the -/// column range checks, and the `init_epoch < fini_epoch` ordering are NOT -/// re-asserted here. They are enforced once in the epoch proof's `l2g_memory_air`, -/// and `verify_l2g_commitment_binding` ties this global L2G sub-table to the *same* -/// committed trace (equal Merkle roots). So under collision resistance the trace the -/// global bus runs over already satisfies all those constraints — do not add them -/// here (it would be redundant, not a missing check). +/// Uses `empty_constraints()` deliberately: the column range checks and the +/// `init_epoch < fini_epoch` ordering are NOT re-asserted here. They are enforced +/// once in the epoch proof's `l2g_memory_air`, and `verify_l2g_commitment_binding` +/// ties this global L2G sub-table to the *same* committed trace (equal Merkle +/// roots). So under collision resistance the trace the global bus runs over already +/// satisfies all those checks — do not add them here (it would be redundant, not a +/// missing check). The table has no AIR transition constraints of its own (there is +/// no longer any selector column to bound). fn l2g_global_air( opts: &ProofOptions, epoch_label: u64, @@ -151,7 +137,10 @@ fn l2g_global_air( /// Carries the column range checks and the `init_epoch < fini_epoch` ordering /// check too: this proof has the BITWISE provider, and the global proof commits /// the identical trace (the commitment binding compares roots), so checking here -/// covers both. `epoch_label` is the `fini_epoch` constant used by both. +/// covers both. `epoch_label` is the `fini_epoch` constant used by both. The table +/// has no AIR transition constraints (every row is real — a touched cell or a +/// brought-forward filler — so there is no selector to bound); soundness rests on +/// the bus balance and the range/ordering lookups. fn l2g_memory_air( opts: &ProofOptions, epoch_label: u64, @@ -166,7 +155,7 @@ fn l2g_memory_air( AuxiliaryTraceBuildData { interactions }, opts, 1, - l2g_constraints(), + empty_constraints(), ) } @@ -231,6 +220,33 @@ fn global_memory_configs_from_init_page_data( .collect() } +/// Page bases (in preference order) from which one epoch draws brought-forward +/// filler rows for [`local_to_global::append_bring_forward_fillers`]: the epoch's +/// own touched pages first (already in the global touched-page set, so fillers on +/// them add no `GLOBAL_MEMORY` table), then any genesis page as a fallback for +/// epochs that touched no cell of their own. Deduplicated, deterministic. +fn filler_candidate_pages( + boundary: &[CellBoundary], + init_page_data: &HashMap>, +) -> Vec { + let mut seen: std::collections::BTreeSet = std::collections::BTreeSet::new(); + let mut pages: Vec = Vec::new(); + for b in boundary { + let base = page::page_base_for_address(b.address); + if seen.insert(base) { + pages.push(base); + } + } + let mut genesis: Vec = init_page_data.keys().copied().collect(); + genesis.sort_unstable(); + for base in genesis { + if seen.insert(base) { + pages.push(base); + } + } + pages +} + /// Per-epoch register state and label. struct EpochStart<'a> { register_init: &'a [u32], @@ -532,9 +548,19 @@ fn prove_global( init_page_data: &HashMap>, opts: &ProofOptions, ) -> Result, Error> { - // Each cell's final state (boundaries are in epoch order, so the last fini wins). + // Each cell's final state (boundaries are in epoch order and each epoch touches + // an address at most once — touched cells are unique and fillers are drawn from + // untouched cells — so iterating in order makes the highest-epoch fini win, which + // is the true final value). let mut final_state: global_memory::FiniStateMap = HashMap::new(); for epoch in boundaries { + debug_assert!( + { + let mut seen = std::collections::HashSet::new(); + epoch.iter().all(|b| seen.insert(b.address)) + }, + "an epoch's boundary must not repeat an address (touched + filler rows are disjoint)" + ); for b in epoch { final_state.insert( b.address, @@ -726,20 +752,47 @@ pub fn prove_continuation( #[cfg(feature = "disk-spill")] stark::storage_mode::StorageMode::Ram, )?; - let boundary = + let mut boundary = local_to_global::epoch_boundary(&mut provenance, label, &traces.touched_memory_cells); + // Carry the image forward from this epoch's real writes (the touched cells, + // which are all of `boundary` before fillers are appended): this epoch's fini + // is the next epoch's init. Filler rows are value-preserving no-ops, so they + // are deliberately excluded here. + for cell in &boundary { + image.set(cell.address, (cell.fini.value & 0xFF) as u8); + } + + // Pad the epoch's L2G table to a power of two with brought-forward filler + // rows for untouched cells (so it needs no MU selector). Source from this + // epoch's own touched pages first — they never enlarge the global + // touched-page set — then genesis pages as a fallback (needed when the epoch + // touched no cell of its own). Fails closed if an epoch touches too large a + // fraction of total memory (the `#total cells ≥ next_pow2(#touched)` + // assumption); the verifier would reject such a proof anyway. + let candidate_pages = filler_candidate_pages(&boundary, &init_page_data); + local_to_global::append_bring_forward_fillers( + &mut boundary, + &mut provenance, + &candidate_pages, + label, + ) + .map_err(|s| { + Error::ContinuationFillerShortage(format!( + "epoch {label} needs {} local-to-global rows (a power of two) but only \ + {} could be filled (touched cells plus every untouched cell available \ + to bring forward); the execution touches too large a fraction of total \ + memory in one epoch (use a smaller epoch size)", + s.needed, s.got + )) + })?; + 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()); - - // 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); - } epochs.push(epoch); if is_final { @@ -874,8 +927,57 @@ pub fn prove_and_verify_continuation( #[cfg(test)] mod tests { use super::*; + use crate::tables::local_to_global::{FiniClaim, InitClaim}; use crate::test_utils::asm_elf_bytes; + fn boundary_at(address: u64) -> CellBoundary { + CellBoundary { + address, + init: InitClaim { + value: 0, + originating_epoch: 0, + timestamp: 0, + }, + fini: FiniClaim { + value: 0, + epoch: 1, + timestamp: 0, + }, + } + } + + // filler_candidate_pages lists the epoch's own touched pages FIRST (so fillers + // don't enlarge the global touched-page set), then genesis pages as a fallback, + // deduplicated. This exercises the fallback branch used when an epoch touches no + // cell of its own (which the self-contained bus tests bypass by passing pages + // directly). + #[test] + fn test_filler_candidate_pages_touched_first_then_genesis_fallback() { + let page = page::DEFAULT_PAGE_SIZE as u64; + // Touched cell on page 1; genesis image spans pages 0, 1, 2. + let boundary = vec![boundary_at(page + 5)]; + let init_page_data: HashMap> = + HashMap::from([(0, vec![1]), (page, vec![1]), (2 * page, vec![1])]); + + let pages = filler_candidate_pages(&boundary, &init_page_data); + + // Touched page (1) comes first; genesis pages 0 and 2 follow (page 1 is not + // repeated), sorted. + assert_eq!(pages, vec![page, 0, 2 * page]); + } + + // With no touched cells (a compute-only epoch), the candidate set is exactly the + // genesis pages, sorted — this is the fallback the streaming prover relies on to + // pad a zero-touch epoch's L2G table. + #[test] + fn test_filler_candidate_pages_zero_touch_uses_genesis_pages() { + let page = page::DEFAULT_PAGE_SIZE as u64; + let init_page_data: HashMap> = + HashMap::from([(2 * page, vec![1]), (0, vec![1])]); + let pages = filler_candidate_pages(&[], &init_page_data); + assert_eq!(pages, vec![0, 2 * page]); + } + // `test_commit_split` issues two Commit syscalls, one early and one late, so a // small epoch puts the second commit in a later epoch. That epoch starts with // x254 > 0 (the carried commit index), which exercises the cross-epoch commit diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 760383003..472b7bafa 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -192,6 +192,10 @@ pub enum Error { InvalidContinuationEpochSize(String), /// Continuation proof construction hit an internal invariant failure. ContinuationInvariant(String), + /// A continuation epoch touches too large a fraction of total memory to pad its + /// local-to-global table to a power of two with brought-forward filler rows + /// (`#total live cells < next_pow2(#touched this epoch)`). + ContinuationFillerShortage(String), /// A non-final continuation epoch contains the program-terminating /// instruction. The terminating instruction must be in the final epoch. HaltInNonFinalEpoch, @@ -214,6 +218,9 @@ impl fmt::Display for Error { Error::ContinuationInvariant(msg) => { write!(f, "continuation invariant failed: {msg}") } + Error::ContinuationFillerShortage(msg) => { + write!(f, "continuation local-to-global filler shortage: {msg}") + } Error::HaltInNonFinalEpoch => { write!( f, diff --git a/prover/src/tables/local_to_global.rs b/prover/src/tables/local_to_global.rs index ada19baf5..28313f7b5 100644 --- a/prover/src/tables/local_to_global.rs +++ b/prover/src/tables/local_to_global.rs @@ -46,20 +46,45 @@ //! guarantee. There is no `init_timestamp` column: timestamps are epoch-local, and //! the cross-epoch chain is ordered by epoch. //! -//! ## Padding +//! ## Padding via brought-forward (filler) rows //! -//! Real rows carry `MU = 1`; the power-of-two padding rows carry `MU = 0`. Every -//! interaction uses `Multiplicity::Column(MU)`, so padding rows fire nothing — -//! we never rely on token self-cancellation (this is the standard pattern used -//! by every variable-length table). `MU` is self-enforced: dropping a real row -//! (`MU = 0`) breaks its telescoping link → bus imbalance. +//! The table has no selector column. Every interaction fires with multiplicity 1 +//! on every row (exactly like PAGE). The power-of-two padding rows are therefore +//! not inert — they are **real "brought-forward" rows** for genuinely-untouched +//! memory cells, carried forward unchanged from their previous owner to the +//! current epoch: `init_value == fini_value`, `fini_timestamp = 0`, +//! `init_epoch = the cell's previous owner` (`GENESIS_EPOCH` if never written), +//! `fini_epoch = the current epoch`. +//! +//! Such a filler is a genuine no-op on both buses: +//! - On the epoch-local `Memory` bus its init-receive `[0, addr, 0, 0, value]` and +//! fini-send `[0, addr, 0, 0, value]` are the *identical* token (fini_ts = 0, +//! init_value = fini_value), so they self-cancel — exactly as PAGE's init/fini +//! bookend cancels for a never-accessed cell (`page.rs`). An untouched cell has +//! no MEMW to balance any non-cancelling token, so this self-cancellation is the +//! *only* shape a filler can take without dangling a Memory-bus token; it forces +//! both `fini_ts = 0` and `init_value = fini_value`. +//! - On the cross-epoch `GlobalMemory` bus it consumes the cell's current head +//! token `(addr, value, prev_owner)` and produces `(addr, value, current_epoch)` +//! — a value-preserving telescoping link, grounded (like every chain) at the +//! `GENESIS_EPOCH` source and ordered by the `init_epoch < fini_epoch` check. The +//! constant `fini_epoch` is fine here precisely because a filler is a real link, +//! not a self-cancel. +//! +//! Because the trace must be a power of two, each epoch needs +//! `next_pow2(#touched) - #touched` such fillers, drawn from distinct live cells not +//! touched that epoch (see [`append_bring_forward_fillers`]). This relies on +//! `#total live cells ≥ next_pow2(#touched per epoch)`; the continuation prover +//! sources fillers from the epoch's own touched pages (and genesis pages as a +//! fallback) and fails closed if that pool is ever too small. -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; use super::bitwise::{BitwiseOperation, BitwiseOperationType}; +use super::page::DEFAULT_PAGE_SIZE; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField}; use crate::paged_mem::PagedMem; @@ -189,6 +214,92 @@ pub fn genesis_provenance(genesis: impl IntoIterator) -> Prov provenance } +/// The number of filler rows [`append_bring_forward_fillers`] could not supply: the +/// candidate cell pool was too small to pad the epoch's table to a power of two. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct FillerShortage { + /// Power-of-two row count the table needed. + pub needed: usize, + /// Rows actually available (touched cells + all sourceable untouched cells). + pub got: usize, +} + +/// Pad `boundary` up to a power of two with brought-forward filler rows for +/// genuinely-untouched cells, so the L2G table needs no selector column. +/// +/// Each filler is a value-preserving no-op carried forward to `epoch` (the 1-based +/// label): `init` is the cell's current `provenance` entry `(prev_owner, value)`, +/// `fini` repeats the same `value` at `epoch` with `timestamp = 0`. This +/// self-cancels on the epoch-local Memory bus and telescopes on the GlobalMemory +/// bus (see the module docs). Every brought-forward cell's `provenance` is updated +/// to `(epoch, value, 0)` so the next epoch to touch it sees the correct owner. +/// +/// Cells are drawn from `candidate_pages` (page bases, tried in order), skipping any +/// address already in `boundary` (touched this epoch) — so the caller lists the +/// epoch's own touched pages first (they never grow the global touched-page set) and +/// genesis pages as a fallback (needed when the epoch touched no cell of its own). +/// The `init_value` read from `provenance` equals the cell's live GlobalMemory head +/// value (genesis default `0`, or the last fini), so the filler's init token matches +/// that head. +/// +/// Returns `Err(FillerShortage)` if the pool cannot fill the table — i.e. the +/// `#total live cells ≥ next_pow2(#touched per epoch)` assumption is violated for +/// this epoch. The trace is left partially filled; the caller must abort. +pub fn append_bring_forward_fillers( + boundary: &mut Vec, + provenance: &mut Provenance, + candidate_pages: &[u64], + epoch: u64, +) -> Result<(), FillerShortage> { + let target = boundary.len().next_power_of_two().max(1); + if boundary.len() >= target { + return Ok(()); + } + // Addresses already claimed this epoch: real touched cells, plus each filler as + // it is drawn. Tracking appended fillers here (not just touched cells) keeps the + // function correct even if `candidate_pages` contains a duplicate page — a filler + // address can then never be emitted twice. + let mut occupied: HashSet = boundary.iter().map(|b| b.address).collect(); + + for &page_base in candidate_pages { + if boundary.len() == target { + break; + } + for offset in 0..DEFAULT_PAGE_SIZE as u64 { + if boundary.len() == target { + break; + } + let address = page_base + offset; + if !occupied.insert(address) { + continue; + } + let (originating_epoch, value, _ts) = provenance.get(address); + boundary.push(CellBoundary { + address, + init: InitClaim { + value, + originating_epoch, + timestamp: 0, + }, + fini: FiniClaim { + value, + epoch, + timestamp: 0, + }, + }); + provenance.set(address, (epoch, value, 0)); + } + } + + if boundary.len() != target { + return Err(FillerShortage { + needed: target, + got: boundary.len(), + }); + } + Ok(()) +} + // ========================================================================= // AIR trace columns // ========================================================================= @@ -200,7 +311,8 @@ pub fn genesis_provenance(genesis: impl IntoIterator) -> Prov /// halfword columns ([`RANGE_CHECKED_HALFWORDS`]), checked via `IsHalfword`, and /// rebuilt into its 32-bit bus value via [`word`]. The value bytes get the /// batched `AreBytes` check. `fini_epoch` is a per-table constant (not a column). -/// `MU` is the real-row selector / multiplicity. +/// There is no selector column: every row is real (touched cell or brought-forward +/// filler) and every interaction fires with multiplicity 1. pub mod cols { /// address_lo: 32-bit; matched on the Memory bus against MEMW. pub const ADDRESS_LO: usize = 0; @@ -228,10 +340,7 @@ pub mod cols { /// fini_timestamp_hi: 32-bit; matched on the Memory bus against MEMW. pub const FINI_TIMESTAMP_HI: usize = 7; - /// MU: real-row selector / LogUp multiplicity (1 on real rows, 0 on padding). - pub const MU: usize = 8; - - pub const NUM_COLUMNS: usize = 9; + pub const NUM_COLUMNS: usize = 8; /// The halfword columns (cross-epoch-only quantities), in order — every column /// that is `IsHalfword`-checked. @@ -249,9 +358,16 @@ fn epoch_halfwords(epoch: u64) -> [u64; 2] { // Trace generation // ========================================================================= -/// Build the local-to-global trace: one row per touched cell's boundary claims, -/// padded up to a power of two. Real rows set `MU = 1`; padding rows stay all-zero -/// (`MU = 0`), so they fire no interactions. +/// Build the local-to-global trace: one row per boundary claim. +/// +/// Every row is real and every interaction fires with multiplicity 1, so any trace +/// that is committed on the range-check or `GlobalMemory` bus MUST be passed a +/// power-of-two-length, fully-real `boundaries` slice (touched cells plus +/// brought-forward fillers — see [`append_bring_forward_fillers`]). If a shorter +/// slice is passed it is zero-padded to a power of two; those all-zero rows +/// self-cancel on the epoch-local `Memory` bus (identical init/fini token) but would +/// dangle on the range-check / `GlobalMemory` buses, so callers proving those buses +/// must fill first. pub fn generate_local_to_global_trace( boundaries: &[CellBoundary], ) -> TraceTable { @@ -273,8 +389,6 @@ pub fn generate_local_to_global_trace( // Cross-epoch-only quantity as IsHalfword-checked halfwords. data[base + cols::INIT_EPOCH_0] = FE::from(init_epoch[0]); data[base + cols::INIT_EPOCH_1] = FE::from(init_epoch[1]); - // Real-row selector. - data[base + cols::MU] = FE::one(); } TraceTable::new_main(data, cols::NUM_COLUMNS, 1) @@ -306,10 +420,6 @@ pub(crate) fn direct(column: usize) -> BusValue { } } -fn mu() -> Multiplicity { - Multiplicity::Column(cols::MU) -} - /// Cross-epoch memory bus interactions, two per row (one touched cell): /// - **receive** the `init` token `(address, value, originating_epoch)` left by the /// epoch that last wrote the cell; @@ -323,14 +433,16 @@ fn mu() -> Multiplicity { /// /// These tokens are matched ACROSS epochs by the final aggregation LogUp (step 4), /// so within a single epoch's table the GlobalMemory bus is deliberately -/// unbalanced (real rows have `init != fini`). Padding rows fire nothing (`MU = 0`). +/// unbalanced (rows have `init_epoch != fini_epoch`). Every row fires with +/// multiplicity 1; brought-forward filler rows telescope here just like touched +/// cells (their value is preserved, `init_epoch < fini_epoch`). pub fn bus_interactions(epoch_label: u64) -> Vec { vec![ // init: receive the token left by the originating epoch. No timestamp: the // chain is ordered by epoch, and timestamps are epoch-local (see cols). BusInteraction::receiver( BusId::GlobalMemory, - mu(), + Multiplicity::One, vec![ direct(cols::ADDRESS_LO), direct(cols::ADDRESS_HI), @@ -341,7 +453,7 @@ pub fn bus_interactions(epoch_label: u64) -> Vec { // fini: send the token for the next epoch to consume. BusInteraction::sender( BusId::GlobalMemory, - mu(), + Multiplicity::One, vec![ direct(cols::ADDRESS_LO), direct(cols::ADDRESS_HI), @@ -362,6 +474,12 @@ pub fn bus_interactions(epoch_label: u64) -> Vec { /// `[is_register, address_lo, address_hi, timestamp_lo, timestamp_hi, value]`; /// RAM only, so `is_register = 0`, and the byte value is the LO column. /// +/// Brought-forward filler rows (untouched cells, `fini_ts = 0`, +/// `init_value = fini_value`) emit an init-receive and a fini-send that are the +/// identical token, so they self-cancel here — exactly as PAGE's bookend cancels +/// for a never-accessed cell. An untouched cell has no MEMW partner, so this is the +/// only shape a filler can take without dangling a token. +/// /// Address, fini timestamp and the values appear here, so MEMW range-checks them /// for us — they need no L2G range check (see [`range_check_interactions`]). pub fn memory_bus_interactions() -> Vec { @@ -369,7 +487,7 @@ pub fn memory_bus_interactions() -> Vec { // init: receive the cell's initial token at the epoch-start seed (ts = 0). BusInteraction::receiver( BusId::Memory, - mu(), + Multiplicity::One, vec![ BusValue::constant(0), direct(cols::ADDRESS_LO), @@ -382,7 +500,7 @@ pub fn memory_bus_interactions() -> Vec { // fini: send the cell's final token at the last access timestamp. BusInteraction::sender( BusId::Memory, - mu(), + Multiplicity::One, vec![ BusValue::constant(0), direct(cols::ADDRESS_LO), @@ -396,12 +514,15 @@ pub fn memory_bus_interactions() -> Vec { } /// Range-check + ordering bus interactions for the columns nothing else -/// constrains, all with multiplicity `MU` (so padding fires none): +/// constrains, all with multiplicity 1 (every row is real — touched cell or +/// brought-forward filler — so all fire, and [`collect_bitwise_from_l2g`] must +/// supply BITWISE multiplicities for every row): /// - one `AreBytes` for the two value bytes (the `init` value is a trusted source); /// - one `IsHalfword` per cross-epoch-only halfword column; /// - one `IsB20` proving `init_epoch < fini_epoch` (the ordering constraint), via /// `fini_epoch − 1 − init_epoch` being a valid 20-bit value. With genesis epoch -/// `0` this also covers genesis cells (`0 < fini_epoch`) with no special case. +/// `0` this also covers genesis cells (`0 < fini_epoch`) with no special case. A +/// filler's `init_epoch` is its previous owner (`< fini_epoch`), so it passes too. /// /// Address and fini timestamp are NOT here — MEMW checks them on the Memory bus. /// These are committed only on the epoch-local table (`l2g_memory_air`), whose @@ -417,13 +538,13 @@ pub fn range_check_interactions(epoch_label: u64) -> Vec { let mut interactions = Vec::with_capacity(2 + cols::RANGE_CHECKED_HALFWORDS.len()); interactions.push(BusInteraction::sender( BusId::AreBytes, - mu(), + Multiplicity::One, vec![direct(cols::INIT_VALUE), direct(cols::FINI_VALUE)], )); for &column in &cols::RANGE_CHECKED_HALFWORDS { interactions.push(BusInteraction::sender( BusId::IsHalfword, - mu(), + Multiplicity::One, vec![direct(column)], )); } @@ -431,7 +552,7 @@ pub fn range_check_interactions(epoch_label: u64) -> Vec { // init_epoch = INIT_EPOCH_0 + 2^16·INIT_EPOCH_1. interactions.push(BusInteraction::sender( BusId::IsB20, - mu(), + Multiplicity::One, vec![BusValue::linear(vec![ LinearTerm::Constant(epoch_label as i64 - 1), LinearTerm::Column { @@ -449,9 +570,10 @@ pub fn range_check_interactions(epoch_label: u64) -> Vec { /// The BITWISE lookups the L2G range checks + ordering check send, so the BITWISE /// table's multiplicities balance the [`range_check_interactions`] senders. Emits, -/// per real row, one `AreBytes`, one `IsHalfword` per cross-epoch halfword, and one -/// `IsB20` for the ordering difference. Padding rows fire nothing (`MU = 0`), so -/// none are emitted for them. +/// per boundary row, one `AreBytes`, one `IsHalfword` per cross-epoch halfword, and +/// one `IsB20` for the ordering difference. `boundaries` MUST include the +/// brought-forward filler rows (they fire the range checks with multiplicity 1 too), +/// or the BITWISE table under-provisions and the epoch proof cannot balance. pub fn collect_bitwise_from_l2g(boundaries: &[CellBoundary]) -> Vec { let per_row = 2 + cols::RANGE_CHECKED_HALFWORDS.len(); let mut ops = Vec::with_capacity(boundaries.len() * per_row); @@ -642,7 +764,7 @@ mod tests { #[test] fn test_num_columns() { - assert_eq!(cols::NUM_COLUMNS, 9); + assert_eq!(cols::NUM_COLUMNS, 8); assert_eq!(cols::RANGE_CHECKED_HALFWORDS.len(), 2); } @@ -672,23 +794,70 @@ mod tests { word_value(&trace, cols::INIT_EPOCH_0, cols::INIT_EPOCH_1), FE::from(GENESIS_EPOCH) ); - // Real row carries MU = 1. - assert_eq!(at(cols::MU), FE::one()); } #[test] - fn test_padding_rows_are_zero_including_mu() { - // 3 boundaries pad up to 4 rows; the padding row is all zero, MU = 0. - let boundaries: Vec = (0..3).map(sample_boundary).collect(); - let trace = generate_local_to_global_trace(&boundaries); - assert_eq!(trace.num_rows(), 4); - for col in 0..cols::NUM_COLUMNS { - assert_eq!(*trace.main_table.get(3, col), FE::zero()); - } - // And real rows have MU = 1. - for row in 0..3 { - assert_eq!(*trace.main_table.get(row, cols::MU), FE::one()); - } + fn test_append_fillers_pads_to_power_of_two() { + // 3 touched cells on page 0; fillers pad the table to 4 rows. + let mut provenance = genesis_provenance([(10u64, 5u64), (11, 6)]); + let mut boundary = epoch_boundary( + &mut provenance, + epoch_label(0), + &[(10, 7, 3), (11, 8, 4), (12, 9, 5)], + ); + assert_eq!(boundary.len(), 3); + + append_bring_forward_fillers(&mut boundary, &mut provenance, &[0], epoch_label(0)).unwrap(); + assert_eq!(boundary.len(), 4, "padded to next power of two"); + + // The filler row is a value-preserving no-op brought forward to this epoch. + let filler = &boundary[3]; + assert_eq!(filler.init.value, filler.fini.value, "value unchanged"); + assert_eq!( + filler.fini.timestamp, 0, + "fini timestamp is zero (self-cancels)" + ); + assert_eq!(filler.fini.epoch, epoch_label(0)); + assert!( + filler.init.originating_epoch < filler.fini.epoch, + "ordering holds for fillers" + ); + // The brought-forward cell is a distinct, previously-untouched address. + assert!(![10u64, 11, 12].contains(&filler.address)); + + // And its provenance now records this epoch as the owner. + let (owner, value, _) = provenance.get(filler.address); + assert_eq!(owner, epoch_label(0)); + assert_eq!(value, filler.fini.value); + } + + #[test] + fn test_append_fillers_is_noop_when_already_power_of_two() { + // 2 touched cells is already a power of two → no fillers added. + let mut provenance = genesis_provenance([(10u64, 5u64)]); + let mut boundary = + epoch_boundary(&mut provenance, epoch_label(0), &[(10, 7, 3), (20, 9, 4)]); + assert_eq!(boundary.len(), 2); + append_bring_forward_fillers(&mut boundary, &mut provenance, &[0], epoch_label(0)).unwrap(); + assert_eq!(boundary.len(), 2, "already a power of two, unchanged"); + } + + #[test] + fn test_append_fillers_reports_shortage_when_pool_too_small() { + // A single candidate page of 3 addresses (via a synthetic tiny page) cannot + // supply enough fillers when the pool is exhausted. We simulate exhaustion by + // offering NO candidate pages while the table needs padding. + let mut provenance = genesis_provenance(std::iter::empty()); + let mut boundary = epoch_boundary( + &mut provenance, + epoch_label(0), + &[(10, 7, 3), (11, 8, 4), (12, 9, 5)], + ); + assert_eq!(boundary.len(), 3); + let err = append_bring_forward_fillers(&mut boundary, &mut provenance, &[], epoch_label(0)) + .unwrap_err(); + assert_eq!(err.needed, 4); + assert_eq!(err.got, 3); } #[test] @@ -745,7 +914,8 @@ mod tests { #[test] fn test_collect_bitwise_matches_sender_count() { // Per row: 1 AreBytes + one IsHalfword per cross-epoch halfword + 1 IsB20. - // No padding ops (padding has MU = 0 and fires nothing). + // Every row (touched cell or brought-forward filler) is real, so `boundaries` + // — which must include fillers — gets exactly `per_row` ops each. let boundaries: Vec = (0..3).map(sample_boundary).collect(); let ops = collect_bitwise_from_l2g(&boundaries); let per_row = 2 + cols::RANGE_CHECKED_HALFWORDS.len(); diff --git a/prover/src/tests/local_to_global_bus_tests.rs b/prover/src/tests/local_to_global_bus_tests.rs index 263e3d938..25568c4ee 100644 --- a/prover/src/tests/local_to_global_bus_tests.rs +++ b/prover/src/tests/local_to_global_bus_tests.rs @@ -577,9 +577,9 @@ fn test_l2g_binding_rejects_mismatch() { /// Like `prove_verify_memory` but accepts a pre-built (possibly mutated) /// l2g trace instead of deriving it from a boundary slice. /// -/// Used by tests that forge individual columns (MU, epoch halfwords) after -/// trace generation — the mutation must survive into the proof so the -/// verifier sees the forged commitment. +/// Used by tests that forge individual columns (values, timestamps, epoch +/// halfwords) after trace generation — the mutation must survive into the proof so +/// the verifier sees the forged commitment. fn prove_verify_memory_with_trace( l2g_trace: &mut TraceTable, memw_boundary: &[CellBoundary], @@ -674,135 +674,221 @@ fn prove_and_verify_global_with_traces( } // ========================================================================= -// Soundness regression tests: MU selector (Design X / Statement S) +// Soundness regression tests: brought-forward filler rows // ========================================================================= - -/// (1a) MU=0 on a real row silences its Memory-bus tokens → the bus dangles. -/// -/// Property guarded: the `MU` selector gates EVERY L2G interaction on the -/// epoch-local Memory bus. Clearing MU on a genuinely-touched cell means its -/// init-receive and fini-send never fire; the MEMW-substitute chain still -/// sends/receives for that cell, leaving both tokens unmatched → bus -/// imbalance → proof must fail. -/// -/// Modelled on `test_local_memory_bus_rejects_tamper` (same Memory-bus path) -/// extended to mutate MU rather than a value column, using the new -/// `prove_verify_memory_with_trace` helper. +// +// The L2G table has no MU selector: padding rows are real brought-forward +// (filler) rows for untouched cells. A filler is a value-preserving no-op only +// because the epoch-local Memory bus forces it to be one — an untouched cell has +// no MEMW partner, so its init-receive and fini-send must be the identical token +// (`fini_ts = 0`, `init_value = fini_value`) or the bus dangles. These tests pin +// that: an honest filler balances, and any non-no-op filler is rejected. + +/// Honest filler rows self-cancel on the epoch-local Memory bus: the MEMW +/// substitute only covers the genuinely-touched cell, and the filler's identical +/// init/fini tokens net to zero, so the bus balances. #[test] -fn test_l2g_mu_zero_on_real_row_rejects() { - // Two touched cells; row 0 is real (MU=1). We forge row 0's MU to 0. - let initial_memory = HashMap::from([(10u64, 5u64)]); - let epochs = vec![vec![(10, 7, 3), (20, 9, 4)]]; - let boundaries = epoch_boundaries(&initial_memory, &epochs); +fn test_l2g_filler_self_cancels_on_memory_bus() { + // 3 touched cells → padded to 4 rows with one brought-forward filler (row 3). + let mut provenance = local_to_global::genesis_provenance([(10u64, 5u64)]); + let mut l2g_boundary = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(0), + &[(10, 7, 3), (11, 8, 4), (12, 9, 5)], + ); + local_to_global::append_bring_forward_fillers( + &mut l2g_boundary, + &mut provenance, + &[0], + local_to_global::epoch_label(0), + ) + .unwrap(); + assert_eq!( + l2g_boundary.len(), + 4, + "padded to a power of two with one filler" + ); - // Honest round-trip must pass. + // The MEMW substitute covers only the real touched cells (rows 0..3); the filler + // (row 3) has no MEMW partner and must self-cancel on its own. assert!( - prove_verify_memory(&boundaries[0], &boundaries[0]), - "baseline must verify before forgery" + prove_verify_memory(&l2g_boundary, &l2g_boundary[..3]), + "an honest brought-forward filler must self-cancel on the Memory bus" ); +} - // Forge: clear MU on the first real row. - let mut forged_trace = generate_local_to_global_trace(&boundaries[0]); - forged_trace +/// A filler with `init_value != fini_value` breaks self-cancellation: its +/// init-receive and fini-send become different Memory-bus tokens, and an untouched +/// cell has no MEMW partner for either → the bus dangles → reject. +#[test] +fn test_l2g_filler_value_mismatch_rejects() { + // 3 touched cells → one filler at row 3. + let mut provenance = local_to_global::genesis_provenance([(10u64, 5u64)]); + let mut l2g_boundary = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(0), + &[(10, 7, 3), (11, 8, 4), (12, 9, 5)], + ); + local_to_global::append_bring_forward_fillers( + &mut l2g_boundary, + &mut provenance, + &[0], + local_to_global::epoch_label(0), + ) + .unwrap(); + + // Forge the filler row (row 3) to change its value between init and fini. + let mut forged = generate_local_to_global_trace(&l2g_boundary); + forged .main_table - .set(0, local_to_global::cols::MU, FE::zero()); + .set(3, local_to_global::cols::FINI_VALUE, FE::from(0x33u64)); - // The Memory bus is now unbalanced: L2G's init-receive and fini-send for - // cell 10 are silenced (MU=0), but the MEMW-substitute sends cell 10's - // init and expects its fini — neither token finds its counterpart. assert!( - !prove_verify_memory_with_trace(&mut forged_trace, &boundaries[0]), - "MU=0 on a real row must cause the Memory bus to reject" + !prove_verify_memory_with_trace(&mut forged, &l2g_boundary[..3]), + "a filler with init_value != fini_value must dangle on the Memory bus" ); } -/// (1b) MU=1 on a padding row injects phantom tokens → the GlobalMemory bus -/// cannot balance. -/// -/// Property guarded: same Design-X property, opposite direction. A padding row -/// with MU=1 fires a spurious init-receive and fini-send on the GlobalMemory -/// bus. The two phantom tokens carry different values — the init token carries -/// originating_epoch=0 (zero-filled padding) while the fini token carries -/// `fini_epoch=epoch_label` (the per-table constant, always ≥ 1). Because the -/// epoch field differs, the phantom receive and send do NOT self-cancel; neither -/// the genesis anchor nor the program-end anchor has a matching row for address 0 -/// → both tokens dangle → bus imbalance → proof fails. -/// -/// Note: the epoch-local Memory bus would NOT catch this because the phantom -/// row's init and fini tokens are identical (all columns zero) and self-cancel -/// in the LogUp. The GlobalMemory bus carries the epoch constant in the fini -/// token but not the init token, breaking the self-cancellation. -/// -/// Three real boundaries pad to four rows; row 3 is the padding row (all-zero). -/// Uses `prove_and_verify_global_with_traces` (same path as test 1c and test 3). +/// A filler with `fini_timestamp != 0` breaks self-cancellation: its fini-send +/// token carries a nonzero timestamp while its init-receive is at ts=0, so the two +/// differ and neither finds a MEMW partner → reject. #[test] -fn test_l2g_mu_one_on_padding_row_rejects_global_bus() { - // 3 real rows → 4-row trace (padding row at index 3). - let initial_memory = HashMap::new(); - let epochs = vec![vec![(10, 7, 3), (20, 9, 4), (30, 1, 5)]]; - let boundaries = epoch_boundaries(&initial_memory, &epochs); - assert_eq!(boundaries[0].len(), 3, "expect 3 real rows"); +fn test_l2g_filler_nonzero_fini_timestamp_rejects() { + // 3 touched cells → one filler at row 3. + let mut provenance = local_to_global::genesis_provenance([(10u64, 5u64)]); + let mut l2g_boundary = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(0), + &[(10, 7, 3), (11, 8, 4), (12, 9, 5)], + ); + local_to_global::append_bring_forward_fillers( + &mut l2g_boundary, + &mut provenance, + &[0], + local_to_global::epoch_label(0), + ) + .unwrap(); + + // Forge the filler row (row 3) to carry a nonzero fini timestamp. + let mut forged = generate_local_to_global_trace(&l2g_boundary); + forged + .main_table + .set(3, local_to_global::cols::FINI_TIMESTAMP_LO, FE::from(7u64)); - // Honest baseline on the GlobalMemory bus. assert!( - prove_and_verify(&boundaries), - "baseline must verify before forgery" + !prove_verify_memory_with_trace(&mut forged, &l2g_boundary[..3]), + "a filler with fini_timestamp != 0 must dangle on the Memory bus" ); +} - // Forge: set MU=1 on the padding row (row 3, all-zero columns). - let mut forged_trace = generate_local_to_global_trace(&boundaries[0]); - let num_rows = forged_trace.num_rows(); - assert_eq!(num_rows, 4, "trace must be padded to 4 rows"); - forged_trace - .main_table - .set(3, local_to_global::cols::MU, FE::one()); - let mut l2g_traces = vec![forged_trace]; +/// Honest brought-forward fillers telescope on the cross-epoch GlobalMemory bus: +/// an epoch with a non-power-of-two touched count is padded with fillers and still +/// balances end-to-end (genesis → epoch fini/filler → program-end). +#[test] +fn test_global_memory_bus_balances_with_fillers() { + let mut provenance = local_to_global::genesis_provenance(std::iter::empty()); + let mut epoch0 = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(0), + &[(10, 7, 3), (20, 9, 4), (30, 1, 5)], + ); + assert_eq!(epoch0.len(), 3, "3 touched cells (not a power of two)"); + local_to_global::append_bring_forward_fillers( + &mut epoch0, + &mut provenance, + &[0], + local_to_global::epoch_label(0), + ) + .unwrap(); + assert_eq!(epoch0.len(), 4, "padded to a power of two with one filler"); - // The phantom row fires on the GlobalMemory bus: - // - init-receive: epoch=0 (zero-filled), addr=0 — no genesis anchor row sends this. - // - fini-send: epoch=epoch_label=1, addr=0 — no program-end anchor receives this. - // The two tokens differ in the epoch field, so they do not self-cancel. + let boundaries = vec![epoch0]; assert!( - !prove_and_verify_global_with_traces(&boundaries, &mut l2g_traces), - "MU=1 on a padding row must cause the GlobalMemory bus to reject" + prove_and_verify(&boundaries), + "brought-forward fillers must telescope on the GlobalMemory bus" ); } -/// (1c) MU=2 (non-boolean) on a real row unbalances the GlobalMemory bus. -/// -/// Property guarded: MU is the LogUp multiplicity for ALL bus interactions. -/// With MU=2 the fini-sender fires twice but the program-end anchor receives -/// only once, and the init-receiver fires twice but the genesis anchor sends -/// only once → both sides of the GlobalMemory bus are off by 1 → proof fails. -/// -/// Uses `prove_and_verify_global_with_traces` (forked from `prove_global`) -/// to inject the pre-mutated trace. Modelled on -/// `test_prove_elfs_ecsm_forged_ecdas_mu_rejected` (prove_elfs_tests.rs:1230) -/// for the "set MU to 2, assert reject" pattern. +/// Multiple fillers in one epoch (5 touched → padded to 8, i.e. 3 fillers) telescope +/// on the GlobalMemory bus. The single-filler tests never exercise more than one +/// filler row nor a wider power-of-two gap. #[test] -fn test_l2g_mu_nonboolean_rejects_global_bus() { - let initial_memory = HashMap::from([(10u64, 5u64)]); - let epochs = vec![vec![(10, 7, 3)]]; - let boundaries = epoch_boundaries(&initial_memory, &epochs); +fn test_global_memory_bus_balances_with_multiple_fillers() { + let mut provenance = local_to_global::genesis_provenance(std::iter::empty()); + let mut epoch0 = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(0), + &[(10, 1, 3), (20, 2, 4), (30, 3, 5), (40, 4, 6), (50, 5, 7)], + ); + assert_eq!(epoch0.len(), 5, "5 touched cells (not a power of two)"); + local_to_global::append_bring_forward_fillers( + &mut epoch0, + &mut provenance, + &[0], + local_to_global::epoch_label(0), + ) + .unwrap(); + assert_eq!( + epoch0.len(), + 8, + "padded to a power of two with three fillers" + ); - // Honest baseline on the GlobalMemory bus. + let boundaries = vec![epoch0]; assert!( prove_and_verify(&boundaries), - "baseline must verify before forgery" + "multiple brought-forward fillers must telescope on the GlobalMemory bus" ); +} - // Forge: set MU=2 on row 0 of epoch 0's L2G trace. - let mut l2g_trace = generate_local_to_global_trace(&boundaries[0]); - l2g_trace - .main_table - .set(0, local_to_global::cols::MU, FE::from(2u64)); - let mut l2g_traces = vec![l2g_trace]; +/// A cell brought forward as a filler in one epoch and then genuinely TOUCHED in a +/// later epoch must telescope correctly: the later epoch's init consumes the +/// filler's produced token (init_epoch = the filler epoch), and the value flows +/// through. Locks in the filler→real-touch chaining the security/spec reviews +/// verified only by inspection. +#[test] +fn test_filler_then_real_touch_telescopes() { + let mut provenance = local_to_global::genesis_provenance(std::iter::empty()); + + // Epoch 0 touches 3 cells (10, 11, 12) → padded to 4 with one filler. With + // candidate page 0 and those cells occupied, the filler is address 0. + let mut epoch0 = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(0), + &[(10, 7, 3), (11, 8, 4), (12, 9, 5)], + ); + local_to_global::append_bring_forward_fillers( + &mut epoch0, + &mut provenance, + &[0], + local_to_global::epoch_label(0), + ) + .unwrap(); + assert!( + epoch0.iter().any(|b| b.address == 0), + "the filler brought forward cell 0" + ); + + // Epoch 1 genuinely touches cell 0 (the brought-forward cell), writing 42. Its + // init must link to the filler's fini (init_epoch = 1, the filler's epoch). + let epoch1 = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(1), + &[(0, 42, 10)], + ); + assert_eq!( + epoch1[0].init.originating_epoch, + local_to_global::epoch_label(0) + ); + assert_eq!( + epoch1[0].init.value, 0, + "consumes the filler's preserved value" + ); - // Multiplicity 2 on both the init-receiver and fini-sender; genesis and - // program-end anchors only send/receive multiplicity 1 → bus imbalance. + let boundaries = vec![epoch0, epoch1]; assert!( - !prove_and_verify_global_with_traces(&boundaries, &mut l2g_traces), - "MU=2 (non-boolean) must cause the GlobalMemory bus to reject" + prove_and_verify(&boundaries), + "a filler cell later touched for real must telescope (genesis → filler → touch → final)" ); } @@ -934,72 +1020,90 @@ fn test_l2g_init_epoch_ordering_live_is_b20_rejects() { } // ========================================================================= -// Soundness regression tests: Design-Y orphan attack +// Soundness regression tests: chain truncation / forged fillers // ========================================================================= -/// (3) Design-Y orphan attack: MU=0 on a later epoch's L2G row truncates the -/// cross-epoch chain → the GlobalMemory bus rejects. -/// -/// Property guarded: setting MU=0 on an L2G row for epoch i+1 silences that -/// epoch's fini-send on the GlobalMemory bus. If the global finalisation -/// (program-end anchor) still expects the last fini to come from epoch i+1, -/// the fini token is never sent → program-end anchor receives a token that -/// nobody sent → bus imbalance. -/// -/// Concretely: cell 10 is touched in both epoch 0 (label 1) and epoch 1 -/// (label 2). The forged trace sets MU=0 on epoch 1's L2G row for cell 10. -/// Epoch 1's fini-send is silenced; the program-end anchor still tries to -/// receive `(10, 8, 2, 10)` (the last honest fini) — but it was never sent. -/// Separately, epoch 1's init-receive is also silenced, leaving epoch 0's -/// fini token (which epoch 1 was supposed to consume) dangling. Both -/// produce bus imbalances. +/// Design-Y (orphan a touched epoch by silencing its L2G row with `MU=0`) is +/// STRUCTURALLY IMPOSSIBLE now: there is no MU column, so no row can be silenced — +/// every L2G row fires with multiplicity 1. Instead, the closest remaining lever is +/// forging a *filler* row's committed value so it does not telescope. This test +/// guards that such a forgery dangles on the cross-epoch GlobalMemory bus. /// -/// Modelled on `test_global_memory_bus_rejects_tampered_boundary` (which -/// tampers a boundary value) and uses the new -/// `prove_and_verify_global_with_traces` helper to inject the forged epoch-1 -/// trace. `prove_and_verify` (which generates its own traces) is used for the -/// baseline check; the forged proof is built via the helper. +/// Cell 10 is touched in epochs 0 and 1; epoch 1 is padded with a brought-forward +/// filler for an untouched cell. Forging that filler's fini value makes the token it +/// produces (consumed by the program-end anchor) disagree with the token it consumed +/// (its init), so the GlobalMemory bus cannot balance. Uses +/// `prove_and_verify_global_with_traces` to inject the pre-forged epoch-1 trace. #[test] -fn test_l2g_design_y_orphan_mu_zero_rejects() { - // Cell 10 touched in epoch 0 (label 1, fini value=7, ts=3) and epoch 1 - // (label 2, fini value=8, ts=10). Cell 20 touched in epoch 0 only. - let initial_memory = HashMap::from([(10u64, 5u64)]); - let epochs = vec![vec![(10, 7, 3), (20, 9, 4)], vec![(10, 8, 10)]]; - let boundaries = epoch_boundaries(&initial_memory, &epochs); +fn test_l2g_forged_filler_value_rejects_global_bus() { + // Epoch 0 touches cells 10 and 20 (2 cells, already a power of two). Epoch 1 + // touches 3 cells, so it is padded with one brought-forward filler (row 3). + let mut provenance = local_to_global::genesis_provenance([(10u64, 5u64)]); + let epoch0 = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(0), + &[(10, 7, 3), (20, 9, 4)], + ); + let mut epoch1 = local_to_global::epoch_boundary( + &mut provenance, + local_to_global::epoch_label(1), + &[(10, 8, 10), (20, 5, 11), (30, 2, 12)], + ); + local_to_global::append_bring_forward_fillers( + &mut epoch1, + &mut provenance, + &[0], + local_to_global::epoch_label(1), + ) + .unwrap(); + assert_eq!( + epoch1.len(), + 4, + "epoch 1 padded to a power of two with one filler" + ); + let boundaries = vec![epoch0, epoch1]; - // Honest baseline on the GlobalMemory bus. + // Honest baseline balances. assert!( prove_and_verify(&boundaries), "baseline must verify before forgery" ); - // Build honest traces for both epochs. + // Forge the filler row (epoch 1, row 3) to change its fini value. Its + // GlobalMemory fini-send now produces a token no anchor / later init consumes, + // while the value it consumed still expects the honest value → bus imbalance. let epoch0_trace = generate_local_to_global_trace(&boundaries[0]); let mut epoch1_trace = generate_local_to_global_trace(&boundaries[1]); - - // Epoch 1 has exactly one real row (cell 10). Forge MU=0 on that row. - // This orphans cell 10's cross-epoch chain at epoch 1: the init-receive - // (consuming epoch 0's fini token for cell 10) and the fini-send (which - // the program-end anchor expects to receive) both fire with multiplicity 0. - assert_eq!( - boundaries[1].len(), - 1, - "epoch 1 must have exactly one real row" - ); epoch1_trace .main_table - .set(0, local_to_global::cols::MU, FE::zero()); - + .set(3, local_to_global::cols::FINI_VALUE, FE::from(0x33u64)); let mut l2g_traces = vec![epoch0_trace, epoch1_trace]; - // The GlobalMemory bus cannot balance: - // - Epoch 0's fini token for cell 10 was sent (epoch 0's MU=1) but not - // consumed by epoch 1 (epoch 1's init-receive is silenced → MU=0). - // - The program-end anchor tries to receive epoch 1's fini for cell 10 - // (the last honest value), but that fini-send is also silenced. assert!( !prove_and_verify_global_with_traces(&boundaries, &mut l2g_traces), - "MU=0 on a later epoch's L2G row (Design-Y orphan) must cause the GlobalMemory bus to reject" + "a forged filler value must break the GlobalMemory telescoping chain" + ); +} + +/// A touched cell cannot be dropped from the L2G table without dangling its +/// MEMW-chain tokens: the epoch-local Memory bus rejects. This is the property that +/// replaces the old `MU`-gating — participation is no longer selectable, so omitting +/// a row (the only way to "drop" one) leaves the MEMW substitute's init-send and +/// fini-receive for that cell unmatched. +#[test] +fn test_l2g_dropped_touched_row_rejects_memory_bus() { + let initial_memory = HashMap::from([(10u64, 5u64)]); + let epochs = vec![vec![(10, 7, 3)]]; + let boundaries = epoch_boundaries(&initial_memory, &epochs); + + // Honest baseline: L2G bookend matches the MEMW substitute. + assert!(prove_verify_memory(&boundaries[0], &boundaries[0])); + + // Drop the L2G row for cell 10 (empty L2G boundary) while the MEMW substitute + // still accesses cell 10 → its tokens have no L2G partner → reject. + assert!( + !prove_verify_memory(&[], &boundaries[0]), + "dropping a touched cell's L2G row must dangle its MEMW tokens" ); } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 10013b5ed..f1ccbb749 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -3249,7 +3249,57 @@ fn test_continuation_pipeline_end_to_end() { register_inits.push(register_init_i); all_touched.push(touched_i); } - let boundaries = local_to_global::epoch_boundaries(&initial_memory, &all_touched); + // Build each epoch's boundary and pad it to a power of two with brought-forward + // filler rows for untouched cells — exactly as `prove_continuation` does (the L2G + // table has no selector column, so padding must be real rows that self-cancel on + // the Memory bus and telescope on the GlobalMemory bus). Sourcing mirrors the + // prover: this epoch's own touched pages first, then genesis pages as a fallback. + let genesis_pages: std::collections::BTreeSet = image0 + .keys() + .map(|&a| crate::tables::page::page_base_for_address(a)) + .collect(); + let mut provenance = + local_to_global::genesis_provenance(initial_memory.iter().map(|(&a, &v)| (a, v))); + let mut boundaries: Vec> = + Vec::with_capacity(all_touched.len()); + for (i, touched) in all_touched.iter().enumerate() { + let label = local_to_global::epoch_label(i as u64); + let mut boundary = local_to_global::epoch_boundary(&mut provenance, label, touched); + let mut candidate_pages: Vec = Vec::new(); + let mut seen = std::collections::BTreeSet::new(); + for cell in &boundary { + let base = crate::tables::page::page_base_for_address(cell.address); + if seen.insert(base) { + candidate_pages.push(base); + } + } + for &base in &genesis_pages { + if seen.insert(base) { + candidate_pages.push(base); + } + } + local_to_global::append_bring_forward_fillers( + &mut boundary, + &mut provenance, + &candidate_pages, + label, + ) + .expect("filler shortage building the pipeline test boundaries"); + boundaries.push(boundary); + } + + // Guard against silent degradation: this test exists to exercise brought-forward + // filler padding, so at least one epoch must have had fillers appended (its padded + // boundary is longer than its touched-cell count). If the ELF ever touched a + // power-of-two count in every epoch, no fillers would be added and the test would + // pass while exercising none. + assert!( + boundaries + .iter() + .zip(&all_touched) + .any(|(b, touched)| b.len() > touched.len()), + "no epoch required filler rows — the filler path is not being exercised" + ); let proof_options = ProofOptions::default_test_options();