diff options
author | 2017-06-09 22:11:26 -0400 | |
---|---|---|
committer | 2017-06-09 22:11:26 -0400 | |
commit | 8ac6a73847e49aa89136c28d02ad6fdd0c72a209 (patch) | |
tree | fd3811074fd75a195be29e2b010a627f00f8a511 /src/Arithmetic/MontgomeryReduction | |
parent | 79f5b2e1089c50a18b94da2b22fefdec90392abb (diff) |
Admit-free proof of cS3_mod_N
Fix the algorithm to not talk about join, based on
http://colinandmargaret.co.uk/Research/CDW_ELL_99.pdf (p2) and
discussions over Signal with @andres-erbsen.
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v | 108 |
1 files changed, 13 insertions, 95 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v index 3d54294f7..44a62c5fe 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v @@ -21,11 +21,8 @@ Section WordByWordMontgomery. {R : positive}. Local Notation bn := (r * R) (only parsing). Context - {add : T -> T -> T * Z} (* produces carry *) - {eval_fst_add : forall a b, eval (fst (add a b)) = (eval a + eval b) mod bn} - {eval_snd_add : forall a b, snd (add a b) = (eval a + eval b) / bn} - {join : T * Z -> T} (* adds limb to high end *) - {eval_join : forall p, eval (join p) = eval (fst p) + (bn / r) * (snd p)} + {add : T -> T -> T} (* joins carry *) + {eval_add : forall a b, eval (add a b) = eval a + eval b} {eval_nonneg : forall v, 0 <= eval v} (N : T) (Npos : positive) (Npos_correct: eval N = Z.pos Npos) (B : T) @@ -35,10 +32,8 @@ Section WordByWordMontgomery. Hint Rewrite eval_div eval_mod - eval_fst_add - eval_snd_add + eval_add eval_scmul - eval_join : push_eval. @@ -49,12 +44,11 @@ Section WordByWordMontgomery. Context (k : Z) (k_correct : k * eval N mod r = -1). (* Given A, B < R, we want to compute A * B / R mod N. R = bound 0 * ... * bound (n-1) *) Let A_a := dlet p := divmod A in p. Let A' := fst A_a. Let a := snd A_a. - Let S1 := fst (add S (scmul a B)). + Let S1 := add S (scmul a B). Let s := snd (divmod S1). Let q := s * k mod r. Let cS2 := add S1 (scmul q N). - Let c := snd cS2. - Let S3 := fst (divmod (fst cS2)). + Let S3 := fst (divmod cS2). Local Coercion eval : T >-> Z. @@ -64,12 +58,12 @@ Section WordByWordMontgomery. Lemma S3_bound : 0 <= eval S < eval N + eval B - -> 0 <= eval (join (S3, c)) < eval N + eval B. + -> 0 <= eval S3 < eval N + eval B. Proof. Unset Printing Coercions. intro HS. - unfold S3, c. - Local Notation "x 'div' 'r'" := (join ((fst (divmod (fst x)), snd x))) (at level 10). + unfold S3. + Local Notation "x 'div' 'r'" := (fst (divmod x)) (at level 10). unfold cS2. Local Infix "+" := add (only printing). Local Infix "*" := scmul (only printing). @@ -102,86 +96,20 @@ Section WordByWordMontgomery. *) Abort. - Lemma S_aB_over_R_bound : (eval S + a * eval B) / R <= 1 + ((r - 1)^2 / r + 1 + 1). - Proof. - assert (Hmod0 : forall v r, 0 < r -> v mod r < r) by (intros; apply Z_mod_lt; lia). - assert (Hmod : forall v r, 0 < r -> v mod r <= r - 1) by (intros v m; specialize (Hmod0 v m); omega). - rewrite (Z_div_mod_eq (eval S) R), <- Z.add_assoc, Z.div_add_l' by lia. - apply Z.add_le_mono; auto. - transitivity ((R-1 + (r-1)*(R-1)) / R). - { Z.peel_le; apply Z.add_le_mono; auto with lia. - unfold a, A_a, Let_In. - autorewrite with push_eval. - apply Z.mul_le_mono_nonneg; try solve [ auto with lia | lia | apply Z_mod_lt; lia ]. } - { admit. (* - Unset Printing Coercions. - Require Import Algebra.Ring. - ring_simplify_subterms. - - transitivity (r + (-r) / R). - admit. - transitivity (r - 2 + 1/r + 2); [ | admit ]. - transitivity r. - admit. - - am - SearchAbout ((?x * _ + _) / ?x). - - - - SearchAbout ((?x * _ + _) / ?x). - SearchAbout (?x / ?y) (?x mod ?y). - SearchAbout ((_ + _) / _). *) } - Admitted. - - Lemma S_aB_range : 0 <= eval S + a * eval B < bn. - Proof. - pose proof S_aB_over_R_bound. - assert (eval S + a * eval B <= (R - 1) + R + ((Z.pos r - 1) ^ 2 / Z.pos r + 1 + 1) * R) by admit. - (*Z.div_mod_to_quot_rem. - nia. - assert (eval A mod Z.pos r < r) by (apply Z_mod_lt; lia). - assert (Hmod : eval A mod Z.pos r <= r - 1) by omega. - repeat match goal with H := _ |- _ => progress unfold H end. - unfold Let_In. - rewrite eval_mod. - split; [ solve [ auto with zarith ] | ]. - eapply (@Z.le_lt_trans _ (2 * R - 1 + (r - 1) * (R - 1))). - Focus 2. - rewrite Z.mul_sub_distr_l, !Z.mul_sub_distr_r, !Z.add_sub_assoc. - Require Import Crypto.Algebra.Ring. - ring_simplify_subterms. - Unset Printing Coercions. - autorewrite with zsimplify. - change - repeat (apply Z.add_le_mono || apply Z.mul_le_mono_nonneg); try lia. - Z.peel_le. - rewrite S_small. - - Focus 2. - Unset Printing Coercions. - - rewrite Z.mul_sub_distr_l, !Z.mul_sub_distr_r, !Z.add_sub_assoc. - autorewrite with zsimplify. - omega. - autorewrite with *) - Admitted. - Lemma S1_eq : eval S1 = S + a*B. Proof. cbv [S1 a A']. repeat autorewrite with push_eval. - rewrite (Z.mod_small _ bn) by (apply S_aB_range). reflexivity. Qed. - Lemma cS2_mod_N : (eval (fst cS2) + bn * snd cS2) mod N = (S + a*B) mod N. + Lemma cS2_mod_N : (eval cS2) mod N = (S + a*B) mod N. Proof. assert (bn_large : bn >= r) by (unfold bn; nia). cbv [cS2 q s]; autorewrite with push_eval zsimplify. rewrite S1_eq. reflexivity. Qed. - Lemma cS2_mod_r : fst cS2 mod r = 0. + Lemma cS2_mod_r : cS2 mod r = 0. cbv [cS2 q s]; autorewrite with push_eval. assert (r > 0) by lia. assert (Hr : (-(1 mod r)) mod r = r - 1 /\ (-(1)) mod r = r - 1). @@ -189,7 +117,6 @@ Section WordByWordMontgomery. { rewrite H'; split; reflexivity. } { rewrite !Z_mod_nz_opp_full; rewrite ?Z.mod_mod; Z.rewrite_mod_small; [ split; reflexivity | omega.. ]. } } autorewrite with pull_Zmod. - rewrite (Z.mod_small _ bn) by admit. replace 0 with (0 mod r) by apply Zmod_0_l. eapply F.eq_of_Z_iff. repeat rewrite ?F.of_Z_add, ?F.of_Z_mul, <-?F.of_Z_mod. @@ -208,22 +135,13 @@ Section WordByWordMontgomery. change (-(1)) with (-1) in *. 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. + Qed. Lemma cS3_mod_N ri (ri_correct : r*ri mod N = 1 mod N) - : join (S3, c) mod N = (S + a*B)*ri mod N. + : S3 mod N = (S + a*B)*ri mod N. Proof. assert (r_div_bn : (r | bn)) by apply Z.divide_factor_l. - cbv [S3 c]; autorewrite with push_eval cancel_pair. - replace (eval (fst cS2) / Z.pos r + (bn / r) * snd cS2) - with ((eval (fst cS2) + bn * snd cS2) / Z.pos r) - by (rewrite Z.div_add_exact, !(Z.mul_comm bn), Z.divide_div_mul_exact - by (assumption || apply cS2_mod_r || lia); nia). + cbv [S3]; autorewrite with push_eval cancel_pair. pose proof fun a => Z.div_to_inv_modulo N a r ri eq_refl ri_correct as HH; cbv [Z.equiv_modulo] in HH; rewrite HH; clear HH. etransitivity; [rewrite (fun a => Z.mul_mod_l a ri N)| |