[alex]

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

vg_ecdsa_p384_verify on PPC64LE now computes [u]G + [v]Q by Cfg.pointsWith instead of the joint ladder (Cfg.points, joint):

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

Proofs

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

• combPts_ok uses TComb.comb_ok and Window.P384.mul_ok. The windows write the same bytes as brainpoolP384r1's (PPC64LE brainpoolP256r1, P384r1 ECDSA: verification's [u]G by the comb #4795), apart from U's slots and the second table of bits.
• verify_ppc uses verifyWith_ok, and verify_ct uses taintSym on the table's symbol.
• The witnesses hold the table, and verifyHash_verified uses Hash.verifyHash_verified_cons.

combPts_ok takes set_option exponentiation.threshold 512 in, as brainpoolP384r1's does. Without it, 2 ^ 384 in the bound on u is not evaluated.

No TCB, Spec or registration changes.

Generated crate. Only PPC64LE changes: the verification, and the removal of vg_p384_point_double, an internal function that only the joint ladder called.

Testing

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

Benchmarks

Run 42546707647: arches=powerpc64, ecdsa_p384_sha384_verify, base e6521157 (main).

Benchmark	Base	Head	Change
ecdsa_p384_sha384_verify/64	1.60 ms	888.87 µs	44.3% faster
ecdsa_p384_sha384_verify/1024	1.62 ms	880.37 µs	45.6% faster
ecdsa_p384_sha384_verify/16384	1.65 ms	920.86 µs	44.2% faster

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHHNk9SreF92JBY2H8M