Perf/ecsm affine selector - #879
Conversation
|
Benchmark Results for modified programs 🚀
|
|
/bench |
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 47973 MB | 47903 MB | -70 MB (-0.1%) ⚪ |
| Prove time | 136.340s | 135.634s | -0.706s (-0.5%) ⚪ |
✅ No significant change.
Prove-time spread 1.4% (135.093s / 137.021s / 135.634s)
Commit: ad0ff3c · Baseline: cached · Runner: self-hosted bench
…affine-selector # Conflicts: # crypto/ethrex-crypto/src/tests/ecsm_tests.rs # executor/src/vm/instruction/execution.rs # prover/src/tables/cpu.rs # syscalls/src/syscalls.rs
|
/bench |
|
/ai-review |
Codex Code ReviewNo actionable issues found in the specified PR diff. Static review only; tests/builds were not run as instructed. |
AI ReviewPR #879 · 17 changed files Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-002: EcsmError Display messages don't cover the affine path
Claim The Display impl for EcsmError::NotOnCurve says "ECSM xG is not a valid curve x-coordinate" and CoordinateOutOfRange says "ECSM xG must be < p". With the new affine entry point (prepare_with_y / scalar_mul_xy_with_y), NotOnCurve can also mean the full point (xG, yG) is not on the curve, and CoordinateOutOfRange can mean yG >= p. The messages are now misleading when the affine ecall rejects an input. Evidence lib.rs lines 76-85 show the unchanged Display messages. Lines 127-151 add prepare_with_y, which returns EcsmError::NotOnCurve when yG² ≢ xG³+b (mod p) and EcsmError::CoordinateOutOfRange when xg >= p() || yg >= p(). The executor's affine ecall maps these errors back to the guest (execution.rs lines 540-585). Suggested fix Update the Display strings to describe both cases, e.g. "ECSM input point is not on the curve" for NotOnCurve and "ECSM xG/yG must be < p" for CoordinateOutOfRange, or split the messages per entry point. AI-003: Repeated p() allocations in prepare_with_y
Claim The on-curve check in prepare_with_y calls p() three times, each constructing a new BigUint from P_BYTES. Evidence Line 105: Suggested fix Cache p() in a local variable: 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. |
NotOnCurve and CoordinateOutOfRange both predate the affine ecall and named only xG: "ECSM xG is not a valid curve x-coordinate" and "ECSM xG must be < p". The affine path returns the same two variants for a caller-supplied yG that fails yG² ≡ xG³ + b or is >= p, so the messages pointed at the wrong operand. Rewords them and the variant docs to cover both entry points. Also hoists the modulus in prepare_with_y: it was rebuilt from P_BYTES five times per call (two range checks plus three reductions in the on-curve test). One BigUint either way against the scalar multiplication that follows, so this is for the reader, not the clock.
|
/bench |
1 similar comment
|
/bench |
|
/bench-gpu |
GPU Benchmark (ABBA) —
|
|
/bench |
|
/bench-gpu |
|
Automated review pass (low-effort, full-diff read). No findings. q: stacks on Not run at high effort yet — worth one before merge given this touches |
MauroToscano
left a comment
MauroToscano
left a comment
There was a problem hiding this comment.
Formally verify it, and make a spec for 3mi
|
/bench |
5 participants
What
Adds an affine variant of the ECSM ecall (
ECSM_AFFINE_SYSCALL_NUMBER = u64::MAX - 11): inputxG‖yG(64 B), outputxR‖yR(64 B), against the x-only variant's 32 B in/out. AnIS_AFFINEselector column lets one prover serve both ABIs, so existing x-only consumers (
ecsm.elf, bench,ASM
test_ecsm*) keep working unchanged.With x-only output the guest could not learn
y(k·P), so it recovered it from a second queryx((k+1)·P)plus the chord-addition law — two accelerator calls and a batch of field arithmeticper point. ethrex's ecrecover now takes
yfrom the chip: two ECSM queries per 2-term linearcombination instead of four, and
solve_yis gone.Details
executor/src/vm/instruction/execution.rs):ECSM_AFFINE_SYSCALL_NUMBERgetsits own handler branch (
scalar_mul_xy_with_y). Both operand buffers are 64 B, so theaddress-limb guard spans offset 63 for
xG/xR(31 for the scalar) and thexG/kdisjointness guard widens to 64 B. Validates
0 < k < N,xG < p,yG < pand that(xG, yG)is on the curve.IS_AFFINEselector (prover/src/tables/ecsm.rs, 667 → 684 columns, 413 → 423constraints): the
yG-read (4 dwords ataddr_xG + 32, ts) andyR-write (4 dwords ataddr_xR + 32, ts+3) MEMW buses fire withmult = IS_AFFINE, so they are inert on x-only rowsand on padding. The x-only path is untouched:
yGstays the canonical even lift andyRiswitnessed only for ECDAS.
yR < p(OverflowKind::YrLtP, +16 halfword columns and its carry chain): publishingyRis what makes its representation observable, and the byte range checks only bound it below
2^256.xRwas already forced canonical byXrLtP; this gives the other half of the outputthe same treatment.
ecsm_mul_affineinsyscalls/src/syscalls.rs, andlincomb2_with_oracleincrypto/ethrex-crypto/src/lib.rsnow does two oracle queries instead of four and dropssolve_yentirely. It still needs one field inverse for the final affine addition.ecsm_affine, plus a forged-yRrejection test.Measured (ethrex bench_20, bench server, baseline = the hint branch this sits on)
3 interleaved pairs, each side with its own prover and its own guest ELF, since this touches
both. All proofs verify.
Halving the accelerator calls is the structural part; prove time moves less because ECSM/ECDAS is
a fraction of the trace. An earlier measurement of this work reported −10.2%, on a baseline that
sat 14,466 cycles above
8 × 524,288and therefore carried a ninth CPU chunk the affine sidedropped — a boundary artifact, not the change. Pairs are interleaved rather than run as
sequential blocks, because cross-session drift on that machine exceeds the effect being measured.
Soundness
Returning
ymakes two things observable that were not:yGonly throughyG² ≡ xG³ + b, which holds for both+yGand−yG. On the x-only path that freedom is invisible (x(k·P) = x(k·(−P))), but onceyRis published a witness could pick−yGand get a correctly-computed multiple of adifferent point — indistinguishable to both the AIR (an on-curve check passes either way) and
the guest (it cannot know the parity of
k·Pwithout doing the multiplication it delegated).The
yGMEMW read closes it by pinning the witnessed column to the caller's own buffer.p, so withoutYrLtPawitness could publish
yR + pwheneveryR < 2^256 − p(~2^32), and such points areconstructible:
3 | p−1makes cubing 3-to-1, so a small targetyhas a cube-root preimageabout a third of the time.
IS_AFFINEitself is pinned by theEcallreceiver, whose syscall word isxonly + IS_AFFINE·(affine − xonly); the CPU sends the reala7, so a row claiming the wrongmode leaves the bus unbalanced.
IS_BIT(IS_AFFINE)andIS_AFFINE·(1 − µ) = 0keep it a bitthat is zero on padding. The written
yRinherits its byte range checks through the ECDAS bus,which carries the coordinate byte by byte and range-checks its own columns.
Removing the reconstruction also retires an argument rather than adding one: the x-only path had
to establish that the wrong sign of
yawas excluded by the scalar guards, which is what madek = 1andk = N−1degenerate. Withysupplied by the chip those scalars are ordinary —secp256k1 has cofactor 1 and prime
N, sok·P ≠ Ofor everyk ∈ (0, N).