[alex]

From the rustls provider analysis in #991: the RSA private-key operation without AVX512_IFMA is slower than aws-lc's. This is the first change for it. It removes most of the CRT exponentiation's setup cost per prime.

What changes

vg_rsa_private_crt (x86-64, every variant) brings the input into each prime's Montgomery form through G = 2^E mod n, where E = 64 w_X (K + 1). Until now gPow computed G as 2^D R with D = E - 64 w: it started from R, then did one squaring at n's width, plus a doubling when the bit was set, for each bit of D. That is about 11 squarings of n per prime.

D is a multiple of 64. When 2^D < n, one multiplication gives the same number: Y := 2^D (one word set), then Y := R² Y R⁻¹ = 2^D R.

• 2^D < n holds when n's top word is nonzero and D / 64 < w - 1. That covers every key with primes of half n's length.
• The code tests exactly those two conditions, which depend only on n and the lengths (public data), and keeps the old loop as the fallback.

Proofs

• Impl/Rsa/X86_64/Crt.lean: gPow gains the test, with gFast and gSlow (the old loop, unchanged).
• Proof/Bignum/X86_64/CrtGPow.lean:
  • gPow_ok's statement is unchanged.
  • It now goes through gLd_ok, gTest_ok, gCmp_ok, and either gFast_ok or gSlow_ok (the old proof).
• Proof/Bignum/CrtGPow.lean: gC (D = 64 gC), wv_top, gFast_lt (2^D < n).
• Proof/Bignum/X86_64/CrtCTGPow.lean: gPow_ct_of is reproven over the new branches. Each branch condition is pinned to public data: n's top word and D / 64 versus w - 1. gFast_ct and gSlow_ct cover the two paths.
• Proof/Bignum/X86_64/Mont.lean: MmUse, the list of multiplications the Montgomery implementations are proven constant time for, gains Y := R² Y (o = aY, a = aR2, b = aY). Each implementation's ct proof (Mont.base, fnBase, adx, adxSquare, fnAdx) covers it with the same taint_decide as the others.

No change to Spec/ or TCB/.

Benchmark

Sapphire Rapids, VG_CPU_FEATURES=avx,avx2,bmi2,adx, OPENSSL_ia32cap=":~0x200000", ci/bench_compare.py --modules rsa --rounds 3 (fastest of 3 interleaved runs per side):

benchmark	base	head	change
rsa_private/256	712.72 µs	679.20 µs	4.7% faster
rsa_private/384	2.14 ms	2.10 ms	1.9% faster
rsa_private/512	4.85 ms	4.78 ms	1.6% faster
rsa_pss_sha256_mgf1_sha256_sign/256	715.19 µs	683.87 µs	4.4% faster
rsa_pss_sha256_mgf1_sha256_sign/384	2.18 ms	2.11 ms	3.1% faster
rsa_pss_sha256_mgf1_sha256_sign/512	4.84 ms	4.77 ms	1.6% faster
rsa_pkcs1_sign/256	708.57 µs	682.59 µs	3.7% faster
rsa_pkcs1_decrypt/256	718.01 µs	691.73 µs	3.7% faster

Every other RSA benchmark is within noise. The IFMA variant calls the same gPow (through vg_rsa_mont_mul_adx), so it gains the same setup time.

Checks run locally: the full lake build and Emit.lean (only src/asm/x86_64/rsa.rs changes), check_lean_imports, check_lean_speed, check_variants, check_mcdt, check_vectors, check_arch_gates, cargo fmt, clippy -D warnings, and the RSA tests with Wycheproof by default (IFMA on this machine) and with VG_CPU_FEATURES=none and avx,avx2,bmi2,adx. algorithms_table.py leaves the README unchanged.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PqW9NMssoiBx9i4PpksckL

---

Generated by Claude Code