[alex]

Part of #4141 (the PPC64LE audit). This restacks #4753 onto main and replaces it, now that its base, the comb with the addition inlined (TCombI, #4793), has merged. The Lean commit is #4753's, cherry-picked unchanged. The crate was regenerated with the full emitter on main.

On PPC64LE, brainpoolP512r1's [d]G (public keys) and [k]G (RFC 6979 signatures) used the Montgomery ladder. They now use the signed seven-bit comb with the addition inlined, as P-521's do (#4793). brainpoolP512r1's eight-word coordinates don't fit the point functions' six, as P-521's nine don't. brainpoolP256r1 and P384r1 use the comb since #4785.

What changes

The per-curve files are P-521's (#4793) with the curve's names and these sizes:

• coordinates: 8 words;

• windows: 74 (7 · 74 ≥ 512);

• scalar bits: 512;

• table: 75,776 words;

• scalar, key and signature: 64, 129 and 128 bytes.

• Impl/Ecdsa/BrainpoolP512r1/PPC64LEComb.lean: the comb's configuration on the signature's layout, with the other targets' tables (Impl/BrainpoolP512r1/CombTable7.lean). Also publicKeyBrainpoolP512r1Comb and signBrainpoolP512r1Comb.

• Proof/BrainpoolP512r1/PPC64LE/Comb.lean: LayoutI, ConfigI, the table's words and comb_generator_ok (by combI_ok).

• Proof/BrainpoolP512r1/Comb7Shape.lean (new, target-independent): the tables' length and rows, as Proof/P521/Comb7Shape.lean.

• Proof/EcKey|Ecdsa/PPC64LE/BrainpoolP512r1/Comb{,Lit}.lean: correctness, constant time (taint_decide, with the table's address public) and Verified, with the table as a constant.

• RFC 6979: the core passes the comb's table, and the registration requires VG_BRAINPOOLP512R1_COMB not to be one of the HMAC table's names.

• Removed: the ladder-based public key and signature, with their literals and Verified (and Impl/EcKey/BrainpoolP512r1/PPC64LE.lean). Nothing else used them.

No TCB, Spec or Rust change. The crate changes are only in crates/verified-garbage-asm-powerpc64le: ec_brainpoolp512r1, internal/vg_ecdsa_brainpoolp512r1_sign_k, and the new consts/vg_brainpoolp512r1_comb.rs.

Table size

The table adds 606,208 bytes of constants to the ppc64le crate, 75,776 words of 8 bytes. The other targets already ship the same size:

Crate's comb table	Bytes
x86-64 vg_brainpoolp512r1_comb	606,208
AArch64 vg_brainpoolp512r1_comb7	606,208
ppc64le vg_brainpoolp512r1_comb (this PR)	606,208
ppc64le vg_p521_comb (#4793), as on x86-64 and AArch64	764,928

The rows are the same tables, Impl/BrainpoolP512r1/CombTable7.lean, in each target's Montgomery form.

Testing

• On main (ac27cf36), 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 curve's Wycheproof and RFC 7027 vectors.

Benchmark

Measured on #4753, whose code this is: Benchmarks run 42527666626, with arches=powerpc64, the curve's public-key and SHA-512 signing groups, and base 9206b9ee (the ladder).

Benchmark	Base	Head	Change
ec_brainpoolp512r1_public_key/129	7.00 ms	502.72 µs	92.8% faster
ecdsa_brainpoolp512r1_sha512_sign/64	8.09 ms	1.40 ms	82.7% faster
ecdsa_brainpoolp512r1_sha512_sign/1024	4.04 ms	702.32 µs	82.6% faster
ecdsa_brainpoolp512r1_sha512_sign/16384	4.08 ms	736.43 µs	82.0% faster

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

---

Generated by Claude Code