[alex]

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

Before this change, every call of a curve's field function stored the modulus into its working space with setConst, which takes 24 instructions for four words. Add and sub then ran the memory chains of Impl/Mont/PPC64LE.lean. For moduli of at most four words (P-192, P-224, P-256, secp256k1, brainpoolP256r1, and their n), nothing touches the modulus in memory any more.

• Impl/Mont/PPC64LE.lean:
  • movImm64 loads a 64-bit constant into a register, in one to five instructions.
  • rmul4's qload puts the words of m into mReg as immediates (mword m j) instead of loading them.
  • add4 and sub4 keep the sum or difference in r7–r10.
    • add4 subtracts m with immediates. When that borrows, the mask (carry + CA) - 1 adds m back.
    • sub4 adds m back under the borrow's mask (subfe r11, r11, r11).
• Impl/Weierstrass/PPC64LE/Mont.lean:
  • The entry stores the modulus only for more than four words.
  • addFn and subFn choose add4/sub4 inside their block, as rmulSel does, so the code's shape and noFrames do not change.
• Proof/Mont/PPC64LE/Ops.lean:
  • movImm64_ok, add4_ok and sub4_ok.
  • rmul4_ok now takes RegPre, which is OpPre without the modulus in memory, and m < 2^(64n).
• Proof/Weierstrass/PPC64LE/MontFn.lean:
  • entry_ok gives the modulus in memory only for n > 4.
  • The statements of mulFn_ok, addFn_ok and subFn_ok are unchanged.
• The register rule for callers is the same: callers keep public values in r14 and r25–r31. The docs of Call.lean and mulCall_ok now say that the multiplication saves and restores registers within r15–r24 (r15–r(15 + 2n) for at most four words).

P-256's add goes from 95 to 65 instructions, sub from 89 to 45, and mul from 146 to 131 (static counts).

No TCB or Spec change.

Testing

• The full lake build, Emit.lean and Emit.lean --check pass. The crate changes are the ≤4-word moduli's add/sub/mul functions, their assembly, and ecdh_p256.rs.
• The static checks and check_lean_public_imports.py pass.
• The ppc64le tests run in CI.

Benchmark

POWER9, run 42538012356, scoped to arches=powerpc64, base 7cfde1c4:

Benchmark	Base	Head	Change
ec_p256_public_key/65	67.89 µs	57.35 µs	15.5% faster
ecdh_brainpoolp256r1/32	290.04 µs	229.07 µs	21.0% faster
ecdh_p192/24	365.63 µs	256.65 µs	29.8% faster
ecdh_p224/28	272.12 µs	200.98 µs	26.1% faster
ecdh_p256/32	272.44 µs	201.78 µs	25.9% faster
ecdh_secp256k1/32	339.19 µs	277.38 µs	18.2% faster
ecdsa_p256_sha256_sign/64	585.90 µs	444.84 µs	24.1% faster
ecdsa_p256_sha256_sign/1024	589.04 µs	447.55 µs	24.0% faster
ecdsa_p256_sha256_sign/16384	640.34 µs	500.06 µs	21.9% faster
ecdsa_p256_sha256_verify/64	361.19 µs	279.64 µs	22.6% faster
ecdsa_p256_sha256_verify/1024	365.45 µs	282.61 µs	22.7% faster
ecdsa_p256_sha256_verify/16384	418.28 µs	335.43 µs	19.8% faster
ecdsa_p256_sha384_sign/64	587.65 µs	446.03 µs	24.1% faster
ecdsa_p256_sha384_sign/1024	588.51 µs	448.71 µs	23.8% faster
ecdsa_p256_sha384_sign/16384	622.13 µs	481.74 µs	22.6% faster
ecdsa_p256_sha384_verify/64	361.81 µs	279.37 µs	22.8% faster
ecdsa_p256_sha384_verify/1024	363.37 µs	281.50 µs	22.5% faster
ecdsa_p256_sha384_verify/16384	396.57 µs	314.91 µs	20.6% faster

---

Generated by Claude Code