[alex]

Part of #991.

RFC 7748 clamping clears bits 0, 1 and 2 of the scalar. The ladder's last three iterations therefore always double (x2, z2), after one conditional swap that folds in the pending swap. On the baseline and ADX x86-64 ladders (the shared x25519With F), the loop now runs bits 254 down to 3 (cmp rbx, 3). A tail follows it:

• two muxes, selecting (x2, z2) or (x3, z3) by the pending swap;
• three unrolled doublings (dbl: 2 sqr, 2 mul, a24add, 3 add/sub each, instead of a full step's 4 mul, 4 sqr, a24add and muxes);
• clearing swap, so lastSwap is a no-op.

IFMA's own vladder is unchanged.

Proof

• LPre gains low: bits 0, 1 and 2 of the clamped scalar are 0. Main proves it from scalar_bit.
• step_ok now reports zf = decide (n = 3), and loop_ok runs from 255 down to 3.
• tail_ok proves that the tail reaches ladderAfter k u 0's (x2, z2) up to the final swap. It uses ladderStep_zero: a step on bit 0 with swap 0 is a doubling of (x2, z2), and (x3, z3) does not matter.
• LPost's per-slot equalities become res: for some sw < 2 in the swap word, cswap sw of slots 3/5 and 4/6 gives the spec's cswap fin.swap. This is all Main needs, since it passes sw to lastSwap_ok. LPost.of builds it from the old fields for the IFMA ladder.

No change to TCB/, Spec/, any contract or any registration.

Benchmarks

Run 39069565593, x86_64. All three jobs ran on Zen 3 (AMD EPYC 7763):

configuration	x25519/32	x25519_raw/32
detected (ADX)	27.53 → 27.40 µs (−0.4%)	27.52 → 27.40 µs (−0.4%)
avx,avx2,bmi1,bmi2,adx	27.57 → 27.39 µs (−0.6%)	28.21 → 27.38 µs (−2.9%)
none	41.73 → 41.72 µs (0.0%)	41.78 → 41.51 µs (−0.6%)

The fixed-base rows (x25519_generate, x25519_public_key) don't run the ladder, so their executed code is unchanged (unchanged code / placement). They read between 0.0% and 2.1% faster. Nothing is slower. With the ADX ladder, we're now ahead of aws-lc-rs's 27.99 µs.

---

Generated by Claude Code