[alex]

Part of #4141 (the PPC64LE audit, finding 1). Stacked on #4722 (P-521 ECDH, three-bit windows), so it stays a draft until #4722 merges. It replaces #4761, which carried #4719's and #4722's commits before #4722 was restacked. These two commits are #4761's, cherry-picked unchanged.

vg_ecdh_brainpoolp512r1 on PPC64LE computed [d]P with the Montgomery ladder. It now uses three-bit windows with the formulas for any a.

Why three bits, and why start from the top two bits

• Four-bit windows don't fit. brainpoolP512r1's coordinates are 8 words, so an entry is 192 bytes. Sixteen entries from the end of the tables of bits (5632) would end at 8704, past the 8192-byte working space. Eight entries end at 7168, as for P-521 (PPC64LE P-521 ECDH: [d]P by three-bit windows #4722).
• The top window would read past the table of bits. The scalar's 512 bits are 3 · 170 + 2. So PPC64LE P-521 ECDH: [d]P by three-bit windows #4722's loop of 171 windows from R = O would read bit 512 in its top window. That is one byte past the table of bits, the first entry of the next table (p − 2's bits), which is 1. Instead, R starts at the table's entry for the top two bits (top2, then the usual masked scan, then R = D), and the 170 windows below follow.

What changes

• Impl/Ecdsa/PPC64LE/Window3A.lean (new): build3, trip, step3 and mul3top.
  • These are PPC64LE P-521 ECDH: [d]P by three-bit windows #4722's three-bit windows with PPC64LE brainpoolP256r1, P384r1 ECDH: [d]P by four-bit windows for any a #4731's complete addition and doubling for any a (rcb with a at AP and 3b at B3P; dblJa).
  • They reuse Window.Cfg.entry, select3 and scanEntry.
  • As before, the only branch is on the public counter, and every address is r3 plus a constant (plus 3 j for a window's bits).
• Proof/Ecdsa/PPC64LE/BrainpoolP512r1/Window.lean (new): mul_ok, which proves R = [k]P for every k < 2^512.
  • It is PPC64LE P-521 ECDH: [d]P by three-bit windows #4722's P-521 proof on brainpoolP512r1's field and eight-word layout, with PPC64LE brainpoolP256r1, P384r1 ECDH: [d]P by four-bit windows for any a #4731's general-a steps (InvJ.dblA', Rep.add).
  • New: top2_ok and top2_eq for the start, where R holds [k >>> 510]Q, which is the windows' invariant at j = 170.
• Impl/Ecdh/BrainpoolP512r1/PPC64LE.lean: exchangeWith with WindowA.Cfg.mul3top … B3P.
• Proof/Ecdh/PPC64LE/BrainpoolP512r1/Verified.lean: win_mulPowOk, as P-521's (PPC64LE P-521 ECDH: [d]P by three-bit windows #4722) with 3b from Fixed (F'.b3p). Verified goes through exchangeWith_ok, and constant time is checked by taint_decide on the new literal.

No TCB, Spec or Rust change. The only crate change is ecdh_brainpoolp512r1.rs and its assembly.

Testing

• The full lake build and Emit.lean pass on main with PPC64LE P-384 ECDH: [d]P by four-bit windows #4719 and PPC64LE P-521 ECDH: [d]P by three-bit windows #4722, and the full emitter's output is committed. Since then PPC64LE P-521 ECDH: [d]P by three-bit windows #4722's window code hasn't changed, and main has had no TCB or emitter change.
• The Static checks and check_lean_public_imports.py pass.
• CI runs the PPC64LE Rust tests on POWER: the curve's Wycheproof ECDH vectors.

Benchmark

A scoped run of this code is queued on #4761's branch: arches=powerpc64, modules=ecdh_brainpoolp512r1, base bd7184fc (main, whose vg_ecdh_brainpoolp512r1 is the ladder). I'll add its results here.

---

Generated by Claude Code

[github-actions]

This pull request has conflicts with claude/ppc64le-ecdh-p521, found after c7fea7a 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]

Replaced by the PR for claude/ppc64le-brainpool512-ecdh-v3, restacked onto #4722's latest head (the addition chain).

---

Generated by Claude Code