CRT support for signing?

[tomato42]

Is your feature request related to a problem? Please describe.
The implementation of RSAPSS doesn't seem to be using the CRT optimisation:

hacl-star/code/rsapss/Hacl.Spec.RSAPSS.fst

Lines 317 to 324 in d59b0b0

	let k = blocks modBits 8 in
	Math.Lemmas.pow2_le_compat (bits * nLen) modBits;
	SM.bn_precomp_r2_mod_n_lemma (modBits - 1) n;
	let s = bn_mod_exp_consttime_precompr2 nLen n r2 m dBits d in
	let m' = bn_mod_exp_vartime_precompr2 nLen n r2 s eBits e in
	let eq_m = bn_eq_mask m m' in
	let s = map (logand eq_m) s in
	BB.unsafe_bool_of_limb eq_m, s

Describe the solution you'd like
It would be nice if the code used the Chinese Reminder Theorem optimisation, as that would increase performance by a factor of 2 to 3

Describe alternatives you've considered
Not using CRT hurts performance in typical case

Additional context
Basically every production grade implementation of RSA uses the CRT approach for the RSA private key operation.

That being said, I'm far from familiar with F*, so I may be reading the code completely incorrectly, feel free to point out to me that I'm reading the code incorrectly or looking at wrong piece of code.

[karthikbhargavan]

Good point, we do not do this yet, because the code is designed to be super general.

[tomato42]

OK, but

1. it's a significant performance difference
2. 99% of keys people will want to use in practice will have CRT coefficients included
3. it's possible to recover p, and q from d using algorithm specified in appendix C (page 118) of NIST SP-800-56B rev 1
4. the code can use either algorithm, depending on which coefficients were provided