[alex]

The x86-64 field inversion of X25519 and Ed25519 (invertDS, Bernstein–Yang divsteps in ten batches of 59) ran each batch's divsteps one at a time on the low words of f and g and the four matrix entries: 44 instructions per step, ten cmovs among them, about 13 cycles per step, for 590 steps. That was about a fifth of vg_ed25519_scalar_base_adx, and the largest single difference left between our fixed-base multiplication and s2n-bignum's (which aws-lc-rs uses): 2.2 µs against bignum_inv_p25519's 1.6 µs.

This runs each batch's 59 divsteps in the packed chunks of the short Weierstrass curves' inversion (Impl/Weierstrass/X86_64/Inv.lean): four chunks of 15, 15, 15, 14 steps, each on two rows u P + v Q and q P + r Q of the chunk's matrix in one word each, so that a step is 15 instructions and updates f and u, v (or g and q, r) at once; the chunk's matrix is read from the rows' fields, updates the low words, and multiplies the batch's. The rows (fRow, aRow) and everything else are unchanged.

Code

That module imports this one (through Impl/Mont/X86_64.lean), so Impl/X25519/X86_64.lean repeats its 60 lines of chunk code under the names pk… (pkStep, pkSteps, pkSet, pkExt, pkLow, pkComp, pkChunk), the low words and a temporary at dsT = 744 (the end of the inversion's working area, unused until now). The batch count moves to r14 during the chunks, which use rbp. dstep and its loop are gone.

Proof

The structure of the proof is unchanged: the code proofs show the code computes a word-level function for any words, and Divstep/Sound.lean (imported only by the registration files) shows that function inverts.

• Divstep/Spec.lean: a batch's divsteps are now pkBatchV, four pkChunkVs on words (Divstep.psteps, pextLo/pextHi, the low words' update, the matrix product) in place of Divstep.wsteps 59.
• Divstep/Packed.lean (new): the code computes pkChunkV (pkChunk_ok), the proofs of Proof/Weierstrass/X86_64/InvPacked.lean without their integers, on this file's Scr, Keeps and drun.
• Divstep/Loop.lean: dsteps_ok composes the start, the four chunks and the stores; Batch.lean takes it as before.
• Divstep/Sound.lean: pkChunkV_rel and pkBatchV_rel show the chunks are 59 divsteps (msteps 59) for an odd f and a small d, with Proof/Divstep/Packed.lean's psteps_rel, pext_rel, low_upd and msteps_gen (the integer half of InvPacked's pchunk_ok); run_step uses it where it used wsteps_rel.
• Divstep/Step.lean keeps only drun.

No change to Spec/ or TCB/.

Measurements

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

Benchmark	Base	Head	Change
ed25519_keygen/32	9.68 µs	9.30 µs	4.0% faster
ed25519_sign/64	10.85 µs	10.47 µs	3.5% faster
ed25519_sign/1024	14.39 µs	13.89 µs	3.4% faster
x25519_generate/32	9.72 µs	9.29 µs	4.4% faster
x25519_public_key/32	9.20 µs	8.74 µs	5.1% faster
x25519_raw/32	32.30 µs	31.83 µs	1.5% faster

and with all of its features (the _ifma variants):

Benchmark	Base	Head	Change
ed25519_keygen/32	7.22 µs	6.82 µs	5.6% faster
ed25519_sign/64	8.42 µs	8.03 µs	4.6% faster
x25519_generate/32	7.09 µs	6.82 µs	3.9% faster
x25519_public_key/32	6.70 µs	6.54 µs	2.4% faster
x25519_raw/32	24.91 µs	24.54 µs	1.5% faster

Ed25519 verification, which compares points without encoding one, moved by under 0.5%. On the same machine (ADX only), aws-lc-rs's ed25519_sign/64 was 10.41 µs and its ed25519_keygen/32 9.09 µs.

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 after #1351, #1358 and #1360 the field inversion was most of what remained between our fixed-base multiplication and s2n-bignum's. Every x86-64 X25519 and Ed25519 function that encodes a point inverts once, so X25519 (key generation and the ladder), Ed25519 key generation and signing all gain about 0.4 µs, with or without IFMA.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RLVbycsRXKPfaW1swVZejG

---

Generated by Claude Code