[alex]

Part of #4141 (PPC64LE audit, finding 1). Follows #4719 (P-384), #4715 (P-224) and #4712 (P-256).

vg_ecdh_p521 computed [d]P with the Montgomery ladder of complete additions (4.83 ms on POWER9, 12× OpenSSL). P-521's coordinates are nine words. A four-bit window's sixteen entries (16 × 216 bytes) do not fit the working space past the tables of bits (5824–8192), so P-521 uses three-bit windows instead.

• Impl/Ecdsa/PPC64LE/Window3.lean: the three-bit variant of PPC64LE P-256 ECDH: [d]P by four-bit windows #4712's windows, reusing its table additions, copies, masks and entry scan.
  • A table of [e]P for e < 8 takes 1728 bytes, from 5824 to 7552.
  • Each of the 176 windows over the 528 bits of a 66-byte scalar does R = 8 R (three Jacobian doublings), reads three bits of the table of bits, scans the eight entries under masks, and does one complete addition.
  • As before, the only branch is on the public counter, and every address is r3 plus a constant.
• Proof/Ecdsa/PPC64LE/P521/Window.lean: mul_ok, which proves R = [k]P for every k < 2^528. It is P-256's proof on P-521's field and nine-word layout, with the three-bit window step (wstep with 8, nib3_eq).
• Proof/Ecdh/PPC64LE/P521/Verified.lean: win_mulPowOk and the Verified theorem through exchangeWith_ok. As in PPC64LE: inverses by sliding windows of p − 2 and n − 2 #4762 for the other curves, Z^(p-2) is taken by the addition chain (chainPow_ok). Constant time is checked by taint_decide on the new literal.

Signed four-bit windows (eight entries, Booth digits) would save about 10% more. They need the recoding and negation proofs, so they are left for later.

No TCB or Spec change.

Testing

• EmitOne.lean EcdhP521.PPC64LE passes after the rebase onto PPC64LE: inverses by sliding windows of p − 2 and n − 2 #4762. The only crate change is ecdh_p521.rs and its assembly.
• The static checks and check_lean_public_imports.py pass.
• The ppc64le tests run in CI.

Benchmark

POWER9, run 42521138146 (before the rebase onto #4762's chain), scoped to arches=powerpc64, modules=ecdh_p521:

Benchmark	Base	Head	Change
ecdh_p521/66	4.81 ms	2.34 ms	51.3% faster

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHH4GefHP3pmPRSL4N4

[github-actions]

This pull request has conflicts with main, found after 85135ee landed on main: rebase it to resolve them. Before rebasing, see CLAUDE.md on checking how much Lean main changed, and on restacking a stacked pull request.

_{Posted by .github/workflows/conflicts.yml, once per push to a conflicting pull request.}

[alex]

The merge queue's failure (run 42533231916) is not this PR's. The failing job is the x86-64 Rust (sde -arl), which failed before any test ran: curl: (6) Could not resolve host: downloadmirror.intel.com while downloading Intel SDE. This PR changes only PPC64LE code. All of CI passed on the PR head (eaad41a), so it only needs to be re-queued.

---

Generated by Claude Code