perf(ec): pair EC byte range checks, and replace ecrecover's four scalar muls with one joint chain (−61.9% EC cells, z3-gated, unconditional)

[MauroToscano]

Two EC optimizations that ship together: the existing single-scalar chips get their byte range checks paired (−13.3% ECDAS cells), and a new joint-chain lincomb2 precompile replaces ecrecover's four x-only scalar multiplications with one (−61.9% EC cells). Both paths stay live and both are specified in the new EC spec chapter.

Stacked on #860 (keccak HWSL-inline). Review that first; the diff here is EC-only.

---

Part 1 — AreBytes send-pairing on the existing chips (42ba68ff)

Every single-byte range check shipped as [b, 0] while the bus contract already checks both slots. Pairing them halves the sends:

	interactions/row
ECDAS	388 → 290	≈ −13.3% committed cells
ECSM	579 → 515

This is a bus repacking only — no witness, column, constraint or degree change. The equivalence argument (thoughts/ec-recover-opt/gate/pairing-equivalence.md) is that every gate lemma consumes the byte contract per column, not per send, so the theorem survives verbatim. keccak_rnd already paired; ECSM/ECDAS were the outliers, so this restores the house convention.

Part 2 — the lincomb2 precompile (new ecsm2.rs / ecdas2.rs)

ecrecover computes pk = u1·G + u2·R. The guest used to evaluate that with four x-only ECSM syscalls — x(k·P) and x((k+1)·P) per term, the +1 queries existing only so solve_y could recover y from an x-only oracle — plus an affine add. Four ~256-bit ladders, ~1528 ECDAS rows.

lincomb2 does it in one blinded joint Shamir/Straus chain returning both coordinates: mean 449.1 rows per ecrecover.

• New syscall ecsm_lincomb2 (u64::MAX - 11), beside ecsm_mul rather than replacing it. Status returned in a register; non-zero means the guest takes its existing proven-Rust fallback. Degenerate values never trap — they arrive from transaction data, so a trap would let one crafted transaction abort a whole block's proof.
• New chips ECSM2 (1,155 cols) and ECDAS2 (658 cols / 288 constraints), plus a preprocessed EC_T0 table holding −2^i·T₀ for the blinding correction. New buses: Addend = 29, EcT0 = 32, JointBit = 33.
• Guest switch: the call site was already ecsm_lincomb2(..).unwrap_or_else(|| ProjectivePoint::lincomb(..)), so only the body changed — four queries and solve_y became one ecall. The guest keeps decompressing (r, v) itself and remains the parity authority; the chip's obligations are membership and canonicalisation.

Numbers

Measured against the post-pairing baseline (1.467M cells/ecrecover), because the pairing win is already banked in Part 1:

	cells/ecrecover	vs baseline
mean (449.1 rows)	0.559M	−61.9%
worst case (514 rows)	0.640M	−56.4%

Guest cycles: −78,823 and −78,493 per ecrecover on the 5- and 20-transfer blocks (agreeing to 0.4%). The design doc predicted 100–150k, so the secondary win is real but below the low end — quoting the measurement.

The design study's headline of −74.3% is denominated against the pre-pairing 1.69M baseline and would count Part 1's win twice. −61.9% is the honest figure against what actually ships.

Soundness: two forgeries found and closed

Both were found by deriving claims the design docs asserted, and both survived a chip that proved, verified, balanced every bus and passed lint. Each is now a permanent negative control.

1. The NUMS blinding argument does not close the incomplete-addition edge. The design mitigated attacker-reachable degenerate additions by seeding the accumulator at a nothing-up-my-sleeve point T₀, arguing a collision implies a known linear relation on dlog(T₀). But the prover chooses P2 = lift_x(r) from free signature bytes, so setting P2 = μ·T₀ cancels T₀'s coefficient: with P1 = G, u1 = 1 the condition collapses to μ·(c2 − 1) ≡ −2^j (mod N) — one modular inversion, no discrete log, and cheaper than the same attack on the unblinded chain. At the collision λ is unconstrained and Q is free. Verified 5/5, each packaged as a well-formed (z,v,r,s).

Fixed by an unconditional fourth relation, D_INV·(xB − xA) ≡ 1 (mod p), gated to addend-consuming rows. This retires the assumption rather than patching it: the joint-chain path rests on no cryptographic assumption the single-scalar path did not. The blind is kept only because it drops the exact-MSB lemma — convenience, not soundness.

2. Padding rows could mint scalar digits ⇒ arbitrary chosen sender. ECDAS2's per-stream digit sender was gated by the raw D1/D2 columns, not by MU. A padding row is inert on every other bus, so MU=0, PH1=1, D1=1 satisfied all 217 constraints while emitting a live JointBit send. A prover could drop a real add and supply its count from phantom rows, computing Q' = (u1−a)·G + u2·R while claiming u1·G + u2·R — and since the attacker picks the effective multipliers first (u1'=u2'=1, R = T−G), that yields any chosen recovered key, i.e. an arbitrary transaction sender, with no discrete log and no search.

The existing chip has exactly this defence (ecdas.rs:444); the rewrite dropped it. Fixed by (1−MU)·{D1,D2,S1,S2,S3,S_CORR} = 0.

Verification

• z3 gate (thoughts/ec-recover-opt/gate/RESULTS-lincomb2.md): all lemmas UNSAT, 7 genuine forgeries SAT, 2 redundancy probes, 0 live holes. Two controls are driven by the working attacks above rather than by hypotheses. L1–L5a port by proving ECDAS2's relation arms textually identical to ECDAS's per-arm. Positive anchor: 3.32M checks over 5,960 rows.
• Oracle: 611 three-way lincomb differentials, 1,536 exhaustive small-scalar cases, 489 Wycheproof verdicts, 40/40 ecrecover, and 69,431 rows compared field-by-field against the Rust witness — zero discrepancies.
• Width audit: the convolution widths hold with a varying, chip-produced addend (~2^39 headroom, z3 UNSAT ×36, 6,346 real rows cross-checked). P12 needs no canonicalisation.
• Tests: prover suite 566 passed (5 pre-existing recursion_* failures from missing program_artifacts/recursion/*.elf); ethrex-crypto 13/0; ecsm 26/0; executor lincomb2 18/0; ec_t0 17/0; lincomb2 31/0; prove_elfs 107/0. make lint clean. Both real blocks prove and verify.

Two verification gaps closed on the way past

• range_check_balance_tests — the debug-checks bus tracker reports buses 14..33 only, so AreBytes/IsHalfword/Zero — exactly the buses fed by the hand-written collect_bitwise_from_* mirrors, several of which carry comments warning that a mismatch is "a silent bus break" — had nothing enforcing them; a drift surfaced only as an unattributed whole-proof imbalance. The new test asserts every table's range-check interactions cancel per tuple across all ~30 tables, and guards mirrors that predate this work.
• CI cache keys (pr_main.yaml) hashed executor/programs/rust/** and syscalls/** but not crypto/ethrex-crypto/**, which the ethrex guest depends on by path — so a change confined to that crate restored a stale ethrex.elf and CI kept proving the old guest. That matters here specifically: the guest falls back to software lincomb and returns identical output, so a stale ELF is invisible to every output assertion.

Spec

spec/ecsm.typ is the first spec chapter for the EC chips (none existed — the ecsm.toml references were dead). It documents both implementations: the single-scalar path including the pairing, and the joint-chain path including the schedule, buses, the T₀ table, both constraint families above, and the canonicalisation obligations. The security section states that the path is unconditional and records why the T0-DL assumption is not load-bearing.

Not done in this PR

• Bench — the harness and commands are in thoughts/ec-recover-opt/lincomb2/BENCH.md; nothing has been benched. Note the trap documented there: the guest falls back to software lincomb and returns the same answer, so output equality cannot detect a run where the precompile never fired — only the cell slope can.
• Retiring the old path. ecsm_mul, ecsm.rs and ecdas.rs are now unused except by their own tests, deliberately kept as a fallback and as a control (the degenerate-add test runs the identical forged row through the old chip and asserts it passes, which is what makes the new test a test of the new relation). Removing them is follow-up work once the bench confirms the win.
• EC share of a real block — the multiplier that converts −61.9% EC cells into a whole-prover figure. count_elements_by_table is in; the measurement is not. It is only meaningful on a real ethrex block: on a small guest, fixed tables (BITWISE at 2^16 rows, PAGE) are ~95% of the trace.

[github-actions]

Benchmark Results for modified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head ecrecover	44.7 ± 0.6	43.9	46.0	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head ecsm	2.8 ± 0.1	2.7	2.9	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head hashmap	99.6 ± 1.7	97.9	102.5	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head keccak	104.0 ± 2.5	101.5	108.9	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head syscall_commit	80.1 ± 1.6	78.1	82.6	1.00

[MauroToscano]

/bench

[github-actions]

Benchmark — ethrex 20 transfers (median of 3)

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

Metric	main	PR	Δ
Peak heap	51199 MB	64040 MB	+12841 MB (+25.1%) 🔴
Prove time	27.291s	34.162s	+6.871s (+25.2%) 🔴

⚠️ Regression detected — heap or time increased by more than 5%.

✅ Low variance (time: 1.7%, heap: 0.8%)

_{Commit: 3e4b16f · Baseline: cached · Runner: self-hosted bench}