[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 #4763 (and #4761 before it), restacked onto #4722's latest head (5f5d77cc). That head takes Z^(p-2) by #4762's addition chain, so this PR's win_mulPowOk does too, the same change #4722 made for P-521.

Known red until #4722 is fixed: #4722's committed ecdh_p521.rs still declares P-521's internal field modules that ec_p521.rs already declares since #4762. The full emitter on #4722's head regenerates ecdh_p521.rs without them. I've left that file to #4722 and told its session. Any failure in that file or its clippy run is #4722's, not this PR's.

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 still 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 PPC64LE P-521 ECDH: [d]P by three-bit windows #4722's P-521 one:
  • the windows, then Z^(p-2) by the 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

• The full lake build and Emit.lean pass on PPC64LE P-521 ECDH: [d]P by three-bit windows #4722's head with this PR. The emitter's output for ecdh_brainpoolp512r1 is committed. The one other file it changes, ecdh_p521.rs, is left to PPC64LE P-521 ECDH: [d]P by three-bit windows #4722, as above.
• The Static checks pass.
• CI runs the PPC64LE Rust tests on POWER: the curve's Wycheproof ECDH vectors.

Benchmark

Benchmarks run 42529524175, on #4761's branch, the same windows before the addition chain. It used arches=powerpc64, modules=ecdh_brainpoolp512r1, and base bd7184fc (main with the ladder and the old power):

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

---

Generated by Claude Code

[alex]

Rust: lints (library) (and the Lean emit check) fail here because of #4722, not this PR. #4722's ecdh_p521.rs declared P-521's internal field modules a second time; ec_p521.rs already declares them since #4762. #4722 has since fixed it with a fast-forward (eaad41a0, regenerated by the full emitter), so this PR's diff is still only its own two commits. This branch's head is on 5f5d77cc, just before that fix. I'll restack it onto #4722 when #4722 merges, as this draft needs anyway, and CI will go green then.

---

Generated by Claude Code

[github-actions]

This pull request has conflicts with main, found after 66a3329 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-main: the same two commits, restacked onto main now that #4722 has merged. The full build and emit pass there.

---

Generated by Claude Code