[alex]

From the rustls provider analysis in #991. rustls loads server keys with PrivateKey::from_crt, which ran at 0.10–0.20 of aws-lc-rs's speed because it checked the key with a whole constant-time private-key operation on 0. This PR replaces that check, on x86-64, with vg_rsa_check_crt_key, whose spec is #1343.

Stacked on #1343 (the spec, Spec/Rsa.lean and Spec/Rsa/Contract.lean). This PR changes no file in Spec/ or TCB/.

Implementation (Impl/ + Proof/ + registration)

Impl/Rsa/X86_64/CheckCrtKey.lean is vg_rsa_check_key's code with the checks of d removed and the remainders shortened:

• Its entry stores the arguments in vg_rsa_check_key's header slots, with p also in d's slots, which nothing reads. That lets the proof reuse check_key's context (MainPre, KCtx, KK) and its proven pieces: loads, ltMask, p q = n, mulE, mulXR and eqOne.

• e and n are checked first. Those are the only branches; every other check is and'ed into a mask, so timing depends only on the lengths, n and e.

• Shorter restoring division (reduceTop). vg_rsa_check_key divides a product by doubling once per bit of the whole product, over n's width: 64 (w + 2) or 64 (2 w + 2) doublings of w-word numbers. Here each remainder needs a small quotient only when the comparison before it holds:

  • e dX < 2^33 (X − 1) when dX < X − 1
  • q qInv < 2^(64 c) p when qInv < p, for c = ⌈q_len / 8⌉

  So r starts as the product's words from c up, which are below the divisor, and only its low c words are divided a bit at a time. All of this is over numbers as long as the divisor, ⌈len / 8⌉ words. When the comparison fails, the mask is already clear and the remainder isn't used.

Proofs:

• Proof/Rsa/X86_64/CrtKey*.lean
  • reduceTop_ok rests on reduceLoopFrom_ok, which runs check_key's word loop from c words left.
  • Correctness: ckCode_correct.
  • Constant time: ckCode_constantTime. Its reduceTop pieces are checked by taint_decide.
  • ck_implies gives the shared contract, and ck_verified the Verified theorem.
• Proof/Rsa/CrtKeyParts.lean (crtKeyValid_parts) shows the masks the code computes equal crtKeyValid.
• KeyReduce.lean's loop invariants gain a hypothesis Q (check_key passes True), so the loop can run from a remainder known only under the comparison.

Before writing the proofs, I ran the code on the x86-64 model interpreter (scratch only, not committed) with a 512-bit key and 10 altered versions. It agreed with checkCrtKey on all 11: the valid key, swapped primes, each of dP, dQ, qInv off by one, dP + p − 1, qInv + p, leading zeros on p and on q, e = 3, and q + 2.

Rust

PrivateKey::from_crt

• On x86-64 it calls vg_rsa_check_crt_key and returns InvalidPrivateKey unless it returns 1.
• On AArch64 it keeps today's check, the private-key operation on 0, because there is no AArch64 implementation yet (a follow-up). CLAUDE.md allows a cfg for a function only one target has, and the docs say so.
• private_op is unchanged, including its fault check.

What from_crt guarantees, before and after

• Before, on both targets, it accepted a key exactly when the operation released a result for 0. That held when:

  • n is valid (odd, 512–8192 bits, no leading zero byte) and e is within BoringSSL's limits
  • p q = n and qInv < p
  • the CRT result m for 0 passes m^e ≡ 0 (mod n), which fails only in degenerate cases such as dP = 0 with qInv ≠ 0

• After, on x86-64, it accepts a key exactly when checkCrtKey holds: RSA_check_key's checks without d.

  • Valid n and e; p q = n
  • dP < p − 1 and e dP ≡ 1 (mod p − 1); dQ < q − 1 and e dQ ≡ 1 (mod q − 1)
  • qInv < p and q qInv ≡ 1 (mod p)

  This implies everything the operation checks of the key, so a refusal from private_op still means the input is out of range. It also implies dP, dQ ≥ 1, so 0's result is 0: every key accepted now was accepted before. Keys whose CRT values don't match e are now refused at load with InvalidPrivateKey, where before they loaded and every operation returned Fault. Like RSA_check_key, nothing checks that p and q are prime, which is why private_op's fault check still matters.

• from_primes (and from_components) go through from_crt, so on x86-64 they now also require d e ≡ 1 modulo p − 1 and q − 1. Their docs say so.

Tests

• Tests that loaded inconsistent keys to reach Fault would now fail at load. They use a new helper instead, rsa::tests::composite: CRT values that match e = 3 for composite factors.
  • p = 2^(8a) − 1, q = 2^(8a) + 1, n = 2^(16a) − 1
  • dP = p/3, dQ = (2^(8a+1) + 1)/3, qInv = 2^(8a−1)
  • The key passes every check, but the operation's result for 2 still fails its check against e.
  • Sizes: a from 32 to 511, either prime first.
• private_invalid covers each new check.
• from_primes with d = p dP passes check_key.
• rsa_pkcs1_enc gets a unit test of its Fault path, which only tests/rsa_guidance reached before.
• tests/rsa_guidance and tests/wycheproof/rsa_keys.rs expect mismatched CRT values to be refused on x86-64.

Benchmark

Measured with the rsa_from_crt group from #1352 (its own PR, so not in this one). Sapphire Rapids, VG_CPU_FEATURES=avx,avx2,avx512f,bmi2,adx, OPENSSL_ia32cap=":~0x200000", mean times:

bytes	before	after	aws-lc-rs	after vs aws-lc-rs
256	744 µs	42.8 µs	147 µs	3.4× faster
384	2.24 ms	88.0 µs	253 µs	2.9× faster
512	4.92 ms	169 µs	494 µs	2.9× faster

Local checks run before pushing:

• cargo fmt and clippy -D warnings
• RSA tests with Wycheproof, by default and with VG_CPU_FEATURES=none and avx,avx2,bmi2,adx
• check_vectors, check_arch_gates, check_variants, check_mcdt, check_lean_imports, check_lean_speed and cpu_tests lint
• the full lake build and Emit.lean

algorithms_table.py leaves the README unchanged.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PqW9NMssoiBx9i4PpksckL

---

Generated by Claude Code