[alex]

Part of #991.

On x86-64, the Montgomery ladder shared by vg_x25519 and vg_x25519_adx now runs the iteration of s2n-bignum's curve25519_x25519: no swap of the points in each iteration, and mux (cmove) choosing the point to double. Before, each iteration ran two cswaps of four words. It uses the same field operations as before (F.mul, F.sqr, F.a24add, addCmov, subCmov), in s2n-bignum's order and slot sharing, as the AArch64 _alt ladder does (#2591). vg_x25519_ifma and the fixed-base functions are unchanged.

• Impl/X25519/X86_64.lean:
  • mux o x y: [o] = [y] if ZF is set, else [x]. It loads both, cmoves word by word and stores, and changes no flag.
  • bitCmp: k_t from BITS, cmp with swap (ZF if equal), stored as the new swap.
  • step: the sums and differences of both points, dmsn, the bit, the two muxes, then the addition and the doubling interleaved. z_2's factor is s² + a24·p, RFC 7748's AA + a24·E.
  • The final lastSwap is unchanged.
• Proof/X25519/X86_64/Small.lean, Env.lean: mux_ok and muxEB, and store4Z_ok, a store4 that also keeps the flags.
• Proof/X25519/X86_64/Iter.lean:
  • bitCmp_ok, ops1_ok, ops2_ok.
  • stepEnv_eval: the slots after an iteration are ladderStep's, by cases on swap and k_t. It holds whichever point is doubled, since the addition is symmetric.
  • step_ok: the loop invariant LInv is unchanged, since slots 3–6 keep RFC 7748's (x_2, z_2, x_3, z_3). z_2, z_3 ≤ 2p still carries the single folds of the sums and differences.
• src/asm/x86_64/x25519.rs regenerated.

Constant time: the choice is cmove on ZF, with no branch on the bit; the artifacts' taint_decide covers it. Not trust changes: nothing under TCB/ or Spec/. Contracts and registrations unchanged.

Benchmarks

Run 39066148374: base main (fcdc37c), one run of each side, x86_64, module x25519.

Benchmark	Detected features on Zen 3 (EPYC 7763), choosing _adx	avx,avx2,bmi1,bmi2,adx on Zen 4 (EPYC 9V74)	none on Zen 5 (EPYC 9V45)
x25519/32	28.72 → 27.54 µs (−4.1%)	24.80 → 24.11 (−2.8%)	23.27 → 22.32 (−4.1%)
x25519_raw/32	28.72 → 27.48 (−4.3%)	24.78 → 24.10 (−2.7%)	23.30 → 22.28 (−4.4%)
x25519_generate/32	8.48 → 8.49 (+0.1%)	7.13 → 7.12 (0.0%)	6.36 → 6.36 (−0.1%)
x25519_public_key/32	8.38 → 8.38 (0.0%)	7.05 → 7.03 (−0.2%)	6.25 → 6.24 (−0.3%)

The fixed-base rows (x25519_generate, x25519_public_key) run vg_x25519_base*, whose code is unchanged. On Zen 3, aws-lc-rs's x25519 was 27.99 µs in run 39060668498, so the ADX ladder now leads it.

On this session's Intel Xeon (Ice Lake class), with the ADX path forced, an unproven prototype of the same loop was −1.9% (best of five) and −3.5% (median). llvm-mca on the loop: skylake/icelake-server 265 → 254 cycles an iteration.

Checks

• Full lake build passes, and Emit.lean regenerates src/asm to exactly this PR's file.
• check_lean_imports, check_lean_modules, check_registrations, check_lean_speed, check_vectors, check_arch_gates, check_variants and check_mcdt pass, as does cargo fmt --check.
• The X25519 unit tests and Wycheproof tests pass with VG_CPU_FEATURES unset (IFMA), avx,avx2,bmi1,bmi2,adx and none.

---

Generated by Claude Code