[alex]

Replaces #4752, which the merge queue dropped for a conflict with #4719 (P-384's ECDH windows). It's the same change, rebased linearly onto main (3dfc897). P-384's windows now take Z^(p−2) by the chain too (Proof/Ecdh/PPC64LE/P384/Verified.lean, its own commit), as P-256's, P-224's and the brainpool curves' 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 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; P-256, P-224, P-384, brainpoolP256r1, brainpoolP384r1);
  • 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 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