[alex]

The comb negates the selected cached point [Y - X, Y + X, 2dT] for a negative digit, 52 times per fixed-base multiplication. It did that with a field subtraction 0 - 2dT, whose borrow needs two corrections (sub's second sbb/and/sub round), and two 32-byte conditional swaps through the general registers (cswap: eight loads, five instructions per word, eight stores each) — 116 instructions.

This computes the same thing in 58:

• The two slots are exchanged sixteen bytes at a time in xmm0–xmm2 (swapPieceX), with the mask in both quadwords of xmm15 as the selection already builds it. Only SSE2, which every target of this code has, so the baseline and the ADX variants share it. Four loads and four stores replace sixteen, and the exchange no longer walks a chain of five instructions per word before the multiplications that read these slots can start.
• 2dT is negated as 2p - [x] rather than 0 - [x]. The borrow of 2²⁵⁶ - 38 - [x] means 2²⁵⁶ ≡ 38 too many, subtracted once — and that subtraction cannot borrow again whatever the four words are, since a borrow means [x] > 2²⁵⁶ - 38 and the difference is then above 2²⁵⁶ - 76. 0 - [x] has no such slack: its borrow leaves a difference below 38, so it needs a second correction. cmove, for which test sets ZF exactly for a zero mask, keeps the unnegated value for a positive digit.

combNeg_ok keeps its statement (the specification's negCached under the sign's mask), so nothing above it changed. The new lemmas are in Proof/Ed25519/X86_64/CombNeg.lean: swapFieldX_ok, which concludes exactly what swapFieldWide_ok concludes for cswap, and negWords_ok/negField_ok for the negation, with fe_of_read128 relating a slot's two sixteen-byte halves to its four words. No change to Spec/ or TCB/.

Measurements

On a Sapphire Rapids Xeon restricted to VG_CPU_FEATURES=avx,avx2,bmi1,bmi2,adx (the _adx variants, as on a CPU without AVX512_IFMA), fastest of five interleaved runs of each side (ci/bench_compare.py):

Benchmark	Base	Head	Change
ed25519_keygen/32	10.35 µs	10.01 µs	3.3% faster
ed25519_sign/64	11.47 µs	11.24 µs	2.0% faster
ed25519_sign/1024	14.86 µs	14.66 µs	1.4% faster
x25519_generate/32	10.31 µs	10.08 µs	2.3% faster
x25519_public_key/32	10.03 µs	9.50 µs	5.2% faster

Ed25519 verification, the X25519 ladder and signing long messages, which this does not change or where SHA-512 dominates, moved by under 2.1% either way.

Why

From the analysis of the rustls provider's handshake signing in #991: on a CPU without AVX512_IFMA, Ed25519 signing was the gap against aws-lc-rs, and the fixed-base multiplication is nearly all of a signature's time outside SHA-512. With #1351 and this change, the sign handling and the addition that follows it no longer stall on each other; measured against s2n-bignum's edwards25519_scalarmulbase on the same machine, our vg_ed25519_scalar_base_adx went from 10.1 µs to 9.4 µs against its 8.5 µs. What remains of that difference is mostly the field inversion at the end (2.2 µs against bignum_inv_p25519's 1.6 µs).

🤖 Generated with Claude Code

https://claude.ai/code/session_01RLVbycsRXKPfaW1swVZejG

---

Generated by Claude Code