[alex]

Replaces #4730, which the merge queue dropped for a conflict with #4715 (P-224's ECDH windows). It's the same change, rebased linearly onto main (113f2ef). P-224's windows (Proof/Ecdh/PPC64LE/P224/Verified.lean) now take Z^(p−2) by the chain, exactly as P-256's do.

Part of #4141 (PPC64LE audit). Every PPC64LE elliptic-curve function inverted by the bit-by-bit power: two Montgomery multiplications per bit of p − 2 (affine conversion) and of n − 2 (the signature's k⁻¹). Once the combs (#4729's stack) shrink the scalar multiplication, those powers are the largest part of a public key or a signature.

What changes

• Impl/Weierstrass/PPC64LE/Chain.lean gives a power by the exponent's sliding windows: ChainCfg, slide, chainVal (Impl/Weierstrass/Chain.lean), which AArch64 and x86 already use. It works as on AArch64:

  • build a table x, x³, …, x¹⁵ and x²;
  • then, for each window of at most four bits ending in a one, square and multiply by the table.

  That is about 1.2 multiplications per bit instead of 2. The exponent is the code's, so nothing depends on secret data.

• Proof/Weierstrass/PPC64LE/Chain.lean: chainPow_ok, a port of AArch64's proof onto PPC64LE's calls of the field functions (mulCall_ok). Its postcondition is pow_ok's, except for what it writes (chainW: the result, the nine-slot table, the functions' own space).

• Impl/Ecdsa/PPC64LE.lean: chainP/invP (Z^(p−2)) and chainN/invN (k^(n−2)). Their tables are the nine slots from DX, the ladder's temporaries, which nothing reads after the ladder. Callers:

  • the signature, the public key and ECDH (the ladder, and P-256's and P-224's windows through MulPowOk) take invP;
  • the signature takes invN (Middle.lean).

• CfgOk gains chainP and chainN, each curve's chains checked by chainCheck (decide +kernel, as AArch64's are).

Verification, Impl/Ecdsa/Verify/PPC64LE.lean, still uses pow. Its new owner (the verification session) will switch to invP/invN in its own PR. The setup still writes the bits of p − 2 and n − 2, which verification reads.

No TCB or Spec change.

Testing

• lake build and Emit.lean pass on this tree. The crate changes are only in crates/verified-garbage-asm-powerpc64le: the public key, ECDH and vg_ecdsa_<curve>_sign_k of all nine curves.
• The Static checks pass.
• Locally, under qemu-ppc64le: public keys, ECDH, ECDSA and RFC 6979 on every curve, plus Wycheproof.

Benchmark

Benchmarks run 42519677222, scoped to arches=powerpc64, with base bdbde97 (before #4712 and #4715). On main the ladder still takes most of the time, so the relative gain here is small. In absolute terms it saves about 17 µs per p-inversion on P-256, 120 µs on P-521, and twice that for a signature.

Benchmark	Base	Head	Change
ec_p256_public_key/65	862.81 µs	846.10 µs	1.9% faster
ecdh_p256/32	863.83 µs	844.76 µs	2.2% faster
ecdsa_p256_sha256_sign/64	908.18 µs	874.01 µs	3.8% faster
ec_p521_public_key/133	4.81 ms	4.69 ms	2.4% faster
ecdh_p521/66	4.81 ms	4.69 ms	2.4% faster
ecdsa_p521_sha512_sign/64	5.08 ms	4.85 ms	4.6% faster

---

Generated by Claude Code

[github-actions]

This pull request has conflicts with main, found after 3941020 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 #4752: the same change rebased onto main after #4729 and #4731, with ladPowWith_ok and the brainpool ECDH windows taking the chain too.

---

Generated by Claude Code