diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-22 22:11:35 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-22 22:11:35 -0400 |
commit | e334bb2c3f5e0f845ed996146e02a6bb4d0f33ae (patch) | |
tree | 7b1ae06286203d642cff43dad6fdb8771a537626 /src/Arithmetic/MontgomeryReduction | |
parent | ff040390affcd3a1fdfbddb5301e5ecb47ceeff6 (diff) |
Add (partially admitted) integration tests for add, sub, opp
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v | 15 | ||||
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 21 |
2 files changed, 34 insertions, 2 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v index c904f71d8..60a3e59fc 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v @@ -549,6 +549,21 @@ Section WordByWordMontgomery. break_innermost_match; Z.ltb_to_lt; lia. Qed. + Local Ltac t_mod_N := + repeat first [ progress break_innermost_match + | reflexivity + | let H := fresh in intro H; rewrite H; clear H + | progress autorewrite with zsimplify_const + | rewrite Z.add_opp_r + | progress (push_Zmod; pull_Zmod) ]. + + Lemma eval_add_mod_N : eval (add Av Bv) mod eval N = (eval Av + eval Bv) mod eval N. + Proof. generalize eval_add; clear. t_mod_N. Qed. + Lemma eval_sub_mod_N : eval (sub Av Bv) mod eval N = (eval Av - eval Bv) mod eval N. + Proof. generalize eval_sub; clear. t_mod_N. Qed. + Lemma eval_opp_mod_N : eval (opp Av) mod eval N = (-eval Av) mod eval N. + Proof. generalize eval_opp; clear; t_mod_N. Qed. + Lemma add_bound : 0 <= eval (add Av Bv) < eval N. Proof. do_clear; generalize eval_add; break_innermost_match; Z.ltb_to_lt; lia. Qed. Lemma sub_bound : 0 <= eval (sub Av Bv) < eval N. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 82baad0c0..87f27eb90 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -268,6 +268,13 @@ Section WordByWordMontgomery. Definition eval_opp_no_cps : eval opp_no_cps = (if eval Av =? 0 then 0 else eval N) - eval Av := @eval_opp T (@eval) (@zero) r R R_numlimbs (@small) (@eval_zero) (@small_zero) N (@sub_then_maybe_add _) (@eval_sub_then_maybe_add) Av small_Av Av_bound. + Definition eval_add_no_cps_mod_N : eval add_no_cps mod eval N = (eval Av + eval Bv) mod eval N + := @eval_add_mod_N 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. + Definition eval_sub_no_cps_mod_N : eval sub_no_cps mod eval N = (eval Av - eval Bv) mod eval N + := @eval_sub_mod_N T (@eval) R_numlimbs (@small) N (@sub_then_maybe_add _) (@eval_sub_then_maybe_add) Av Bv small_Av small_Bv Av_bound Bv_bound. + Definition eval_opp_no_cps_mod_N : eval opp_no_cps mod eval N = (-eval Av) mod eval N + := @eval_opp_mod_N T (@eval) (@zero) r R R_numlimbs (@small) (@eval_zero) (@small_zero) N (@sub_then_maybe_add _) (@eval_sub_then_maybe_add) Av small_Av Av_bound. + Lemma add_cps_id_no_cps : add = add_no_cps. Proof. unfold add_no_cps, add, add_cps, Abstract.Dependent.Definition.add; autorewrite with uncps; reflexivity. @@ -301,7 +308,10 @@ Section WordByWordMontgomery. | apply small_opp_no_cps | apply eval_add_no_cps | apply eval_sub_no_cps - | apply eval_opp_no_cps ]. + | apply eval_opp_no_cps + | apply eval_add_no_cps_mod_N + | apply eval_sub_no_cps_mod_N + | apply eval_opp_no_cps_mod_N ]. Local Ltac t := do_rewrite; do_apply. Lemma add_bound : 0 <= eval add < eval N. Proof. t. Qed. @@ -318,7 +328,14 @@ Section WordByWordMontgomery. Proof. t. Qed. Lemma eval_opp : eval opp = (if eval Av =? 0 then 0 else eval N) - eval Av. Proof. t. Qed. - End add_sub. + + Lemma eval_add_mod_N : eval add mod eval N = (eval Av + eval Bv) mod eval N. + Proof. t. Qed. + Lemma eval_sub_mod_N : eval sub mod eval N = (eval Av - eval Bv) mod eval N. + Proof. t. Qed. + Lemma eval_opp_mod_N : eval opp mod eval N = (-eval Av) mod eval N. + Proof. t. Qed. +End add_sub. End WordByWordMontgomery. Hint Rewrite redc_body_cps_id redc_loop_cps_id pre_redc_cps_id redc_cps_id add_cps_id sub_cps_id opp_cps_id : uncps. |