perf: build PAGE trace from dense memory store - #858
Conversation
|
/bench 5 |
|
/bench-gpu |
GPU Benchmark (ABBA) —
|
Benchmark — ethrex 20 transfers (median of 3)Table parallelism: auto (cores / 3)
Commit: 44bcbf2 · Baseline: cached · Runner: self-hosted bench |
|
/bench 10 |
086761e to
82a3d7a
Compare
There was a problem hiding this comment.
⚠️ AI-generated review. Produced by an automated agent and posted from this account — not written by hand. Findings below are leads to verify, not confirmed conclusions.
This PR makes the dense store the single PAGE path, with page_final as the sole source of FINI/TIMESTAMP and the ARE_BYTES multiplicities. The PagedMem invariants behind the binary search hold, both call sites derive bases from page_bases(), and nothing moves on the verifier/transcript/CUDA side. Two items before merge, plus nits.
prover/src/tables/page.rs:297 — page_final collapses every ts == 0 cell to (init, 0), equivalent to the sparse path only under the unenforced invariant that every ts == 0 cell in memory_state.cells holds exactly the init byte for its offset. It holds today (MemoryState::from_image seeds (byte, 0) from the same initial_image that build_init_page_data/PageConfig read, trace_builder.rs:104-110/4244; unset offsets read back as fill (0,0) against a zero init; every runtime write carries op.timestamp = i*4 + 4 >= 4, trace_builder.rs:347), but nothing checks it and the new test assumes it rather than probing it. Breakage is silent: per bus_interactions (page.rs:517-597) PAGE receives memory[0, addr, 0, init] and sends memory[0, addr, ts, fini], so for an untouched cell with init I, stored V, I != V, the old path emitted INIT=I/FINI=V/TS=0 — two non-cancelling tuples, a Memory-bus imbalance that failed the proof — while the dense path emits INIT=I/FINI=I/TS=0, which self-cancels. The trace stays provable while PAGE's final memory disagrees with executor state and with the image carried across a continuation chain. Not a soundness break (FINI is committed main trace, bus-constrained only), but the only signal that caught divergence is gone; debug_assert!(timestamp == 0 => value == init) inside page_final restores it and is inherited by collect_bitwise_from_page.
prover/src/tables/page.rs:237 — generate_page_trace, FinalStateMap (page.rs:101) and FinalByteState (page.rs:93) lose their last non-test callers here; only prover/src/tests/page_tests.rs still references them, yet all three stay pub in the public module tree (tables/mod.rs:47) and generate_page_trace's doc still reads "Generates a PAGE trace table for a single page." with no hint it is retired (the dense fn, the differential test and both trace_builder comments do say which path is live). Mark it as the reference oracle for generate_page_trace_dense_matches_sparse, or better gate it and the two types behind #[cfg(test)] — feasible since lib.rs:27-28 declares #[cfg(test)] pub mod tests;. Retargeting page_tests.rs:33/65/96 at the dense generator is polish, not a coverage gap.
Nits:
- prover/src/tests/page_tests.rs:262 — the
#[cfg(not(feature = "disk-spill"))]gate rests on a false rationale and can be dropped: table.rs:268-269 provides#[cfg(feature = "disk-spill")] impl<F: IsField> PartialEq for Table<F>(element-wise via.get(), unbounded inF), while thenot(disk-spill)derive adds an implicitF: PartialEqthatGoldilocksFieldsatisfies. The second sentence is correct and should stay:TraceTable's derive (trace.rs:22) addsE: PartialEq, whichDegree3GoldilocksExtensionField(extensions_goldilocks.rs:281) lacks. No CI gain — the disk-spill job is name-filtered (pr_main.yaml:233). - prover/src/tables/trace_builder.rs:2131 — comment says "
page_finalcomputes(init, fini)", butpage_final(init, value, timestamp, exclude_touched) -> (u8, u64)takesinitas input and returns(fini_value, fini_ts), with call site 2144 dropping the ts half andinitcomputed at 2141; reword to say it derives(fini, ts)exactly asgenerate_page_trace_from_densedoes, which is the real justification for ARE_BYTES matching PAGE's FINI column. - prover/src/tables/page.rs:350 — the
Nonearm (final_page.map_or((0u8, 0u64), |p| p[offset])) is unreachable: both callers (trace_builder.rs:2637, page_tests.rs:292) passSome, since bases come frompage_bases(), exactly whatpage_data()searches. One comparison in the existing loop againstgenerate_page_trace(&config, &FinalStateMap::new())covers the(0u8, 0u64)constant and passes as written; note the fallback is duplicated at page.rs:350 and trace_builder.rs:2143. - prover/src/paged_mem.rs:110 —
page_dataalone does not normalize its address (get/setgo throughSelf::split(addr); this binary-searches the rawbase), so an unaligned argument can never match and returnsErr(_) => None, indistinguishable from "no set cell in this page". Unreachable today, but the unguarded consumer iscollect_bitwise_from_page, where a spuriousNoneskews ARE_BYTES multiplicities and unbalances the bus — adddebug_assert!(base.is_multiple_of(DEFAULT_PAGE_SIZE as u64))rather than normalizing viaSelf::split(base).0, which would hide the misuse.
…vm into perf-page-dense-gen
Resolved against main's trace-builder rework — #858 (PAGE trace from a dense memory store) and #863 (GPU continuation proving). This branch's contribution to that file is confined to collect_bitwise_from_keccak: it drops the theta and rho HWSL pushes and the doc comments naming them, which does not overlap either change, so main's version stands everywhere else in the file.
What
Generate the PAGE trace tables by reading each cell's final
(value, timestamp)straight from the dense per-page memory store, instead of first building a sparseFinalStateMapand doing one (mostly-miss) lookup per page offset.Why
Those per-offset sparse-map lookups were the dominant cost of PAGE generation.
Reading the dense page slice directly is one indexed read per offset, no hashing.
Impact (ethrex 5-tx block, RTX 5090)
Produces the exact same PAGE trace —
prove+verifypass.Changes (3 files)
prover/src/paged_mem.rs: addPagedMem::page_data()(dense per-page slice).prover/src/tables/page.rs: addgenerate_page_trace_from_dense().prover/src/tables/trace_builder.rs:generate_page_tablesuses the dense path.