Refined/Signed Barrett Reduction #2013
Conversation
There was a problem hiding this comment.
👍 , I'd be happy to have this with or without whatever changes my comments inspire you to undertake
cc @jadephilipoom who looked into Barrett reduction variants earlier
| apply Z.mod_eq. discriminate. | ||
| Qed. | ||
|
|
||
| Definition signed_mod: Z -> positive -> Z := mod_approx Qround_half_up. |
There was a problem hiding this comment.
Is this the same operation as https://github.com/coq/coq/pull/19753/files#diff-e9ef30d177736b8c6718e9269085a03dafd5a90d3a65225c622e297474a97909R78 ? I think I have a slight preference towards importing that one if so.
There was a problem hiding this comment.
Yes, here is a proof below. I don't mind using your smodulo as the specification instead, do you want to add your file to Fiat-Crypto first and I rebase over it? Or the other way around, merge this first and you can fix it in another PR later?
Lemma smodulo_eq_signed_mod (a: Z) (b: positive):
smodulo a b = signed_mod a b.
Proof.
cbv [smodulo]. rewrite (omod_inj_mod _ a (signed_mod a b)) by (apply Zmod_signed_mod).
apply omod_small_iff. left.
rewrite Z.quot_div_nonneg by lia.
rewrite signed_mod_eq_Zmod. pose proof (Zlt_cases (2 * (a mod b)) b) as Hlt.
destruct (_ <? _); Z.to_euclidean_division_equations; lia.
Qed.|
|
||
| (* Barrett reduction is the special case with b = 1 *) | ||
| Definition barrett_multiplication_approx | ||
| (approx: Q -> Z) (R a b: Z) (q: positive): Z := |
There was a problem hiding this comment.
approx seems to be always called with freshly constructed fractions, maybe it would look better taking two arguments?
| (approx: Q -> Z) (R a b: Z) (q: positive): Z := | ||
| (a * b - q * Qround_half_up ((a * (approx ((b * R)#q)))%Z / R))%Z. | ||
|
|
||
| (* Not the same bounds on |a| and |b| as in the paper, as theirs cannot be proved *) |
There was a problem hiding this comment.
This sounds like it could be a fun story. Did formal verification help identify a gap here?
There was a problem hiding this comment.
I don't think formal verification was necessary to identify the issue here. I believe it's mainly an off-by-1 calculation error, unless I'm missing something in the reasoning.
This is Fact 2 on page 7 https://eprint.iacr.org/2022/439.pdf
One difference is that they consider |a| < 2 ^ (M - 1) which would fail to account for a = INT16_MIN = - 2 ^ 15 when M = 16. Though, this doesn't really change the proof.
The main issue is at the end of their proof on page 7, where one needs to prove that |a| < (2^(k + w - 1)) / q, and since q < 2 ^ (1 + log2 q), then it should suffice to show that |a| <= (2^(k + w - 1)) / (2 ^ (1 + log2 q)) = 2 ^ (k + w - 2 - log2 q), whereas the paper concludes with 2 ^ (k + w - 1 - log2 q).
| (approx: Q -> Z) (M R a b: Z) (k q: positive) | ||
| (Hk: Qabs (((b * R)#q) - approx ((b * R)#q)) <= 1#(Pos.pow 2 k)) | ||
| (HOddq: Z.Odd q) (HR: R = Z.pow 2 (M - 1 + Z.log2 q - Z.log2_up (Z.abs b))%Z) | ||
| (HM: (2 <= M)%Z) (Ha: (Z.abs a <= Z.pow 2 (M - 1))%Z) |
There was a problem hiding this comment.
I understand there is some value in following the paper here, but I do wonder whether Z.pow 2 (M - 1) could be quantified over instead of `M and so on.
This proves the correctness of the Barrett reduction strategy that is used for instance in Kyber/ML-KEM with regards to a signed modulo operation.
I haven't proved that this signed modulo operation gives rise to a field structure isomorphic to the usual one used in Fiat-Crypto, though it shouldn't be too hard if one needs it.