[alex]

Part of the PPC64LE audit, #4141 (ECDSA verification).

On PPC64LE, vg_ecdsa_<curve>_verify used to compute [u]G + [v]Q with two ladders and a complete addition. That is four point operations per bit. For the curves of at most six words (P-192, P-224, P-256, P-384, secp256k1, brainpoolP256r1, brainpoolP384r1), it now uses one joint double-and-add, Point.JointCfg.joint (Impl/Weierstrass/PPC64LE/Joint.lean):

• Setup: the point functions add G + Q once.
• Each bit: R is doubled once. Then O, G, Q or G + Q is added, chosen by masks of u's and v's bits. The selection is T = u ? G : O, D = u ? G+Q : Q, then v ? D : T.
• Cost: two point operations per bit.

The selection is branch-free, so the constant-time proof stays the existing taint_decide from the pointers, and no contract changes.

P-521 and brainpoolP512r1 (more than six words, where the point functions don't apply) keep the ladders: points := if c.n ≤ 6 then joint c else ladders c.

Proofs

• Proof/Weierstrass/PPC64LE/Joint.lean (new, generic over the curve):
  • The group law of the accumulator: acc, acc_step, with acc j = [u >>> j]G + [v >>> j]Q.
  • The iteration, in pieces: dbl_ok, selU_ok, selV_ok, add_ok, body_ok.
  • The loop (loop_ok, by countLoop_ok), the setup (setup_ok), the start (start_run, start_ok), and joint_ok.
  • joint_ok states that R represents [u]G + [v]Q and that only powClob and jointW change.
• Proof/Ecdsa/Verify/PPC64LE/Points.lean:
  • jointLay: the slots, with G + Q in K/D/E and v's bits at bitsAt n 3.
  • jointPts_ok, for the new code.
  • ladders_ok: the old proof, renamed.
  • points_ok: splits on c.n ≤ 6.
  • Pts.pt now states Rep R ([u]G + [v]P) directly. The ladder branch gets it through Rep.add, and Main.lean uses it as is.

No TCB, Spec or registration changes.

Generated crate. Only PPC64LE changes:

• The seven curves' ecdsa_<curve> verification is rewritten.
• internal/vg_secp256k1_point_add and internal/vg_secp256k1_point_double are new. secp256k1's verification now calls the generic point functions, where its ladders called the a = 0 ones.

Testing

• Under qemu-ppc64le with Wycheproof, cargo test --target powerpc64le-unknown-linux-gnu --release ecdsa passes for all nine curves: Wycheproof, CAVP P-256 and RFC 7027.
• After rebasing onto main (PPC64LE P-256: public keys by the signed seven-bit comb #4729 included):
  • lake build (all modules) passes.
  • The emitter regenerated the crate.
  • The qemu tests pass again.
• Before that rebase:
  • The static checks pass.
  • check_lean_public_imports.py passes on the edited modules.
• cargo fmt --check and cargo clippy --target powerpc64le-unknown-linux-gnu -- -D warnings pass.

Benchmarks

Run 42526032024: arches=powerpc64, the seven curves' ecdsa_*_verify groups, base e4c4e66a. It measured the head before the rebase onto #4729, which doesn't touch verification.

Benchmark	Base	Head	Change
ecdsa_p192_sha256_verify/64	1.04 ms	544.66 µs	47.7% faster
ecdsa_p224_sha224_verify/64	1.51 ms	802.11 µs	47.0% faster
ecdsa_p256_sha256_verify/64	1.72 ms	904.78 µs	47.3% faster
ecdsa_p384_sha384_verify/64	3.66 ms	1.93 ms	47.4% faster
ecdsa_brainpoolp256r1_sha256_verify/64	1.72 ms	905.70 µs	47.5% faster
ecdsa_brainpoolp384r1_sha384_verify/64	3.66 ms	1.93 ms	47.3% faster
ecdsa_secp256k1_sha256_verify/64	1.08 ms	904.00 µs	16.2% faster

The other sizes (1024 and 16384 bytes) and P-256 with SHA-384 show the same changes: 45–48% faster, and 15–16% for secp256k1. secp256k1 gains less because its ladders used the faster a = 0 point functions (vg_secp256k1_point_a0_*), and the joint loop uses the generic ones.

Follow-ups, separately:

• A joint loop on the a = 0 point functions for secp256k1.
• Windows or a comb table for G, and the sliding-window inverses of PPC64LE: inverses by sliding windows of p − 2 and n − 2 #4714.
• The more-than-six-word curves.

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHHNk9SreF92JBY2H8M

[github-actions]

This pull request has conflicts with main, found after 4b62f01 landed on main: rebase it to resolve them. Before rebasing, see CLAUDE.md on checking how much Lean main changed, and on restacking a stacked pull request.

_{Posted by .github/workflows/conflicts.yml, once per push to a conflicting pull request.}