[alex]

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

vg_ecdsa_p256_verify on PPC64LE now computes [u]G + [v]Q in three steps:

• [u]G: the signed seven-bit comb of P-256's public keys (PPC64LE P-256: public keys by the signed seven-bit comb #4729). The comb reads the same table, VG_P256_COMB, which is now a constant of the verification too. There is one table per curve, and it is public here.
• [v]Q: the four-bit windows of ECDH (Impl/Ecdsa/PPC64LE/Window.lean), with b in Montgomery's form at EM, a slot the verification has finished with.
• The sum: the complete addition, as the old ladders' path did (save, sum).

This replaces #4747's joint double-and-add for P-256. The other curves follow once their combs merge.

Proofs

• Composition. Cfg.pointsWith, backWith and verifyWith build the verification from any computation of [u]G + [v]Q.
• verifyWith_ok (Main.lean) proves the verification from any such computation that meets PtsOk, given s.syms = s₀.syms, obtained by WP.mono_syms after the stages before. verify_ok, for the other curves, is now its instance with points_ok.
• P256Comb.lean, combPts_ok: the bits of u, then b to EM, then comb_ok (Proof/P256/PPC64LE/Comb.lean's configuration), then save_ok, the bits of v, Window.mul_ok and sum_ok. Every slot fact is a decide on P-256's concrete layout.
• Verify/PPC64LE/Hash.lean takes the verification's tables of constants K, as ARM's does:
  • it is now written over hashR I K and coreR I K, with stripConsts/ConstsOk and the tables' addresses in pub;
  • coreR_nil, coreR_cons, hashed_verified_cons and verifyHash_verified_cons are new, the last by Verified.stackScratchLC and narrowK_pre;
  • the curves without tables are unchanged, through verifyHash_verified with K = [].
• Verified.lean (P-256):
  • the contract with the table (vPC) and its implication of verifyContract … (abi.withConsts p256CombConsts);
  • constant time by taint_decide with taintSym [VG_P256_COMB], which makes the table's address public;
  • witnesses with the table, vSat and verifyHash_sat.

No TCB or Spec changes. The registration is unchanged textually; its contract now carries the table (consts_of).

Generated crate. Only PPC64LE's ecdsa_p256 changes: vg_ecdsa_p256_verify now reads VG_P256_COMB.

Testing

• Under qemu-ppc64le with Wycheproof, cargo test --target powerpc64le-unknown-linux-gnu --release p256 and … ecdsa pass: Wycheproof, CAVP and RFC 6979.
• On this tree, rebased onto main (PPC64LE: inverses by sliding windows of p − 2 and n − 2 #4762 included):
  • lake build (all modules) passes;
  • Emit.lean leaves the crates as committed.
• Before that rebase:
  • the Static checks and check_lean_public_imports.py (edited modules) pass;
  • cargo fmt --check and clippy -D warnings pass.

Benchmarks

Run 42532702800: arches=powerpc64, modules=ecdsa_p256, the verify groups, base 85135eea (this PR's base, #4762 included).

Benchmark	Base	Head	Change
ecdsa_p256_sha256_verify/64	675.68 µs	401.11 µs	40.6% faster
ecdsa_p256_sha256_verify/1024	679.08 µs	404.35 µs	40.5% faster
ecdsa_p256_sha256_verify/16384	731.86 µs	457.08 µs	37.5% faster
ecdsa_p256_sha384_verify/64	675.59 µs	400.95 µs	40.7% faster
ecdsa_p256_sha384_verify/1024	677.83 µs	403.25 µs	40.5% faster
ecdsa_p256_sha384_verify/16384	711.10 µs	436.72 µs	38.6% faster

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHHNk9SreF92JBY2H8M