[alex]

Part of #4141 (PPC64LE audit, finding 1: per-operation cost of the curves).

Every curve's field multiplication on PPC64LE, vg_<curve>_mul_mod_<p|n>, kept the CIOS accumulator T in memory. Each step of a row loaded t_j and stored it back, so every carry chain ran through store-to-load forwarding. In P-256's ECDH this function is about 70% of the time: 52 calls per window, about 470 instructions each.

Change

• Impl/Mont/PPC64LE.lean: rmul replaces mul. The n + 1 words of T live in r15–r(15 + n) (treg).
  • The rows (rrowB, rrowM), the step (rmac) and the reduction (rcsub) are mul's, with registers in place of words: the second row moves each word one register down.
  • The registers are callee-saved, so rmul saves them in its own working space, where the accumulator was, clears them, and restores them at the end.
  • For P-256 this takes the function from 467 to 357 instructions run, and the loop body from 85 to 67, with no load or store of T.
  • The memory version (mul, its rows and their proofs) is deleted.
• Proof/Mont/PPC64LE/Ops.lean: rmul_ok, with the same statement as the old mul_ok: the same result, written ranges and Kp opClob.
  • The restored registers are what make Kp hold.
  • It is built from rmacs_ok, rrow_ok (invariant RLoopInv), rloop_ok, rcsub_ok and the save, clear and restore lemmas.
• Proof/Weierstrass/PPC64LE/MontFn.lean: mulFn_ok uses rmul_ok. Its statement is unchanged, so no caller's proof changes.

Callers: which registers stay public

The constant-time analysis (Proof/Framework/PPC64LE/Taint.lean) treats memory as secret. A register restored from the stack is therefore secret after a call, even though it holds the caller's value again. A value that must be public after a field multiplication — a pointer or a counter — has to be in r14 or r25–r31.

That is why treg starts at r15: the signing, key and ECDH code keep their output pointer in r14 and their counters in r31. The rule is stated in Impl/Weierstrass/PPC64LE/Call.lean's module doc and in mulCall_ok's docstring. The open PPC64LE curve branches (the combs, brainpool, #4747) keep their public values only in r14 and r31.

No TCB or Spec change.

Testing

• The full lake build, Emit.lean and --check pass. The crate changes are every curve's internal/vg_*_mul_mod_{p,n} and ecdh_p256.rs (its literal includes the callee).
• Every artifact that calls these functions passes taint_decide again.
• The static checks and check_lean_public_imports.py pass.
• The ppc64le tests run in CI.

Benchmark

POWER9, run 42528026249 against main (cd85a7b), arches=powerpc64, ECDH, ECDSA and keys for P-256, P-224 and brainpoolP256r1, with OpenSSL. The deterministic operations:

Benchmark	Base	Head	Change	OpenSSL
ecdh_p256/32	414.69 µs	317.93 µs	23.3% faster	106.47 µs
ecdh_p224/28	410.25 µs	359.67 µs	12.3% faster	152.66 µs
ecdh_brainpoolp256r1/32	792.84 µs	341.73 µs	56.9% faster	512.52 µs
ec_p256_public_key/65	116.34 µs	88.23 µs	24.2% faster	16.42 µs
ec_p224_public_key/57	766.78 µs	596.27 µs	22.2% faster	59.33 µs
ec_brainpoolp256r1_public_key/65	912.32 µs	899.39 µs	1.4% faster	441.15 µs

An earlier run (42526697406, on the previous base) measured ecdh_p256 409 → 314 µs and ec_p256_public_key 861 → 648 µs, from before #4729's comb.

The ECDSA rows of the same run are noisy on this runner, between 23% slower and 68% faster for the same code at different message sizes. Most are faster: P-256 signing 12–32%, P-256 verification 1–52%, P-224 signing 42–68%. Two of brainpoolP256r1's verification rows came out 12% and 24% slower. Nothing in this change runs more instructions, so I read those two rows as the runner's variance; they can be re-measured on request.

---

Generated by Claude Code