From 339ee4ec95624751f84997064a6a985478ca5645 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Mar 2019 02:33:39 -0500 Subject: Finish reifying list lemmas After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 22m23.84s | Total | 21m34.63s || +0m49.21s | +3.80% -------------------------------------------------------------------------------------------- 1m52.62s | RewriterRulesInterpGood.vo | 1m37.14s || +0m15.48s | +15.93% 3m25.91s | p384_32.c | 3m14.24s || +0m11.66s | +6.00% 1m32.94s | RewriterRulesGood.vo | 1m42.36s || -0m09.42s | -9.20% 0m33.72s | RewriterWf1.vo | 0m24.30s || +0m09.41s | +38.76% 1m17.31s | Rewriter.vo | 1m12.10s || +0m05.21s | +7.22% 0m43.01s | ExtractionHaskell/unsaturated_solinas | 0m39.84s || +0m03.16s | +7.95% 0m45.21s | p521_32.c | 0m42.86s || +0m02.35s | +5.48% 1m46.30s | Fancy/Barrett256.vo | 1m45.08s || +0m01.21s | +1.16% 0m38.74s | p521_64.c | 0m37.49s || +0m01.25s | +3.33% 0m23.16s | ExtractionOCaml/word_by_word_montgomery | 0m21.44s || +0m01.71s | +8.02% 0m18.74s | p256_32.c | 0m16.88s || +0m01.85s | +11.01% 0m15.00s | ExtractionOCaml/unsaturated_solinas | 0m13.98s || +0m01.01s | +7.29% 0m11.92s | ExtractionOCaml/saturated_solinas | 0m10.13s || +0m01.78s | +17.67% 0m07.82s | ExtractionOCaml/saturated_solinas.ml | 0m05.98s || +0m01.83s | +30.76% 1m47.42s | RewriterWf2.vo | 1m47.81s || -0m00.39s | -0.36% 0m58.35s | ExtractionHaskell/word_by_word_montgomery | 0m57.41s || +0m00.94s | +1.63% 0m45.47s | RewriterInterpProofs1.vo | 0m45.67s || -0m00.20s | -0.43% 0m37.34s | Fancy/Montgomery256.vo | 0m37.09s || +0m00.25s | +0.67% 0m36.14s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.52s || -0m00.38s | -1.04% 0m29.91s | ExtractionHaskell/saturated_solinas | 0m29.70s || +0m00.21s | +0.70% 0m26.77s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.72s || +0m00.05s | +0.18% 0m25.87s | SlowPrimeSynthesisExamples.vo | 0m25.49s || +0m00.38s | +1.49% 0m18.72s | p448_solinas_64.c | 0m19.16s || -0m00.44s | -2.29% 0m16.94s | secp256k1_32.c | 0m17.18s || -0m00.23s | -1.39% 0m13.92s | p434_64.c | 0m13.08s || +0m00.83s | +6.42% 0m13.15s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.58s || +0m00.57s | +4.53% 0m08.97s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.95s || +0m00.02s | +0.22% 0m08.37s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.51s || -0m00.14s | -1.64% 0m08.35s | p224_32.c | 0m08.10s || +0m00.25s | +3.08% 0m07.77s | p384_64.c | 0m07.29s || +0m00.47s | +6.58% 0m06.92s | BoundsPipeline.vo | 0m06.85s || +0m00.07s | +1.02% 0m05.70s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.14s || -0m00.43s | -7.16% 0m05.12s | ExtractionHaskell/saturated_solinas.hs | 0m06.09s || -0m00.96s | -15.92% 0m03.53s | PushButtonSynthesis/Primitives.vo | 0m03.55s || -0m00.02s | -0.56% 0m03.38s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.04s | +1.19% 0m03.16s | PushButtonSynthesis/BarrettReduction.vo | 0m03.24s || -0m00.08s | -2.46% 0m03.06s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.23s || -0m00.16s | -5.26% 0m02.81s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.84s || -0m00.02s | -1.05% 0m02.62s | curve25519_32.c | 0m02.22s || +0m00.39s | +18.01% 0m01.88s | p224_64.c | 0m01.47s || +0m00.40s | +27.89% 0m01.68s | curve25519_64.c | 0m02.19s || -0m00.51s | -23.28% 0m01.32s | CLI.vo | 0m01.33s || -0m00.01s | -0.75% 0m01.24s | secp256k1_64.c | 0m01.30s || -0m00.06s | -4.61% 0m01.22s | p256_64.c | 0m01.47s || -0m00.25s | -17.00% 0m01.16s | RewriterProofs.vo | 0m01.16s || +0m00.00s | +0.00% 0m01.10s | StandaloneHaskellMain.vo | 0m01.00s || +0m00.10s | +10.00% 0m01.05s | CompilersTestCases.vo | 0m01.09s || -0m00.04s | -3.66% 0m01.04s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.00s | +0.00% --- src/RewriterWf1.v | 300 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 300 insertions(+) (limited to 'src/RewriterWf1.v') diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index 49af85a60..411287bcc 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -27,6 +27,7 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Sigma.Related. Require Import Crypto.Util.ListUtil.SetoidList. +Require Import Crypto.Util.ListUtil.Forall. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Option. Require Import Crypto.Util.Logic.ExistsEqAnd. @@ -2569,5 +2570,304 @@ Module Compilers. End with_interp. End with_var. End Compile. + + Module Reify. + Import Compile. + Import Rewriter.Compilers.RewriteRules.Compile. + Import Rewriter.Compilers.RewriteRules.Reify. + + Local Notation type := (type.type base.type). + Local Notation expr := (@expr.expr base.type ident). + Local Notation value := (@value base.type ident). + Local Notation UnderLets := (@UnderLets.UnderLets base.type ident). + + Ltac wf_ctors := + repeat first [ match goal with + | [ |- UnderLets.wf _ _ (UnderLets.Base _) (UnderLets.Base _) ] => constructor + | [ |- expr.wf _ (_ @ _) (_ @ _) ] => constructor + | [ |- expr.wf ?seg (#_) (#_) ] + => (tryif is_evar seg then instantiate (1:=nil) else idtac); + constructor + | [ |- expr.wf _ ($_) ($_) ] => constructor + | [ |- expr.wf _ (expr.Abs _) (expr.Abs _) ] => constructor; intros + | [ |- expr.wf _ (UnderLets.to_expr _) (UnderLets.to_expr _) ] => apply UnderLets.wf_to_expr + | [ H : expr.wf ?G ?x ?y |- expr.wf ?seg ?x ?y ] => first [ is_evar seg | constr_eq G seg ]; exact H + | [ H : List.Forall2 (expr.wf _) ?x ?y |- List.Forall2 (expr.wf _) ?x ?y ] + => eapply Forall2_Proper_impl; [ | reflexivity | reflexivity | exact H ]; repeat intro + | [ H : List.Forall2 (expr.wf ?G) ?x ?y |- List.Forall2 (expr.wf ?seg) ?x ?y ] + => first [ is_evar seg | constr_eq seg G ]; exact H + | [ H : List.Forall2 ?P ?x ?y |- List.Forall2 ?Pe ?x ?y ] + => first [ is_evar Pe | constr_eq Pe P ]; exact H + | [ H : forall x y, List.In (x, y) ?G -> expr.wf ?G' x y, H' : List.In (?v1, ?v2) ?G |- expr.wf ?seg ?v1 ?v2 ] + => first [ is_evar seg | constr_eq seg G' ]; exact (H _ _ H') + | [ |- expr.wf _ (reify_list _) (reify_list _) ] + => rewrite expr.wf_reify_list + | [ H : expr.wf _ (reify_list ?xs) (reify_list ?ys) |- List.Forall2 _ ?xs ?xy ] + => rewrite expr.wf_reify_list in H + | [ |- ?G ] => tryif has_evar G then fail else solve [ destruct_head'_ex; subst; wf_t ] + end ]. + Ltac handle_wf_rec do_try := + let tac _ + := solve + [ repeat + first + [ progress wf_ctors + | handle_wf_rec do_try + | match goal with + | [ |- List.In ?v ?seg ] => is_evar seg; unify seg (cons v nil) + | [ |- List.In ?v (?seg1 ++ ?seg2) ] + => rewrite in_app_iff; + first [ is_evar seg1; left + | is_evar seg2; right ] + (*| [ |- ?x ++ ?y = ?x ++ ?z ] => apply f_equal2*) + | [ |- ?x = ?y ] + => is_evar x; tryif has_evar y then fail else reflexivity + | [ |- forall t v1 v2, List.In (existT _ t (v1, v2)) (?x ++ ?G1) -> List.In (existT _ t (v1, v2)) (?x ++ ?G2) ] + => is_evar G2; + tryif first [ has_evar x | has_evar G1 ] then fail else (do 3 intro; exact id) + end ] ] in + match goal with + | [ H : expr.wf ?segv ?x1 ?x2 + |- UnderLets.wf _ ?Gv (nat_rect _ _ _ _ ?x1) (nat_rect _ _ _ _ ?x2) ] + => unshelve + (eapply UnderLets.wf_Proper_list; + [ | | eapply @UnderLets.wf_nat_rect_arrow with (R' := fun G' => expr.wf G') (seg:=segv) (G:=Gv); intros ]; + [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ]; + [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ]; + [ try match goal with |- _ = _ => shelve end.. ]); + shelve_unifiable; + do_try tac + | [ H : expr.wf ?segv ?x1 ?x2 + |- UnderLets.wf _ ?Gv (list_rect _ _ _ _ ?x1) (list_rect _ _ _ _ ?x2) ] + => unshelve + (eapply UnderLets.wf_Proper_list; + [ | | eapply @UnderLets.wf_list_rect_arrow with (R' := fun G' => expr.wf G') (seg:=segv) (G:=Gv); intros ]; + [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ]; + [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ]; + [ try match goal with |- _ = _ => shelve end.. ]); + shelve_unifiable; + do_try tac + | [ |- UnderLets.wf _ _ ?x ?y ] + => let f := head x in + let g := head y in + is_var f; is_var g; + unshelve + (lazymatch goal with + | [ H : context[UnderLets.wf _ _ (f _) (g _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + | [ H : context[UnderLets.wf _ _ (f _ _) (g _ _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + | [ H : context[UnderLets.wf _ _ (f _ _ _) (g _ _ _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + | [ H : context[UnderLets.wf _ _ (f _ _ _ _) (g _ _ _ _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + end; + [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ]; + [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ]; + [ try match goal with |- _ = _ => shelve end.. ]); + shelve_unifiable; + do_try tac + end. + + Ltac reify_wf_t_step := + first [ progress subst + | match goal with + | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ] + => first [ erewrite <- expr.wf_reflect_list in H' by eassumption + | erewrite -> expr.wf_reflect_list in H' by eassumption ]; + exfalso; clear -H H'; congruence + end + | progress inversion_option + | progress destruct_head'_False + | progress intros + | progress cbn [invert_expr.invert_Literal invert_expr.ident.invert_Literal value' type.interp base.interp base.base_interp] in * + | match goal with + | [ H : ident.Literal _ = ident.Literal _ |- _ ] + => pose proof (f_equal invert_expr.ident.invert_Literal H); clear H + end + | progress expr.inversion_wf_constr + | break_innermost_match_hyps_step + | progress expr.inversion_wf_one_constr + | progress expr.invert_subst + | progress expr.inversion_expr + | progress expr.invert_match + | progress wf_ctors + | match goal with + | [ |- UnderLets.wf _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ] + => apply UnderLets.wf_nat_rect; intros + | [ |- UnderLets.wf _ ?G (list_rect _ _ _ _) (list_rect _ _ _ _) ] + => apply @UnderLets.wf_list_rect with (RA := expr.wf G) + | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] + => apply @UnderLets.wf_splice with (P := fun G => expr.wf G); intros; subst + | [ H : expr.wf _ (reify_list ?l1) (reify_list ?l2) + |- expr.wf ?G (nth_default ?d1 ?l1 ?n) (nth_default ?d2 ?l2 ?n) ] + => cut (List.Forall2 (expr.wf G) l1 l2 /\ expr.wf G d1 d2); + [ rewrite Forall2_forall_iff''; + let H := fresh in intro H; apply H + | split ] + | [ |- ?x = ?x ] => reflexivity + end + | progress handle_wf_rec ltac:(fun tac => try tac (); tac ()) ]. + Ltac reify_wf_t := repeat reify_wf_t_step. + + Section with_var. + Context {var1 var2 : type -> Type}. + + Lemma wf_reflect_ident_iota G {t} (idc : ident t) + : option_eq + (wf_value G) + (@reflect_ident_iota var1 t idc) + (@reflect_ident_iota var2 t idc). + Proof using Type. + destruct idc; cbv [reflect_ident_iota option_eq]; try reflexivity. + all: cbv [wf_value wf_value']; intros; subst; break_innermost_match; cbn [reify reflect] in *; + lazymatch goal with + | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ] + => first [ erewrite <- expr.wf_reflect_list in H' by eassumption + | erewrite -> expr.wf_reflect_list in H' by eassumption ]; + exfalso; clear -H H'; congruence + | _ => idtac + end; + expr.invert_subst; subst. + all: reify_wf_t. + Qed. + + Lemma wf_reflect_expr_beta_iota + {ident} + {reflect_ident_iota1 reflect_ident_iota2} + (Hwf_reflect_ident_iota + : forall G {t} (idc : ident t), + option_eq + (@wf_value _ ident var1 var2 G _) + (@reflect_ident_iota1 t idc) + (@reflect_ident_iota2 t idc)) + G G' + (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> wf_value G v1 v2) + {t} e1 e2 + (Hwf : expr.wf G' e1 e2) + : UnderLets.wf + (fun G'' => wf_value G'') + G + (@reflect_expr_beta_iota ident var1 reflect_ident_iota1 t e1) + (@reflect_expr_beta_iota ident var2 reflect_ident_iota2 t e2). + Proof using Type. + revert G HG'; induction Hwf; cbn [reflect_expr_beta_iota]; intros. + all: repeat first [ match goal with + | [ |- UnderLets.wf _ _ _ _ ] => constructor + | [ |- expr.wf _ _ _ ] => constructor + | [ |- wf_value' _ (UnderLets.Base _) (UnderLets.Base _) ] => constructor + | [ Hwf_reflect_ident_iota : forall G t' idc', option_eq (wf_value G) (?reflect_ident_iota1 t' idc') (?reflect_ident_iota2 t' idc'), + H1 : ?reflect_ident_iota1 ?t ?idc = _, H2 : ?reflect_ident_iota2 ?t ?idc = _ |- _ ] + => let H' := fresh in + pose proof (fun G => Hwf_reflect_ident_iota G t idc) as H'; + rewrite H1, H2 in H'; clear H1 H2; cbv [option_eq] in H' + | [ H : list _ -> ?T |- _ ] => specialize (H nil) + | [ |- UnderLets.wf ?Pv ?Gv (UnderLets.splice _ _) (UnderLets.splice _ _) ] + => apply @UnderLets.wf_splice with (P:=fun G => wf_value G); intros; subst + | [ H : context[reflect_expr_beta_iota] |- UnderLets.wf _ _ (reflect_expr_beta_iota _ _) (reflect_expr_beta_iota _ _) ] + => apply H; intros + | [ |- wf_value _ (fun x => _) (fun y => _) ] => hnf; intros; subst + | [ |- wf_value' _ (splice_under_lets_with_value _ _) (splice_under_lets_with_value _ _) ] + => apply wf_splice_under_lets_with_value + | [ |- UnderLets.wf (fun G a1 a2 => wf_value_with_lets G (Base_value a1) (Base_value a2)) ?G' ?x ?y ] + => cut (UnderLets.wf (fun G => wf_value G) G' x y); + [ apply UnderLets.wf_Proper_list_impl; cbv [wf_value_with_lets Base_value] + | ] + end + | progress destruct_head'_False + | progress inversion_option + | solve [ auto ] + | break_innermost_match_step + | apply wf_reflect + | apply wf_reify + | progress intros + | progress cbn [List.In eq_rect fst snd] in * + | progress destruct_head'_or + | progress inversion_sigma + | progress subst + | progress inversion_prod + | cbn [wf_value wf_value'] in *; + handle_wf_rec ltac:(fun tac => try tac (); try eassumption; tac ()) + | eapply wf_value'_Proper_list; [ | match goal with H : _ |- _ => now eapply H end ]; solve [ destruct_head'_ex; subst; wf_t ] + | match goal with + | [ H : wf_value _ ?f ?g |- wf_value _ (?f _) (?g _) ] + => eapply wf_value'_Proper_list; revgoals; [ hnf in H; eapply H; revgoals | ]; try eassumption; try reflexivity; now destruct_head'_ex; subst; wf_t + end ]. + Qed. + + Lemma wf_reify_expr_beta_iota + {ident} + {reflect_ident_iota1 reflect_ident_iota2} + (Hwf_reflect_ident_iota + : forall G {t} (idc : ident t), + option_eq + (@wf_value _ ident var1 var2 G _) + (@reflect_ident_iota1 t idc) + (@reflect_ident_iota2 t idc)) + G G' + (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> wf_value G v1 v2) + {t} e1 e2 + (Hwf : expr.wf G' e1 e2) + : UnderLets.wf + (fun G'' => expr.wf G'') + G + (@reify_expr_beta_iota ident var1 reflect_ident_iota1 t e1) + (@reify_expr_beta_iota ident var2 reflect_ident_iota2 t e2). + Proof using Type. + cbv [reify_expr_beta_iota reify_to_UnderLets]. + eapply @UnderLets.wf_splice with (P := fun G => wf_value G); + intros; destruct_head'_ex; subst. + all: repeat first [ break_innermost_match_step + | progress cbn [reflect reify] in * + | progress fold (@reflect ident var1) (@reflect ident var2) + | progress fold (@reify ident var1) (@reify ident var2) + | progress intros + | assumption + | apply wf_reify + | apply wf_reflect + | eapply wf_reflect_expr_beta_iota + | match goal with + | [ |- List.In ?x ?seg ] => is_evar seg; unify seg (cons x nil); left + end + | constructor + | match goal with H : _ |- _ => eapply H; revgoals; clear H end ]. + Qed. + + Lemma wf_expr_value_to_rewrite_rule_replacement + {ident} + {reflect_ident_iota1 reflect_ident_iota2} + (Hwf_reflect_ident_iota + : forall G {t} (idc : ident t), + option_eq + (@wf_value _ ident var1 var2 G _) + (@reflect_ident_iota1 t idc) + (@reflect_ident_iota2 t idc)) + (should_do_again : bool) + G {t} e1 e2 + (Hwf : @wf_maybe_do_again_expr ident var1 var2 t true true G e1 e2) + : UnderLets.wf + (fun G' => @wf_maybe_do_again_expr ident var1 var2 t should_do_again should_do_again G') + G + (@expr_value_to_rewrite_rule_replacement ident var1 reflect_ident_iota1 should_do_again t e1) + (@expr_value_to_rewrite_rule_replacement ident var2 reflect_ident_iota2 should_do_again t e2). + Proof using Type. + cbv [expr_value_to_rewrite_rule_replacement]. + eapply @UnderLets.wf_splice with (P := @wf_maybe_do_again_expr ident var1 var2 _ true true); intros; destruct_head'_ex; subst. + { destruct Hwf as [G' [HG' Hwf] ]. + eapply UnderLets.wf_flat_map; + cbv [wf_value] in *; + eauto using wf_value'_Proper_list, UnderLets.wf_of_expr, wf_reify_expr_beta_iota. + { intros; eapply wf_reflect; now repeat constructor. } } + { repeat first [ progress cbv [wf_maybe_do_again_expr] in * + | break_innermost_match_step + | progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | eapply wf_reify_expr_beta_iota; try eassumption + | constructor + | solve [ eauto ] ]. } + Qed. + End with_var. + End Reify. End RewriteRules. End Compilers. -- cgit v1.2.3