Feat/hint ecall - #876
Conversation
|
/bench |
Benchmark — ethrex 20 transfers (median of 3)Table parallelism: auto (cores / 3)
Commit: 71ba613 · Baseline: cached · Runner: self-hosted bench |
|
Benchmark Results for modified programs 🚀
|
|
/ai-review |
Codex Code Review
|
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
| /// We compute the recovery directly rather than calling k256's | ||
| /// `recover_from_prehash`, which internally runs a *second* lincomb to | ||
| /// re-verify the key — doubling the ECSM ecalls for no gain here. | ||
| /// Obtain a 32-byte big-endian hint for `x_be` via the executor `hint` ecall |
There was a problem hiding this comment.
get_hint was inserted between ecsm_ecrecover's doc block and its signature, so the 17-line doc comment above (lines 63-79: "Recover the uncompressed public key bytes … doubling the ECSM ecalls for no gain here.") now documents get_hint, and ecsm_ecrecover ends up undocumented. Move the three new helpers above line 63 (or below ecsm_ecrecover).
| /// then `Q = A + B` is one affine addition. All three inversions are batched. | ||
| /// | ||
| /// Generic over the oracle so unit tests can substitute a software stand-in. | ||
| /// Base-field inverse `x⁻¹ mod p`. On riscv64 the host supplies it via the |
There was a problem hiding this comment.
Same doc-misattachment here: field_inv is inserted between lincomb2_with_oracle's doc block and its #[cfg]/signature, so the whole chord-addition derivation ("The lambda-vm ECSM precompile returns only x(k·P) … Generic over the oracle so unit tests can substitute a software stand-in.") now documents field_inv, and lincomb2_with_oracle loses its docs. Move field_inv above that doc block.
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 · 24 changed files Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-001: Missing MEMW register reads for Hint ecall operands in trace builder
Claim collect_hint_ops reads registers x10, x11, x12 but does not emit MEMW register-read operations or update register_state timestamps, unlike collect_ecsm_ops which does both. Evidence In collect_hint_ops (lines 1080-1120), hint_id/in_addr/out_addr are read via register_state.read() but no MemwOperation is pushed for these register reads and register_state.write() is not called to update timestamps. In contrast, collect_ecsm_ops (lines 882-980) explicitly creates MEMW register reads for x11, x12, x10 at timestamps T, T+1, T+2 and calls register_state.write() after each. The CPU's register collector (collect_register_ops_from_cpu) only handles regular instruction registers (rs1/rs2/rd), not ecall argument registers (a0-a7). Suggested fix Either explicitly emit MemwOperation rows for x10/x11/x12 (matching the pattern of the other ECALL handlers) and advance register_state.write(..., t), or extend the doc comment to explain why omitting them is sound (currently it only justifies the memory-side omission). Consistency with the other ECALL handlers is the safest choice. AI-005: Doc comment above ecsm_ecrecover is malformed (extra doc paragraph for get_hint merged into ecsm_ecrecover's block)
Claim The PR adds a new doc-comment block for fn get_hint but inserts it inline in the middle of fn ecsm_ecrecover's existing doc comment (between its existing trailing description and its body), producing a single oversized /// block that rustdoc will attribute to ecsm_ecrecover rather than get_hint. Functionally harmless but the documentation is now misleading: Evidence Lines 74-93: the text starting at line 83 ('Obtain a 32-byte big-endian hint for Suggested fix Close the ecsm_ecrecover doc block with AI-006: Hint guest .cargo/config.toml has CC/CFLAGS but ecsm/keccak guests do not — likely inconsistent copy-paste from ethrex
Claim The new hint_min and hint_multi .cargo/config.toml files duplicate the CC_riscv64im_lambda_vm_elf / CFLAGS_riscv64im_lambda_vm_elf block from ethrex/ckzg, but the simpler ecsm and keccak guests (which use the same lambda-vm-syscalls dependency) build without it. The hint_min/hint_multi source uses no Evidence Programs using lambda-vm-syscalls with std (ethrex, ckzg) set CC/CFLAGS; programs using syscalls without std (ecsm, keccak) don't. hint_min / hint_multi use syscalls without std but copy the CC/CFLAGS block verbatim from ethrex. Suggested fix Drop the [env] CC/CFLAGS section from hint_min and hint_multi (they don't need a C linker for std), or — if they are required for these specific builds — document why in a comment so the difference vs ecsm/keccak isn't mysterious. AI-009: debug_assert on hint timestamp <= u32::MAX is the only defense against T_hi != 0
Claim generate_hint_trace debug-asserts op.timestamp <= u32::MAX so TIMESTAMP_1 is 0 and matches the CPU's ECALL send (which always sends ts_hi=0). The assert disappears in release builds; if a future change ever pushes a timestamp above u32::MAX, the HINT table would silently produce TIMESTAMP_1 != 0 and unbalance the bus only when verifier inputs the malicious trace. ECSM does not have an equivalent guard. This is a latent soundness cliff rather than an active bug. Evidence prover/src/tables/hint.rs line 86-90: Suggested fix Either (a) make the assert a runtime error (return Err) so it cannot be optimized away, or (b) document the invariant in the bus_interactions() comment so any future contributor doesn't bypass it, or (c) drop the assert and add a transition constraint on TIMESTAMP_1 == 0 in the HINT AIR. 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 |
1 participant
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.