[alex]

Part of #4141 (PPC64LE audit, finding 1). Stacked on #4688, which is stacked on #4675, so it stays a draft until they merge.

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 #4675's generic comb 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.

No TCB or Spec change.

Testing

• lake build and Emit.lean pass. The only crate changes are in crates/verified-garbage-asm-powerpc64le:
  • ec_p384, the new consts/vg_p384_comb.rs and consts/mod.rs;
  • internal/vg_ecdsa_p384_sign_k;
  • vg_p384_mul moving to the module of its first caller.
• The Static checks and check_lean_public_imports.py pass.
• Locally, under qemu-ppc64le, the 19 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 (#4688's head):

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 with Claude Code

https://claude.ai/code/session_01TKUFHJ728Kwktcff5BR2sx

[alex]

Replaced by #4739: the same change, restacked onto #4732 (which replaced #4688).

---

Generated by Claude Code