[alex]

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

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.

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 P-224, P-256, P-384 and P-521 tests pass together on this branch, including RFC 6979 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 same change on an earlier base, before the chain and the new field multiplication):

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

[alex]

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

---

Generated by Claude Code