[alex]

Part of #4141 (the PPC64LE audit). Replaces #4711, restacked onto #4732 (which replaced #4688). This PR's two commits are cherry-picked unchanged, and the rebuild and full emit of the new base gave the same crate. It stays a draft until #4732 merges.

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 of #4675 (Impl/Weierstrass/PPC64LE/TComb.lean), as P-256 and P-384 do.

brainpoolP512r1 will follow, on the widened comb for P-521 (#4736).

What changes

The per-curve files are P-384's 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 this base, the curves' artifacts build and the full Emit.lean passes with nothing to commit beyond the two commits. The Static checks pass.
• On PPC64LE brainpoolP256r1, P384r1: public keys and signatures by the comb #4711, CI passed, including the PPC64LE Rust tests on POWER (the curves' Wycheproof and RFC 7027 vectors). CI runs again here.

Benchmark

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

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

The signing groups were noisy on that runner (the job flagged spreads of 12–93%), but every group is faster, by 58–84%.

---

Generated by Claude Code

[alex]

Replaced by #4768, the same change restacked onto #4754 (claude/ppc64le-p256-comb-sign-v3), which replaced #4732.

---

Generated by Claude Code