[alex]

Part of #4141 (the PPC64LE audit). This PR replaces #4743, restacked onto #4754 (P-256's signatures by the comb, on #4752's inversion chain). It stays a draft until #4754 merges.

#4743's Lean commits are cherry-picked unchanged. On this base the comb proofs build with the inversion chain as they are. The crate was regenerated with the full emitter on this base. One more commit adds the -- separate module: line to the two Comb7Shape.lean files, which check_lean_single_importer.py asks for.

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 and P-384 do. brainpoolP512r1 is #4753, on the comb with the addition inlined.

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 full lake build and Emit.lean pass, and the full emitter's output is committed.
• The Static checks 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 this base's inversion chain (#4752), which this PR doesn't change. I haven't measured on this base.

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHFbSpgWBYWAsEnfUks