diff options
| author |  jadep <jade.philipoom@gmail.com> | 2018-09-18 14:41:52 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-12-21 10:22:41 -0500 |
| commit | 79d26ccb78ada2e4d4c4665a776542fa967efc36 (patch) | |
| tree | 30496a8e84781e8471f70e3346182d7e11bd787b /src | |
| parent | 647c8392769e90cd24c050d3945e93c60fe4407a (diff) | |
fix hints and [Proof using] statements so that proofs go through
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 32286a9f3..037f286fe 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -3871,8 +3871,8 @@ Module WordByWordMontgomery. clear dependent B; clear dependent k; clear dependent ri. Lemma small_add : small (add Av Bv). - Proof using small_Bv small_Av lgr_big N_lt_R Bv_bound Av_bound. - clear -small_Bv small_Av N_lt_R Bv_bound Av_bound partition_Proper r_big'. + Proof using small_Bv small_Av lgr_big N_lt_R Bv_bound Av_bound small_N ri k R_numlimbs_nz N_nz B_bounds B. + clear -small_Bv small_Av N_lt_R Bv_bound Av_bound partition_Proper r_big' small_N ri k R_numlimbs_nz N_nz B_bounds B sub_then_maybe_add. unfold add; t_small. Qed. Lemma small_sub : small (sub Av Bv). @@ -3881,8 +3881,8 @@ Module WordByWordMontgomery. Proof using Type. unfold opp, sub; t_small. Qed. Lemma eval_add : eval (add Av Bv) = eval Av + eval Bv + if (eval N <=? eval Av + eval Bv) then -eval N else 0. - Proof using small_Bv small_Av lgr_big N_lt_R Bv_bound Av_bound. - clear -small_Bv small_Av N_lt_R Bv_bound Av_bound partition_Proper r_big'. + Proof using small_Bv small_Av lgr_big N_lt_R Bv_bound Av_bound small_N ri k R_numlimbs_nz N_nz B_bounds B. + clear -small_Bv small_Av lgr_big N_lt_R Bv_bound Av_bound partition_Proper r_big' small_N ri k R_numlimbs_nz N_nz B_bounds B sub_then_maybe_add. unfold add; autorewrite with push_mont_eval; reflexivity. Qed. Lemma eval_sub : eval (sub Av Bv) = eval Av - eval Bv + if (eval Av - eval Bv <? 0) then eval N else 0. @@ -3903,7 +3903,7 @@ Module WordByWordMontgomery. | 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 using small_Bv small_Av lgr_big N_lt_R Bv_bound Av_bound. + Proof using small_Bv small_Av lgr_big N_lt_R Bv_bound Av_bound small_N ri k R_numlimbs_nz N_nz B_bounds B. 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. @@ -3912,7 +3912,7 @@ Module WordByWordMontgomery. Proof using small_Av N_nz Av_bound. generalize eval_opp; clear; t_mod_N. Qed. Lemma add_bound : 0 <= eval (add Av Bv) < eval N. - Proof using small_Bv small_Av lgr_big R_numlimbs_nz N_lt_R Bv_bound Av_bound. + Proof using small_Bv small_Av lgr_big R_numlimbs_nz N_lt_R Bv_bound Av_bound small_N ri k N_nz B_bounds B. generalize eval_add; break_innermost_match; Z.ltb_to_lt; lia. Qed. Lemma sub_bound : 0 <= eval (sub Av Bv) < eval N. @@ -4120,8 +4120,10 @@ Module WordByWordMontgomery. push_Zmod; rewrite ?eval_from_montgomery_mod; pull_Zmod; repeat apply conj; cbv [valid addmod] in *; destruct_head'_and; auto; try rewrite m_enc_correct_montgomery; - try (eapply small_add || eapply add_bound); rewrite <- ?m_enc_correct_montgomery; eauto with omega; []. - push_Zmod; erewrite eval_add by (rewrite <- ?m_enc_correct_montgomery; eauto with omega); pull_Zmod; rewrite <- ?m_enc_correct_montgomery. + try (eapply small_add || eapply add_bound); + cbv [small]; rewrite <- ?m_enc_correct_montgomery; + eauto with omega; [ ]. + push_Zmod; erewrite eval_add by (cbv [small]; rewrite <- ?m_enc_correct_montgomery; eauto with omega); pull_Zmod; rewrite <- ?m_enc_correct_montgomery. break_innermost_match; push_Zmod; pull_Zmod; autorewrite with zsimplify_const; apply f_equal2; nia. Qed. |