[alex]

Replaces #4786, which the merge queue dropped. #4785 (the brainpoolP256r1 and brainpoolP384r1 combs) landed first, and its two Layouts lacked the qAt field this PR adds. It's the same change, rebased linearly onto main (b3fcb1b), with a commit giving both of #4785's layouts qAt := rfl. Part of #4141 (PPC64LE audit, finding 1).

P-521's [d]G and [k]G on PPC64LE used the Montgomery ladder. The comb (#4729) 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 Layouts (P-256's, brainpoolP256r1's, brainpoolP384r1's) gain 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 (with_nbits: all 64 n bits), 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 pass.
• Locally, under qemu-ppc64le, the P-521, brainpoolP256r1 and brainpoolP384r1 tests pass, including RFC 6979's vectors and Wycheproof.

Benchmark

Benchmarks run 42524105072, scoped to arches=powerpc64, modules=ec_p521 ecdsa_p521, groups=ec_p521_public_key ecdsa_p521_sha512_sign, with base 3ae8b0e (the same change on an earlier base, before the chain and the new field arithmetic):

Benchmark	Base	Head	Change
ec_p521_public_key/133	4.81 ms	679.60 µs	85.9% faster
ecdsa_p521_sha512_sign/64	5.09 ms	955.09 µs	81.2% faster
ecdsa_p521_sha512_sign/1024	5.10 ms	952.70 µs	81.3% faster
ecdsa_p521_sha512_sign/16384	5.12 ms	986.35 µs	80.7% faster

---

Generated by Claude Code