[alex]

Replaces #4688. It's the same change, restacked onto #4729, which replaced #4675. Part of #4141 (PPC64LE audit, finding 1). Stacked on #4729, so it stays a draft until that merges.

What changes

vg_ecdsa_p256_sign_k, the core of vg_ecdsa_p256_sign (RFC 6979), now computes [k]G with #4729's comb instead of the Montgomery ladder: signP256Comb = p256.signWith mulGeneratorP256.

• The RFC 6979 wrapper takes a core with tables of constants (Core.cs), as x86-64's already does:
  • The contract (rfcPPC … cs) and the layout (Lay.cs, TBLs) carry the tables' regions.
  • The core's call supplies them (CoreTables, corePre, coreCall).
  • Two runs' layouts agree whenever the tables' addresses do (csSyms).
  • The contract with the tables, specK T cs vs, is satisfiable with the table in memory (sat_one).
  • The other curves pass cs := [], and their proofs are otherwise unchanged.
• Proof/Ecdsa/PPC64LE/P256Comb.lean: the signature by the comb meets signContract with the table as a constant (Abi.withConsts). Correctness comes from signWith_ok with comb_generator_ok. Constant time uses taint_decide with taintSym, which makes the table's address public.
• Registration: the RFC 6979 registration, like x86-64's, requires that VG_P256_COMB is not one of the HMAC table's function names.
• Removed: the ladder-based P-256 signature (signP256), its literal and its Verified, which nothing else uses. combSatMem moves to Proof/P256/PPC64LE/Comb.lean, where the public key and the signature share it.

No TCB or Spec change.

Testing

• lake build and Emit.lean pass on this tree. The only crate change is internal/vg_ecdsa_p256_sign_k in crates/verified-garbage-asm-powerpc64le.
• The Static checks and check_lean_public_imports.py pass, and so does cargo fmt --check.
• Locally, under qemu-ppc64le, the P-256 and ECDSA tests pass, including RFC 6979's P-256 vectors and Wycheproof.

Benchmark

Benchmarks run 42515542591, scoped to arches=powerpc64, modules=ecdsa_p256, groups=ecdsa_p256_sha256_sign, with base 2d9b293 (#4675's head; same change):

Benchmark	Base	Head	Change
ecdsa_p256_sha256_sign/64	916.27 µs	161.46 µs	82.4% faster
ecdsa_p256_sha256_sign/1024	916.32 µs	164.86 µs	82.0% faster
ecdsa_p256_sha256_sign/16384	970.04 µs	217.91 µs	77.5% faster

---

Generated by Claude Code

[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.}

[alex]

Replaced by #4754: #4729 has merged, so the same change is now restacked onto #4752 (the inversion chain).

---

Generated by Claude Code