[alex]

Part of #4141 (PPC64LE audit, finding 1). Stacked on #4732, so it stays a draft until that merges.

P-521's [d]G and [k]G on PPC64LE used the Montgomery ladder. #4729's comb needs the point functions' slots, which fit at most 6 words, and P-521 has 9.

What changes

• Impl/Weierstrass/PPC64LE/TCombI.lean: the comb for coordinates of more than 6 words, on the ladder's layout, as the ladder runs them (ladder). It keeps the comb's window, digit, scan and sign (TComb.lean).
  • The entry is selected into the ladder's T.
  • R = R + T is the complete addition inlined (rcb, calls of the field's functions) into the ladder's D, then copied to R.
  • TCombCfg gains qBase, where the entry goes. Its default is the point functions' Q, so the existing combs are unchanged; their Layout gains qAt := rfl.
• Proof/Weierstrass/PPC64LE/TCombI.lean: combI_ok proves R = [k]G, reduced, changing only powClob and the ladder's writes (ladWx).
  • LayoutI and ConfigI hold the side conditions: the ladder's LadLayI, the entry in T, -y in D.x, zero apart from what the ladder writes, RcbApart S R T D.
  • The proof reuses TComb.lean's digit, scan, select and sign lemmas. entryI_ok and negateI_ok follow entry_ok and negate_ok on this layout. addI_gen is rcb_ok then copyPt_ok.
• P-521 (Impl/Ecdsa/P521/PPC64LEComb.lean, Proof/P521/PPC64LE/Comb.lean, and the public-key, signature and RFC 6979 files, as for P-256):
  • The tables are the other targets' (Impl/P521/CombTable7.lean): 83 windows of seven bits over the ladder's table of all 576 bits of the scalar.
  • The ladder-based P-521 public key and signature, their literals and their Verified are deleted.
  • The RFC 6979 registration requires VG_P521_COMB not to be one of the HMAC table's function names.

No TCB or Spec change.

Testing

• lake build and Emit.lean pass on this tree. The only crate changes are P-521's, in crates/verified-garbage-asm-powerpc64le (ec_p521, internal/vg_ecdsa_p521_sign_k, and the new consts/vg_p521_comb.rs).
• The Static checks and check_lean_public_imports.py pass.
• Locally, under qemu-ppc64le, the P-521 and P-256 tests pass, including RFC 6979's P-521 vectors and Wycheproof.

Benchmark

A Benchmarks run is queued, scoped to arches=powerpc64, modules=ec_p521,ecdsa_p521, groups=ec_p521_public_key,ecdsa_p521_sha512_sign, with base 3ae8b0e (#4732's head). I'll add the link and results here.

---

Generated by Claude Code

[alex]

Replaced by #4756: the same change restacked onto #4754 (which replaced #4732), with the benchmark results.

---

Generated by Claude Code