[alex]

Part of #4141 (the PPC64LE audit, finding 1). Now that #4722 has merged, this restacks #4769 onto main and replaces it. The two commits are #4769'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 MulPowOk provides), 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.
  • 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:
  • the windows, then Z^(p-2) by PPC64LE: inverses by sliding windows of p − 2 and n − 2 #4762's addition chain (chainPow_ok);
  • 3b from Fixed (F'.b3p);
  • Verified through exchangeWith_ok, with constant time 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

• On main (66a33292, with PPC64LE P-521 ECDH: [d]P by three-bit windows #4722 and PPC64LE Montgomery multiplication of up to four words: [b] and m in registers, rows as two carry chains #4774), the full lake build and Emit.lean pass, and the committed crate is the emitter's output.
• 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

Benchmarks run 42529524175, the same windows. It ran before the addition chain and #4774's multiplication reached either side, with arches=powerpc64, modules=ecdh_brainpoolp512r1, and base bd7184fc (main with the ladder):

Benchmark	Base	Head	Change
ecdh_brainpoolp512r1/64	3.84 ms	2.11 ms	45.0% faster

---

Generated by Claude Code