diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-14 22:18:51 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-14 22:18:51 -0500 |
commit | 1c4ab0f67cf8350add23b8feff5df563ceded904 (patch) | |
tree | 70d83605f46f11aaf718fed86b35b3117fa40a5e /src | |
parent | 43c5265c24bd1df125f8de00d1f89379a920659a (diff) |
Speed up some GF25519 tactics
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/GF25519BoundedCommon.v | 18 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 11 |
2 files changed, 23 insertions, 6 deletions
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index cc864606a..9184d0dc8 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -289,15 +289,29 @@ Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW app_wire_digitsW x (Tuple.map word64ize). (** TODO: Turn this into a lemma to speed up proofs *) +Ltac unfold_is_bounded_in' H := + lazymatch type of H with + | andb _ _ = true + => apply andb_prop in H; + let H1 := fresh in + let H2 := fresh in + destruct H as [H1 H2]; + unfold_is_bounded_in' H1; + unfold_is_bounded_in' H2 + | _ => idtac + end. Ltac unfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519WToZ, wire_digitsWToZ in H; cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519 List.length wire_widths] in H; - rewrite ?Bool.andb_true_iff in H. + unfold_is_bounded_in' H. Ltac unfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519WToZ, wire_digitsWToZ; cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519 List.length wire_widths]; - rewrite ?Bool.andb_true_iff. + repeat match goal with + | [ |- andb _ _ = true ] => apply andb_true_intro + | [ |- and _ _ ] => split + end. Local Transparent bit_width. Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width. diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index c6750fa3c..324113101 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -352,12 +352,14 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; match goal with | [ |- fe25519WToZ ?x = _ /\ _ ] - => destruct x; destruct_head_hnf' prod + => generalize dependent x; intros | [ |- wire_digitsWToZ ?x = _ /\ _ ] - => destruct x; destruct_head_hnf' prod + => generalize dependent x; intros | [ |- _ = _ ] => exact Hbounds_left end; + cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *; + destruct_head' prod; change word64ToZ with WordW.wordWToZ in *; (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; @@ -367,11 +369,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe25519WToZ; simpl @wire_digitsWToZ; - unfold_is_bounded; destruct_head' and; Z.ltb_to_lt; change WordW.wordWToZ with word64ToZ in *; - repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity. + unfold_is_bounded; + Z.ltb_to_lt; + try omega; try reflexivity. Ltac rexpr_correct := |