[alex]

Part of #4141 (the PPC64LE audit). Before this PR, on PPC64LE, vg_ecdh_brainpoolp256r1 and vg_ecdh_brainpoolp384r1 computed [d]P with the Montgomery ladder, at 1.6–2.2× OpenSSL in the audit. They now use #4712's four-bit windows, for a curve with any a, and are about 1.9× faster.

brainpoolP512r1 needs the 3-bit layout of #4722 (Window3.lean), because a 16-entry table of 8-word points doesn't fit in the working space. It will follow in a separate PR.

What changes

• Impl/Ecdsa/PPC64LE/WindowA.lean (new): the windows of Impl/Ecdsa/PPC64LE/Window.lean for any a, as RISC-V's Impl/Ecdsa/RISCV64/WindowA.lean is for RISC-V's.
  • It keeps the same table, nibbles, scan and loop, reusing Window.Cfg's entry, select, copyPt and points.
  • The additions use the complete addition for any a (rcb, which reads a at AP and 3 b at B3P) instead of rcb3.
  • The doublings use the Jacobian doubling for any a (dblJa) instead of dblJ.
  • Window.lean, which four curves use, is unchanged.
• dblJa moves from RISC-V's Impl/Ecdsa/RISCV64/WindowA.lean to Impl/Weierstrass/JacDblA.lean, so both targets share it and its proof (Proof/Weierstrass/JacDblA.lean). RISC-V's references now name it there. RISC-V's generated code is unchanged.
• Proof/Ecdsa/PPC64LE/<Curve>/Window.lean (new): these are P-224's and P-384's proofs (PPC64LE P-224 ECDH: [d]P by four-bit windows #4715, PPC64LE P-384 ECDH: [d]P by four-bit windows #4719), for 4 and 6 words.
  • Where those use the lemmas for a = -3, these use the ones for any a: completeness for any a (Rep.add) with 3 b at B3P, and InvJ.dblA' with a at AP, which each doubling now takes.
  • The curve-independent lemmas are P-256's (PPC64LE P-256 ECDH: [d]P by four-bit windows #4712).
• Impl/Ecdh/<Curve>/PPC64LE.lean and Proof/Ecdh/PPC64LE/<Curve>/Verified.lean: exchangeWith with the windows, and win_mulPowOk, as in P-224's and P-384's. Constant time is taint_decide on the new literal.

No TCB or Spec change. No sorry, native_decide, bv_decide or new axioms. No Rust change, and no new tests: the curves' Wycheproof and RFC 7027 vectors already cover ECDH.

Testing

• CI passes, including the PPC64LE Rust tests on POWER.
• The full lake build and Emit.lean pass. The only crate changes are ecdh_brainpoolp{256,384}r1.rs in crates/verified-garbage-asm-powerpc64le and their assembly.
• RISC-V's brainpool registrations build after the move, and its crate is unchanged.
• The static checks, check_lean_public_imports.py and the ppc64le cross-build pass.

Benchmark

Benchmarks run 42523348043: arches=powerpc64, ecdh_brainpoolp256r1 and ecdh_brainpoolp384r1, base 27804a41, on POWER9.

Benchmark	Base	Head	Change
ecdh_brainpoolp256r1/32	865.15 µs	458.95 µs	47.0% faster
ecdh_brainpoolp384r1/48	1.83 ms	944.58 µs	48.5% faster

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHFbSpgWBYWAsEnfUks