[alex]

Replaces #4759. It's the same change, restacked onto #4771 (P-256 signing, on main). Part of #4141 (PPC64LE audit, finding 1). It stays a draft until #4771 merges, and it doesn't depend on the P-384 or P-521 PRs.

What changes

P-224's [d]G (vg_ec_p224_public_key) and [k]G (vg_ecdsa_p224_sign_k, the core of the RFC 6979 signature) now use the generic comb (#4729) instead of the Montgomery ladder. The comb uses the 32 windows of P-224's shared table (p224Comb7x32), as 32-bit ARM's does: a 16384-word read-only constant.

The files mirror P-256's:

• Impl/Ecdsa/P224/PPC64LEComb.lean: p224Comb, p224CombWords, mulGeneratorP224, publicKeyP224Comb and signP224Comb.
• Proof/P224/PPC64LE/Comb.lean: the configuration, the table's shape (p224Comb7x32_length, _rows), and comb_generator_ok. The ladder's table of bits covers 256 bits; the comb reads its first 224.
• Proof/EcKey/PPC64LE/P224/Comb.lean and Proof/Ecdsa/PPC64LE/P224/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 := p224CombConsts). Its registration requires that VG_P224_COMB is not one of the HMAC table's function names.
• Removed: the ladder's P-224 public key and signature, their literals and their Verified. vg_p224_mul, which no P-224 function calls any more (ECDH has its windows, PPC64LE P-224 ECDH: [d]P by four-bit windows #4715), goes from the crate.

This and #4773 (P-521) each work alone. Whichever lands second needs qAt := rfl in P-224's Layout.

No TCB or Spec change.

Testing

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

Benchmark

Benchmarks run 42517555177, scoped to arches=powerpc64, modules=ec_p224 ecdsa_p224, groups=ec_p224_public_key ecdsa_p224_sha224_sign, with base 8c69d0c (the P-256 signature's head then; same change, before the chain):

Benchmark	Base	Head	Change
ec_p224_public_key/57	760.16 µs	103.74 µs	86.4% faster
ecdsa_p224_sha224_sign/64	804.61 µs	148.75 µs	81.5% faster
ecdsa_p224_sha224_sign/1024	808.34 µs	152.14 µs	81.2% faster
ecdsa_p224_sha224_sign/16384	861.44 µs	205.02 µs	76.2% faster

---

Generated by Claude Code