[alex]

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

For curves of at most four words (P-192, P-224, P-256, secp256k1, brainpoolP256r1, and their n), vg_<curve>_mul_mod_<p|n> now runs rmul4 in place of #4757's rmul:

• [b] and m in registers. [b] sits in the registers after the accumulator, r(16 + n) up (bReg), and the modulus in r6, r7, r10, r0 (mReg), each loaded once per call. A row step no longer loads either.
• Each row is two carry chains (pass): the low words of x · y_j go into the accumulator with adde, then the high words one word up. A product's words no longer need carries of their own, so a step is a multiplication and an adde, two instructions where it was seven.
• The second row's high chain also moves the accumulator one register down, so the shift costs nothing extra.
• m' is at [M.tmp] until the reduction, which subtracts m straight from its registers (qcsub, reusing rcsub's selection).

For P-256 the function now runs 284 instructions instead of 357, with a loop body of 46 instead of 67. Moduli of more words keep rmul.

rmulSel puts the choice between the two inside the code blocks, so the program's shape (noFrames) does not depend on it, and the callers' rfl proofs of it are unchanged.

Proofs

Proof/Mont/PPC64LE/Ops.lean:

• pass_ok: the chain lemma, built on gval/pv and pv_split, x · B = lo + 2⁶⁴ hi.
• qrowB_ok and qrowM_ok: the two rows. The second shows the dropped low word is zero, from mont_low.
• qrow_ok and qloop_ok: the iteration, with invariant QLoopInv, and the loop.
• qsubs_ok and qcsub_ok: the reduction.
• qloadB_ok and qloadM_ok: the loads of [b] and m.
• rmul4_ok: the whole function, with rmul_ok's statement but Kp (.r6 :: opClob). That is still inside fnClob, so mulFn_ok's statement is unchanged and no caller's proof changes.

The registers saved and restored are now r15–r(15 + 2n), at most r23, so #4757's rule for callers still holds: keep public values in r14 or r25–r31.

No TCB or Spec change.

Testing

• The full lake build, Emit.lean and the static checks pass. The crate changes are the internal vg_*_mul_mod_{p,n} of every curve of at most four words.
• check_lean_public_imports.py passes.
• Every artifact that calls the functions passes taint_decide again.
• The ppc64le tests run in CI.

Benchmark

POWER9, run 42533245411 against main (85135ee), arches=powerpc64:

Benchmark	Base	Head	Change
ecdh_p256/32	306.49 µs	276.95 µs	9.6% faster
ecdh_p224/28	305.75 µs	275.43 µs	9.9% faster
ecdh_secp256k1/32	389.48 µs	343.30 µs	11.9% faster
ecdh_brainpoolp256r1/32	329.19 µs	294.05 µs	10.7% faster
ec_p256_public_key/65	76.33 µs	69.14 µs	9.4% faster
ec_p224_public_key/57	556.09 µs	496.91 µs	10.6% faster
ecdsa_p256_sha256_sign/64	656.58 µs	587.40 µs	10.5% faster
ecdsa_p256_sha256_verify/64	684.61 µs	608.52 µs	11.1% faster
ecdsa_p224_sha224_sign/64	579.21 µs	514.09 µs	11.2% faster
ecdsa_p224_sha224_verify/64	599.58 µs	532.16 µs	11.2% faster

Every other row of the run (the 1024- and 16384-byte messages, and SHA-384 with P-256) is 9.3–12.4% faster.

An earlier run, 42531318690, against #4757's head, measured ecdh_p256 4% slower but verification 10% faster. This run, on the rebased branch, does not reproduce the slowdown: every row is faster by a similar margin.

---

Generated by Claude Code