Perf/dma tail wide memset - #896
Draft
diegokingston wants to merge 35 commits into
Draft
Conversation
Routes the guest's strong `memset` symbol through a bounded DMA ecall, the same shape as the memcpy stub #874 added, and proves each chunk with a new 20-column DMA_SET table. memset is cheaper than memcpy rather than a copy of it: there is no source to read, so a row emits one MEMW write and no read (half the memory traffic per byte), and every byte written is the same constant, so one `fill` column replaces memcpy's eight value lanes. `fill_wide` is `fill` on eight-byte rows and zero on one-byte tail rows, which lets one write tuple serve both widths. `fill <= 255` is proven on the first row; the executor rejects wider values and the guest stub masks a1, mirroring how the byte-count bound is handled. Measured on real mainnet block 25368371 (50,781,394 cycles baseline): #874 memcpy alone 41,642,609 -17.99% + memset (this) 40,338,153 -20.57% mem* routines fall from 24.41% to 4.84% of guest cycles. No existing AIR changes: CPU stays at 38 columns and the new table only adds senders to existing buses.
The DMA memcpy ecall already snapshots its entire source range before writing (all reads at T+1, all writes at T+2), so one chunk has memmove semantics for free. Chunking is what breaks it: copying [0,256) -> [4,260) clobbers source bytes a later forward chunk still needs. So the memmove stub walks chunks from the END backwards exactly when the destination starts inside the source range (src < dst < src+n); every chunk then reads bytes no earlier chunk has written. Disjoint regions, and dst below src, keep forward chunking. This costs one guest symbol and nothing else — no table, no syscall, no constraint. Measured on real mainnet block 25368371: memcpy + memset 40,338,153 + memmove (this) 39,867,443 -0.93% Cumulative vs the 50,781,394 baseline: -21.49%. The guest test covers both overlap directions at offsets either side of the 256-byte chunk boundary, plus exact aliasing.
Collaborator
Author
|
/bench |
|
Benchmark Results for modified programs 🚀
|
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 47344 MB | 50524 MB | +3180 MB (+6.7%) 🔴 |
| Prove time | 136.925s | 108.158s | -28.767s (-21.0%) 🟢 |
🎉 Improvement on the real block — prove time down 21.0%.
Prove-time spread 1.1% (108.158s / 108.447s / 107.204s)
Commit: 3c3a2a5 · Baseline: cached · Runner: self-hosted bench
Contributor
|
Automated review pass (high-effort, adversarially verified). Scoped to this PR's own diff on top of 874's current head. Findings:
Soundness of the new |
…886) * perf(guest): read the private input zero-copy via ef_io::read_input get_private_input() to_vec()'s the whole memory-mapped input before rkyv deserializes it; read_input hands rkyv a slice straight into the input region instead. Same bytes, same private-input commitment. Measured vs origin/main (same fixtures, deterministic): transfers_20 8,732,213 -> 8,692,490 (-39,723) erc20_20 10,328,222 -> 10,278,822 (-49,400) mixed_20 9,817,444 -> 9,768,492 (-48,952) Verified: test_prove_ethrex_empty_block (prove+verify) passes. * fix(guest): take the zero-copy input via the safe get_private_input_slice (#898) The zero-copy read is the right call, but it hand-rolls what `syscalls::get_private_input_slice` already does: borrow the mapped private-input region in place and hand back `&'static [u8]`, no copy and no allocation. `get_private_input` is that same call plus a `to_vec()`, so dropping to the slice is the whole win without the pointer plumbing. Three things that buys: - No raw pointers in guest code. `syscalls.rs` deliberately keeps the region layout and its one `unsafe` block in a single place — that is why `get_private_input_slice` exists. Re-reading the length prefix in the guest duplicates layout knowledge that has to stay in step with the executor. - Restores the length-prefix clamp. `get_private_input_slice` bounds the prefix by `MAX_PRIVATE_INPUT_SIZE`; `ef_io::read_input` returns it raw. The executor rejects oversized inputs, so honest runs are identical — but a forged prefix built a slice reaching past the region instead of a bounded one. - Drops a dependency on unspecified behavior. `ef_io::read_input` documents `buf_ptr` as unspecified when `buf_size == 0`, and the previous code fed it to `from_raw_parts` regardless. Harmless in practice (the implementation always writes it, and ethrex input is never empty), but not a contract to lean on. `bench_vs/lambda/recursion` already reads its blob this way. --------- Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>
Resolve the accelerator() conflict: the base gained DMA cycle counting (DmaMemcpy => Some(Accelerator::Dma)) while this branch added DmaMemset and classified both as None. Keep the counting semantics and extend them: DmaMemcpy | DmaMemset => Some(Accelerator::Dma). Two exhaustiveness follow-ups the merged tree needs to compile and pass: - SyscallNumbers::raw() gets the DmaMemset arm (DMA_MEMSET_SYSCALL_NUMBER). - The CLI's EXPECTED_ACCELERATORS gets a DmaMemset row, required by accelerator_of_mirrors_prover_classification's one-row-per-syscall check.
Collaborator
|
/bench |
Merged
…st their sum (#909) * fix(verifier): pin each trace-opening column width to the AIR, not just their sum The verifier pinned only the SUM of a query opening's precomputed/main/aux column counts (against the AIR-pinned OOD width). Nothing pinned the split, and the Merkle leaf hash pins neither: hash_data_from_slices streams evaluations || evaluations_sym with no length prefix and no separator. Each of the three trees is transcript-bound at a different time, so both splits are exploitable: * precomputed<->main: a non-preprocessed AIR never absorbs the precomputed root, so columns declared 'precomputed' are bound by nothing. A prover can sample the round-2 challenges and then solve for them. * main<->aux: the aux root is absorbed after the shared LogUp challenges, so a column moved from main to aux is chosen after challenges it must precede. trace_opening_widths_well_formed pins all three widths, for both the regular and the symmetric slot, once per table before any opening is read. Co-Authored-By: diegokingston <dkingston@fi.uba.ar> * test(verifier): regression tests for the trace-opening column split Six end-to-end cases against a hostile prover that declares one column 'precomputed' for an AIR that is not preprocessed, plus direct tests of the guard on a RAP proof covering all three widths in both the regular and the symmetric slot. On stock main, three of these fail (the proof is accepted): the honest trace under a split declaration, the adaptively forged trace, and a demonstrably false statement. The other three pass on both and are the non-vacuity controls - in particular a genuinely preprocessed table, which has num_precomputed_columns() > 0, must still verify. The end-to-end cases need TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB: a hostile prover does not absorb a root the verifier never reads, and without that the same proof is rejected for transcript divergence instead of for its split, which would prove nothing. Co-Authored-By: diegokingston <dkingston@fi.uba.ar> * style: cargo fmt + drop redundant clones flagged by clippy Co-Authored-By: diegokingston <dkingston@fi.uba.ar> * test(verifier): regression tests for the main<->aux opening split (LogUp break) Ports the aux-instance PoC into a permanent regression: a hostile AIR declaring layout (4, 2) against LogReadOnlyRAP's honest (5, 1) moves the multiplicity column into the auxiliary tree, which is transcript-bound only AFTER the shared LogUp challenges. The prover then solves that column against the sampled z/alpha, and the multiset equality the AIR exists to enforce degenerates into one scalar equation. On stock main both break tests are accepted - the structural mis-split and a false memory read (address 3 carrying two values) - the latter also over the rkyv wire through multi_verify_archived, the recursion-guest path. Unlike the precomputed instance this needs no prover change at all: both sides absorb main-root-then-aux-root either way. Three controls (corrupted aux opening, the same lie without the split, the split without the challenge solve) plus an honest LogReadOnlyRAP round trip pass on both, so the harness discriminates and the pin is not vacuous. Co-Authored-By: diegokingston <dkingston@fi.uba.ar> * docs(verifier): record the aux instance at verify_trace_openings and in the guard doc The aux arm authenticates against the aux root but constrains no width; say so, and point at the upstream pin. Same class of stale comment as the two this PR already corrects. Co-Authored-By: diegokingston <dkingston@fi.uba.ar> * test(verifier): drop the prover hook - both instances now pin hook-free The precomputed regression no longer needs the #[cfg(test)] absorb switch in prover.rs. Handing the prover and the verifier AIRs that disagree about num_precomputed_columns, while both absorb the same commitment constant, keeps the transcripts in sync - so the honest in-repo prover builds a proof that stock main accepts and this branch rejects. prover.rs is back to stock: the whole change is now verifier + tests. What the dropped end-to-end tests covered is kept: the 'a non-preprocessed AIR must declare zero precomputed columns' direction is pinned by the direct guard tests (its end-to-end form is masked by transcript divergence and proves nothing on its own), and the aux file demonstrates an executed false statement. Adds a tripwire (precheck_the_width_pin_is_compiled_in) plus attribution asserts in the break tests, so a rejection cannot be read as evidence unless it comes from the guard - the failure mode that made a sibling PoC look non-reproducing. Co-Authored-By: diegokingston <dkingston@fi.uba.ar> * docs(test): state precisely what the round-1 root check does and does not catch The precomputed-width test's comment implied real preprocessed tables are exploitable through this shape. They are not directly: an honest constant is a root over exactly num_precomputed_columns() columns, so a narrower tree hashes differently and round 1 rejects it. Say that, and say why the defence is incidental - nothing states the invariant, nothing checks it, and it is absent entirely for a non-preprocessed AIR. Co-Authored-By: diegokingston <dkingston@fi.uba.ar> * docs(verifier): trim the opening-width doc to the invariant The header carried the two exploit narratives in full, at ~33 lines for a ~40 line function -- 3x the sibling ood_blocks_well_formed. The mechanics belong in the tests that demonstrate them and in the PR; the header only needs the invariant, why an unpinned split is exploitable at all, and where to look. Co-Authored-By: diegokingston <dkingston@fi.uba.ar> --------- Co-authored-by: diegokingston <dkingston@fi.uba.ar>
…ory contents (two invariants, both with exploits) (#904) * fix(page): preprocess OFFSET on private-input pages A private-input PAGE (and its continuation analogue GLOBAL_MEMORY) skipped `with_preprocessed` entirely, so every column was prover-chosen main trace. PAGE carries `EmptyConstraints` and no constraint anywhere references `cols::OFFSET`, so nothing pinned it — and the Memory-bus address is `address_lo = page_base_lo + OFFSET`. A witness could therefore point a row at any address sharing the page's high limb and mint a second, forged history for it, breaking the one-entry-per-address property the offline memory-checking argument rests on. Reproduced end to end; see below. INIT must stay main-trace — it is the private input, and the verifier must not be able to recompute it. OFFSET has no such constraint: it is the dense `0..page_size-1` enumeration, byte-identical for every page regardless of program or input. Committing it alone binds exactly the column that must not be prover-chosen and publishes nothing. Approach: preprocess OFFSET only, rather than adding AIR constraints (`OFFSET[0] = 0` plus `OFFSET[i+1] = OFFSET[i] + 1`). The constraint route needs a real boundary constraint, and every VM table in this tree is built with `NullBoundaryConstraintBuilder` — there is no boundary machinery to follow, so that route means new infrastructure in the STARK layer. The preprocessed route instead reuses the mechanism that already runs on every proof for ELF-data and zero-init pages, and which `verifier.rs:1184-1213` already enforces. The bug was that private pages bypassed that check; the fix is to stop bypassing it for the one column that is public. It also costs no constraint degree and no constraint-evaluation time. Because OFFSET depends on neither program nor input, one commitment per blowup factor covers every private page, and the same value serves GLOBAL_MEMORY, whose OFFSET column is identical. Static constants follow the existing `static_zero_page_commitment` pattern (generated by `compute_static_commitments`, pinned by a drift test) with the same recompute fallback off the standard coset. Acceptance (full log in fix-acceptance.log): poc_control_honest_harness_verifies ... ok poc_negative_control_forged_run_without_repointed_row_fails ... ok poc_private_page_offset_forges_memory_contents ... FAILED panicked: SOUNDNESS HOLE NOT REPRODUCED: verifier rejected the forged proof The third failing is the point: that test asserts the forgery is ACCEPTED, and it passed on origin/main. The first passing is what shows the fix is not over-broad — honest proving still verifies. The PoC is converted into a regression test in the follow-up commit. * test(page): keep the OFFSET forgery as a regression test Inverts the PoC's central assertion now that the fix is in: the forged proof must be REJECTED. Renamed `poc_private_page_offset_forges_memory_contents` -> `forged_private_page_offset_is_rejected`, and rewrote the module doc, which still described the hole in the present tense. The two controls are unchanged and are what stop this becoming a test that passes for the wrong reason: `poc_control_honest_harness_verifies` fails if the fix breaks honest proving (a verifier that rejects everything would otherwise satisfy the assertion above), and `poc_negative_control_forged_run_without_repointed_row_fails` fails if the harness stops discriminating. Also drops two imports the fix made unused. * fix(verifier): validate and bound runtime_page_ranges before use `runtime_page_ranges` is a prover-chosen `VmProof` field with a free `u64` base and count, and `page_configs_from_elf_and_runtime` expanded it with a plain `for i in 0..count` push loop having validated nothing. The `expected_proof_count` cross-check that would reject a wrong page count runs *after* that loop, so it never got the chance: `RuntimePageRange { base: 0, count: u64::MAX }` made the verifier allocate `PageConfig`s until the process died — a verifier DoS on untrusted input. The function is now fallible and takes a `max_pages` cap enforced before and during expansion. The verifier passes `proofs.len()`: every page config needs its own sub-proof, so a layout wanting more pages than the proof carries can never verify. That makes the bound exact, needing no invented policy constant, and unable to reject anything an honest prover produces. Also validated up front, since all of it is attacker-controlled: - `count == 0`, which the honest run-length encoding never emits; - unaligned bases — which additionally keeps "same base" equivalent to "overlapping" for the duplicate check in the follow-up commit; - ranges running off the end of the address space, which the push loop would otherwise wrap in release. The overflow guard bounds the range's LAST BYTE, not its exclusive end. The stack's top page legitimately sits at the very top of the address space (`0xfffffffffffc0000`), where the exclusive end is exactly 2^64 and only the last byte is representable — bounding the end instead rejects every honest proof. A draft of this commit did exactly that; the PoC harness's honest control caught it, and `the_top_page_of_the_address_space_is_accepted` now pins it. New `Error::MalformedPageLayout`. Test call sites pass `usize::MAX` — they build layouts from honest data, not from a proof. * fix(verifier): reject two page tables covering the same address Second route to the violation the OFFSET binding closed, and this one needs no private input and no free column. `page_configs_from_elf_and_runtime` built a `Vec`, sorted it, and never deduped. So a prover declares `RuntimePageRange { base: <a real ELF .data page>, count: 1 }` and that address gets two PAGE tables: the ELF-data page with the real INIT, and a duplicate zero-init page. Both carry correct, verifier-recomputed preprocessed commitments — the duplicate matches the shipped `static_zero_page_commitment` exactly — so nothing is forged at the commitment layer, which is why pinning OFFSET does not touch it. Two genesis tokens then exist for every address in that page. The offline memory-checking argument needs the init set to hold exactly one entry per address; with two, the real page's row consumes the duplicate's token and the duplicate's row consumes the real one, and the bus balances while a value the program never wrote reaches a load. Every other row of the duplicate page self-cancels for free. `FINI`/`TIMESTAMP` are main-trace on every page, not just private ones, which is what lets the two rows swap which token each consumes. Reject rather than dedupe silently: a duplicate is never legitimate — the honest builder derives ELF pages from a `BTreeSet` and run-length-encodes the rest — so silent dedup would mask a prover bug instead of surfacing it. The check is a single adjacent-equality scan after the sort that already existed, which covers all three config sources at once (ELF, runtime, private) and so cannot be bypassed by adding a fourth. It relies on the alignment check from the previous commit to be a complete *overlap* check and not merely an equality one. Severity note: the OFFSET fix does limit this. The injected value is always `0`, since zero-init is the only page type a prover can conjure at an arbitrary base — so it forces a chosen address to read `0` at genesis instead of its real ELF byte. Still a forged execution (zeroing a length, a bound, a chain-id or a root byte suffices), but not an arbitrary byte at an arbitrary address. The framing: pinning `OFFSET` restores one row per address *within* a page; this restores one page per address. Both are needed. * test(page): end-to-end regression tests for both forgery routes Adopts the prosecutor's PoC harness (branch `poc/page-duplication`, 1bc1def6) wholesale rather than keeping my thinner copy, and inverts the assertions the way the OFFSET one was inverted. Their version is strictly better: it runs under PRODUCTION proof options (`GoldilocksCubicProofOptions::with_blowup(2)`, what public `verify` uses) instead of `default_test_options()`, and it carries two controls mine lacked. Eight tests, all passing, 24s: - `poc_control_honest_harness_verifies` — non-vacuity. The one that catches an over-broad fix; it already caught one (see the `runtime_page_ranges` commit). - `forged_private_page_offset_is_rejected` — route 1. Accepts refusal at either layer: `commit_main_trace` caches precomputed trees keyed by the expected root and skips the re-check on a hit, so a cold cache makes the prover refuse while a warm one leaves it to the verifier. Asserting one would be order-dependent. - `poc_negative_control_forged_run_without_repointed_row_fails` — the forged run without the compensating row must fail, so the harness discriminates. - `poc_negative_control_direct_init_tamper_on_preprocessed_page_fails` — rewrites INIT directly on the target's own ELF-data page. The bus balances perfectly, so the only possible rejector is that page's preprocessed commitment. It rejects: the mechanism works on ELF pages, and its absence on private ones was the whole of route 1. - `poc_real_ethrex_inputs_produce_private_input_pages` — reachability on the workload that matters. - `dup_structural_duplicate_page_coverage_is_rejected` — route 2's invariant in isolation: honest execution, every injected row self-cancelling, only the layout malformed. This is the one that flips pass→fail if the duplicate-base check is removed, and it cannot be satisfied by something incidental the way a forgery test might. - `dup_negative_control_without_compensating_row_fails` - `dup_duplicate_page_forgery_is_rejected` — route 2 end to end: ELF `.data` byte 0x11 read as 0x00, which was ACCEPTED against the unmodified ELF even after the OFFSET fix. A rejection now arrives in two shapes — `Ok(false)` from inside STARK verification, and `Err(MalformedPageLayout)` when the layout is refused before any proof is checked — so `verifier_accepts` collapses both and the tests do not have to care which fired. `craft_proof_with_duplicate_page` asserts the layout rebuild fails on duplicate coverage specifically, then still runs the full prove→verify path so the test stays end-to-end rather than degenerating into a unit test of the check. Also documents the test-only `minimal_bitwise` branch in `VmAirs::new`. That BITWISE AIR has no preprocessed commitment, so its lookup table would be prover-chosen — and since BITWISE backs `AreBytes`, an unpinned table would let a witness prove an arbitrary field element is a byte. It is safe only because all three production callers pass `false`; a fourth passing `true` would reintroduce the hole silently. The reconstruction-level tests in `page_layout_tests` stay: they cover shapes these do not (overflow, unaligned bases, count bounds, the top-of-address-space page). * test(page): tolerate prove-time refusal in the tamper regression tests CI failed on `poc_negative_control_direct_init_tamper_on_preprocessed_page_fails`: panicked at page_offset_forgery_poc.rs:455: this tamper leaves OFFSET alone, so the prover still builds it: PrecomputedCommitmentMismatch The `.expect` message was wrong on its own terms. The tamper does leave OFFSET alone, but it rewrites INIT on an ELF-data page — where the preprocessed columns are OFFSET *and* INIT (`NUM_PREPROCESSED_COLS = 2`). So it touches a preprocessed column after all, and `commit_main_trace` can reject it before a proof exists. Which layer fires is not deterministic. That function caches precomputed Merkle trees keyed by *the expected root* and skips the rebuild check on a hit (`crypto/stark/src/prover.rs:1161-1170`). A cold cache — a fresh CI runner — rebuilds from the tampered column and refuses; a warm cache — a local run that already proved something honest — substitutes the correct cached tree and lets the verifier do the rejecting. Local runs were warm, CI is cold. Both outcomes are rejections, so the test now accepts either via a shared `proof_or_prover_refusal`, which still requires an `Err` to be specifically `PrecomputedCommitmentMismatch` rather than any proving error. The test's meaning is unchanged: it pins that the preprocessed commitment rejects a direct INIT rewrite, which is what shows route 1 was that mechanism's *absence* on private pages rather than a flaw in it. `forged_private_page_offset_is_rejected` now shares the same helper instead of its own inline match. Swept the rest of the file for the same assumption. The rule, now documented on `Tamper`: a tamper touching a PREPROCESSED column may be refused at prove time and must go through the helper; one touching only main-trace columns cannot be and may keep `.expect(..)`. By that rule the three remaining `.expect`s are sound, and each now says why rather than asserting it: - the honest control — no tamper at all; - the uncompensated forged run — the forged execution moves FINI/TIMESTAMP (main trace) while OFFSET/INIT still come from the honest ELF; - duplicate-page injection — writes FINI only. Verified both orderings: 8/8 serial (warm cache, verifier path exercised), and each rejection test passing alone in a fresh process (cold cache, the CI path). * Fix/page offset review followups (#910) * drop the accidentally committed fix-acceptance.log' * docs(page): fix a doc comment on the wrong fn --------- Co-authored-by: jotabulacios <jbulacios@fi.uba.ar>
* Add on-demand hint ecall (host-computed) * Add HINT prover table for the hint ecall * Add hint ecall guest tests and test programs * Route ecsm inverses and sqrt through hint ecall * Make the hint ecall ABI big-endian * Validate the Hint ecall operand addresses * Verify hints by difference instead of byte compare * Bind HINT writes to x12 and range-check bytes * Fix hint doc placement and guest cargo config * Verify hints with a mandatory software fallback * Constrain the HINT multiplicity column as boolean * Drop BENCH-ONLY labels from the hint ecall * Test that IS_BIT rejects a non-boolean HINT mu * Run ethrex-crypto host tests in CI * Add software fallback and test seam to field_inv * GPU parity-check the HINT table * Move HINT syscall off the FEXT_FMA numberD * Bind and range-check the HINT ecall operands * lint * Fix stale hint-ecall comments (#899) - executor/Cargo.toml: drop the BENCH ONLY label on the k256 dep. 515a921 removed those labels everywhere else; compute_hint is production executor code reached by real ecrecover proofs. - hint_min: the ethrex call site is aligned, not unaligned — get_hint in crypto/ethrex-crypto wraps its output in an align(8) buffer. * Correct the hint_min alignment comment The guest doc claimed the ethrex call site is unaligned, but ethrex-crypto's get_hint wraps its output in an align(8) newtype precisely to keep the four HINT writes on the MEMW_A path — a bare [u8; 32] on the stack is only 1-aligned. Someone trusting the comment and dropping the wrapper would add four wide MEMW rows per hint call, on every ecrecover. * Drop the BENCH ONLY label from the k256 dependency k256 is on the prove path, not only in benchmarks: the trace builder's collect_hint_ops recomputes every hint's output with compute_hint because the value is not carried in the CPU log. A maintainer trusting the label and feature-gating the dependency away would break proving. * Range-check the HINT output address low limb, like the input one The HINT table range-checked in_addr's low limb on the ALU bus but left out_addr to the memory bus, reasoning that an output address straddling the 2^32 limb boundary cannot balance. The bus does bound it, but only to 2^32 - 25: the write bases are out_addr_lo + 8i, so the largest one stops being a canonical limb at 2^32 - 24, while MEMW's carry columns resolve the bytes past it correctly. The executor rejects anything above 2^32 - 32 with HintAddressOverflow, which left the seven-value window 2^32-31 ..= 2^32-25 that the AIR accepted and the executor halts on — a prover could prove a hint call the VM rejects. Send the same LT range-check for out_addr's low limb. The existing in_addr bound is reused unchanged, since 2^32 - 31 is exactly addr_limb_ok(addr, 31) for either operand, and is renamed HINT_ADDR_LIMB_BOUND now that it covers both. The trace builder emits the matching LT op, and the sizing pass counts three LT rows per hint call instead of two — LT is an upper-bound table there, so the count only has to stay >= the built trace, which is why the count_table_lengths drift test does not catch an undercount on its own. Tests assert that both address columns carry an ALU LT sender against that bound, and that the bound accepts exactly the limbs addr_limb_ok accepts, with the seven-value window as an explicit regression. * Derive the HINT selector bound from the executor's accepted set HINT_SELECTOR_BOUND was a literal 3 in the prover, while the executor decided validity with matches!(hint_id, HINT_FIELD_INV | HINT_SCALAR_INV | HINT_FIELD_SQRT). Nothing linked the two, so appending a fourth selector would make the HINT table assert LT(selector, 3) = 1 against an LT row the builder emits as 0 — an unbalanced ALU bus with no algebraic pointer to the cause. Move the bound next to the selectors it bounds, express the ecall's rejection as is_valid_hint_selector, and const-assert that every selector below the bound is valid and that the bound itself is not. The prover re-exports the bound instead of restating it, so a selector added without moving the bound fails to compile rather than surfacing as a bus imbalance at proving time. * ci(executor): run the executor lib unit tests The unit tests under `executor/src/tests/` live in the lib target (`#[cfg(test)] pub mod tests;` in lib.rs), so none of the `--test <name>` steps select them, and the `test_ckzg` step filters by name and runs only ignored tests. They therefore never ran in CI — including the hint ecall's `HintUnknownSelector` / `HintAddressOverflow` / per-selector coverage, which has no other home. The new step shares the lib test binary with the `test_ckzg` step, so it costs a test run rather than an extra compile. * test(ethrex-crypto): cover the negated-sqrt and canonical-but-wrong hints The existing lying-hint tests all feed `[0; 32]` / `[0xFF; 32]`, which die in `Scalar::from_repr` / `FieldElement::from_bytes` and never reach the verify predicate. So the checks the fast paths' soundness actually rests on — `(x * inv) == 1` and `x·inv - 1 == 0` — had no test that exercised their rejecting branch. - `field_inv` / `scalar_inv`: hints that parse cleanly and simply are not the inverse (`inv + 1`, `-inv`), which must be rejected and recomputed. - `decompress_r`: an oracle returning the *other* root. That is not a lie — `-y` is as valid a root of x³+7 as `y` — so the verify accepts it and the fallback never runs, leaving the parity-selection branch solely responsible for the sign. With the honest oracle that branch fires only for the `k` whose root happens to have the wrong parity; forcing the negation exercises it for every `k`. Also drops a dangling "property C1" reference from the module doc and states the property directly. * test(hint): exercise all three selectors in the hint_multi guest The guest called `HINT_FIELD_INV` three times, so the AIR's `selector < 3` range-check was only ever exercised at 0 — an accepted-value bound that no end-to-end test pushed against. One call per selector (`HINT_FIELD_INV`, `HINT_SCALAR_INV`, `HINT_FIELD_SQRT`) covers the whole accepted range; `sqrt`'s input is 4, a quadratic residue mod p, so the hint is a real root rather than the zeros `compute_hint` returns on a numeric failure. `test_prove_hint_multi_rust_guest`'s expected value follows, now computed through `compute_hint` per selector instead of assuming three field inverses. * test(hint): pin the guest's selector constants against the executor's `is_valid_hint_selector` and its const-assert tie the AIR's range-check to the executor's accepted set, so the prover and executor can no longer disagree. The *guest* is a third declaration and is still unbound: `lambda-vm-syscalls` re-declares the same three selectors as `usize`, in a crate the workspace excludes, linked to the executor's `u64` copies by nothing but a comment. A divergence there is silent. The ecall would either trap on an unknown selector, or — worse, for a value that stays in range — return the wrong function's answer, which the guest's verify-then-fallback swallows as "the host lied" and quietly recomputes in software. Nothing fails; the guest just runs ~2000x slower for the right result. `lambda-vm-syscalls` is added as a dev-dependency for it. Unlike `crypto/crypto`'s and `ethrex-crypto`'s copies it is not target-gated, so it does build on the host — safe because that crate's guest-only items (the `#[global_allocator]` and the `_start`/`main` entrypoint) are already `cfg(target_arch = "riscv64")`, and `executor::tests` is itself `#[cfg(test)]`, so the non-test lib build never links it. * docs(hint): correct three comments the operand work left stale Follow-on to "Range-check the HINT output address low limb" and "Derive the HINT selector bound", which added interactions and constants but left these behind. - `hint.rs`: the `HintConstraints` doc still said the LogUp argument "already fixes `mu`'s value via the timestamp-unique `Ecall` tuple", framing `IS_BIT` as belt-and-braces. That contradicts the module doc directly above it: the `Ecall` tuple carries a per-instruction timestamp, a free column, so LogUp pins only the *sum* of `mu` over rows sharing a tuple — which a witness can satisfy by spreading `mu` with integer weights summing to 1. `IS_BIT` is load-bearing, and the doc now says so and points at that argument. Its bus list was also stale (one register read, no LT senders); it is three and three. - `prover/src/test_utils.rs`: same stale bus surface on `create_hint_air`. - `crypto/ethrex-crypto/src/lib.rs`: the comment justifying `negate(y2)` over `negate(rhs)` claimed negating `rhs` "would silently compute the wrong value in release". That is not what happens. k256's `negate(magnitude)` computes `2*(magnitude+1)*P_limb - self` under a `debug_assert!(self.magnitude <= magnitude)`; for a magnitude-2 operand the result stays non-negative, so the value is correct and it is the debug assert that fires. The reason to prefer `negate(y2)` is real, but it is a build-configuration hazard, not a wrong answer — worth stating accurately in a comment that exists to explain a non-obvious choice. * ci(ethrex-crypto): run the hint tests in release too, not only debug k256 0.13.4 swaps its FieldElement implementation on `debug_assertions` (arithmetic/field.rs): debug selects the magnitude-tracking `field_impl` wrapper, release selects the raw `FieldElement5x52`. The guest ELF is built with `cargo build --release`, so every hint-verification test was exercising an implementation the guest never compiles -- and `test-ethrex-crypto` was the only test step in pr_main.yaml without `--release`. The two builds are not interchangeable for these tests. `ConstantTimeEq` differs between them: the debug wrapper compares the magnitude and normalized tags alongside the limbs, the release type compares limbs only. A magnitude-contract violation would panic loudly in the tested build and compute a silently wrong value in the shipped one. Keep both: release is what ships, and debug's magnitude asserts turn a contract violation into a panic rather than a wrong answer. --------- Co-authored-by: MauroFab <maurotoscano2@gmail.com> Co-authored-by: Diego K <43053772+diegokingston@users.noreply.github.com>
…mcpy-symbol-resolution
# Conflicts: # Cargo.lock # executor/Cargo.toml # executor/src/vm/instruction/execution.rs # prover/src/lib.rs # prover/src/tables/cpu.rs # prover/src/tables/trace_builder.rs # prover/src/test_utils.rs # prover/src/tests/count_table_lengths_drift_tests.rs # prover/src/tests/prove_elfs_tests.rs # prover/tests/gpu_constraint_interp_real.rs # syscalls/src/syscalls.rs
…clines, close an R2 corruption race (#914) * fix(gpu): recover device-only tables by downloading the resident LDEs on an R2 miss The device-only gate is a static predicate over a dynamic dispatch: it cannot mirror every reason the device R2 path might decline (parts count, kernel eligibility, transient errors, shapes a new workload brings), and each miss was a hard abort that deadlocked the epoch pipeline — DECODE on the synthetic workload, then a second table on the real-block bench. Instead of excluding tables one by one, treat the resident handles as the source of truth: on a miss, download the main/aux LDEs back to host, clear the device-only flag, and continue on the host path. Slower for that table, never wrong; the abort remains only when the handles themselves cannot serve the data. gpu_device_only_downgrades() counts recoveries so a persistently-missing condition still gets mirrored into the gate. * fix(gpu): drain-and-retry, then host downgrade, for resident-aux LDE declines A transient CUDA OOM on the resident aux LDE was a hard prove failure: the resident build leaves no host aux trace to fall back to. A device drain releases the concurrent VRAM peaks, so one retry usually keeps the table fully resident; if it still declines, download the resident aux trace (and the main LDE when the table is device-only) and continue host-backed. The drain before dropping the resident buffer also keeps kernels enqueued by the failed attempt from reading pool memory reused by a concurrent table. * fix(gpu): serialize the device R2 window to close a transient H corruption race Concurrent device R2 windows under VRAM pressure can transiently produce a fully wrong H for one or two tables while every input stays correct (rerunning the same chain on the same resident inputs matches the host), yielding a proof that fails the composition check. Serializing only the constraint-eval + decompose window across tables eliminates it; commits and host arms stay parallel, and the windows overlap rarely enough that the lock is near-free. LAMBDA_VM_GPU_SERIALIZE_R2=0 lifts the lock to bisect further or once the underlying race is found. * fix(gpu): device-only requires the d=2 composition path The device R2 path only exists for the d=2 quotient split; a table with any other composition bound (DECODE proves with num_parts == 1) would skip it entirely and hard-abort on its device-only trace. * fix(gpu): keep already-present host buffers in the downgrade recovery A mixed state (one commit fell back to CPU while the other stayed device-only) left the recovery refusing to proceed: it treated a missing device handle as fatal even when that side already had a valid host copy. Only the missing side is downloaded now, and the R3 host-arm guards check the buffer they are about to read instead of the table-wide flag. * chore(gpu): drop an orphaned diagnostic helper download_ext3_columns came along in a cherry-pick but its only consumer (the cross-check post-mortem) ships separately; dead code under the cuda feature. * fix(gpu): run the host decompose of a downloaded H outside the R2 lock The fallback arm (download H, host iFFT + LDEs) executed under the serialization lock, so under VRAM pressure — exactly when that arm runs — it serialized every other table's device window behind pure CPU work. The lock now covers only the device eval + decompose + the H download; the host decompose and every host arm run outside it. The lock is also acquired only for d=2 tables (the others never enter the device path). * chore(gpu): review follow-ups on the downgrade recovery set_host_data had been inserted between set_num_rows' doc and its signature, stealing its doc comment and un-gating it from the cuda feature; the serialization lock now recovers from poisoning instead of cascading PoisonErrors over the original panic; the downgrade counter joins reset_all_gpu_call_counters and the device-only residency test asserts it stays at zero on the happy path; stale comments about the aux gate mirroring the main gate rewritten with the actual contract. * fix(gpu): harden the downgrade downloads, parallelize the recovery transposes (#921) * fix(gpu): harden the downgrade download recovery Three fixes on the device-only downgrade path, all in the graceful degradation function whose whole point is to avoid a hard abort. - The aux branch of `materialize_lde_trace_host` sliced the downloaded slabs without checking their length, so a short download would panic inside the recovery instead of degrading. Both sibling download paths already validate (`download_main_lde_row_major` checks `col_major.len() != m * lde`, `materialize_aux_trace_host` checks `raw.len() != rows * cols * 3`); this adds the matching check. - Restore the `len/capacity % 3` guard the other two ext3 `from_raw_parts` sites carry, spelled `is_multiple_of` because clippy's `manual_is_multiple_of` rejects the older form here. - The failure error claimed "host aux trace is empty" on a path where that is false: when the aux download succeeded and the follow-up main-LDE download failed, the host aux trace had just been populated. Track which recovery step failed and name it. Control flow unchanged. * perf(gpu): parallelize the downgrade recovery transposes Both conversions in the recovery path were single-threaded nested loops over the full LDE: the col-major -> row-major main transpose in `download_main_lde_row_major`, and the de-interleaved-slabs -> row-major interleaved aux conversion in `materialize_lde_trace_host`. For MEMW at LDE 2^20 those are a 411 MB and a 327 MB buffer respectively, walked with a strided access on one core. Both now follow the existing idiom in `trace.rs` ("Parallel col-major -> row-major transpose"): parallelize over OUTPUT row chunks with `par_chunks_exact_mut`, so every element is still written exactly once and no unsafe is involved. The index math is unchanged -- chunk `r` of width `m` is `row_major[r * m + c]`, and chunk `r` of width `m * 3` sub-chunked by 3 is `interleaved[(r * m + c) * 3 + k]` -- because the layout was verified against the kernels. Gated on the `parallel` feature with the sequential loop kept for builds without it, and skipped when `m == 0` since `chunks_exact_mut(0)` panics. These loops run on a scheduler driver thread holding no locks, so rayon is safe here, unlike the pinned-staging unpack in math-cuda. * docs(gpu): align device-only and downgrade docs with the recovery semantics (#920) This branch turned two of the device-only hard-aborts into downloads that recover and continue host-backed, but the surrounding docs still describe the old contract: "every host read hard-aborts", "the prove aborts loudly", "a mis-gate panics one of the guards". Rewrite those to say what the code now does — R2 and the R1 resident-aux commit recover and bump GPU_DEVICE_ONLY_DOWNGRADES, R3/R4 still abort, and the R3 guards check the individual buffer so mixed states are legal. Also correct the R2 lock comment (it serializes submission, not execution, for device-only tables), note that the numeric gate is not the complete predicate on its own, broaden the downgrade counter's doc to cover resident-aux declines on tables that were never device-only, and drop the false "only" from materialize_lde_trace_host's failure list. Comments, doc comments, two assertion message strings and one doc-comment run command (--test-threads=1, matching the Makefile target). No behavior changes. * chore(gpu): read the R2 serialize env var directly The OnceLock cache bought nothing — the var is consulted a handful of times per prove and does not change over the binary's lifetime. * fix(gpu): cap the GPU test targets, count the aux retries, split the downgrade counter (#924) * ci(gpu): cap each GPU prover test target with a wall clock A panic on a device-only cliff assert can leave the prover hung instead of aborting: the panicking thread unwinds while its siblings stay parked in CUDA driver waits, so the process never exits. Observed repeatedly on rented 5090s under VRAM pressure. The merge-queue GPU job runs the Makefile targets through scripts/gpu_test.sh with no per-target limit, so one hang holds the box until the workflow timeout kills the whole job with no indication of which group stalled. Wrap the four cuda targets that run the prover in `timeout -k 30 2700`. 45 minutes is well above their normal runtime and well below the job timeout, and timeout's 124 exit fails the target, so gpu_test.sh names the stalled group and the merge is blocked. test-math-cuda is left alone: kernel parity never enters the prover. * feat(gpu): count the resident-aux drain-and-retry The R1 resident-aux path retries the device LDE after a full device drain when the first attempt declines, and that retry usually succeeds — which is the problem: a successful retry left no trace anywhere except an eprintln, so how often the device actually declines under VRAM pressure was unmeasurable in production, where nobody is reading stderr. GPU_RESIDENT_AUX_RETRIES makes the decline rate observable and separates it from its consequence: retries with no downgrades means the drain absorbed the pressure, while the two rising together means the drain is no longer enough. * fix(gpu): split the downgrade counter by site GPU_DEVICE_ONLY_DOWNGRADES counted two unrelated events: the R2 device-only downgrade in materialize_lde_trace_host, which is always a device-only gate miss, and the R1 resident-aux downgrade in materialize_aux_trace_host, which is entered whenever aux_resident() is set and so fires on tables the gate never marked device-only. A GPU run made that concrete: a preprocessed BITWISE table took the R1 downgrade despite never being device-only, and the combined counter reported it as a gate miss with nothing to distinguish it from one. Keep GPU_DEVICE_ONLY_DOWNGRADES on the R2 site alone and add GPU_RESIDENT_AUX_DOWNGRADES for the R1 site, so a nonzero value names its own fix: mirror the missing condition into the gate for the former, relieve VRAM pressure for the latter. The integration test now asserts both are zero with per-site messages, and the gate docs say which counter each round bumps. --------- Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>
* Add opt-in dlmalloc guest allocator * Use dlmalloc as the default guest allocator * Fix and test the dlmalloc bump provider * Regenerate guest program lockfiles * Default the guest allocator to bump * Drop the TLSF guest allocator * Regenerate the ethrex-tests lockfile * Regenerate the guest lockfiles left stale by the ChaCha20 removal * docs * Correct the guest allocator's documented claims * fix(syscalls): review follow-ups for the bump allocator default Mechanical follow-ups on the allocator swap. No behaviour change on any path that runs today; the one code change closes a failure mode that is currently prevented by a linker flag rather than by anything in this file. benchmark-pr.yml missed syscalls. The push-to-main paths filter listed prover, crypto, executor, bin/cli, tooling/ethrex-fixtures and the Makefile, but not syscalls -- so a change landing only in syscalls, which is exactly what this branch is, would not refresh main's benchmark baseline. syscalls is linked into the guest ELF, so an allocator swap moves cycles on every workload; main's baseline would have stayed stale until some prover file happened to change, and until then the comparison guard would have suppressed the table. pr_main.yaml:99 already hashes 'syscalls/**' into the guest-ELF cache key, so the two workflows disagreed about what rebuilds the guest. Two lockfiles still carried embedded-alloc. crypto/ethrex-crypto and tooling/ethrex-block-converter are detached workspaces with their own Cargo.locks, which is why the sweep missed them: both still listed embedded-alloc under lambda-vm-syscalls after syscalls/Cargo.toml stopped declaring it. Regenerated via cargo metadata in each workspace. The only removals are embedded-alloc's own transitive tree (const-default, linked_list_allocator, rlsf, and in ethrex-crypto also rustversion, svgbobdoc, base64 0.13, syn 1.0.109, unicode-width); no other package's version moved. The 10 added lines are all ` "syn",` losing its version-disambiguation suffix now that only one syn remains. bench_vs/sp1/fibonacci/Cargo.lock also names embedded-alloc, but that is sp1-zkvm 6.0.1's own dependency and is left alone. imp::init is now idempotent in both arms. Both arms stored HEAP_POS unconditionally, so a second call rewound the cursor back over live allocations. With alloc_zeroed's memset removed -- sound only because bump never re-serves a region -- the next alloc_zeroed would then return dirty bytes, and the guest would compute on garbage while the prover produced a perfectly valid proof of that wrong execution. No crash and no diagnostic, so it is worth a guard rather than a comment. HEAP_END serves as the initialized flag (init_allocator always passes a nonzero MAX_MEMORY_SIZE), a debug_assert makes a double call loud in debug builds, and the host tests gain a #[cfg(test)] reset() since they deliberately re-point the global cursor at their own heap. Worth stating why this could not happen already, because the reason is not the call sites: all six guests that call init_allocator() explicitly also override the ELF entry with `-C link-arg=-e -C link-arg=main` in their .cargo/config.toml, so _start -- the only other caller -- never runs for them, and guests entering through _start never call it explicitly. The safety rested on an entry-point flag; a guest that dropped `-e main` while keeping its explicit call would have rewound. Three comment corrections and one warning. - The dlmalloc dep comment called it the allocator to pick "for continuations". Wrong criterion: continuations are a prover-side split of a single guest execution and change nothing about what the guest allocates. The criterion is a guest whose cumulative allocation has no per-execution bound, which is how src/allocator.rs already frames it. - allocates_zeros()'s comment described an "mmapped marker" that dlmalloc may set. There is no marker bit: Chunk::mmapped(p) is `(*p).head & INUSE == 0`, the absence of both in-use bits (dlmalloc 0.2.14 src/dlmalloc.rs:1805). The old comment's "the Rust port has no mmap path, so nothing is ever mmapped" is also not quite true -- init_top (dlmalloc.rs:789) writes a segment-end sentinel with head = top_foot_size() = 80 on 64-bit, and 80 & INUSE == 0, so that sentinel is mmapped()-true (harmless: never returned to a caller). Replaced with the durable argument: every path that returns a pointer to a caller goes through set_inuse / set_inuse_and_pinuse / set_size_and_pinuse_of_inuse_chunk, all of which set CINUSE, and calloc_must_clear is only ever evaluated on a user pointer, so no user chunk is ever mmapped. Consequence the old comment omitted: calloc_must_clear is therefore always true, calloc always memsets, and allocates_zeros() == true is inert -- not a performance win, kept only for correctness-by-construction should upstream grow an mmap path. - The comment on the bump arm's checked_add claimed the overflow is unconstructible from the Layout invariant alone. It is not: Layout gives size <= isize::MAX - (align - 1), which with aligned <= pos + align - 1 bounds aligned + size <= pos + isize::MAX, and that is < 2^64 only if pos < 2^63. The missing half is that alloc stores new_pos only when new_pos <= HEAP_END, so pos <= HEAP_END = 0xC000_0000. The checked_add stays -- it keeps the argument local to alloc instead of resting on both halves. - New note on the DLMALLOC static: an initialized Dlmalloc is address-sensitive and must never be moved. smallbin_at returns a pointer into self.smallbins and init_bins writes self-pointers into that array, so relocating it after first use (into a Box, a OnceCell, or a local) silently corrupts the bins. Safe as a static; the note is for whoever refactors it. Verified: syscalls tests pass on both arms -- 9 passed on the default bump arm (5 allocator + 4 keccak) and 12 on --features dlmalloc-alloc (8 allocator + 4 keccak). cargo fmt --check and cargo clippy --all-targets clean on both arms (the two surviving warnings are pre-existing manual_is_multiple_of in src/keccak.rs:104-105). benchmark-pr.yml parses and its paths list resolves to the seven expected entries. * Grow the top bump block in place on realloc * Trigger the hyperfine bench on syscalls changes * Test the allocator init guard in both profiles * Replace the bump ceiling claim with measurements * fix doc * fix a comment * Drop the TLSF reference from the allocator proof test's doc This PR removes the TLSF heap, so the test no longer exercises TLSF init. It proves the same program against whichever allocator is built in, so name the step rather than the implementation. Comment-only. --------- Co-authored-by: Diego K <43053772+diegokingston@users.noreply.github.com> Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com> Co-authored-by: MauroFab <maurotoscano2@gmail.com> Co-authored-by: Nicole <nicole.graus@lambdaclass.com>
* perf(prover): default the cuda table scheduler to K = num_airs
`table_parallelism()`'s cuda arm scaled K by `available_parallelism()`
(`cores * 2 / 3`). Measured over 881 runs on two RTX 5090 boxes, that is the
wrong shape. All eight core-count curves fit `T(K) = S + max(Tmax, W/K)` within
run-to-run noise, and the work K divides — W ≈ 5.3-8.0 s — is invariant to host
core count over an 8x range, to CPU model, and to rayon pool width: cutting
RAYON_NUM_THREADS 32 -> 4 leaves W alone and merely doubles S, with the best K
still num_airs at every pool width. `available_parallelism()` sizes precisely
that rayon pool, so it is the wrong quantity to scale K by. K is not a thread
count; each table's work runs on the one global pool.
Worst case against the best measured K, over four core counts on both boxes:
cores/3 +30.2 %
cores*2/3 +13.0 % (what this replaces)
constant 12 +7.0 %
num_airs +1.6 % (both non-zero cells inside noise, p = 0.88 / 0.80)
`cores*2/3` fails where it was predicted to: low core counts, K=2 at 4 cores
(+13.0 %) and K=5 at 8 cores (+8.1 %).
Taking the ceiling rather than solving for an optimum is right in both regimes
of the fit: if W/num_airs > Tmax more K strictly helps, and if W/num_airs < Tmax
the extra drivers are floor-limited and cost nothing — the one staging slab is
held 56 % of wall at K=31 and wall time still improves. The old doc comment's
mechanism ("in-flight tables mostly sit in GPU waits") is not what happens —
mean GPU utilisation never exceeded ~38 % at any K — so it is rewritten rather
than re-tuned. What is meant to bound concurrency is memory admission rather
than a count: that is what VramGate is for, and it never binds at the default
budget.
`table_parallelism` now takes `num_airs` and clamps to it, replacing the
`.min(num_airs)` the call site applied. `auto_storage::decide` keeps a bounded
figure through the new `storage_estimate_parallelism()`: `peak_bytes` sums the
transient bytes of the top-k tables, so an unbounded k there sums every table —
measured +27 % at 128 PAGE tables, +44 % at 512 — and would spill proofs to disk
that fit in RAM. Its value is unchanged, so no storage decision moves.
The CPU arm keeps `cores / 3`. The sweep ran only on cuda builds, where the
parallelized work is device-bound; on a CPU-only build every table is pure host
work and none of this evidence transfers.
* docs(stark): compress the table_parallelism doc comment
The sweep record moves out of the tree to a gist linked from PR #911, and
the full defense of the K = num_airs choice (curve fit, rayon-width legs,
per-cell p-values) lives there and in the PR body. The code site keeps the
conclusion, the mechanism in one sentence, the headline numbers, and the
pointer.
* fix(stark): satisfy unnecessary_lazy_evaluations on the cuda clippy pass
Under the cuda feature the unwrap_or_else closure in table_parallelism
collapses to a plain num_airs, tripping the lint on the Makefile's cuda
clippy pass. Move the cfg split outside the closure: the cuda arm uses
unwrap_or, the CPU arm keeps its lazy host_cores() call.
---------
Co-authored-by: Diego K <43053772+diegokingston@users.noreply.github.com>
…R4 DEEP, comp-tree, R3 barycentric) (#935) * fix(gpu): recover device-only declines at the remaining cliff sites (R2 commit, R3 OOD, R4 DEEP) Under VRAM pressure a device dispatch can decline after the device-only gate already skipped the host drain, and the host fallbacks at the R2 comp-poly commit, the R3 parts/trace OOD and the R4 DEEP loop hard-abort on the empty host buffers. Download the resident data instead: the trace LDEs via materialize_lde_trace_host, the H part evaluations via a new download off the resident R2 parts handle. The asserts remain only for handles that cannot serve the data. The R4 DEEP host loop reads both the trace and the part evals, so it recovers both sides. Also adds sticky fault-injection hooks (test-faults) to the cuda barycentric, DEEP and comp-tree entries: the drain-and-retry absorbs one-shot faults, so the cliff paths need a fault that keeps firing. * test(gpu): exercise the cliff-site recoveries end to end Three prove+verify runs under sticky faults (comp-tree, barycentric, DEEP), each requiring the device-only path to fire on the warm-up and the recovery counters to move. * fix(gpu): address cliff-recovery review — race-free sticky hook, parallel parts download Review follow-ups on the device-only cliff recovery: - check_sticky: collapse the load-then-decrement into one fetch_update that saturates at 0, so concurrent per-table dispatches can't underflow the counter — which would break both the sticky guarantee and the `== 0` fired check. - cuda_fallback_tests: disarm the sticky faults with a Drop guard, so a panic in prove or a failing assert can't leave one armed and cascade into the next test in the single-threaded binary. - download_composition_parts_host: de-interleave under rayon and reinterpret the u64 buffer in place, matching materialize_lde_trace_host instead of copying again through u64_to_ext3_vec — this path fires often under VRAM pressure. - Docs: the device-only downgrade counter now also covers transient device declines, not only gate misses; note the new &mut contract on get_trace_evaluations_from_lde. * style(gpu): rustfmt check_sticky and correct its doc cargo fmt collapses the aligned match-arm comments (the CI lint failure); also drop a stale doc sentence describing an earlier post-load variant that the fetch_update version does not use. * test(gpu): assert the parts-download counter is zero on the happy path (#938) The device-only cliff recoveries replace hard aborts with a silent download-and-continue, so the counters are now the only thing that surfaces a gate/dispatch lockstep break. GPU_DEVICE_ONLY_DOWNGRADES (trace side) already has its == 0 guard here; its parts-side counterpart did not, and its only readers were the > 0 assertions in cuda_fallback_tests, which run with a fault deliberately armed. Without this, a decline in the R2 comp-poly tree build on a device-only table recovers, verifies and passes green, while every such table pays a full parts D2H plus a CPU commit_bit_reversed and loses the resident composition tree. The R4 DEEP site is already covered transitively (it needs the trace to be device-only too, which moves the trace counter), so this closes the R2 commit and R3 parts-OOD sites. Zero is the right expectation: materialize_composition_parts_host early-returns without bumping when the part evals are already populated, so the counter only moves for a device-only table that had to pull its parts back. The message names both causes rather than blaming the gate, matching the counter's own doc, which now allows a transient VRAM decline as well as a gate miss. --------- Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>
* ci(bench-gpu): stop building on half-provisioned or bad-RAM boxes The GPU ABBA bench kept failing on rented Vast boxes in ways that looked like code bugs but were the harness building before the box was ready: - The provisioning-complete check fell back to "these few artifacts exist" and started the build while onstart was still populating the sysroot, so the C compiler read a half-written header (truncated bits/timex.h -> "unterminated #ifndef"). Require the "=== done ===" marker only; drop the premature fallback. - Add a toolchain sanity gate (trivial gcc + rustc compile) after provisioning: a bad-RAM host that SIGSEGVs the compiler on the first heavy crate (jemalloc, serde_derive) now fails fast here with a clear message instead of mid-build with an internal-compiler-error backtrace. - Cap the dual build at CARGO_BUILD_JOBS=8 so the initial ramp (LLVM codegen units + jemalloc's nested make -j) can't transiently exceed the box's RAM and trigger OOM-induced compiler crashes. - Filter offers by reliability>=0.95 to skip chronically-flaky hosts before renting (fails safe: over-strict just yields no offers). A full box-reroll (rent another host on a build/prove failure) is the next step but needs a live run to validate against paid infra, so it is left out of this change. * fix(bench-gpu): make the toolchain gate able to fail, and say why (#940) * fix(bench-gpu): make the toolchain gate able to fail, and say why Follow-ups from review of the provisioning hardening. - The sanity gate could not fail on a compiler failure. Under `set -e` a non-final operand of an `&&` list is exempt from errexit, and the list's non-zero status does not re-trigger it, so a dead cc/rustc was swallowed and the remote exit status was that of the trailing `rm -rf`. The gate returned 0 and printed "toolchain sane" on a host whose compiler had just crashed. Measured, before -> after: cc SIGSEGV 0 -> 139, cc missing 0 -> 127, cc error 0 -> 1, rustc SIGSEGV 0 -> 139, rustc missing 0 -> 127, healthy 0 -> 0. Every command is now a bare statement; a trap keeps the tmpdir cleanup on both paths. - Distinguish ssh's own exit 255 from a verdict on the toolchain, so a network blip no longer reports the host's compilers as broken. - Run the probe from the repo so rustup resolves the pinned toolchain in rust-toolchain.toml rather than whatever default the image carries. - A failure in this step posted "Run failed" above an EMPTY code block: the PR-comment step tails $RUNNER_TEMP/abba_out.txt, and only the bench step ever wrote it. Record the reason and the compiler output there. - Reword the gate's error. It establishes "cc or rustc could not compile and run a trivial program"; bad RAM is named as one possible cause rather than asserted as the diagnosis. Comments, each previously at odds with the code or with each other: - the gate blamed bad RAM while the CARGO_BUILD_JOBS comment blamed memory pressure for the same symptom. The latter now describes OOM as it actually presents (SIGKILL, or an allocation failure) and names jemalloc-sys's CARGO_MAKEFLAGS forwarding, which is what makes the cap bind its nested make. - drop the unmeasured "~10 min dual build", and annotate the 3 min 56 s ETA reference as a pre-cap measurement that CARGO_BUILD_JOBS=8 will raise. - the no-offer error and the env header now list reliability, gpu_frac and cuda_max_good, which they had drifted from. - state the gate's scope: it does not exercise /opt/lambda-vm-sysroot, and a 1 s compile surfaces marginal RAM only sometimes. * fix(bench-gpu): tell the operator to wait before re-rolling the box Both host-fault messages said "Re-run /bench-gpu to reroll the box", but offer selection is deterministic — `sort_by(.dph_total) | reverse | .[0]` with no machine_id exclusion — so an immediate re-run can re-pick the same machine once it relists and fail identically. Say to wait a few minutes instead, and say why, so the advice matches what the picker actually does. The ssh-255 message is left as an immediate retry: a transport failure is not a verdict on the host, so there is nothing to roll off. Still not an automated reroll (the sibling gpu-tests.yml carries a TRIED machine_id list for that); this only stops the message promising something the selection logic does not do. --------- Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>
* perf(gpu): grind the proof-of-work nonce on the GPU Grinding (generate_nonce) runs a ~2^grinding_factor parallel Keccak search per table per epoch and is the prover's dominant CPU cost — 64.7% of on-CPU time in a 100tx flamegraph, on the 16 cores while the GPU sits ~66% idle. Add a keccak nonce-search kernel (each thread strides a nonce block, atomicMin keeps the smallest valid nonce), a math-cuda wrapper that searches in expanding blocks from 0, and a stark dispatch that computes the inner hash on the host, validates the device result unconditionally, and falls back to the CPU search on any device miss or invalid nonce. Result-valid: the verifier only checks is_valid_nonce, so any valid nonce works. A device launch is skipped below a minimum grinding factor (tiny factors are faster on the CPU), and LAMBDA_VM_NO_GPU_GRIND forces the CPU path. GPU_GRIND_CALLS counts the dispatches so a silent fallback is caught by the integration test. 100tx e20 (ABBA, same binary): 18.89s -> 13.10s = -30.6%. * fix(gpu): review follow-ups on the GPU grinding PR (#945) Route the GPU dispatch and its tests through one inner-hash-to-lanes conversion. The tests built their own copy, so the line the prover actually runs was executed by nothing: swapping it to from_be_bytes would have kept every test green while is_valid_nonce rejected every device nonce at runtime and the search sat on the CPU fallback forever. stark::grinding:: inner_hash_lanes is now the single entry point, which also lets get_inner_hash go back to private. Report that fallback on stderr instead of log::warn. The CLI initialises env_logger with no default filter, so a warn-level line never prints unless RUST_LOG is set — and it is the only signal that the kernel has started returning garbage. The other device-decline paths already use eprintln with a [gpu] prefix. Wrap test-math-cuda in GPU_TEST_TIMEOUT. It was the only one of the five GPU targets without it, and it is Group 1 of gpu_test.sh, so a hang there costs Groups 2-5 as well and a job timeout yields `cancelled`, which skips the run-summary step and leaves no readable output. Document LAMBDA_VM_NO_GPU_GRIND in the profiling README's knob list. Drop the "Parity" framing from the test module: there is nothing to be at parity with, since any valid nonce is acceptable and the CPU's find_any does not agree with itself between runs. What is pinned is validity, plus the search completeness that minimality stands in for — noted as a probe rather than a contract, so a future kernel that deliberately returns any valid nonce relaxes the assertion instead of being treated as broken. Same for the doc on generate_nonce_maybe_gpu, which claimed "smallest" for both arms. --------- Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>
…-size tables (#888) * add profiling * fix(profiling): field fixes from the first sessions on the 5090 box - run_profile.sh: nsys export needs --force-overwrite (nsys stats already materializes the sqlite); tolerate runs that produce no timeline JSON - flamegraphs.sh: fixed off-CPU capture window sized from the on-CPU run (SIGINT through sudo is unreliable and produced 0-byte captures); find offcputime-bpfcc in /usr/sbin (Debian) - bench_mode.sh: set the CPU governor via sysfs when cpupower is absent - setup_machine.sh: Debian-aware perf install (linux-perf); extract libnvToolsExt from the cuda-nvtx-12-8 deb into ~/nvtx (CUDA >= 12.9 removed NVTX v2 from the toolkit) with LAMBDA_VM_NVTX_LIB override - docs: benchmark/profiling examples use ethrex 5tx/10tx fixtures only (team convention: never fibonacci); plan status updated * docs(profiling): complete the toolkit README as a reference Adds the pieces needed to use the tooling without reading the scripts: column-by-column semantics for phase_table.md and phase_busy.md (including NVML gpu% vs nsys busy% and launch-site attribution), a reference table of every script with its flags, the environment variables the tooling understands plus the pre-existing prover knobs for A/B experiments, and a troubleshooting section (missing NVTX ranges, silent CPU fallback, empty off-CPU captures, jitter, concurrent-thread span nesting). * perf(gpu): async pinned D2H + pre-created event pool + precomputed-tree cache The optimization half of the original campaign commit, without its profiling layer (this branch keeps gpu-profiling-tooling's toolkit as the only instrumentation): - async_dtoh_via/PendingD2H: big D2H copies go through per-worker pinned slabs via raw cuMemcpyDtoHAsync + a reusable completion event, instead of cudarc's memcpy_dtoh whose pageable path blocks the calling thread for all prior stream work (host DtoH blocking 12.4s -> 6.7s on the original ethrex A/B). - GpuLdeBase/GpuLdeExt3 carry a 'ready' event; consumers wait device-side (cuStreamWaitEvent) instead of producers host-synchronizing. - Events are pre-created at backend init plus a reusable pool: a mid-prove cuEventCreate convoys the driver lock (~30ms/call measured under load). - Precomputed-column Merkle trees are cached process-wide keyed by their commitment root, so preprocessed tables (DECODE/BITWISE/range) stop rebuilding identical trees on every prove; only the multiplicity columns are recommitted. * perf(prover): pipeline + concurrent epoch proving in continuations Producer thread executes and builds epoch i+1's traces while epoch i proves; K epoch provers (LAMBDA_VM_EPOCH_CONCURRENCY, default 3) consume prepared epochs concurrently — epoch proofs are mutually independent (label-domain-separated transcripts), results re-ordered by index so proof bytes match the sequential schedule. The DECODE commitment is computed once per continuation prove instead of per epoch. Same as the original campaign commit minus its epoch-timeline instrumentation (this branch keeps the profiling toolkit's spans as the only instrumentation; they are re-homed onto this pipelined flow at the end of the series). * perf(gpu): dim-split constraint interpreter with liveness-reused value slots The constraint interp/composition kernels evaluated every IR node as ext3 and kept one global-memory scratch slot per node, so scratch size and traffic scaled with program length (KECCAK_RND/ECSM/ECDAS at full thread count needed 26-39 GB, failing the alloc and silently falling back to CPU via result.ok()). Lowering (constraint_ir/device.rs) now assigns dim-split slots: - Base-dim nodes compute in the base field (1 mul vs 9 for ext3) and live in u64 slots (8B vs 24B); mixed base*ext ops use mul_base / componentwise shortcuts that are bit-identical to the full ext op on the embedded operand (SUB components keep the literal sub(0, x) form, which is NOT bitwise neg on non-canonical limbs). - Slots are liveness-reused (linear scan, freed at last use, roots pinned), so per-thread scratch is the max-live-set, not the node count: 8-35x smaller across the 26 tables (CPU 14.4KB -> 1.3KB, ECDAS 596KB -> 17KB per thread). Scratch allocs drop the memset. - Row-invariant leaves (constants, RAP challenges, alpha powers, table offset) are propagated into operand encodings (kind<<29|payload) and never touch scratch; they only materialize when a root needs them. The CPU walker eval_device_program mirrors the new walk and stays the pre-GPU parity oracle; the 26-table differential vs the production folder and the on-GPU parity tests (synthetic + all real programs) pass bit-for-bit. ir_stats_dump (ignored) prints per-table node/slot stats to size scratch when tuning. Measured on RTX 5090 (nsys, ethrex): constraint_composition_kernel 814ms -> 267ms (-67%) over the same 29 launches; ethrex 10tx continuations ABBA 15.16s -> 14.77s. * perf(gpu): commit preprocessed tables through the fused GPU pipeline Preprocessed tables (DECODE/BITWISE: precomputed + multiplicity column split) skipped the fused GPU commit entirely — commit_main_trace only tried the GPU when precomputed.is_none() — so they paid the CPU row-major LDE plus two CPU subset Merkle trees (~2.2s thread-time of R1 'Main commit Merkle CPU' on ethrex). - keccak256_leaves_base_row_major_row_pair_range: column-range variant of the row-pair leaf kernel, byte-identical to the CPU commit_rows_bit_reversed_subset layout. - coset_lde_row_major_split_trees: one row-major GPU LDE of all columns plus the two subset trees built on device; both node buffers download to host and rebuild full host trees via from_precomputed_nodes, so the preprocessed opening path, the process-wide precomputed-tree cache and disk-spill work unchanged. The shared expansion stage is factored into expand_row_major_on_stream (same code path as the existing fused commit). - The table now gets a GpuLdeBase handle (column-major LDE + trace snapshot, no device tree), so its rounds 2-4 (composition, DEEP, barycentric) run on GPU too. Preprocessed openings short-circuit to the host trees via is_preprocessed, as before. - REGISTER stays on CPU (LDE below the dispatch threshold). Parity: split_tree_tests pins roots and opening paths against the CPU subset commits on device; cross-binary verification of full ethrex bundles passes both ways. Measured on RTX 5090: ethrex 10tx continuations interleaved 3-way 14.77s -> 14.23s (cumulative -6.1% vs the pre-kernel baseline). * perf(prover): overlap the global prove with the epoch proves' tail prove_global consumes only execution artifacts — the per-epoch cell boundaries built by the producer, the ELF and the genesis pages — never an epoch proof, yet it ran serially after every epoch prove finished (~0.9s of pure tail on ethrex 10tx). The producer now publishes each epoch's boundary (an Arc share of the one already flowing to the epoch provers — no data copy) on a dedicated channel, in epoch order. A scoped thread drains that channel until the producer hangs up (last epoch prepared) and proves the global memory argument while the tail epochs are still proving. On an epoch failure first_err still wins and the global result is discarded; proof bytes and bundle content are unchanged — only the schedule moves. The epoch timeline confirms the tail is gone: the global prove runs fully inside the window of the last three in-flight epoch proves. Measured on RTX 5090: ethrex 10tx continuations ABBA 14.16s -> 13.66s (-3.5%); cross-binary verification passes both ways. Day cumulative across the three optimizations: -9.4% (15.16s -> 13.66s). * perf(prover): share per-ELF DECODE artifacts across continuation epochs Every epoch's trace build re-parsed the ELF and regenerated the pristine DECODE trace (~1M rows) inside the serial producer chain, plus moved a ~900K-entry pc->row map by value per epoch. DecodeArtifacts (instruction map + pristine DECODE trace + pc->row index) is a pure function of the ELF: prove_continuation builds it once and every epoch's build clones the pristine trace (a memcpy) and fills its own multiplicities; build_traces now borrows the pc->row map. The monolithic entry point delegates and is unchanged. Net work removal with identical trace bytes (cross-binary verification passes). Wall-neutral within noise on a 32-core box; groundwork for pipelining the epoch trace build out of the producer chain, where parallel builders would otherwise each redo the ELF parse. * perf(prover): pipeline epoch trace builds onto a builder pool The continuation producer built every epoch's full trace tables inline, so the serial chain feeding the provers was execute + collect + BUILD per epoch (~95% of it table generation) — 7.2s of a ~18s wall on a 32-core box, with the last epochs' proves gated on it. The epoch trace build is now split at its real sequential boundary: - Traces::collect_epoch (Phases 1-2): op collection over the advancing memory image — stays on the producer, in epoch order. - Traces::build_from_collected (Phases 3-5): table generation — pure epoch-local work, runs on a small builder pool (LAMBDA_VM_TRACE_BUILDERS, default 2) between the producer and the epoch provers, bounded channels capping peak memory. The cross-epoch chain no longer touches traces: the boundary derives from CollectedEpoch::touched_memory_cells (same function, same immutable memory_state as the build) and the next epoch's register init from register::fini_from_final_state — a trace-free mirror of the REGISTER FINI column, pinned by fini_from_final_state_matches_trace. PAGE tables are the build's only image consumers and continuation mode skips them, so builders need no image snapshot. Measured on a 32-core RTX 5090 box (ethrex 10tx continuations): the producer chain drops 7.2s -> 2.9s and the first three proves start ~1s earlier, but the wall ties (~18s) — the box is bound by total CPU work, which this change conserves (proves and the global dilate to absorb the freed schedule). A K/builders sweep confirms K=3/B=2 stays optimal. Expected to pay on wider boxes where idle cores can absorb the parallelism; groundwork for cutting per-epoch CPU work (AIR/capture caching), which is the binding constraint on narrow boxes. * perf(prover): cache pre-captured AIR prototypes per table type Constructing an AirWithBuses runs every constraint body through a MetaBuilder, and the first constraint_program() runs them again for the IR capture — for ECDAS/ECSM/KECCAK_RND (16-25K IR nodes) that dominates AIR construction (0.78s per VmAirs::new on ethrex). Continuation epochs rebuild the full AIR set per epoch and shard tables build one instance per shard, so the same walks re-ran dozens of times per prove. build_air now keeps a process-wide prototype cache keyed by (table name, proof options): the prototype is built and pre-captured once, and every later request clones it — Clone on AirWithBuses copies the derived meta, LogUp layout and the captured IR inside the OnceLock, never re-running the bodies. PAGE stays correct because its page base is part of its name. with_name/with_preprocessed apply to the caller's clone; the cached prototype stays pristine. Wall-neutral within noise on the 32-core box (the removed work is a few core-seconds against a ~580 core-second prove); cross-binary verification passes both ways. Also cuts AIR construction out of the monolithic path and the test suites. * profiling: re-home the toolkit spans onto the pipelined continuation flow The toolkit's continuation instrumentation assumed the sequential epoch loop. With the producer/builder/prover pipeline the stages run on different threads, so the spans move to where the work actually happens: - prove_continuation_total root span + timeline reset at entry, drained at the end exactly like the monolithic path (stdout tree + LAMBDA_VM_TIMELINE_JSON for phase_table.py). - epoch_execute / epoch_collect on the producer, epoch_trace_build on the builder pool, epoch_prove on the prove workers — each prove/build/ collect also opens an NVTX range with per-epoch identity (epoch_*[i=N]) for Nsight timelines. - Spans close BEFORE blocking channel sends, so backpressure waits are never booked as work. - prove_global span on the overlapped global-prove thread. * perf(prover): cache constraint-program lowering and share captured IR across clones * perf(prover): cache domain-derived values process-wide Domain and LdeTwiddles are now shared across epochs and concurrent epoch provers via a process-wide cache keyed by (field, trace_length, blowup, coset_offset). The OOD barycentric constants, FRI inverse twiddles, and the d=2 decomposition inverses hang off them as lazy per-domain values instead of being rebuilt (each an LDE-size-order batch inversion or clone) per table per epoch. * perf(prover): dedup boundary-zerofier inverses per (domain, step) Each boundary constraint paid its own LDE-size batch inversion even when sharing the step with its neighbours, and the vectors are identical for every table and epoch on the same domain. The inverted vector now lives in the shared domain, keyed by step, and constraints hold an Arc to it. * perf(gpu): keep boundary-zerofier columns resident on device Upload each distinct column once (GpuBaseVec, cached keyed by its host Arc — storing the Arc pins the allocation so the key can never alias) and D2D-copy into each dispatch's flat buffer, instead of re-uploading tens of MB per table per epoch over PCIe. * perf(gpu): keep the d=2 composition pipeline on device The composition evaluations stay resident after the fused kernel; a pointwise kernel decomposes them into the H0/H1 slabs, the batched slab LDE extends both halves with no H2D, and the parts handle feeds R4 DEEP. One drain of the final evaluations (still read by the commit tree and the query openings) replaces four codeword-sized PCIe trips per table per epoch. Falls back to downloading H and running the host decompose on any device failure. * perf(gpu): fold FRI directly from the device-resident DEEP codeword The fully-resident DEEP arm keeps its output on device, bit-reverses it into FRI order with a permutation kernel, and hands the buffer to the FRI fold state as its working codeword — removing the download / CPU-bit-reverse / re-upload round trip. The commit loop is shared between the host and device entries and restores the transcript on any mid-loop failure so the CPU path reruns cleanly. * fix(prover): keep lazy domain-cache initialization off the rayon pool The shared domain caches ran the parallel batch inversion inside their OnceLock initializers. A rayon worker that starts such an initialization farms chunks to the pool while sibling workers block on the same cell; with every worker parked the chunks never run and the prove deadlocks (observed as a full-process futex stall). Initializers now use the sequential inversion, and domain construction pre-fills every lazy cell from the setup thread so pool workers never run — or wait on — an initializer mid-prove. * chore(gpu): drop the unused DEEP download bridge and silence clippy * fix(prover): drain the epoch pipeline on error instead of stranding its senders The prove/build channel receivers live in the outer scope, so a worker that returned on error left the bounded senders parked in send() with no consumer — any mid-run proving error hung prove_continuation forever instead of surfacing. Workers now drain-and-discard until the channels disconnect, the producer stops executing epochs once an error is recorded, and the global-prove thread skips its (whole-prove-sized) run when the bundle can no longer be assembled. * fix(gpu): harden device-path edge cases from review - PendingD2H now synchronizes on drop: an error between enqueue and wait no longer releases the pinned slab to reuse/free while the DMA is in flight. - domain_and_twiddles re-checks the cache under the insert lock so a build race can't pin a duplicate instance's columns in the pointer-keyed device caches. - Hard-assert b_z_inv column length at the D2D copy (a short column left uninitialized VRAM in the kernel's window), mirror the batched-LDE input asserts in the split-trees entry, gate mismatched FRI twiddles to the CPU path, and pin the ext3 tower in the shared FRI drive. - Refresh the event-tracking safety note to the wait_ready_on contract. * test(prover): cover the epoch pipeline's mid-run error path A builder-injected fault (keyed by a magic private input, so it is stateless and inert for every real caller and for concurrent tests) fails epoch 3 of a ~9-epoch prove — enough pending work past the bounded channels' slack that a shutdown regression wedges instead of returning. The test runs the prove under a timeout so that regression fails CI rather than hanging it. * chore: fix profiling doc drift, untrack pycache, drop inert braces - The per-entry-point NVTX shape ranges were dropped when the math-cuda pipelines were rewritten; four doc sites still promised them and the nsys report mislabeled its innermost-range table. Align them with what the nvtx feature actually emits (mirrored instruments spans). - Untrack scripts/profiling/__pycache__ and ignore Python bytecode. - Remove ~86 brace wrappers in math-cuda left inert by the async-DMA refactor (kept the ones that scope real borrows) and reword three comments that referenced a deleted sync label. * style: cargo fmt * chore: keep working notes out of the tree * refactor(prover): prove continuation epochs on a single worker * chore: sync recursion bench lockfile with ecsm's num-integer dep * new opt * fix(gpu): harden round-2 residency paths after review Grid-stride the fused row-major NTT past gridDim.y (lde >= 2^24 silently fell back to CPU), assert the device-only contract in the R2 composition commit and preprocessed opening fallbacks, validate htod_via bounds, retain FRI device evals only under device-only, and move the inverse fault-injection hook so every batch-inverse entry is covered. * perf(prover): replace table chunks with a VRAM-admitted per-table scheduler Fiat-Shamir only requires the main roots absorbed in index order before the shared challenges; past that fork every table's chain is independent. Phase A now runs all main commits under a byte-budget admission gate (no chunk barriers), and aux build, aux commit and rounds 2-4 run fused as one task per table, heaviest first — while a big table works through a host-bound stretch, the other tables' GPU stages fill the device. GPU builds default TABLE_PARALLELISM to 2/3 of the cores (swept flat at 10 on a 16-core RTX 5090). ethrex 10tx continuations on RTX 5090: 10.64s -> 8.54s (-19.7%, 8 ABBA pairs). * perf(gpu): device-only preprocessed tables, lower LDE threshold, PCIe hygiene - Extend the device-only gate to preprocessed tables (BITWISE/DECODE): the split-trees path takes retain_host_lde, R4 openings serve both subsets from the device row gather (multiplicity range + precomputed range), and the is_preprocessed exclusion is gone. - Default GPU LDE threshold 2^19 -> 2^14: CPU-committed mid tables had no device handle, so every R2-R4 dispatch re-uploaded their LDE per round. - Multi-eval-point chunked barycentric kernels for R3 OOD (one pass over the LDE for all eval points, cols x chunks grid) with per-point fallback. - Device cache for domain coset points keyed by (len, p0, p1). - Pre-upload big main traces from the epoch builder thread; the R1 commit D2D-copies instead of paying the H2D in its chain. BITWISE is excluded (prove_epoch edits its multiplicities post-build) and update_multiplicities drops any stale pre-upload defensively. - scripts/profiling/h2d_histo.py: memcpy attribution histogram by NVTX phase and transfer size from an nsys sqlite export. * chore(gpu): clippy manual_range_contains on the bary multi asserts * chore(gpu): allow too_many_arguments on the split-trees wrapper * fix(gpu): keep the aux D2H when the GPU main commit fell back A static device-only gate on the aux commit could mark the trace device-only with no main GPU handle to serve it, turning a recoverable CPU fallback of the main commit into a hard abort downstream. * build(gpu): single-source the barycentric eval-point cap BARY_MAX_K (kernel accumulator array) and BARY_MAX_EVAL_POINTS (dispatch assert) were defined independently; build.rs now defines both from one constant, so they cannot drift into kernel stack corruption. * fix(gpu): verify the coset-cache invariant, cap trace pre-upload by VRAM budget The device coset cache keys on (len, p0, p1), which only determines the contents for a geometric sequence — verify it at sampled indices on insert. The builder's pre-uploaded traces ride ahead of the admission gate, so cap them to a slice of the device budget instead of competing with the prove peak on small cards. * fix(gpu): decouple the device-only envelope from the GPU commit threshold Lowering the commit threshold to 2^14 silently widened device-only to every mid-size table. The gate cannot mirror kernel-side dispatch eligibility, so a single R2 decline on one of those tables hard-aborts the prove (seen at 100tx once main's keccak rework landed) and deadlocks the epoch pipeline. GPU commits and resident handles keep paying from 2^14; dropping the host copy stays at the proven 2^19 envelope (LAMBDA_VM_GPU_DEVICE_ONLY_THRESHOLD overrides). * fix(gpu): device-only requires the d=2 composition path; name the table in the R2 abort The device-resident R2 path only exists for the d=2 quotient decomposition. DECODE proves with a single part, so admitting it to device-only skipped the whole device path and hard-aborted into the empty host trace, deadlocking the epoch pipeline at 100tx. Mirror the parts count in the gate, and include the table identity in the abort message — finding this one took a live-process backtrace because the message did not say which table died. * fix(gpu): default the trace pre-upload off Wall-neutral on the 5090 (the scheduler already hides the H2D) and its riding-ahead buffers sit outside the VRAM admission gate: at epoch 2^22 the real-block prove peaks at ~23 GiB and the extra 4 GiB pushed it into CUDA_ERROR_OUT_OF_MEMORY. Opt-in via LAMBDA_VM_TRACE_PREUPLOAD_MB. * fix(gpu): recover device-only tables by downloading the resident LDEs on an R2 miss The device-only gate is a static predicate over a dynamic dispatch: it cannot mirror every reason the device R2 path might decline (parts count, kernel eligibility, transient errors, shapes a new workload brings), and each miss was a hard abort that deadlocked the epoch pipeline — DECODE on the synthetic workload, then a second table on the real-block bench. Instead of excluding tables one by one, treat the resident handles as the source of truth: on a miss, download the main/aux LDEs back to host, clear the device-only flag, and continue on the host path. Slower for that table, never wrong; the abort remains only when the handles themselves cannot serve the data. gpu_device_only_downgrades() counts recoveries so a persistently-missing condition still gets mirrored into the gate. * feat(gpu): in-process cross-check diagnostics for device-side corruption LAMBDA_VM_GPU_XCHECK runs the verifier's composition consistency check inside the prover after round 3, per table at negligible cost; on a failure a post-mortem recomputes each device stage on host, reports the corruption shape, reruns the device chain to tell a transient race from a corrupted resident input, and aborts. LAMBDA_VM_GPU_FORCE_DOWNGRADE exercises the device-only R2 recovery end to end. The R2 downgrade path now names the table it recovered. A proof_diff ignored test structurally diffs two continuation bundles. * fix(gpu): drain-and-retry, then host downgrade, for resident-aux LDE declines A transient CUDA OOM on the resident aux LDE was a hard prove failure: the resident build leaves no host aux trace to fall back to. A device drain releases the concurrent VRAM peaks, so one retry usually keeps the table fully resident; if it still declines, download the resident aux trace (and the main LDE when the table is device-only) and continue host-backed. The drain before dropping the resident buffer also keeps kernels enqueued by the failed attempt from reading pool memory reused by a concurrent table. * fix(gpu): serialize the device R2 window to close a transient H corruption race Concurrent device R2 windows under VRAM pressure can transiently produce a fully wrong H for one or two tables while every input stays correct (rerunning the same chain on the same resident inputs matches the host), yielding a proof that fails the composition check. Serializing only the constraint-eval + decompose window across tables eliminates it; commits and host arms stay parallel, and the windows overlap rarely enough that the lock is near-free. LAMBDA_VM_GPU_SERIALIZE_R2=0 lifts the lock to bisect further or once the underlying race is found. * fix(gpu): keep already-present host buffers in the downgrade recovery A mixed state (one commit fell back to CPU while the other stayed device-only) left the recovery refusing to proceed: it treated a missing device handle as fatal even when that side already had a valid host copy. Only the missing side is downloaded now, and the R3 host-arm guards check the buffer they are about to read instead of the table-wide flag. * test(gpu): exercise the forced-downgrade recovery end to end LAMBDA_VM_GPU_FORCE_DOWNGRADE declines every device R2 path so each device-only table goes through materialize_lde_trace_host and finishes on the host evaluator; the test proves a small ethrex fixture with a lowered device-only threshold, asserts the downgrade counter moved and that the proof verifies. Wired into the test-cuda-fallback group. * fix(gpu): run the host decompose of a downloaded H outside the R2 lock The fallback arm (download H, host iFFT + LDEs) executed under the serialization lock, so under VRAM pressure — exactly when that arm runs — it serialized every other table's device window behind pure CPU work. The lock now covers only the device eval + decompose + the H download; the host decompose and every host arm run outside it. The lock is also acquired only for d=2 tables (the others never enter the device path). * chore(gpu): review follow-ups on the downgrade recovery set_host_data had been inserted between set_num_rows' doc and its signature, stealing its doc comment and un-gating it from the cuda feature; the serialization lock now recovers from poisoning instead of cascading PoisonErrors over the original panic; the downgrade counter joins reset_all_gpu_call_counters and the device-only residency test asserts it stays at zero on the happy path; stale comments about the aux gate mirroring the main gate rewritten with the actual contract. * chore(gpu): read the R2 serialize env var directly The OnceLock cache bought nothing — the var is consulted a handful of times per prove and does not change over the binary's lifetime. * style(gpu): drop needless refs in the coset-geometric assert * fix(gpu): review follow-ups on the round-4 residency PR (#937) Wrap the new gpu_force_downgrade target in GPU_TEST_TIMEOUT. That variable exists because a device-only cliff panic leaves the prover hung rather than aborting, holding the rented merge-queue box until the workflow timeout, and this target is the one that deliberately drives every device-only table through the decline path. Correct three comments that overstate or misdescribe what the code does: - DEFAULT_DEVICE_ONLY_MIN_LDE promises mid tables "degrade to CPU instead of aborting". That holds for the sites that read the LDE, which all gate on host_trace_empty(), but not for the R4 Merkle-proof gather: the host tree is root-only for every GPU-committed table whatever retain_host_lde says, so a declined gather has nothing to fall back to. Lowering the commit threshold widens that one abort site even though the device-only envelope is unmoved. - The new is_root_only assert claims the host walk would emit an empty path for position 0. get_proof_by_pos refuses root-only trees, so it panics instead — the assert's value is naming the cause, not preventing a bad proof. - gather_proofs_dev says callers fall back to the host tree on None. All three call sites .expect() and abort. Note that DEFAULT_GPU_LDE_THRESHOLD gates the whole dispatch layer, not just the commit, so moving it moves R2/R3/R4/FRI together. Document the four new env vars and h2d_histo.py in the profiling README, which is the toolkit's reference. Pin bary_num_chunks' three branches with unit tests, and cover the 64-chunk cap in the kernel parity tests — every existing case is rows-bound at 1-2 chunks, including the one annotated as exercising the occupancy branch. * fix flaky test --------- Co-authored-by: Diego K <43053772+diegokingston@users.noreply.github.com> Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>
…ution Align DMA memcpy with the EF's Accelerated Memory Operations standard
Collaborator
|
/bench |
Collaborator
|
/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. |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 20 pairs, per-side) | 2.556s | 2.568s | +0.46% 🔴 |
| Proof size (exact, 1 reading) | 115.67 MiB | 116.29 MiB | +0.53% 🔴 |
Per-side (
⚠️ PR REJECTS the baseline's valid proof — likely a VERIFY REGRESSION, not a format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.
pairs: 20 mean A (PR): 2.568s mean B (main): 2.556s
[parametric] paired-t mean +0.46% sd 0.85% se 0.19%
95% CI: [+0.06%, +0.86%] (t df=19 = 2.093)
[robust] median +0.57% Wilcoxon W+=166 W-=44 p(exact)=0.0215 (z=+2.26)
run-to-run jitter: A CV 0.59% B CV 0.49% (lower = steadier)
within-session drift: +0.12% over the run, 1st->2nd half -0.10%
🔴 REAL REGRESSION — PR verifies ~0.46% slower (paired-t and Wilcoxon agree).
ethrex 20-tx block · continuations, epoch 2^20 (4 epochs) · blowup=2, 219 queries
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 8 pairs, per-side) | 3.970s | 3.949s | -0.53% ⚪ |
| Proof size (exact, 1 reading) | 231.37 MiB | 233.84 MiB | +1.07% 🔴 |
Per-side (
⚠️ PR REJECTS the baseline's valid proof — likely a VERIFY REGRESSION, not a format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.
pairs: 8 mean A (PR): 3.949s mean B (main): 3.970s
[parametric] paired-t mean -0.53% sd 0.66% se 0.23%
95% CI: [-1.08%, +0.03%] (t df=7 = 2.365)
[robust] median -0.76% Wilcoxon W+=6 W-=30 p(exact)=0.1094 (z=-1.61)
run-to-run jitter: A CV 0.28% B CV 0.47% (lower = steadier)
within-session drift: +0.34% over the run, 1st->2nd half +0.08%
⚪ INCONCLUSIVE — effect not separable from 0 at n=8 (point estimate ~-0.76%). Add pairs to resolve.
Verify-time rows only: drift-free interleaved A/B/B/A, with paired-t and exact Wilcoxon — trust the verdict when the two agree. Proof sizes are single exact readings (no averaging). - = PR faster.
Recursion guest cycles — verifier running INSIDE the VM (main vs PR)
empty program · monolithic · blowup=2, 1 query (diagnostic — NOT a real verifier cost)
Single exact reading per ref — no ABBA: guest cycles are deterministic for a fixed
(guest ELF, input blob), so there is no machine drift to cancel.
| Metric | main | PR | Δ |
|---|---|---|---|
| Guest cycles | 331.7M | 332.8M | +1.1M (+0.34%) |
| Keccak calls | 3029 | 3091 | +62 |
baseline origin/main 8064a8efee guest=recursion-min.elf
PR 3c3a2a5e0e07c394b09037f5426c9f197a75c5c1 3c3a2a5e0e 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=8064a8efee4bd3edc9f064337d4e1d8bad54ae1a ref_b_elf=recursion-min.elf ref_b_cycles=331650450 ref_b_keccak=3029 ref_b_execute_wall_s=9
ref_a_sha=3c3a2a5e0e07c394b09037f5426c9f197a75c5c1 ref_a_elf=recursion-min.elf ref_a_cycles=332783220 ref_a_keccak=3091 ref_a_execute_wall_s=9
delta_cycles=1132770 delta_keccak=62
ethrex 20-tx block · continuations, epoch 2^21 (2 epochs) · blowup=2, 219 queries (128-bit)
Single exact reading per ref — no ABBA: guest cycles are deterministic for a fixed
(guest ELF, input blob), so there is no machine drift to cancel.
| Metric | main | PR | Δ |
|---|---|---|---|
| Guest cycles | 2280.0M | 2036.5M | -243.5M (-10.68%) |
| Keccak calls | 3538646 | 3287861 | -250785 |
baseline origin/main 8064a8efee guest=recursion-cont-blowup2.elf
PR 3c3a2a5e0e07c394b09037f5426c9f197a75c5c1 3c3a2a5e0e guest=recursion-cont-blowup2.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=8064a8efee4bd3edc9f064337d4e1d8bad54ae1a ref_b_elf=recursion-cont-blowup2.elf ref_b_cycles=2280036712 ref_b_keccak=3538646 ref_b_execute_wall_s=37
ref_a_sha=3c3a2a5e0e07c394b09037f5426c9f197a75c5c1 ref_a_elf=recursion-cont-blowup2.elf ref_a_cycles=2036495266 ref_a_keccak=3287861 ref_a_execute_wall_s=34
delta_cycles=-243541446 delta_keccak=-250785
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.