[alex]

Part of #4141 (PPC64LE audit, finding 1). This follows #4783.

Each row of rmul4's reduction computes q = t₀ m' mod 2⁶⁴. It loads m' from the working space and multiplies, which puts a load and a multiply on the row's loop-carried path. For a modulus with m' = 1 (m ≡ -1 mod 2⁶⁴: P-256's and P-192's p), q is t₀ itself.

• Impl/Mont/PPC64LE.lean: qhead M is ori r9, t₀, 0 when M.minv.toNat = 1, and the load and mulld otherwise. qrowM starts with it. The choice is made inside the block, so the code's shape does not change.
• Proof/Mont/PPC64LE/Ops.lean:
  • qhead_ok gives either branch as r9 = t₀ · mp mod 2⁶⁴ for some mp with m · mp ≡ -1.
  • qrowM_ok now starts from qhead_ok, and the rest of its proof is unchanged.
  • QPre gains one: m' = 1 means the word at [M.tmp] is 1. rmul4_ok already knows that word is M.minv.
• The only crate changes are vg_p256_mul_mod_p and vg_p192_mul_mod_p: in each, one ld and one mulld become one ori.

No TCB or Spec change. The statements of rmul4_ok and mulFn_ok are unchanged.

Testing

• The full lake build and Emit.lean pass, as does Emit.lean --check (run before the rebase onto 7bb62d40).
• The static checks and check_lean_public_imports.py pass.
• The ppc64le tests run in CI.

Benchmark

POWER9, run 42540441353, scoped to arches=powerpc64, base 7bb62d40:

Benchmark	Base	Head	Change
ec_p256_public_key/65	57.57 µs	49.67 µs	13.7% faster
ecdh_p192/24	257.47 µs	189.28 µs	26.5% faster
ecdh_p256/32	202.45 µs	167.48 µs	17.3% faster
ecdsa_p256_sha256_sign/64	77.43 µs	84.15 µs	8.7% slower
ecdsa_p256_sha256_sign/1024	80.73 µs	73.66 µs	8.8% faster
ecdsa_p256_sha256_sign/16384	134.11 µs	126.66 µs	5.6% faster
ecdsa_p256_sha256_verify/64	262.55 µs	227.95 µs	13.2% faster
ecdsa_p256_sha256_verify/1024	265.73 µs	223.90 µs	15.7% faster
ecdsa_p256_sha256_verify/16384	318.92 µs	278.45 µs	12.7% faster
ecdsa_p256_sha384_sign/64	80.51 µs	71.22 µs	11.5% faster
ecdsa_p256_sha384_sign/1024	81.78 µs	73.70 µs	9.9% faster
ecdsa_p256_sha384_sign/16384	115.79 µs	107.34 µs	7.3% faster
ecdsa_p256_sha384_verify/64	262.64 µs	220.38 µs	16.1% faster
ecdsa_p256_sha384_verify/1024	264.47 µs	222.76 µs	15.8% faster
ecdsa_p256_sha384_verify/16384	297.69 µs	256.58 µs	13.8% faster

The one slower row, sha256_sign/64, looks like noise. Every other signing row is faster, including the same signature over SHA-384, and the change only removes instructions from the multiplication.

---

Generated by Claude Code