[alex]

Part of #4141 (the PPC64LE audit). This restacks #4768 onto main and replaces it, now that its base, the P-256 signing comb (#4780, which replaced #4754 and #4771), has merged. The Lean commits are #4768's, cherry-picked unchanged. The crate was regenerated with the full emitter on main.

On PPC64LE, [d]G (public keys) and [k]G (RFC 6979 signatures) for brainpoolP256r1 and brainpoolP384r1 used the Montgomery ladder, one double, add and select per bit. They now use the fixed-base signed seven-bit comb (Impl/Weierstrass/PPC64LE/TComb.lean), as P-256 does (#4729, #4780). brainpoolP512r1 follows on the comb with the addition inlined, once that lands for P-521.

What changes

The per-curve files are P-256's comb files with the curve's names and sizes. Nothing shared changes: TComb, the RFC 6979 wrapper, the README tables, the dispatch and the variants all stay as they are.

• Impl/Ecdsa/<Curve>/PPC64LEComb.lean: the comb's configuration, built on the curve's ladder layout, with the other targets' tables (Impl/<Curve>/CombTable7.lean, with 37 and 55 windows). Also publicKey<Curve>Comb and sign<Curve>Comb.
• Proof/<Curve>/PPC64LE/Comb.lean: the layout and Config, the table's words, and comb_generator_ok, i.e. the comb as the stages' generator. The complete addition takes a from memory, so brainpool's a ≠ −3 needs nothing special.
• Proof/<Curve>/Comb7Shape.lean (new, target-independent): the tables' length and rows, as Proof/P384/Comb7Shape.lean.
• Proof/EcKey/PPC64LE/<Curve>/Comb{,Lit}.lean and Proof/Ecdsa/PPC64LE/<Curve>/Comb{,Lit}.lean: correctness, constant time (taint_decide, with the table's address public) and Verified, with the table as a constant (Abi.withConsts).
• RFC 6979: the core passes the comb's table (cs), and the registration requires that VG_<CURVE>_COMB is not one of the HMAC table's names.
• Removed: the ladder-based public keys and signatures for the two curves, with their literals and Verified. Nothing else used them.

No TCB, Spec or Rust change. The crate changes are crates/verified-garbage-asm-powerpc64le only: the two curves' modules, internal/vg_ecdsa_<curve>_sign_k, and the new consts/vg_<curve>_comb.rs.

Testing

• On main (e9073229), the full lake build and Emit.lean pass, and the full emitter's output is committed.
• The Static checks and check_lean_public_imports.py pass.
• CI runs the PPC64LE Rust tests on POWER: the curves' Wycheproof and RFC 7027 vectors.

Benchmark

Measured on #4711, whose comb code this is: Benchmarks run 42519119906, with arches=powerpc64, the two curves' public-key and signing groups, and base 8c69d0ca (the ladder).

Benchmark	Base	Head	Change
ec_brainpoolp256r1_public_key/65	1.24 ms	204.25 µs	83.6% faster
ec_brainpoolp384r1_public_key/97	1.85 ms	438.31 µs	76.3% faster
ecdsa_brainpoolp256r1_sha256_sign/64	1.47 ms	294.76 µs	80.0% faster
ecdsa_brainpoolp256r1_sha256_sign/1024	928.55 µs	318.26 µs	65.7% faster
ecdsa_brainpoolp256r1_sha256_sign/16384	979.49 µs	411.95 µs	57.9% faster
ecdsa_brainpoolp384r1_sha384_sign/64	1.93 ms	333.52 µs	82.7% faster
ecdsa_brainpoolp384r1_sha384_sign/1024	3.86 ms	666.08 µs	82.8% faster
ecdsa_brainpoolp384r1_sha384_sign/16384	1.97 ms	368.92 µs	81.2% faster

That run predates main's inversion chain (#4762) and Montgomery multiplication (#4774), which this PR doesn't change. I haven't measured on this base.

---

Generated by Claude Code