[alex]

Part of the PPC64LE audit, #4141 (ECDSA verification). This follows #4793, which gave P-521's public keys and signatures the comb, and does for P-521 what #4770 did for P-256 and #4795 for brainpoolP256r1/P384r1.

vg_ecdsa_p521_verify on PPC64LE now computes [u]G + [v]Q by Cfg.pointsWith instead of the two ladders (Cfg.points, ladders):

• [u]G: PPC64LE P-521: public keys and RFC 6979 signatures by the signed seven-bit comb #4793's signed seven-bit comb, with the addition inlined (TCombI, combI). Its table is the artifact constant the key and signature code already use, VG_P521_COMB.
• [v]Q: ECDH's three-bit windows (Window.Cfg.mul3). They read b, in Montgomery's form, from EM, where pointsWith writes it.
• The sum: as P-256's.

Proofs

Proof/Ecdsa/Verify/PPC64LE/P521/Verified.lean follows P-256's (P256Comb.lean, Verified.lean):

• combPts_ok uses TComb.combI_ok, whose writes are ladWx, covered by comb_writes_cover. It also uses Window.P521.mul_ok.
• The windows' writes (mulW: bytes 1072–2152, 3520–4096 and 5824–7552) are apart from U's slots and the second table of bits (4672–5248), which the sum and the final step read.
• verify_ppc uses verifyWith_ok, and verify_ct uses taintSym on the table's symbol.
• The witnesses hold the table. verifyHash_verified uses Hash.verifyHash_verified_cons with wide := true.

combPts_ok takes set_option exponentiation.threshold 1024 in, as #4793's comb_generator_ok does.

No TCB, Spec or registration changes.

Generated crate. Only PPC64LE changes: the verification, and the removal of vg_p521_mul, the internal ladder that only the verification's ladders called.

Testing

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

Benchmarks

Run 42544295596: arches=powerpc64, ecdsa_p521_sha512_verify, base ac27cf36 (main), eight copies of each side. Verification is about 3.3 times as fast. These are the copies' medians from the run's per-run estimates:

Benchmark	Base	Head	Change
ecdsa_p521_sha512_verify/64	8.41 ms	2.52 ms	70% faster
ecdsa_p521_sha512_verify/1024	8.42 ms	2.52 ms	70% faster
ecdsa_p521_sha512_verify/16384	8.45 ms	2.55 ms	70% faster

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHHNk9SreF92JBY2H8M