[alex]

Part of #4141 (the PPC64LE audit, finding 1). Draft, and depends on #4719 and #4722. This PR needs #4722's Window3.lean and #4731's WindowA.lean, and #4722's branch is older than #4731. So the branch is main with #4719's and #4722's commits cherry-picked (9abd52f7, 6f8bc069), then this PR's two commits (6cb33371, d8f8279a). Review only those two. I'll restack onto #4722 once #4722 includes #4731, or onto main once #4722 merges.

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, and the full emitter's output is committed.
• 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

To follow: a scoped run, arches=powerpc64, modules=ecdh_brainpoolp512r1, against main.

---

Generated by Claude Code

[alex]

Replaced by #4763: the same two commits, now stacked on #4722's restacked branch, so its diff has only them.

---

Generated by Claude Code