Feat/hint ecall

[jotabulacios]

What

Adds a Hint ecall (u64::MAX - 20): the executor computes a value that is expensive in the
guest 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. A HINT table puts the ecall's direct memory writes
into 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

• The ecall (executor/src/vm/instruction/execution.rs): a0 selects the operation
  (HINT_FIELD_INV, HINT_SCALAR_INV, HINT_FIELD_SQRT), a1 and a2 point at the input and
  output buffers, both 32-byte big-endian (k256's own serialization). compute_hint uses the same
  k256 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 than
  producing a silent zero.
• HINT table (37 columns, one boolean constraint, 22 bus interactions, one row per call):
  receives the ecall on the Ecall bus, reads x12 through the memory argument to bind the
  output address, sends the four 8-byte MEMW writes of the output at out_addr +0/8/16/24, and
  range-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.
• Guest wrapper (syscalls/src/syscalls.rs) and the call site in
  crypto/ethrex-crypto/src/lib.rs: scalar_inv, decompress_r and the field inverse verify the
  hinted 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.
• Two test guests, hint_min (one call, commits the result) and hint_multi.

Compatibility

Like the ECSM accelerator (#657), this adds an always-on table, so FIXED_TABLE_COUNT goes
10 → 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 on main this branch
was 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:

Metric	main	hint	Δ
Prove time	25.134 s	17.100 s	−32.0%
Peak heap	50.39 GiB	32.78 GiB	−35.0%
Proof size	158.5 MiB	121.9 MiB	−23.1%
Guest cycles	9,098,740	5,087,162	−44.1%

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_addr is bound to x12 by a MEMW register read at the ecall timestamp. The four write
  addresses 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.
• The 32 output cells are range-checked as bytes. MEMW range-checks nothing it receives, so every
  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), matching
  every other multiplicity-column table (ECSM/ECDAS/COMMIT/STORE/MEMW_R). The Ecall bus alone
  does not give this: its tuple carries a free timestamp column, so LogUp pins only the sum of
  mu over the rows sharing a tuple — a 1/2 + 1/2 split would satisfy it. The bit constraint
  makes 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:

• Accepting a wrong value is caught by the in-guest check: x·inv == 1 for the inverses,
  y² == x³+7 plus parity selection for the root. All three verify by difference rather than
  ct_eq, because k256 compares magnitude and normalization tags too — a naive comparison never
  matches.
• Steering a rejection is not left to the hint either. A failed check is not treated as
  "the value is invalid"; the guest recomputes in software. scalar_inv falls back to
  invert_vartime (its caller guarantees r ≠ 0, so a failed check means the host lied);
  decompress_r falls back to AffinePoint::decompress (a genuine non-residue must still yield
  None). Without this, a prover feeding garbage could turn a valid signature into a recovery
  failure — 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.
• A witness that writes the same wrong value in both the HINT and MEMW rows satisfies every
  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 possible
and 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 to lo32
alone.

[jotabulacios]

/bench

[github-actions]

Benchmark — ethrex 20 transfers (median of 3)

_{Table parallelism: auto (cores / 3)}

Metric	main	PR	Δ
Peak heap	50217 MB	30877 MB	-19340 MB (-38.5%) 🟢
Prove time	24.695s	16.628s	-8.067s (-32.7%) 🟢

🎉 Improvement detected — heap or time decreased by more than 5%.

✅ Low variance (time: 3.1%, heap: 1.0%)

_{Commit: 64a22ff · Baseline: cached · Runner: self-hosted bench}

[github-actions]

Benchmark Results for modified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head ecsm	3.2 ± 0.1	3.1	3.3	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head hashmap	111.2 ± 1.5	109.2	113.8	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head keccak	128.9 ± 4.3	122.6	136.9	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head syscall_commit	90.3 ± 0.7	89.7	91.6	1.00

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

• High — HINT writes are not bound to the syscall’s a2 output pointer. hint.rs:142 receives only the timestamp/syscall, then uses an unconstrained out_addr for memory writes. A malicious prover can therefore inject the hinted bytes at any address, diverging from executor semantics and potentially altering unrelated VM state. Add a constrained MEMW register-read interaction linking out_addr to x12, as the ECSM table does.

[claude]

Review — Hint ecall

The 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, collect_hint_ops mirroring collect_ecsm_ops, Makefile globbing the new guests, FIXED_TABLE_COUNT/air_refs kept in sync) looks correct. I found one soundness gap that is materially worse than the one the PR body documents, plus a set of doc/cleanup items. Details inline.

Critical

The HINT row's out_addr is unconstrained — this is an arbitrary-memory-write, not just an unconstrained value. (prover/src/tables/hint.rs)

The Ecall receive carries [ts, syscall]; nothing binds ADDR_OUT_0/1 to the ecall's a2. Both existing ecall receivers do bind their operands to the register file — ecsm.rs:318 reads x11/x12/x10, keccak.rs:185 "read register x10 to bind addr". So a prover chooses any address and any 32 bytes, emits matching MEMW writes, and the memory argument balances.

This breaks the PR's stated soundness anchor. The "Soundness surface" section argues the guest's x·inv == 1 / y² == x³+7 check rejects a wrong value — true, but irrelevant when the write can be redirected: aim it at the recovered pubkey, EVM state, or the commit buffer and no verify is in the path at all. Fix is the ECSM pattern: bind x12 via a MEMW register read at T on both the bus and in collect_hint_ops.

High

Nothing prevents this from reaching a production proof. (executor/src/vm/instruction/execution.rs) All "BENCH ONLY" markers are comments. The syscall is live in the default executor build, HINT is in FIXED_TABLE_COUNT for every proof, and any guest can call it. A default-off cargo feature (syscall recognition + k256 dep + table + AIR slot) would make the bench possible and the hole impossible.

Medium

• prover/src/tests/prove_elfs_tests.rs — the forgery test's doc claims the test makes "the hint value load-bearing"; it only catches an internally inconsistent trace. The PR body says the opposite, correctly.
• crypto/ethrex-crypto/src/lib.rs — two insertions land between an existing doc block and its function, so ecsm_ecrecover and lincomb2_with_oracle both lose their docs to the new helpers.

Low

• prover/src/tables/hint.rs:37 re-declares HINT_SYSCALL_NUMBER instead of importing it (ecsm.rs imports).
• Stray [env] CC/CFLAGS block in both new guests' .cargo/config.toml (only C-dependent guests need it).
• hint_min's module doc overstates the bus surface (no read is modelled) and the alignment requirement (unaligned routes to general MEMW; the ethrex call site is unaligned anyway).
• MU is unconstrained under EmptyConstraints — a boolean constraint or a note on why the Ecall receive suffices.

Checked, no issue found

Guest-side verifies are correct: the normalizes_to_zero comparisons and the negate(1)-vs-Neg magnitude reasoning hold; a zeros-on-failure hint is rejected by every one of the three checks; the parity re-selection in decompress_r is safe because x³+7 = 0 has no solution over F_p (secp256k1 has odd prime order, so no 2-torsion). Executor/trace-builder byte order agrees (both little-endian-packed in address order), addr_limb_ok bounds rule out addr + 24 overflow, MemoryState is image-backed so collect_hint_ops can't diverge from the executor on rodata inputs, and unaligned buffers are handled (executor store_doubleword byte path, prover general MEMW route).

[github-actions]

AI Review

PR #876 · 38 changed files

Warning: the diff was truncated before review.

Findings

Status	Sev	Location	Finding	Found by
confirmed	low	executor/Cargo.toml:10	executor/Cargo.toml k256 dep comment "BENCH ONLY" is inaccurate — it is used in production proving	glm openrouter/z-ai/glm-5.2 kimi openrouter/moonshotai/kimi-k2.7-code
confirmed	low	prover/src/tables/hint.rs:60	Unused import in new HINT table	kimi openrouter/moonshotai/kimi-k2.7-code
confirmed	low	prover/src/tables/trace_builder.rs:3774	Disk-spill sizing omits HINT table rows	kimi openrouter/moonshotai/kimi-k2.7-code

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

• Status: confirmed
• Severity: low
• Location: executor/Cargo.toml:10
• Found by: glm:openrouter/z-ai/glm-5.2, kimi:openrouter/moonshotai/kimi-k2.7-code
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

The dependency comment says k256 is for host-side hint computation and is 'BENCH ONLY', but compute_hint (which needs k256) is called unconditionally from the production trace builder, not just benchmarks/tests.

Evidence

executor/src/vm/instruction/execution.rs::compute_hint is pub and uses k256::FieldElement/Scalar (from_bytes, invert, sqrt). It is invoked from prover/src/tables/trace_builder.rs:1010 inside collect_hint_ops, which runs during every production Traces::from_elf_and_logs/collect_epoch build for any program issuing a hint ecall — not only under a bench feature or #[cfg(test)]. The Cargo.toml comment # Host-side computation of non-constraining hints ... BENCH ONLY. is therefore misleading.

Suggested fix

Drop the BENCH ONLY qualifier from the comment (e.g. # Host-side computation of non-constraining hints (modular inverse / sqrt) for the Hint ecall — same k256 arithmetic the guest verifies against.), so a future maintainer does not attempt to feature-gate or demote k256 to a dev-dependency and break production proving.

AI-007: Unused import in new HINT table

• Status: confirmed
• Severity: low
• Location: prover/src/tables/hint.rs:60
• Found by: kimi:openrouter/moonshotai/kimi-k2.7-code
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

prover/src/tables/hint.rs imports VmTable from super::types but never uses it, leaving dead code in a newly added table file.

Evidence

Line 60 of prover/src/tables/hint.rs contains use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable};. Searching the file shows no reference to VmTable.

Suggested fix

Remove VmTable from the import list.

AI-008: Disk-spill sizing omits HINT table rows

• Status: confirmed
• Severity: low
• Location: prover/src/tables/trace_builder.rs:3774
• Found by: kimi:openrouter/moonshotai/kimi-k2.7-code
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

count_table_lengths (used for disk-spill peak-heap estimation) does not count HINT table rows, so programs that make many hint ecalls will have underestimated table lengths. The same omission already exists for ECSM, but the PR introduces a new fixed-size table and should account for it.

Evidence

prover/src/tables/trace_builder.rs lines 3774-3956 define count_table_lengths, which counts cpu, memw, memw_aligned, memw_register, load, lt, shift, mul, dvrm, branch, commit, decode, pages, etc. There is no hint_count field in TableLengths and no counting of cpu_op.ecall_hint. In contrast, the actual trace builder (collect_ops_from_cpu and build_traces) generates a hint trace with one padded row per hint ecall.

Suggested fix

Add a hint_padded_rows field to TableLengths and increment a hint_count counter when cpu_op.ecall_hint is true in the count_table_lengths pass, mirroring how other fixed tables are sized.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings
glm	openrouter/z-ai/glm-5.2	general	success	1
kimi	openrouter/moonshotai/kimi-k2.7-code	general	success	3
minimax	minimax/MiniMax-M3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
moonmath	zro/minimax-m3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
nemotron	openrouter/nvidia/nemotron-3-ultra-550b-a55b	general	success	4

Verification Lanes

Lane	Model	Status	Confirmed	Rejected	Uncertain
deepseek-verifier	openrouter/deepseek/deepseek-v4-pro	success	3	4	0

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

• Hint ecall lacks operand overlap check between in_addr and out_addr (executor/src/vm/instruction/execution.rs:550, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The hint ecall's input read (in_addr) is intentionally not modeled on the MEMW bus (documented in hint.rs: 'The input read... is intentionally not modelled'). The ECSM overlap check exists because both xG and k operands have MEMW bus interactions at different timestamps — overlap would break the MEMW chain. For hint, the input is read into a local buffer before any writes and generates no bus interactions, so overlap cannot create a trace provability issue. Behavior is deterministic: read first, compute, write. The 'inconsistency' with ECSM is by design, not a bug.
• Executor adds k256 dependency for host-side hint computation (executor/Cargo.toml:18, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — This is not an actual issue — it merely observes that the PR adds a k256 dependency to the executor. The dependency is required for the new feature (compute_hint). The finding itself says 'this is acceptable.' Adding a necessary dependency is not a defect.
• Test programs hint_min and hint_multi omit in-guest verification (executor/programs/rust/hint_min/src/main.rs:1, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — Both hint_min and hint_multi are explicitly documented as test programs exercising the HINT table's bus surface for the prover. hint_min line 2: 'No in-guest verify — this exercises exactly the Hint table's bus surface.' The ethrex-crypto crate properly implements verify-then-fallback. These are not templates for production guests — they are P0 provability tests.
• compute_hint returns zeros for non-canonical inputs without error (executor/src/vm/instruction/execution.rs:142, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The zero-return on non-canonical input is the documented design (execution.rs lines 121-126): 'not a loud failure... guest's in-circuit verify rejects the value and recomputes.' The dispatch already rejects unknown hint_id before compute_hint is called. This is correct for the verify-then-fallback pattern.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

[jotabulacios]

/bench

[jotabulacios]

/bench

[github-actions]

Benchmark Results for unmodified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base binary_search	59.9 ± 1.0	58.6	61.5	1.00 ± 0.02
head binary_search	59.8 ± 0.4	59.3	60.5	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base bitwise_ops	60.0 ± 1.4	58.2	61.5	1.01 ± 0.03
head bitwise_ops	59.2 ± 1.2	58.4	61.6	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base fibonacci_26	63.6 ± 0.7	62.8	65.3	1.00
head fibonacci_26	65.4 ± 1.8	62.9	69.6	1.03 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base matrix_multiply	64.9 ± 1.0	63.6	67.5	1.00
head matrix_multiply	65.8 ± 1.2	64.3	68.0	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base modular_exp	59.6 ± 0.6	58.6	60.5	1.00
head modular_exp	63.1 ± 9.7	58.6	89.8	1.06 ± 0.16

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base quicksort	63.3 ± 0.4	62.7	63.7	1.00
head quicksort	63.6 ± 0.7	62.6	64.9	1.01 ± 0.01

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sieve	65.3 ± 0.5	64.7	66.1	1.00
head sieve	65.4 ± 1.1	64.4	68.2	1.00 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sum_array	74.5 ± 1.0	73.5	76.9	1.01 ± 0.01
head sum_array	73.9 ± 0.4	73.4	74.5	1.00

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

• High — prover/src/tables/hint.rs:189: The AIR deliberately leaves a0 and a1 unbound, while the executor rejects unknown selectors and overflowing input addresses. A malicious prover can therefore prove executions that the VM executor would reject. Bind these registers and constrain the rejection conditions, or remove those executor-only semantics.

[jotabulacios]

/bench