[alex]

The comb's AVX2 selection (Ifma.vselect, which combSelectY, the _adx variants' selection, shares with the IFMA comb) scans all sixteen entries of a table and keeps each under a mask that is all ones exactly for the digit's magnitude. Each entry's mask took six instructions: combEqMask's four in the general registers (mov, xor, cmp, sbb), then vmovq and vpbroadcastq to move it into ymm15. That is 96 of the 240 instructions of each scan, 52 selections per fixed-base multiplication.

This builds each mask with one instruction:

• The static VG_ED25519_COMB now ends with the magnitudes 1 … 16, each in all eight doublewords of 32 bytes (combMagWords, 512 bytes after the 26 tables).
• Before the scan, vselMag puts the static's address in rax and the digit's magnitude r8 into every doubleword of ymm14 (vmovq, vpbroadcastd).
• Each entry's mask is then vpcmpeqd ymm15, ymm14, [rax + 39936 + 32 (m - 1)], all ones in every doubleword exactly when the magnitude is m. Its address depends only on m.

I also tried a counter in a register (vpcmpeqd with a register incremented by vpaddd, as the Weierstrass comb's selEntryY does). It saved nothing on this core: the scan is bound by the vector ports, and the counter adds as many vector instructions as it removes in the general registers. With the selection's other registers taken (the IFMA comb's lanes live in ymm0–ymm9), the memory operand also needs no free register.

Proof

Ifma.vselect_ok keeps its conclusion, but ymm14 joins the registers it writes (selRegs; one caller's frame proof gains a case). The changes are in Proof/Ed25519/X86_64/Ifma/CombSelect.lean:

• qword_pcmpeqd: pcmpeqd of quadwords holding A and B in both doublewords is the mask of A = B.
• vMagMask_ok (the compare against the static) and vselMag_ok (the setup). vselEntry_ok and vselEntries_ok carry ymm14 and the magnitudes in the static (MagsAt) where they carried rcx.
• vselect_ok reads the magnitudes from CombTbl, as the entries are read, through combWords_mag (Proof/Ed25519/X86_64/CombSelect.lean). combWords is now combTblWords ++ combMagWords, so combWords_getD reads the tables through the append.

The static grows from 4992 to 5056 words. The five witness states that write its size as a literal (per CLAUDE.md's "Tables of constants") now say 40448 bytes. The SSE selection (combSelect, the baseline variants) and the AVX-512 one (zselect) are unchanged; they ignore the words after the tables. 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), against #1358 (now merged), fastest of seven interleaved runs of each side (ci/bench_compare.py):

Benchmark	Base	Head	Change
ed25519_keygen/32	10.00 µs	9.73 µs	2.7% faster
ed25519_sign/64	11.14 µs	10.88 µs	2.3% faster
ed25519_sign/1024	14.60 µs	14.37 µs	1.6% faster
x25519_generate/32	10.04 µs	9.73 µs	3.1% faster
x25519_public_key/32	9.54 µs	9.25 µs	3.0% faster

Verification and the X25519 ladder, which don't select from the comb, moved by about 1% either way. With all of this CPU's features, the IFMA variants (whose fixed-base multiplication uses the zmm selection) were within 2% 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. The table scan was about a seventh of vg_ed25519_scalar_base_adx; this removes a third of its instructions (each entry's fifteen become ten). X25519 key generation shares the comb and gains the same.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RLVbycsRXKPfaW1swVZejG