[alex]

Part of #4141 (PPC64LE audit, finding 1). Stacked on #4688, which is stacked on #4675, so it stays a draft until they merge. It doesn't depend on #4700 (P-384).

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

No TCB or Spec change.

Testing

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

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

https://claude.ai/code/session_01TKUFHJ728Kwktcff5BR2sx

[alex]

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

---

Generated by Claude Code