[alex]

This change comes from the rustls provider analysis in #991, which found the RSA private-key operation without AVX512_IFMA slower than aws-lc's. This is the second change for it, after #1357, and removes more of the CRT exponentiation's setup cost.

What changes

vg_rsa_private_crt (x86-64, every variant) needs R² mod n to bring the input into n's Montgomery form. Until now nSetup computed it as vg_rsa_public does:

• it doubled modulo n, one bit at a time, from n's top bit up to 2^w R mod n (doubles, about w doublings over w words each);
• then it squared six times.

It now uses R2Words.choice, which vg_rsa_public_precompute already uses for the same number. When n's top bit is set and w is a multiple of 4, it reaches 2^(16 w) R mod n in w / 4 steps of one word each (long division, Knuth's Algorithm D, with a precomputed reciprocal), then makes two Montgomery squarings. Other moduli take the old computation. Every branch depends only on n and w, both public.

Proofs

• Impl/Rsa/X86_64/Crt.lean: nSetup calls R2Words.choice mul in place of the doubling-and-squaring steps.
• Proof/Bignum/X86_64/CrtFront.lean: the R² step goes through R2w.choice_ok, where it used the local r2_ok.
• Proof/Bignum/X86_64/CrtCTMain.lean: likewise through R2w.choice_ct, where it used r2_ct.

No change to Spec/ or TCB/, and no new multiplication shapes: MmUse already covers every multiplication R2Words.choice makes.

Benchmark

ci/bench_compare.py was too noisy on this VM to resolve a change under 1%: unchanged benchmarks moved by ±20%. So the comparison is an interleaved A/B instead:

• one binary links main and this change;
• it alternates private_op calls between the two with the same OpenSSL-generated key;
• it reports the median of the per-pair time ratios, which frequency drift doesn't affect.

Setup: Sapphire Rapids, VG_CPU_FEATURES=avx,avx2,bmi2,adx (the _adx backend, IFMA excluded), 2000 pairs.

key	head/base median ratio	change
2048	0.9916	0.8% faster
3072	0.9934	0.7% faster
4096	0.9921	0.8% faster

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_vectors, check_arch_gates, check_variants, check_mcdt, algorithms_table (unchanged);
• cargo fmt and clippy -D warnings;
• the RSA tests with Wycheproof, by default and with VG_CPU_FEATURES=none and avx,avx2,bmi2,adx.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PqW9NMssoiBx9i4PpksckL

---

Generated by Claude Code