[alex]

Part of the PPC64LE audit, #4141 (ECDSA verification), following #4762 and #4770.

vg_ecdsa_<curve>_verify on PPC64LE takes its two inverses by the chains signing has used since #4762, for all nine curves:

• s^(n-2): by invN.
• Z^(p-2): by invP.

These are the sliding windows of n − 2 and p − 2 (Impl/Weierstrass/PPC64LE/Chain.lean), about 1.2 multiplications per bit instead of the bit-by-bit power's two. The chain's table is the nine slots from DX. At both points the verification reads nothing there afterwards: uv only needs EM', D, K, RM' and ACC, and the final step R, RM' and ACC.

Proofs

• Scalars.lean, mid_ok: chainPow_ok with chainN in place of pow_ok.
  • Its writes are chainWN_eq, and midW now names the table's slots.
  • The bit tables stay apart from the writes, since the writes all lie below byte 4096.
• Final.lean, vtail_ok: chainPow_ok with chainP, likewise.
• Main.lean: the composition's statement, rfl, names the new steps.

The bit tables of p − 2 and n − 2 are still written at setup but no longer read. Removing them is left to a follow-up.

No TCB, Spec or registration changes.

Generated crate. Only PPC64LE changes: the nine ecdsa_<curve> verifications.

Testing

• Under qemu-ppc64le with Wycheproof, cargo test --target powerpc64le-unknown-linux-gnu --release ecdsa passes for all nine curves (Wycheproof, CAVP, RFC 7027).
• lake build (all modules) 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

Run 42538020637: arches=powerpc64, the nine curves' verify groups, base 7cfde1c4 (main). Two inversions are a small part of a verification, and every curve is 2–6% faster.

Benchmark (1024 bytes)	Base	Head	Change
ecdsa_p192_sha256_verify	392.22 µs	381.34 µs	2.8% faster
ecdsa_p224_sha224_verify	537.34 µs	515.84 µs	4.0% faster
ecdsa_p256_sha256_verify	365.87 µs	346.57 µs	5.3% faster
ecdsa_p384_sha384_verify	1.65 ms	1.59 ms	3.6% faster
ecdsa_p521_sha512_verify	8.64 ms	8.43 ms	2.4% faster
ecdsa_secp256k1_sha256_verify	606.50 µs	589.19 µs	2.9% faster
ecdsa_brainpoolp256r1_sha256_verify	606.74 µs	588.39 µs	3.0% faster
ecdsa_brainpoolp384r1_sha384_verify	1.68 ms	1.62 ms	3.4% faster
ecdsa_brainpoolp512r1_sha512_verify	6.84 ms	6.64 ms	2.9% faster

The 64- and 16384-byte sizes show the same changes, but one cell: P-192's base at 64 bytes measured 691.68 µs, an outlier against the 392 µs of its other sizes, so that row's 45% is not real.

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHHNk9SreF92JBY2H8M