[alex]

Part of the PPC64LE audit, #4141 (ECDSA verification). This follows #4785, which gave these curves' public keys and signatures the comb, and #4770, which did this for P-256.

vg_ecdsa_brainpoolp{256,384}r1_verify on PPC64LE now compute [u]G + [v]Q the way P-256's verification does (Cfg.pointsWith), instead of the joint ladder (Cfg.points, joint):

• [u]G: the signed seven-bit comb of PPC64LE brainpoolP256r1, P384r1: public keys and signatures by the comb #4785. Its table is the same artifact constant the key and signature code already use, VG_BRAINPOOLP{256,384}R1_COMB.
• [v]Q: ECDH's four-bit windows for any a (Impl/Ecdsa/PPC64LE/WindowA.lean), with 3b read from B3P.
• The sum: as P-256's.

pointsWith still writes b in Montgomery's form to EM, which P-256's windows read and these curves' do not. That costs a few instructions per verification. Removing the write would mean changing P-256's proof as well, so I left it.

Proofs

Proof/Ecdsa/Verify/PPC64LE/BrainpoolP{256,384}r1/Verified.lean:

• combPts_ok follows P-256's (P256Comb.lean). Its window step is Window.BrainpoolP{256,384}r1.mul_ok, whose constants are the layout's own: F.b3p, with no setConst.
• verify_ppc uses verifyWith_ok.
• verify_ct uses taintSym on the table's symbol.
• The witnesses are states holding the table, and verifyHash_verified uses Hash.verifyHash_verified_cons, all as P-256's.

The combined proof is in the Verified module that uses it, rather than in a module of its own. brainpoolP384r1's combPts_ok takes set_option exponentiation.threshold 512 in, as #4785's comb_generator_ok does.

No TCB, Spec or registration changes.

Generated crate. Only PPC64LE changes: the two verifications, and the removal of vg_brainpoolp{256,384}r1_point_double, internal functions that only the joint ladder called.

Testing

• Under qemu-ppc64le, cargo test --target powerpc64le-unknown-linux-gnu --release brainpool passes: Wycheproof's brainpool ECDSA vectors and RFC 7027.
• lake build (every module) and Emit.lean pass on this tree, which is main plus this commit.
• The Static checks and check_lean_public_imports.py pass.
• cargo fmt --check and clippy -D warnings pass.

Benchmarks

The run is pending, scoped to arches=powerpc64 and the two curves' verify groups, with base b3fcb1b1 (main). I'll link it here.

---

Generated by Claude Code