diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-09 21:51:16 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-09 21:51:16 -0400 |
| commit | af22c75aab190683c2f6a199d91fe2d110fb739d (patch) | |
| tree | 0535db658dd942837dde3bdeb173aeec700709d6 /src/Arithmetic/MontgomeryReduction | |
| parent | 09ea18c06030ee2416aea20efb709b9c56f50e1d (diff) | |
Minor progress on bounds
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v index cb5e325b7..8d11c9062 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v @@ -127,10 +127,9 @@ Section WordByWordMontgomery. Proof. cbv [S1 a A']. repeat autorewrite with push_eval. - rewrite (Z.mod_small _ bn). (* by (apply aB_range). *) + rewrite (Z.mod_small _ bn) by (apply S_aB_range). reflexivity. - Unset Printing Coercions. - Admitted. + Qed. Lemma cS2_mod_N : (eval (fst cS2) + bn * snd cS2) mod N = (S + a*B) mod N. Proof. @@ -166,7 +165,10 @@ Section WordByWordMontgomery. apply path_sig_hprop; [ intro; exact HProp.allpath_hprop | ]; simpl. rewrite (proj1 Hr), (proj2 Hr); reflexivity. } Grab Existential Variables. - + { unfold S1. + autorewrite with push_eval. + rewrite (Z.mod_small _ bn) by apply S_aB_range. + admit. } Admitted. Lemma cS3_mod_N ri (ri_correct : r*ri mod N = 1 mod N) |