x86-64 P-521 ECDH: an affine window table and the mixed addition

[alex]

Summary

P-521 ECDH on x86-64 now brings the window table into affine coordinates with one inversion. Every window but the last then adds its entry with the mixed Jacobian addition (maddJ, madd-2004-hmv: 8 products and 3 squares) instead of the full Jacobian addition (16 products).

The table. It is built in projective coordinates by WinCfg.build, the table the other curves' window method uses, then normalized by WinCfg.normTbl (Montgomery's trick):

1. The prefix products c_m = Z_1 ⋯ Z_m go into the addition's temporaries, with c_8 in R.z.
2. One inversion leaves c_8^(p-2) in E.x.
3. Back from entry 8: Z_m^(p-2) = c_m^(p-2) c_{m-1} and c_{m-1}^(p-2) = c_m^(p-2) Z_m, and each entry's X and Y are multiplied by its Z^(p-2).
4. Every Z is set to one.

The inversion. It is the divsteps inversion ECDH already runs for Z^(p-2) (InvCfg.inv). It is a second instance, Cfg.invWin, writing E.x and with its working area over the table of the bits of n - 2, which only ECDSA reads.

• Placement. The usual working area overlaps the recoded scalar's bits, which the window method reads after the table. The n - 2 table ends below them for three words or more.
• What the window proof assumes. The generic proof takes the inversion as a hypothesis (InvSpecW: E.x = R.z^(p-2), and what it writes). ECDH discharges it with InvSound and the inversion's existing InvOk (invSpecQ).

The iterations. Each iteration but the last adds the entry by maddJ into D and then selects as before (selSum):

• E where R is O;
• R where the entry is O (digit 0, (0 : 1 : 0));
• otherwise the sum.

The mixed addition fails only for equal points (it gives O for opposite ones), which win_sep already rules out (InvJ.sumSelM). The last iteration adds the affine entry, already a projective representative, by the complete formulas, so toProjE is gone.

Proofs.

• Proof/Weierstrass/WindowJA.lean (target-independent): Fermat's little theorem in Fe C from the group law's x_eq (Law.fermat), the step of Montgomery's trick (trick_step), and RepA (a representative with Z ∈ {0, 1}).
• Proof/Weierstrass/X86_64/WinJNorm.lean: normTbl_ok, from a table of Rep to a table of RepA, for entries other than O. That holds since P-521 has prime order (PrimeOrder). It goes one product at a time (slotMul_ok), the prefix products and back-substitution by invariants (PreInv, BackInv).
• windowJ_ok now takes InvSpecW, and changes invClob, winW and the inversion's writes. mulQJ4_ok (Proof/Ecdh/X86_64/MulJ4.lean) takes the wider WinMulPostJ and writes mulQJ4W (winXJ: winX and the inversion's working area), with mulQJ4_w for the exchange. mulQ's WinMulPost, winX and mulQW, which the other curves and ECDSA verification share, are unchanged.
• Dead code removed. The table in Jacobian coordinates (buildJ, RepJ, toProjE) and the 16-product addition (jacAddS from x86-64 P-521: order the Jacobian doubling's and addition's field operations #1258, InvJ.sumSel) are no longer used.

Constant time. The taint summaries gain one for the normalization (winNormJSum, winNormJXSum).

No change to TCB/ or Spec/.

Speed

ci/bench_compare.py --rounds 5 --modules ecdh_p521 against #1258's head, on a Cascade Lake:

Benchmark	Base	Head	Change
ecdh_p521/66	289.22 µs	271.72 µs	6.0% faster

Each of the 130 iterations saves 4 products and a square. The table costs one inversion and 37 products more, and saves the 7 conversions into Jacobian coordinates.

Checks

• Lean: before the rebase onto x86-64 P-521 ECDH: windows in Jacobian coordinates #1255's merge, lake build and Emit.lean --check passed. After it, the P-521 modules build, EmitOne.lean --check P521.X86_64 finds the same code, and the full build is running locally.
• Rust: the P-521 ECDH 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