Feat/hint ecall - #876
Conversation
|
/bench |
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 47024 MB | 46980 MB | -44 MB (-0.1%) ⚪ |
| Prove time | 157.521s | 140.811s | -16.710s (-10.6%) 🟢 |
🎉 Improvement on the real block — prove time down 10.6%.
Prove-time spread 0.3% (140.604s / 140.982s / 140.811s)
Commit: 02d8168 · Baseline: cached · Runner: self-hosted bench
|
/ai-review |
Codex Code Review
|
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
Review — Hint ecallThe mechanics are well built and the docs are unusually thorough about why each piece exists. The wins are real and the plumbing (Ecall receive + 4 MEMW write sends, CriticalThe HINT row's The This breaks the PR's stated soundness anchor. The "Soundness surface" section argues the guest's HighNothing prevents this from reaching a production proof. ( Medium
Low
Checked, no issue foundGuest-side verifies are correct: the |
AI ReviewPR #876 · 38 changed files
Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-002: executor/Cargo.toml k256 dep comment "BENCH ONLY" is inaccurate — it is used in production proving
Claim The dependency comment says k256 is for host-side hint computation and is 'BENCH ONLY', but Evidence
Suggested fix Drop the AI-007: Unused import in new HINT table
Claim
Evidence Line 60 of Suggested fix Remove AI-008: Disk-spill sizing omits HINT table rows
Claim
Evidence
Suggested fix Add a Reviewer Lanes
Verification Lanes
Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report. Discarded candidates (4) — rejected by the verifier
Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts. |
|
/bench |
|
/bench |
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.
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.
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.
…t comments #899 corrected the same two stale comments this branch had already fixed locally: the k256 dependency label, which claimed BENCH ONLY for a prove-path dependency, and hint_min's claim that the ethrex call site is unaligned. Both conflicts resolve to #899's version, which states the same facts, so the two local comment commits are superseded. The output-address range-check and the selector-bound commits touch different files and are unaffected.
|
/bench |
|
/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. |
|
/bench-gpu |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 20 pairs, per-side) | 3.058s | 3.057s | -0.04% ⚪ |
| Proof size (exact, 1 reading) | 155.88 MiB | 156.27 MiB | +0.25% 🔴 |
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): 3.057s mean B (main): 3.058s
[parametric] paired-t mean -0.04% sd 0.56% se 0.13%
95% CI: [-0.30%, +0.22%] (t df=19 = 2.093)
[robust] median +0.03% Wilcoxon W+=105 W-=105 p(exact)=1.0000 (z=+0.02)
run-to-run jitter: A CV 0.56% B CV 0.49% (lower = steadier)
within-session drift: -0.05% over the run, 1st->2nd half -0.04%
⚪ INCONCLUSIVE — effect not separable from 0 at n=20 (point estimate ~+0.03%). Add pairs to resolve.
ethrex 20-tx block · continuations, epoch 2^20 (9 epochs) · blowup=2, 219 queries
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 8 pairs, per-side) | 8.182s | 8.169s | -0.15% ⚪ |
| Proof size (exact, 1 reading) | 470.68 MiB | 474.18 MiB | +0.74% 🔴 |
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): 8.169s mean B (main): 8.182s
[parametric] paired-t mean -0.15% sd 1.49% se 0.53%
95% CI: [-1.40%, +1.09%] (t df=7 = 2.365)
[robust] median -0.15% Wilcoxon W+=14 W-=22 p(exact)=0.6406 (z=-0.49)
run-to-run jitter: A CV 0.66% B CV 0.99% (lower = steadier)
within-session drift: +0.07% over the run, 1st->2nd half -0.17%
⚪ INCONCLUSIVE — effect not separable from 0 at n=8 (point estimate ~-0.15%). 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 | 460.1M | 463.3M | +3.2M (+0.69%) |
| Keccak calls | 2994 | 3029 | +35 |
baseline origin/main 8b88a8d676 guest=recursion-min.elf
PR 2c3b3e8c0027bd73665a5b61118bc03fe98db3a6 2c3b3e8c00 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=8b88a8d676280d25de7e8690423a502c55f6ec27 ref_b_elf=recursion-min.elf ref_b_cycles=460138973 ref_b_keccak=2994 ref_b_execute_wall_s=9
ref_a_sha=2c3b3e8c0027bd73665a5b61118bc03fe98db3a6 ref_a_elf=recursion-min.elf ref_a_cycles=463311810 ref_a_keccak=3029 ref_a_execute_wall_s=9
delta_cycles=3172837 delta_keccak=35
ethrex 20-tx block · continuations, epoch 2^21 (main 5 / PR 3 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 | 4860.3M | 3191.8M | -1668.5M (-34.33%) |
| Keccak calls | 6807496 | 4263971 | -2543525 |
baseline origin/main 8b88a8d676 guest=recursion-cont-blowup2.elf
PR 2c3b3e8c0027bd73665a5b61118bc03fe98db3a6 2c3b3e8c00 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=8b88a8d676280d25de7e8690423a502c55f6ec27 ref_b_elf=recursion-cont-blowup2.elf ref_b_cycles=4860321552 ref_b_keccak=6807496 ref_b_execute_wall_s=79
ref_a_sha=2c3b3e8c0027bd73665a5b61118bc03fe98db3a6 ref_a_elf=recursion-cont-blowup2.elf ref_a_cycles=3191814035 ref_a_keccak=4263971 ref_a_execute_wall_s=50
delta_cycles=-1668507517 delta_keccak=-2543525
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.
…ints 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.
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.
`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.
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.
MauroToscano
left a comment
MauroToscano
left a comment
There was a problem hiding this comment.
Blocking on one concrete item, plus a process point about the approval. The feature itself reviewed well — the verify-then-fallback design survived an adversarial pass (5,138 end-to-end ecrecover comparisons plus ~7,000 per-seam, debug and release, against the vendored k256) and I could not find a hint for which field_inv, scalar_inv or decompress_r returns anything other than the software result. This is not about the design.
Blocking: the tests that validate the operand checks never run in CI
test-executor runs only --test asm, --test rust, --test flamegraph, and a test_ckzg-filtered --ignored step. Because executor/src/lib.rs is #[cfg(test)] pub mod tests;, everything under executor/src/tests/ is a lib target that no CI command selects. I checked every cargo test / nextest invocation in the workflow — the nextest archive is scoped -p lambda-vm-prover -p stark -p crypto -p ecsm, executor absent.
Concretely: the tests covering HintUnknownSelector, HintAddressOverflow (both operands, plus the accepted 2^32 − 32 boundary) and compute_hint's three selectors — including the ones added by 5c55e4c1 — are not executed anywhere. The soundness-relevant validation this PR added is unverified by CI.
The fix is one step in an already-required job, with no added compile time (the lib test binary is already built by the test_ckzg step):
- name: Run executor lib unit tests
run: cargo test --release -p executor --libThe mechanism is pre-existing — ecsm_tests, keccak_tests and memory_tests are equally dark — so this is not a regression introduced here. But this PR is what makes it matter.
#905 carries that fix, along with three still-stale comments and three test gaps, and targets this branch so merging it folds everything in. It is green. Merging it first is the smallest path; cherry-picking d7380474 alone would also unblock.
Process: the approval predates all of the soundness work
The current approval is from be9066bf (2026-07-31). Head is now 2c3b3e8c — 20 commits later, and the operand-binding work is entirely inside that window:
c2283bfbBind and range-check the HINT ecall operands5c55e4c1Range-check the HINT output address low limb, like the input oned3a85f49Derive the HINT selector bound from the executor's accepted set- plus two main merges and
#899
Those commits are the AIR's soundness surface — they are what make the table's accepted set match the executor's. They have not been reviewed by the approver. Worth a fresh look before merge, independent of the CI item above.
For what it is worth, I reviewed them and they are good: 5c55e4c1 is complete (bus interaction, the matching LtOperation, lt_count += 2 → += 3, and with_capacity(26) → 27), and d3a85f49 is better than the const-assert I had proposed — is_valid_hint_selector as a single source of truth with set equality asserted in both directions catches a fourth selector added below the bound, which mine would not have. I dropped mine in favour of it.
Two non-blocking asks
The body's numbers are stale: 41 columns not 37, and 27 bus interactions after 5c55e4c1, not 22. The Details and "In the AIR" sections also omit the x10/x11 bindings and the LT range-checks — which are exactly the checks an auditor most needs to see, since they are what align the AIR with the executor.
The Impact table needs re-baselining. 5fd961a0 was the right control when written, but 9ccdaf28 (#861, guest thin LTO — its own commit message measures −2.28%/−2.37% guest cycles on the ethrex fixtures) and d83b4d9e (#863, GPU continuation proving) have landed between it and this branch. Roughly 2 points of the −44.1% belong to #861.
More importantly the fixture is unrepresentative: this PR's own /bench on the real block reports −10.4% prove time and +2.1% peak heap against the body's −32% / −35%. The two reconcile — 3 hints per ecrecover × 29 ecrecovers × ~67k cycles ≈ −11% of the real block's 50.78M guest cycles — because the 20-transfer fixture runs 9.16 ECSM per Mcycle versus a real block's 2.28, so the work this PR accelerates is ~4× denser there. The win is real and well separated (0.7% spread); the suggestion is just to lead with the real-block number. The +2.1% heap is not this table — a marginal always-on AIR measures ~5 MB — it is that cutting guest cycles packed the same crypto into 11 epochs instead of 13.
Merge-order hazard, for whoever lands this
#874 also takes FIXED_TABLE_COUNT 10 → 11, at byte-identical lines (86, 546, 621). Whichever merges second must resolve to 12, not keep 11. prove_elfs_tests.rs:2825 asserts the length — but nothing asserts the two AIR lists agree in order, and lines 546 and 621 are separate conflict hunks, so an independent resolution can order hint and dma differently in the prover and verifier lists. That surfaces only as a prove/verify failure. ~10 lines zipping the lists by name would close it permanently. #896 stacks on #874 and #879 on this branch, so it is a four-PR sequence.
Review follow-ups for #876: the CI gap, three stale soundness comments, and three test gaps
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.
905ff68 to
02d8168
Compare
MauroToscano
left a comment
MauroToscano
left a comment
There was a problem hiding this comment.
Lifting my change request — the blocking item is fixed.
#905 merged, so feat/hint-ecall now carries both:
cargo test --release -p executor --libin thetest-executorjob, so the tests coveringHintUnknownSelector,HintAddressOverflowand the three selectors actually run. Those include the ones5c55e4c1added, which were previously unexecuted anywhere.test-ethrex-cryptorunning both profiles. k256 0.13.4 swaps itsFieldElementimplementation ondebug_assertions, and the guest ships--release— so the hint-verification tests had been exercising an implementation the guest never compiles, in the one workflow step without--release.
Verified both are present on the branch; CI is running.
On the operand work that landed after the original approval — I reviewed those commits and they hold up:
5c55e4c1is complete, not just similarly named: the thirdBusInteraction, the matchingLtOperationin the trace builder,lt_count += 2 → += 3, and the capacity bump. It derives the same 7-value window independently.d3a85f49is better than theconst _: () = assert!I had proposed and supersedes it —is_valid_hint_selectoras a single source of truth with set equality asserted in both directions catches a fourth selector added below the bound, which mine would not have. I dropped mine in its favour.
The design itself I could not break: an adversarial sweep of 5,138 end-to-end ecrecover comparisons plus ~7,000 per-seam, debug and release against the vendored k256, found no hint for which field_inv, scalar_inv or decompress_r returns anything other than the software result, and the fallback cannot be skipped.
Two things left for whoever merges, neither blocking:
Merge order with #874. Both take FIXED_TABLE_COUNT 10 → 11 at byte-identical lines (86, 546, 621). Whichever lands second must resolve to 12. prove_elfs_tests.rs:2825 asserts the length, but nothing asserts the two AIR lists agree in order — and 546 and 621 are separate conflict hunks, so an independent resolution can order hint and dma differently in the prover and verifier lists, which surfaces only as a prove/verify failure. ~10 lines zipping the lists by name would close it permanently. #896 stacks on #874 and #879 on this branch, so it is a four-PR sequence.
Body numbers are stale — 41 columns not 37, and 27 bus interactions after 5c55e4c1, not 22; and the Impact table is baselined at 5fd961a0, which predates #861's guest thin LTO (worth ~2 points of the −44.1%). The real-block /bench on this PR reports −10.4% prove time and +2.1% peak heap against the body's −32%/−35%; the two reconcile via ecrecover density, and the heap delta is the epoch-count shift, not the new table. Worth leading with the real-block figure.
|
/bench |
4 participants
What
Adds a
Hintecall (u64::MAX - 20): the executor computes a value that is expensive in theguest and cheap to check — secp256k1 field inverse, scalar inverse, field square root — writes
it into guest memory, and the guest verifies it with ordinary constrained instructions and
recomputes it in software if the check fails. The call site is ecrecover's inversions and
root in
crypto/ethrex-crypto/src/lib.rs. AHINTtable puts the ecall's direct memory writesinto the memory argument.
Why
The flamegraph of a hinted ethrex block put field and scalar inversion plus square root at
most of the guest's cycles: each software inversion is thousands of instructions, while
checking one is a single multiplication. The ecall moves the computation to the host and keeps
the check in-circuit.
Details
executor/src/vm/instruction/execution.rs):a0selects the operation(
HINT_FIELD_INV,HINT_SCALAR_INV,HINT_FIELD_SQRT),a1anda2point at the input andoutput buffers, both 32-byte big-endian (k256's own serialization).
compute_hintuses the samek256 arithmetic the guest verifies against; a numeric failure (non-canonical input, no
inverse/sqrt) returns zeros, which the guest treats as a failed check and recomputes in
software. An unrecognized selector is rejected up front (
HintUnknownSelector) rather thanproducing a silent zero.
receives the ecall on the
Ecallbus, readsx12through the memory argument to bind theoutput address, sends the four 8-byte
MEMWwrites of the output atout_addr+0/8/16/24, andrange-checks the 32 output cells. The ecall writes guest memory directly, bypassing the
load/store decode, so without those sends the output's initial→final memory chain is
unexplained and the memory argument does not balance. The input read is deliberately not
modelled: a read leaves the value unchanged and the guest supplied the input with ordinary
stores.
syscalls/src/syscalls.rs) and the call site incrypto/ethrex-crypto/src/lib.rs:scalar_inv,decompress_rand the field inverse verify thehinted value, and fall back to a software computation if it does not check out (see Soundness
surface). The output buffer is 8-byte aligned so its writes take the aligned memory path
(
MEMW_A) rather than the general one.hint_min(one call, commits the result) andhint_multi.Compatibility
Like the ECSM accelerator (#657), this adds an always-on table, so
FIXED_TABLE_COUNTgoes10 → 11 and the recursion verifier checks 11 tables. Prover and verifier are built from the same
code and move in lockstep, so the only operational cost is regenerating existing proofs and the
pinned recursion ELFs.
Impact (ethrex 20-tx block, vm-benchmarks-1, 5 interleaved rounds, all verify ✅)
Comparison is with-hints vs without-hints: baseline =
5fd961a0, the point onmainthis branchwas cut from (the same code before the hint ecall), proven by its 10-table prover; treatment =
this branch, proven by its 11-table prover. Medians:
ECSM calls unchanged at 80 and keccak permutations at 411 on both sides: no cryptographic work
is skipped, its inversions and roots just stop costing thousands of guest cycles each. Variance
was ~1–1.5% (prove-time CV) with clean separation.
Soundness surface
The table constrains nothing about which value was hinted — that is deliberate and it is
what makes the ecall cheap. Soundness comes from two places: what the AIR constrains (where the
value lands, that it is 32 bytes, and that the multiplicity is boolean) and what the guest
enforces (that the value is correct, or else recomputed in software).
In the AIR:
out_addris bound tox12by aMEMWregister read at the ecall timestamp. The four writeaddresses come from a trace column, so without that binding the witness picks the destination
and the table is an arbitrary-memory-write gadget — something the in-guest verify cannot
contain, since the adversary just targets a different buffer.
table that writes fresh values into memory (STORE, KECCAK, ECSM, PAGE) checks its own cells;
otherwise the witness can keep the linear combination consistent while encoding field elements
outside
[0, 256)where loads and the ALU expect bytes.mu, the multiplicity gating every interaction, is bit-constrained (mu·(1−mu) = 0), matchingevery other multiplicity-column table (ECSM/ECDAS/COMMIT/STORE/MEMW_R). The
Ecallbus alonedoes not give this: its tuple carries a free timestamp column, so LogUp pins only the sum of
muover the rows sharing a tuple — a1/2 + 1/2split would satisfy it. The bit constraintmakes the argument local instead of resting on how MEMW handles its own multiplicities
downstream.
In the guest (verify-then-fallback). A hinted value is untrusted and prover-chosen, so it
may only ever save work — never change the answer. That rules out two failure modes, not one:
x·inv == 1for the inverses,y² == x³+7plus parity selection for the root. All three verify by difference rather thanct_eq, because k256 compares magnitude and normalization tags too — a naive comparison nevermatches.
"the value is invalid"; the guest recomputes in software.
scalar_invfalls back toinvert_vartime(its caller guaranteesr ≠ 0, so a failed check means the host lied);decompress_rfalls back toAffinePoint::decompress(a genuine non-residue must still yieldNone). Without this, a prover feeding garbage could turn a valid signature into a recoveryfailure — ECRECOVER returns empty — making honest and attacked executions both provable with
different state roots. An unknown selector is a hard ecall error for the same reason.
constraint. The consistency test in this PR catches an inconsistent trace, which is the
failure mode of a buggy trace builder, not of an adversary.
The guarantee is therefore a property of the program, not of the machine, and it extends to
every future call site. Constraining the value in the AIR instead (
out·in == 1) is possibleand costs rows; the guest already performs exactly that multiplication.
The ecall validates that both 32-byte operands stay inside their low 32-bit address limb,
since the tables send addresses as
[lo32, hi32]with the per-write offset added tolo32alone.