Feat/hint arena - #942
Conversation
The non-constraining hint ecall (and its prover HINT table) is replaced by untrusted 32-byte hint slots appended to the private-input region: [u32 len][data][pad8][u32 hint_count][u32 pad][32-byte slots] Guests consume slots positionally (syscalls: hint_count/hint_slot/ next_hint/request_hint) and must still verify each hint in-circuit, falling back to software on failure or arena exhaustion. A lying host can only force fallbacks, never change the result. When hints are not known beforehand, request_hint appends (hint_id, input) to a request log above the private-input window; the host reads it back (Memory::hint_requests / ExecutionResult::hint_requests), answers with compute_hint, and re-runs with a complete arena (executor::collect_hints — the two-pass flow). - executor: encode_private_input_region (single source of truth for the wire format), hints threaded through Executor::new, ecall dispatch and HINT_* error variants removed - prover: HINT table and its trace-builder/CPU plumbing removed; hints threaded through prove_*/count_*/Traces::from_* - ethrex-crypto: field_inv/scalar_inv/decompress_r read from the arena (verify + software fallback kept) - cli: --hints on execute/prove/count-elements, execute --record-hints for the recording pass - guests: hint_arena (slot API) and ecrecover_hints (N recoveries); two-pass measurement drivers on the executor and prover (continuation) sides Measured on 30 ecrecovers: 6.41M guest cycles with software fallback vs 866k with arena hints (7.40x); continuation proof of the hinted run verifies end-to-end (14 epochs @ 2^16).
|
/bench |
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 47352 MB | 47332 MB | -20 MB (+-0.0%) ⚪ |
| Prove time | 137.700s | 110.240s | -27.460s (-19.9%) 🟢 |
🎉 Improvement on the real block — prove time down 19.9%.
Prove-time spread 1.2% (110.240s / 109.242s / 110.537s)
Commit: 1a61b19 · Baseline: cached · Runner: self-hosted bench
|
/bench |
|
Benchmark Results for modified programs 🚀
|
The restack brought in the ethrex bump, which moved lambda-vm-ethrex-crypto to ethrex 4f658c2b while the guest kept its direct dep at 156cb8d6 — two distinct Crypto traits, so the guest no longer compiled. Unify on the bumped rev (lockfile collapses to a single ethrex-crypto entry).
|
Benchmark Results for unmodified programs 🚀
|
The removed hint ecall accelerated hint-consuming guests on EVERY prove, no caller opt-in; the arena made acceleration opt-in, so hint-less flows (plain cli prove, bench_abba.sh) silently proved the software-fallback trace — measured on ethrex_10_transfers: 3.35M cycles without hints vs 1.31M hinted (the ecall baseline was 1.70M). resolve_hints restores the always-on ergonomics: when the caller passes an empty arena, prove_with_options_and_inputs / prove_continuation / count_elements first run the recording pass (collect_hints) and prove the hinted trace. Both runs commit the same output — the arena only changes cost — so the statement being proved is unchanged. Guests that request nothing get an empty arena and an identical trace; the only cost is one extra execution, negligible against proving. Regression coverage: test_prove_ecrecover_hints_auto_records_arena asserts hint-less and explicit-arena calls produce identical element counts and equal verified public outputs.
|
/bench |
- cargo fmt over the hint-arena diff - group private_input/hints paths into ProveInputPaths so cmd_prove and cmd_prove_continuation stay under clippy's too_many_arguments (8/7), matching the FlamegraphCliOptions precedent Verified: cargo fmt --check --all plus all four CI clippy passes (default, debug-checks, disk-spill, cuda) green; the ethrex fixture checksum gate passes.
|
/bench |
…pass. request_hint now publishes its (hint_id, input) entry to the request log before reading the arena slot, and the store that bumps the log's count word is the executor's cue to answer it: it computes the hint and seeds the slot as an INITIAL value, on a cell nobody has touched. That needs no memory write in the trace - a write would have to be justified by a chip, an initial value does not - and it is the same statement as shipping the slot in the private input up front, because the region's bytes always stay exactly encode_private_input_region(input, arena). A test pins that invariant. The bytes stay unconstrained and untrusted: the guest verifies them and falls back to software on failure, exactly as before. A slot an explicit arena already covers is left alone, so passing hints up front keeps working unchanged, and Memory::silence_hints answers nothing so the software-fallback path stays measurable and testable. ExecutionResult now reports the arena the run actually used, and the monolithic prove path takes it from the single execution it already performs instead of calling resolve_hints, which is left as the continuation prover's pre-pass since that path freezes its initial image and provenance before streaming epochs. That pre-pass now drains its logs rather than collecting them: reading back an arena does not need tens of millions of Log entries at 40 bytes per cycle on a path whose whole purpose is bounding memory. Measured on 30 ecrecovers: the proved trace goes from 866,413 to 868,423 cycles (+0.23%, the request-log stores) while total executed cycles drop from 7,280,839 across two runs to 868,423 in one. An arena decided mid-run produces a trace identical cycle for cycle to one supplied up front, and both proofs verify with the same public output. Also reserves fallibly in Memory::hint_requests, whose capacity comes from a guest-written count word, and derives HINT_LOG_START from PRIVATE_INPUT_START and MAX_PRIVATE_INPUT_SIZE instead of restating 512 MiB.
…ex blocks. Each fixture runs three ways - every hint recomputed in software, answered on demand during the run, and supplied up front as an arena - printing cycles and wall clock for each, and asserting the last two produce the same trace. These are the numbers the one-pass change is argued from, and they are not visible in /bench: on the mainnet block it proves, the recording pass a hint-less prove used to run was 40.08M cycles (1.31s) against a proved execution of 34.19M (1.18s). That is about 1% of a 123s prove, under the 2% spread three runs resolve, so it has to be isolated rather than read off a two-branch comparison.
The continuation prover froze three things before streaming epochs - the carried memory image, the genesis provenance, and the PAGE init data the global proof commits - so it needed the arena up front and kept a recording pass after the monolithic path had already dropped one. None of the three has to be frozen: they only ever grow, and the executor discovers the new facts as the guest runs. `GenesisFacts` holds the page data and the arena's slot count behind a mutex. The producer folds in whatever the executor seeded right after each epoch executes and before `collect_epoch` replays that epoch's memory - which is where it has to happen, since that replay reads the image and `epoch_boundary` takes each touched cell's init from the provenance, and both would otherwise read zero for a slot the guest just read. The global prove reads the finished picture after the boundary channel closes, i.e. after the producer is done, so the lock is never contended and the ordering is the channel's rather than the lock's. Three things made this contained, all of them properties of the existing code: the per-epoch trace build never looks at the arena (inside `build_traces` the hints only reach PAGE generation, which continuation epochs skip via the L2G bookend); `init_page_data` and the page count are consumed only by the global prove, after it has drained every boundary; and an epoch executes before its own op collection, which is the gap the fold-in needs. `private_input_page_count` now takes the arena's slot count rather than the slots: the span only ever depended on how many there are, and a continuation knows the count before it has the bytes. Seeding claims a cell as genesis, which is only true of a cell with no history, so a cell an earlier epoch already bound is refused with a ContinuationInvariant instead of producing a bundle that fails to verify with nothing pointing at the cause. `resolve_hints` is gone with its last caller: no prove path executes the guest more than once now. Regression coverage proves and verifies the ecrecover guest four ways - arena answered on demand and supplied up front, monolithic and continuation - and requires the same committed output from all four.
…nputs. The two-pass flow is gone: an empty arena is now the normal case, answered by the executor during the single execution the call already performs. The stale paragraph also left a dangling intra-doc link to a function that no longer exists.
…mory. `Memory::store_word` compared every stored address against the request log's count word. The check belongs on the store INSTRUCTION instead: it means "the guest completed a log entry", not "someone wrote a word into a Memory", and this crate is linked into the in-VM STARK verifier (the recursion guest links `lambda-vm-prover`, which depends on it), which writes words through `Memory` without ever executing a guest store. This does NOT recover the cycles I first attributed to it. Measured on `recursion-min` against feat/hint-arena (328,052,567 cycles): the hint work costs 328,979,652, and moving the hook leaves it at exactly 328,979,652. Deleting the call entirely drops to 328,045,817, so the cost tracks the code being reachable rather than where it is called from, and the verifier never executes it. The +927k is isolated to `executor/src/vm/memory.rs` and remains unexplained; it is not codegen drift (two null perturbations each moved .text while leaving the cycle count exactly at the baseline, and two builds of the same source with different .text give identical cycles). Keeping the move on its own merits, with the measurement recorded here so the next person does not re-derive it.
|
/bench |
|
/ai-review |
Codex Code Review
|
|
/bench-verify |
|
⏳ Benchmark started on the bench server. Two verifier arms (monolithic + continuations over an ethrex 20-tx block), then the recursion-guest cycle comparison, which adds guest builds on top — longer on a cold runner. The bench server is occupied until it finishes. |
AI ReviewPR #942 · 55 changed files
Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-001: Continuation prover trace builder uses stale hint count if PAGE generation is re-enabled for epochs
Claim The build_worker passes the caller's original Evidence Lines 1262-1269: 'Reached only by PAGE generation, which the line above skips — so Suggested fix When PAGE generation is re-enabled for epochs, pass the effective hint count from GenesisFacts instead of the caller's original hints. Consider adding a test that enables PAGE for epochs to catch this. AI-002: CLI read_hints lacks early size validation against MAX_PRIVATE_INPUT_SIZE
Claim read_hints reads the entire hint file into memory before checking if it exceeds the 512 MiB private-input window. A maliciously large file could cause excessive memory allocation in the CLI before the executor rejects it during encoding. Evidence read_hints only validates bytes.len() % 32 == 0. The executor's encode_private_input_region enforces the cap, but only after the CLI has already read the whole file. Suggested fix Add a check in read_hints: if bytes.len() > 32 * (MAX_PRIVATE_INPUT_SIZE / 32) { return Err(...) } using the constant from executor::vm::memory, or stream the file in chunks. AI-004: ecrecover_hints guest doc lists hint request order incorrectly (sqrt, field_inv, scalar_inv vs actual sqrt, scalar_inv, field_inv)
Claim The module doc states the per-recovery hint request order is 'sqrt (decompress), the batched field inverse (lincomb), and the scalar inverse' and that 'the host's arena must follow the same order'. The actual call order in Evidence crypto/ethrex-crypto/src/lib.rs:254 calls Suggested fix Correct the doc to 'sqrt (decompress), the scalar inverse, and the batched field inverse (lincomb), in that order' to match the actual AI-005: Hint-answer hook fires on ANY guest SW to HINT_LOG_START_INDEX, can crash non-hint guests
Claim The Store::Word arm unconditionally calls Evidence execution.rs:273-278 runs Suggested fix Gate the hook on whether the guest is actually using hints — e.g. only answer when AI-007: Sharp edge: mixing request_hint with hint_count/next_hint causes silent desync
Claim The code explicitly documents that request_hint and hint_count/next_hint must not be mixed in the same guest, but provides no runtime guard. A guest that accidentally mixes them will consume slots incorrectly (request_hint uses the count word, next_hint uses a separate static cursor). Evidence Lines 183-188 in syscalls.rs and lines 386-391 in memory.rs both document this as a known sharp edge with no enforcement. The comment suggests a mode flag in the header's spare pad word would close it properly. Suggested fix Add a mode flag in the hint arena header's spare pad word (the 4-byte zero pad after the count) to distinguish 'pre-supplied arena' vs 'on-demand' mode, and reject mixed usage at runtime. 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 (2) — rejected by the verifier
Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts. |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Guest cycles | 331.6M | 329.0M | -2.6M (-0.80%) |
| Keccak calls | 3029 | 2994 | -35 |
baseline origin/main 884eb45780 guest=recursion-min.elf
PR 1a61b199ac20ce05282dd5c6199071690b6689b3 1a61b199ac guest=recursion-min.elf
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism);
treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=884eb45780016f33b729051a1a70c8abe9a511a6 ref_b_elf=recursion-min.elf ref_b_cycles=331649890 ref_b_keccak=3029 ref_b_execute_wall_s=9
ref_a_sha=1a61b199ac20ce05282dd5c6199071690b6689b3 ref_a_elf=recursion-min.elf ref_a_cycles=329007684 ref_a_keccak=2994 ref_a_execute_wall_s=10
delta_cycles=-2642206 delta_keccak=-35
(blowup2-block regime FAILED — see the workflow log.)
2 participants
Hints move from an
ecallserved by a dedicated AIR chip to plain bytes in the private-input region, and the executor answers them during the run instead of in a separate pass.The private-input region is already data the prover chooses and the verifier never recomputes, so hints can live there and the guest reads them with ordinary loads — there is no host write appearing mid-trace, and nothing to justify. The catch is that the initial image is fixed before cycle 0, which would mean executing the guest once to learn which hints it asks for and again to prove. Instead, the guest publishes each request through ordinary stores and bumping the count word is the executor's cue: it computes the answer and seeds the slot as an initial value, for a cell nothing has touched, so it lands in the image as if it had been there since cycle 0 — SP1's
mw_hint. Seeding a written cell or an out-of-order request is an error, since the memory argument requires a read after a write to return the write.resolve_hintsand the second execution are gone.The reason to prefer this over the
ecallis not speed. Anecalladds a mechanism: a write that has to be explained, so a table has to exist, and be argued about in every review and every audit from here on. The arena adds nothing — it reuses a degree of freedom the system already grants, since private-input bytes are already chosen by the prover and already never recomputed by the verifier. Hints stop being a special kind of data and become the kind the system already handles. And a table is not paid for once by whoever proves: it is checked by everyone who verifies that proof afterwards, including the verifier we run inside the VM.What goes away is 41 columns and 373 lines of AIR, and with them two obligations that had to be held every time the chip was reviewed: it had to bind the destination address, or the witness chooses where the 32 bytes land, and
muhad to be a bit, which the Ecall bus alone does not establish since it only fixes the sum over rows sharing a tuple. The arena adds no AIR obligation in exchange — the bytes are private input, which the system already treats as prover-chosen — andHNT-A1is unchanged either way.Prove time is a tie over 12 interleaved pairs on a real block. The in-VM recursion verifier, three runs per side on a real 20-tx block at blowup 2 / 219 queries: 2,216,446,035 -> 2,188,339,913 cycles, -28,106,122 (-1.268%).