[alex]

Replaces #4749, which conflicted with main once #4729 (P-256 public keys by the comb) and #4731 (brainpool ECDH windows) landed. It's the same change, rebased linearly onto main (cd85a7b):

• ladPowWith_ok, PPC64LE P-256: public keys by the signed seven-bit comb #4729's power after any generator, now takes Z^(p−2) by the chain. It no longer needs the table of p − 2's bits, so stage₂With and upToPowWith drop it.
• The ECDH windows of P-256, P-224, brainpoolP256r1 and brainpoolP384r1 (win_mulPowOk) take the chain.

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 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 multiplication. Callers:

  • the public key (upToPowWith) and the signature (ladPowWith_ok), after any generator;
  • ECDH, after the ladder or the windows (MulPowOk);
  • the signature's 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.
• check_lean_speed.py passes.
• Locally, under qemu-ppc64le: public keys, ECDH, ECDSA and RFC 6979 on every curve, plus Wycheproof (56 tests).

Benchmark

Benchmarks run 42519677222, scoped to arches=powerpc64, with base bdbde97 (before the combs and windows). 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 3dfc897 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 #4762: the same change rebased onto main after #4719, with P-384's ECDH windows taking the chain too.

---

Generated by Claude Code