x86-64 P-256 ECDH by 5-bit windows in Jacobian coordinates (−18%)

[alex]

P-256 ECDH on x86-64 (vg_ecdh_p256, vg_ecdh_p256_adx) now computes [d]P by a new window method: 5-bit signed windows in Jacobian coordinates, with no complete additions. P-256's group has prime order, which this PR proves, so the window's additions are never exceptional.

The window method (Impl/Weierstrass/X86_64/WinJac.lean)

• Digits. d is recoded as d + 16 Σ_{j<52} 32^j, giving 52 digits in [-16, 15]. They are read by the comb's digit code with w = 5.
• Table. It holds [1 … 16]P, each entry as (X, Y, Z, Z², Z³) in Jacobian coordinates:
  • [2]P is a doubling, and [m+1]P = [m]P + P by the mixed addition (jacMixedHead/jacMixedTail).
  • Entries are stored at an address computed from the public counter.
• Each window, from R = O:
  1. Five in-place doublings by the halving doubler (doubleHalfPublic, which the joint verification already uses), in a loop.
  2. The digit's entry selected in constant time: every entry is loaded and kept under a mask, 32 bytes at a time with AVX2 on _adx (selPassY) and 16 at a time otherwise (selPassAt). It is then negated for a negative digit.
  3. A Jacobian addition that uses the entry's cached Z² and Z³ (CachedJac.head + jacTail), 11M + 3S.
  4. Two masks: D = T where R = O (nzMask), and R is kept for a zero digit (eqMask 0).
• Output. R is converted to projective coordinates for the existing tail (TCombCfg.outFix/outOps).

The previous method used 4-bit windows (65 digits), complete additions (Renes–Costello–Batina), and conversions between projective and Jacobian coordinates around every window's doublings.

The doubling is a parameter of the window method. Cfg.exchangeJ is the exchange with this multiplication, and only P-256 uses it. The other curves keep Cfg.exchange, and their generated code is unchanged.

Why no addition is exceptional (Proof/Weierstrass/WinJacMath.lean)

• Prime order. Proof/Weierstrass/GroupOrder.lean and Proof/P256/PrimeOrder.lean prove that every point but O has order n:
  • #E ≤ 2p + 1 (an injection into Option (ZMod p × Bool));
  • n ∣ #E, since G has order n;
  • 2p + 1 < 3n;
  • no 2-torsion, by the existing certificate that the cubic has no root;
  • so #E is odd, #E = n, and n is prime.
• Window additions. Before digit j, R = [32 e]P with 0 ≤ e < n, and e < n - 32 for j ≥ 1. Adding [d]P, for e ≥ 1 and d ≠ 0, is exceptional only if 32 e ≡ ±d (mod n).
  • The bounds rule this out except at j = 0 with k = n - 2|d|.
  • That case needs digit d₀ = -|d|. But d₀ = ((k + 16) mod 32) - 16, and n ≡ 17 (mod 32) for P-256, so it never happens (loop_noexc).
• Table additions. [m]P + P for 2 ≤ m ≤ 15 is never exceptional (tbl_noexc).
• Scalars ≥ n. The proof (jstep_pt) only needs R to stay on the curve; the result is used only for 1 ≤ d < n.

winJac_ok (Proof/Weierstrass/X86_64/WinJac.lean) is the window method's theorem. Its pieces are in WinJac{Lay,State,Ops,Store,Build,Dbls,Select,Entry,Step,Iter}.lean, and the P-256 instance with the halving doubler is in Proof/P256/X86_64/WinJac.lean.

The ECDH proof is now generic over the multiplication

• Proof/Ecdh/X86_64/MulOk.lean defines the interface:
  • MulOk c mq W: the old mulPow_ok's hypotheses, concluding R = [k]P for 1 ≤ k < n, with W the bytes mq may write.
  • MulW c W: W is apart from what the rest of the exchange reads.
• exchangeWith_ok (Main.lean) proves the exchange for any mq that satisfies them. d = 0 is handled there directly.
• Instances:
  • The old window/ladder: mulQ_ok. P-224, P-384 and P-521 go through it, unchanged.
  • The new method: mulQJ_ok (Proof/Ecdh/X86_64/WinJac.lean).
• Constant time is checked over the whole new code by taint_decide, as before (ecdh_ct, ecdh_ct_adx).

Prime order in the law variant

• HasLawInvOrd (Proof/Weierstrass/X86_64/InvInterface.lean) extends HasLawInv with prime : PrimeOrder C.
• P-256's x86-64 law variant (Variants/P256/X86_64/Law.lean) now has this type.
• Its generic files (Generic/P256/X86_64/*, Generic/MdHash/P256/X86_64/*) take it.
• The Mathlib group theory (GroupOrder.lean) is imported only through the variant.

Features

vg_ecdh_p256_adx now uses AVX2 for the selection, so it declares ["bmi2", "adx", "avx", "avx2"], as vg_ec_p256_public_key_adx does. The Rust side already chooses the _adx functions together, by ec::p256::Mul::select, which requires all four.

This touches no TCB or spec files.

Measurements

Criterion on Cascade Lake, main and this branch alternated:

ecdh_p256	main	this PR	aws-lc-rs	OpenSSL
_adx	50.2–51.2 µs	41.0–41.9 µs (−18%)	39.1–40.0 µs	116–123 µs
baseline (VG_CPU_FEATURES=none)	62.4 µs	50.5 µs (−19%)

Checks

• lake build and lake env lean --run Emit.lean --check: pass. Only src/asm/x86_64/ecdh_p256.rs changes.
• ci/check_lean_imports.py, check_lean_speed.py, check_vectors.py, check_arch_gates.py, check_variants.py, check_mcdt.py: pass.
• ci/algorithms_table.py: no change.
• cargo fmt --check, cargo clippy --all-targets -- -D warnings: pass.
• cargo test --release with Wycheproof: pass as is and with VG_CPU_FEATURES=none.
• Extra local checks (not committed), against the previous implementation:
  • 2002 small scalars;
  • d = n - j for small j.

🤖 Generated with Claude Code

https://claude.ai/code/session_01KfFYaXu423bswZqpujcACe

---

Generated by Claude Code