perf(executor): back the private-input region with a paged Box map#852
perf(executor): back the private-input region with a paged Box map#852Oppen wants to merge 3 commits into
Conversation
MAX_PRIVATE_INPUT_SIZE is 512 MiB (#843), but Memory::cells stores every guest word (program/stack/heap AND private input) in one HashMap<u64, [u8;4]>. A max-size private input costs ~134M entries there -- measured peak RSS ~9.7 GB for a single store_private_inputs call, and store_private_inputs itself takes ~2.2s. Route the private-input address range to a separate HashMap<u64, Box<[u8; 256 KiB]>>, one boxed page allocated lazily per touched page. Only an 8-byte pointer lives in the hashmap's table slot, so growing/rehashing the table only ever moves pointers, never page payloads -- avoiding the resize-memcpy cost a same-size inline-array page value would pay. Measured: peak RSS ~1.08 GB (vs ~9.7 GB), store_private_inputs ~28ms (vs ~2.2s), for the same 512 MiB input. Guest-visible behavior is unchanged; all load/store paths route by address only.
|
/ai-review |
Codex Code Review
|
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
| let page_idx = private_page_index(address); | ||
| let offset = private_page_offset(address); | ||
| let page = self | ||
| .private_input_pages |
There was a problem hiding this comment.
store_byte is the only private-write path that uses infallible allocation (or_insert_with(|| Box::new([0u8; PRIVATE_INPUT_PAGE_SIZE]))), while store_word/store_doubleword/store_half/set_private_bytes_aligned all go through the fallible get_or_insert_private_page → try_allocate_private_page. Two consequences:
- Bypasses the OOM-safety design.
try_allocate_private_page's doc says a guest touching a page nearMAX_PRIVATE_INPUT_SIZEshould "fail cleanly withMemoryError::AllocationFailedinstead of aborting the host process." A guest-triggeredSBinto the private region (and unalignedstore_word/half/doubleword, which dispatch tostore_byte) still aborts the host on allocation failure. Box::new([0u8; 256 KiB])constructs the array on the stack before boxing in unoptimized builds — a 256 KiB stack allocation footgun thattry_allocate_private_page'sVec-based path deliberately avoids.
store_byte can't return a Result, but it can still allocate through the same heap path (e.g. a helper that builds the page via Vec and unwraps / falls back), rather than a stack-array + infallible-abort. At minimum, avoid the stack-array construction here.
| /// themselves. Chosen to match the prover's `DEFAULT_PAGE_SIZE` concept | ||
| /// (`prover/src/tables/page.rs`); redeclared locally since the executor must | ||
| /// not depend on the prover crate. | ||
| const PRIVATE_INPUT_PAGE_SIZE: usize = 256 * 1024; |
There was a problem hiding this comment.
Every aligned fast-path here relies on an unstated invariant: that PRIVATE_INPUT_START_INDEX and MAX_PRIVATE_INPUT_SIZE are both multiples of PRIVATE_INPUT_PAGE_SIZE (the comments in load_word/load_doubleword say "either fully inside one page or fully outside"). They currently are (0xFF000000 / 256 KiB = 16320, 512 MiB / 256 KiB = 2048), so there's no bug today — but nothing guards it. If someone later moves PRIVATE_INPUT_START_INDEX to a non-page-aligned address, a 4-aligned word could straddle a page boundary and the p[offset..offset + 4] slices would panic with an out-of-bounds range (or read wrong bytes), silently.
Consider pinning the invariant at compile time next to the constant:
const _: () = assert!(PRIVATE_INPUT_START_INDEX % PRIVATE_INPUT_PAGE_SIZE as u64 == 0);
const _: () = assert!(MAX_PRIVATE_INPUT_SIZE % PRIVATE_INPUT_PAGE_SIZE as u64 == 0);
| let mut buf: Vec<u8> = Vec::new(); | ||
| buf.try_reserve_exact(PRIVATE_INPUT_PAGE_SIZE) | ||
| .map_err(|_| MemoryError::AllocationFailed)?; | ||
| buf.resize(PRIVATE_INPUT_PAGE_SIZE, 0); |
There was a problem hiding this comment.
Semantic note on iter_bytes: for the private region this now yields every byte of each allocated page (262 144 addresses per touched page, including never-written words as zeros), whereas the old per-word cells design yielded only the 4-byte words that were actually written. So a single private write now surfaces a full 256 KiB run of (addr, 0) entries in the snapshot.
Reads still return 0 for those addresses either way, and iter_bytes appears to be used only in tests/benches (not the production proving path, which builds from touched_memory_cells), so this is low-impact — but it does change epoch-snapshot content/size and is worth calling out given the unexplained ~1.1% continuation divergence mentioned in the description. Worth double-checking the affected tests actually tolerate the extra zero entries rather than passing by coincidence.
|
Benchmark Results for unmodified programs 🚀
|
|
Review summary Reviewed the paged private-input backing store in Findings (all Medium/Low — no blockers)
Note: the working directory is on The unresolved ~1.1% continuation-proving divergence is acknowledged as a documented follow-up that reproduces on all prototyped backends, so it is not attributable to this diff specifically. |
AI ReviewPR #852 · 1 changed files Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-001: store_byte uses infallible allocation, inconsistent with other private-input write paths
Claim
Evidence The PR's design comment at lines 85-87 explicitly justifies Suggested fix Replace AI-005: set_private_bytes_aligned lacks region bounds check
Claim set_private_bytes_aligned does not verify that the write stays within MAX_PRIVATE_INPUT_SIZE, allowing allocation of pages beyond the 512 MiB region Evidence Lines 477-489: the loop only checks Suggested fix Either reject inputs that would exceed AI-011: Dead error path in try_allocate_private_page: try_into cannot fail here
Claim
Evidence Lines 88-96: the only way the inner Suggested fix Drop the Reviewer Lanes
Verification Lanes
Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report. Discarded candidates (3) — rejected by the verifier
Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts. |
…ate input store_byte used infallible allocation while every other private-input write path was fallible, and store_private_inputs could write 4 bytes past MAX_PRIVATE_INPUT_SIZE (the length prefix wasn't accounted for in the accepted payload size), corrupting the tail of a maximal-size input on readback. Rather than patch the private-input-only paged HashMap, drop the special case entirely: back the whole address space with one HashMap<page_idx, Box<page>>, so private input is just memory written at a fixed address like anything else. This removes the page/region alignment invariant the split design depended on, and every write (private or not) now goes through the same fallible page allocator.
1 participant
Summary
MAX_PRIVATE_INPUT_SIZEis 512 MiB (#843), butMemory::cellsstores every guest word — program/stack/heap and private input — in oneHashMap<u64, [u8;4]>. A max-size private input costs ~134M entries there.Measured on this branch vs. the current per-word design, for a single
store_private_inputscall at exactlyMAX_PRIVATE_INPUT_SIZE:store_private_inputstime: ~2.2s → ~28msThis PR routes the private-input address range (
[PRIVATE_INPUT_START_INDEX, PRIVATE_INPUT_START_INDEX + MAX_PRIVATE_INPUT_SIZE)) to a separateHashMap<u64, Box<[u8; 256 KiB]>>, one boxed page allocated lazily per touched page — everything else (program/stack/heap) still goes through the originalcellsmap, unchanged. Only an 8-byte pointer lives in the page map's table slot, so growing/rehashing that table only ever moves pointers, never 256 KiB page payloads (this was compared against a sibling design storing the page array inline, which pays a real resize-memcpy cost as the table grows — the boxed version avoids that).How this was chosen
Five backing designs were prototyped and benchmarked (dense
Vec, dense-eager, pagedVec, paged inline-array, pagedBox) against both a synthetic max-size input and a real 4-tx ethrex block proven via the continuation system. This one had the best combination of RAM/time and no resize-cost risk. Two independent adversarial reviews (of this diff and the dense-Vecsibling) found no semantic divergence from the original per-word design for any load/store access pattern, at any width, including boundary/alignment edge cases — confirmed further by a raw-execution cycle-count test showing 0.0017% difference against the unmodified backend on the same real ethrex-block input.A separate ~1.1% divergence observed in full continuation-proving cycle/proof-size (not raw execution) between the old and new backends is still not root-caused — it reproduces on every prototyped backend (including a plain dense
Vecwith none of this diff's paging), is unaffected by disabling the STARK grinding parallelism, and isn't explained by anything in the accounting path (which is built from the ELF + raw private-input slice + execution logs, never fromMemory's internals). It's filed as a follow-up investigation, not a blocker for this change.Test plan
cargo build --workspacecargo test -p executor(all pass)cargo test -p lambda-vm-prover --lib(515 passed, 0 failed, 20 ignored)