x86-64 P-521 ECDH: windows in Jacobian coordinates

[alex]

Summary

P-521 ECDH on x86-64 now keeps the window method's accumulator in Jacobian coordinates from one window to the next and adds the entries in Jacobian coordinates (WinCfg.windowJ). Each window saves the conversions into Jacobian coordinates and back (6 products) and the complete addition's 29 field additions; the Jacobian addition costs the same 16 products as the complete addition with its conversions.

• The table's entries are stored in Jacobian coordinates (toJ of each complete addition's result, buildJ).
• Every digit but the last is added by the Jacobian addition (add-1998-cmo-2). The result is replaced by E where R is the point at infinity and by R where the entry is (masks of their Z, selSum); otherwise the operands are never equal or opposite.
• The last digit is added by the complete formulas in projective coordinates (stepLast), so R ends as before.

It is P-521's own scalar multiplication for Cfg.exchangeWith (#1256), Cfg.mulQJ4: the 4-bit windows of mulQ with the Jacobian accumulator. The 5-bit Jacobian window method of #1256 does not fit nine words in the working space (its table alone is 640 n bytes).

Why the incomplete addition is safe

• P-521 has prime order. Proof/P521/PrimeOrder.lean evaluates [n]G = O in the kernel by the ladder, in seconds, and gives PrimeOrder by x86-64 P-256 ECDH by 5-bit windows in Jacobian coordinates (−18%) #1256's primeOrder_of. It reaches the proofs through the x86-64 variant HasLawInvOrd (x86-64 P-256 ECDH by 5-bit windows in Jacobian coordinates (−18%) #1256's interface); only the variant file imports the Mathlib group theory.
• Operands never collide. Multiples of a point P ≠ O agree only for integers congruent modulo n (PrimeOrder.zmul_eq, from x86-64 P-256 ECDH by 5-bit windows in Jacobian coordinates (−18%) #1256's Window5.zmul_dvd). Iteration j adds [d_j]P to [16 e]P, with 16 e + 8 < n for every j ≥ 1 (win_sep, winE_two_bound). So the operands are equal or opposite only if [16 e]P = O.

Supporting changes

• The scalar multiplication. mulQJ4_ok (Proof/Ecdh/X86_64/MulJ4.lean) is its MulOk, writing what mulQ writes (mulQW), so exchangeWith_ok gives P-521's exchange. The other curves are unchanged.
• Generalized lemmas. The x86-64 window lemmas (TblOkR, EntryPostR, WinStR, winEntryR_ok) are generalized over the point representation. The existing statements are unchanged corollaries.
• Taint summaries. New summaries cover the table, the loop and the last iteration. The old window summaries are removed, since verification no longer runs the window method.

No change to TCB/ or Spec/.

Speed

ecdh_p521 on this machine (Cascade Lake, BMI2+ADX):

	before	after
verified-garbage	359 µs	325 µs
aws-lc-rs	258 µs	246 µs
OpenSSL	778 µs	758 µs

The two columns are separate cargo bench runs on a shared machine, so aws-lc-rs also moved by 5%. Against aws-lc-rs the ratio went from 1.39 to 1.32.

Checks

• Lean: after merging main (x86-64 P-256 ECDH by 5-bit windows in Jacobian coordinates (−18%) #1256), the P-521 ECDH proofs build; the full lake build and Emit.lean --check are still running locally.
• Rust: cargo clippy --all-targets -- -D warnings and cargo fmt --check pass. The P-521 tests pass, Wycheproof and CAVP, also with VG_CPU_FEATURES=none.
• CI scripts: check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt, cpu_tests lint and algorithms_table all pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_019KRjToTNRB2yxFCdNMux4P

[reaperhulk]

conflicts

[alex]

CI failing

[alex]

The merge of main (e0befa9) failed Lean shard 2 in the new Proof/P521/PrimeOrder.lean: #1256's primeOrder_of needs a Fact p.Prime instance, which this file didn't supply. 8ecaf59 adds it. That module and the P-521 law variant build locally; CI is re-running.

---

Generated by Claude Code