Perf/dma tail wide memset - #896
Draft
diegokingston wants to merge 15 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 | 47024 MB | 47898 MB | +874 MB (+1.9%) ⚪ |
| Prove time | 157.521s | 137.337s | -20.184s (-12.8%) 🟢 |
🎉 Improvement on the real block — prove time down 12.8%.
Prove-time spread 2.0% (135.223s / 137.337s / 137.929s)
Commit: d1980c6 · Baseline: cached · Runner: self-hosted bench
Collaborator
|
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>
# 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
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
4 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.