diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-24 23:27:27 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-24 23:27:43 -0400 |
commit | e35385ed17d49ddc05928a2cbd74c190516acf66 (patch) | |
tree | 21fc5bd789a0e051d796186ddd7960007e5f50b1 /src/Arithmetic/MontgomeryReduction | |
parent | b2d45a2b52cf2074bb40edea07409fc32372a024 (diff) |
Clean up some montgomery wbw instantiation, make display
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
3 files changed, 7 insertions, 32 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v index 60a3e59fc..266fc1f6f 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v @@ -53,7 +53,7 @@ Section WordByWordMontgomery. {small_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> small (conditional_sub v)} {sub_then_maybe_add : T R_numlimbs -> T R_numlimbs -> T R_numlimbs} (* computes [a - b + if (a - b) <? 0 then N else 0] *) {eval_sub_then_maybe_add : forall a b, small a -> small b -> 0 <= eval a < eval N -> 0 <= eval b < eval N -> eval (sub_then_maybe_add a b) = eval a - eval b + if eval a - eval b <? 0 then eval N else 0} - {small_sub_then_maybe_add : forall a b, small a -> small b -> 0 <= eval a < eval N -> 0 <= eval b < eval N -> small (sub_then_maybe_add a b)} + {small_sub_then_maybe_add : forall a b, small (sub_then_maybe_add a b)} (B : T R_numlimbs) (B_bounds : 0 <= eval B < R) (small_B : small B) diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v index 33a0ea535..1560b702e 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v @@ -26,7 +26,6 @@ Section WordByWordMontgomery. Local Notation addT := (fun n => @Saturated.add (Z.pos r) n n n). Local Notation conditional_sub_cps := (fun V => @conditional_sub_cps (Z.pos r) _ (Z.pos r - 1) V N _). Local Notation conditional_sub := (fun V => @conditional_sub (Z.pos r) _ (Z.pos r - 1) V N). - Local Notation sub_then_maybe_add_cps := (fun V1 V2 => @sub_then_maybe_add_cps (Z.pos r) R_numlimbs (Z.pos r - 1) V1 V2 N). Local Notation sub_then_maybe_add := (fun V1 V2 => @sub_then_maybe_add (Z.pos r) R_numlimbs (Z.pos r - 1) V1 V2 N). diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 6e6b19f3f..837a709b7 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -233,34 +233,10 @@ Section WordByWordMontgomery. (fun p q => @sub_then_maybe_add_cps (Z.pos r) R_numlimbs (Z.pos r - 1) p q N). Local Notation sub_then_maybe_add := (fun p q => @sub_then_maybe_add (Z.pos r) R_numlimbs (Z.pos r - 1) p q N). - - - Local Lemma eval_sub_then_maybe_add : forall a b : T R_numlimbs, - small a -> - small b -> - 0 <= eval a < eval N -> - 0 <= eval b < eval N -> - eval (sub_then_maybe_add a b) = - eval a - eval b + - (if eval a - eval b <? 0 then eval N else 0). - Proof. - intros; cbv beta; apply eval_sub_then_maybe_add; try assumption; nia. - Qed. - - Local Lemma small_sub_then_maybe_add : forall a b : T R_numlimbs, - small a -> - small b -> - 0 <= eval a < eval N -> - 0 <= eval b < eval N -> - small (sub_then_maybe_add a b). - Proof. - intros; cbv beta; apply small_sub_then_maybe_add; try assumption; nia. - Qed. - Local Lemma sub_then_maybe_add_cps_id : forall (Av Bv : T R_numlimbs) cpsT (f : _ -> cpsT), sub_then_maybe_add_cps Av Bv _ f = f (sub_then_maybe_add Av Bv). - Proof. - intros; cbv beta; apply sub_then_maybe_add_id; try assumption; nia. - Qed. - Hint Rewrite sub_then_maybe_add_cps_id : uncps. + Local Notation eval_sub_then_maybe_add := + (fun p q smp smq => @eval_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N smp smq small_N N_mask). + Local Notation small_sub_then_maybe_add := + (fun p q => @small_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N). Definition add_no_cps_bound : 0 <= eval add_no_cps < eval N := @add_bound T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound. @@ -272,9 +248,9 @@ Section WordByWordMontgomery. Definition small_add_no_cps : small add_no_cps := @small_add T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@small_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound. Definition small_sub_no_cps : small sub_no_cps - := @small_sub T (@eval) R_numlimbs (@small) N (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av Bv small_Av small_Bv Av_bound Bv_bound. + := @small_sub T R_numlimbs (@small) (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av Bv. Definition small_opp_no_cps : small opp_no_cps - := @small_opp T (@eval) (@zero) r R R_numlimbs (@small) (@eval_zero) (@small_zero) N (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av small_Av Av_bound. + := @small_opp T (@zero) R_numlimbs (@small) (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av. Definition eval_add_no_cps : eval add_no_cps = eval Av + eval Bv + (if eval N <=? eval Av + eval Bv then - eval N else 0) := @eval_add T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound. |