[alex]

Replaces #4775. It's the same change, now stacked on #4786 (P-521), so that the two don't conflict; P-384's Layout takes qAt := rfl, the field #4786 adds. Part of #4141 (PPC64LE audit, finding 1). It stays a draft until #4786 merges.

What changes

P-384's [d]G (vg_ec_p384_public_key) and [k]G (vg_ecdsa_p384_sign_k, the core of the RFC 6979 signature) now use the generic comb (#4729) instead of the Montgomery ladder. The comb uses P-384's table, the one the other targets already share (Impl/P384/CombTable7.lean): 55 windows of seven bits, a 42240-word read-only constant.

The files mirror P-256's:

• Impl/Ecdsa/P384/PPC64LEComb.lean: p384Comb, p384CombWords, mulGeneratorP384, publicKeyP384Comb and signP384Comb.
• Proof/P384/PPC64LE/Comb.lean: the comb's configuration, and comb_generator_ok. It needs exponentiation.threshold 512, as Proof/P384/Arm/Comb.lean does.
• Proof/EcKey/PPC64LE/P384/Comb.lean and Proof/Ecdsa/PPC64LE/P384/Comb.lean: Verified with the table as a constant (Abi.withConsts), and constant time by taint_decide with taintSym.
• The RFC 6979 core passes the table (cs := p384CombConsts). Its registration requires that VG_P384_COMB is not one of the HMAC table's function names.
• Removed: the ladder's P-384 public key and signature, their literals and their Verified. vg_p384_mul, which no P-384 function calls any more (ECDH has its windows, PPC64LE P-384 ECDH: [d]P by four-bit windows #4719), goes from the crate.

No TCB or Spec change.

Testing

• lake build and Emit.lean pass on this tree. The only crate changes are P-384's, in crates/verified-garbage-asm-powerpc64le.
• Locally, under qemu-ppc64le, the P-384 tests pass, including RFC 6979's P-384 public keys and signatures, and Wycheproof.

Benchmark

Benchmarks run 42517206330, scoped to arches=powerpc64, modules=ec_p384 ecdsa_p384, groups=ec_p384_public_key ecdsa_p384_sha384_sign, with base 8c69d0c (the same change on an earlier base, before the chain and the new field multiplication):

Benchmark	Base	Head	Change
ec_p384_public_key/97	1.83 ms	238.49 µs	87.0% faster
ecdsa_p384_sha384_sign/64	1.93 ms	332.52 µs	82.8% faster
ecdsa_p384_sha384_sign/1024	1.93 ms	334.38 µs	82.7% faster
ecdsa_p384_sha384_sign/16384	1.97 ms	368.18 µs	81.3% faster

---

Generated by Claude Code

[alex]

Replaced by #4797: the same change, restacked onto main after #4793 merged.

---

Generated by Claude Code