[alex]

Part of #4141 (the PPC64LE audit). Stacked on #4736, so it stays a draft until #4736 merges.

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, #4736's TCombI. brainpoolP512r1's eight-word coordinates don't fit the point functions' six, as P-521's nine don't. brainpoolP256r1 and P384r1 are in #4743.

What changes

The per-curve files are #4736's P-521 files, 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 (#4736), as on x86-64 and AArch64	764,928

The rows are the same tables, Impl/BrainpoolP512r1/CombTable7.lean, in each target's Montgomery form. So this is in line with the precedent and adds nothing new in kind.

Testing

• The full lake build and Emit.lean pass, on PPC64LE P-521: public keys and RFC 6979 signatures by the signed seven-bit comb #4736 restacked locally onto main. The emitter's output for brainpoolP512r1 is committed and is the same on PPC64LE P-521: public keys and RFC 6979 signatures by the signed seven-bit comb #4736's base.
• The Static checks pass.
• CI runs the PPC64LE Rust tests on POWER: the curve's Wycheproof and RFC 7027 vectors.

Benchmark

Scoped run: Benchmarks run 42527666626, with arches=powerpc64, the curve's public-key and SHA-512 signing groups, and base 9206b9ee (#4736's head).

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

The job ran 8 copies of each binary for the signing groups and kept the fastest. The base's copies spread 123%, and its 64-byte time (8.09 ms) is about twice its 1024-byte time. The head's copies spread 0.8–2.5% at 64 and 1024 bytes, and 70.7% at 16 KiB. Every group is faster by 82% or more.

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHFbSpgWBYWAsEnfUks