[alex]

This change comes from the rustls provider analysis in #991. It does on AArch64 what #1355 did on x86-64: rsa::PrivateKey::from_crt checks the key's CRT values with vg_rsa_check_crt_key instead of a private-key operation on 0.

Guarantee, before and after

• Before (AArch64): from_crt ran the constant-time private-key operation on 0. That checks:

  • the modulus is valid, p q = n and qInv < p (the operation's own preconditions);
  • the result for 0, which is 0 for any key, passes its check against e.

  It accepted keys whose dP, dQ or qInv do not match: those failed later, at every private_op, with Error::Fault.

• After: from_crt accepts a key exactly when Spec.Rsa.checkCrtKey does, as on x86-64. That is BoringSSL's RSA_check_key on (n, e, p, q, dP, dQ, qInv):

  • 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 what private_op needs (a valid modulus, p q = n, qInv < p). private_op keeps its own check of each result against e.

The Rust code no longer differs by architecture: the #[cfg] split in privatekey.rs and in the tests (rsa_guidance, wycheproof/rsa_keys, private_invalid, private_from_primes) is gone.

The code

Impl/Rsa/AArch64/CheckCrtKey.lean is vg_rsa_check_key's code without the checks of d, in its layout:

• The entry stores p in d's header slots too, so the proofs reuse CkIn, CkS and the phases of vg_rsa_check_key with p as d.
• e and n are checked first; those are the only branches on the key.
• Every other check is computed whatever its outcome and and'ed into a mask.

Each remainder (e dP mod (p - 1), e dQ mod (q - 1), q qInv mod p) is shorter than vg_rsa_check_key's divmod, which runs 64 W steps of bit-serial division over the layout's W = 2 w + 2 words. reduceTop instead:

• starts the remainder at the product's words above its low c;
• puts the low c words at the top of the quotient's register;
• runs 64 c steps.

Here c = 1 for e dX (e < 2^64) and c = ⌈q_len / 8⌉ for q qInv. When the comparison before each remainder holds, the words from c up are below the divisor, so the result is the full remainder (divIter_top, Proof/Rsa/KeyMath.lean). When it fails, the mask is already clear.

Proofs

• Proof/Rsa/KeyMath.lean: divIter_from, divIter_top (restoring division from a partial remainder).
• Proof/Rsa/AArch64/CrtKeyTop.lean: reduceTop_ok, through blkHi_ok, blkLo_ok, blkCnt_ok and stepsTop_ok.
• CrtKeyPhase.lean: ckReduceTop_ok, topE_ok, topQ_ok, ckModOneTop_ok, phModC_ok, phQIC_ok.
• CrtKeyMain.lean: ckcMain_ok; the mask is crtKeyValid (ckc_final).
• CrtKeyCode.lean: ckcA, the shared contract on the registers and the stack, and ckcCode_correct.
• CrtKeyCT.lean, CrtKeyCTCode.lean: constant time. Each reduceTop block reads w and c from the header; its output registers are pinned to the public data by the lemmas above.
• CrtKeyVerified.lean: ckc_implies, ckc_verified.
• Artifacts/Rsa/AArch64.lean: the checkCrtKeyApi artifact.

No change to Spec/ or TCB/ (the spec is #1343's).

Benchmark

bench.yml on AArch64 (Neoverse N2, CPU part 0xd49), base_commit = main, rsa module:

benchmark	base	head	change	aws-lc-rs
rsa_from_crt/256	1.71 ms	158.95 µs	10.8× faster	140.31 µs
rsa_from_crt/384	5.45 ms	332.91 µs	16.4× faster	285.75 µs
rsa_from_crt/512	12.68 ms	570.91 µs	22.2× faster	481.00 µs
rsa_from_primes/256	2.86 ms	1.31 ms	54% faster	–
rsa_from_primes/512	17.13 ms	5.01 ms	71% faster	–
rsa_from_components/256	18.54 ms	16.99 ms	8.4% faster	–

Every other RSA benchmark is within ±0.1%. from_crt is now 1.1–1.2× of aws-lc-rs's key loading, which also checks the key.

Checks run locally:

• the full lake build and Emit.lean;
• check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt, algorithms_table;
• cargo fmt, and clippy -D warnings for x86-64 and --target aarch64-unknown-linux-gnu;
• the RSA tests with Wycheproof on x86-64.

This machine can't run AArch64 code, so CI runs the AArch64 tests. Running the code through the Lean model's interpreter caught one bug before the proofs reached it: head in CheckCrtKey resolved to the enclosing namespace's head, which doesn't set the mask. The code now names CheckKey.head.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PqW9NMssoiBx9i4PpksckL

---

Generated by Claude Code