From a22af596b7136910f521eb0a79af20e88c8b5dd1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Aug 2018 18:06:40 -0400 Subject: Finish rule-specific rewriter wf proofs But don't run them yet, because they are really slow After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 19m35.38s | Total | 19m35.69s || -0m00.30s | -0.02% -------------------------------------------------------------------------------------------------------------------- 5m57.04s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m58.04s || -0m01.00s | -0.27% 1m12.61s | Experiments/NewPipeline/RewriterWf2 | 1m11.61s || +0m01.00s | +1.39% 4m32.41s | Experiments/NewPipeline/Toplevel1 | 4m33.28s || -0m00.87s | -0.31% 1m38.38s | Experiments/NewPipeline/Toplevel2 | 1m38.56s || -0m00.18s | -0.18% 1m16.21s | Experiments/NewPipeline/RewriterRulesGood | 1m16.18s || +0m00.03s | +0.03% 0m39.26s | p521_32.c | 0m39.50s || -0m00.24s | -0.60% 0m37.34s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.33s || +0m00.01s | +0.02% 0m34.83s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m35.33s || -0m00.50s | -1.41% 0m32.68s | p521_64.c | 0m32.73s || -0m00.04s | -0.15% 0m23.62s | p384_32.c | 0m23.67s || -0m00.05s | -0.21% 0m21.00s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.22s || +0m00.78s | +3.85% 0m18.92s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.62s || +0m00.30s | +1.61% 0m13.79s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m13.70s || +0m00.08s | +0.65% 0m10.70s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.51s || +0m00.18s | +1.80% 0m08.55s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.59s || -0m00.03s | -0.46% 0m08.43s | p384_64.c | 0m08.54s || -0m00.10s | -1.28% 0m05.62s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.34s || +0m00.28s | +5.24% 0m05.47s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.48s || -0m00.01s | -0.18% 0m04.40s | Experiments/NewPipeline/RewriterWf1 | 0m04.36s || +0m00.04s | +0.91% 0m03.97s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m03.89s || +0m00.08s | +2.05% 0m03.95s | secp256k1_32.c | 0m03.91s || +0m00.04s | +1.02% 0m03.92s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.01s || -0m00.08s | -2.24% 0m03.78s | p256_32.c | 0m03.77s || +0m00.00s | +0.26% 0m03.31s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.13s || +0m00.18s | +5.75% 0m02.14s | curve25519_32.c | 0m02.11s || +0m00.03s | +1.42% 0m02.14s | p224_32.c | 0m02.23s || -0m00.08s | -4.03% 0m01.55s | p224_64.c | 0m01.69s || -0m00.13s | -8.28% 0m01.54s | p256_64.c | 0m01.52s || +0m00.02s | +1.31% 0m01.52s | curve25519_64.c | 0m01.43s || +0m00.09s | +6.29% 0m01.49s | secp256k1_64.c | 0m01.65s || -0m00.15s | -9.69% 0m01.40s | Experiments/NewPipeline/CLI | 0m01.41s || -0m00.01s | -0.70% 0m01.29s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.23s || +0m00.06s | +4.87% 0m01.24s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.18s || +0m00.06s | +5.08% 0m00.88s | Experiments/NewPipeline/RewriterProofs | 0m00.94s || -0m00.05s | -6.38% --- src/Experiments/NewPipeline/RewriterProofs.v | 3 +- src/Experiments/NewPipeline/RewriterRulesGood.v | 96 ++++++++++++------------- src/Experiments/NewPipeline/RewriterWf1.v | 11 ++- src/Experiments/NewPipeline/RewriterWf2.v | 18 ++--- 4 files changed, 61 insertions(+), 67 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v index 2632560be..d0d106a02 100644 --- a/src/Experiments/NewPipeline/RewriterProofs.v +++ b/src/Experiments/NewPipeline/RewriterProofs.v @@ -66,8 +66,7 @@ Module Compilers. pattern.ident.internal_ident_dec_bl, pattern.ident.try_make_transport_ident_cps_correct, pattern.ident.eta_ident_cps_correct - with nocore; - [ .. | intros; eapply UnderLets.wf_Proper_list; [ | | eapply wf_do_again; assumption ]; solve [ wf_t ] ]. + with nocore. Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0. diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v index 605cbf5ca..3bdfa9913 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesGood.v @@ -166,28 +166,27 @@ Module Compilers. N1 N2 C1 C2 ls1 ls2 G (Hwf : expr.wf G ls1 ls2) (HN : UnderLets.wf (fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) G N1 N2) + /\ expr.wf G'' v1 v2) G N1 N2) (HC : forall G' x xs y ys rec1 rec2, (exists seg, G' = (seg ++ G)%list) -> expr.wf G x y -> expr.wf G (reify_list xs) (reify_list ys) - -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' rec1 rec2) + -> (exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' rec1 rec2) -> UnderLets.wf (fun G' v1 v2 - => forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) - G' (C1 x xs rec1) (C2 y ys rec2)) + => exists G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' v1 v2) + G' (C1 x xs rec1) (C2 y ys rec2)) : option_eq (UnderLets.wf (fun G' v1 v2 - => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P), - forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' - (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) - (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) + => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P) G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' + (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) + (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) G) (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1 _ id) (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2 _ id). @@ -199,8 +198,8 @@ Module Compilers. all: repeat first [ 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 + | erewrite -> expr.wf_reflect_list in H' by eassumption ]; + exfalso; clear -H H'; congruence | [ |- UnderLets.wf _ _ _ _ ] => constructor | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor end @@ -208,10 +207,11 @@ Module Compilers. | progress cbn [sequence_return option_eq] | assumption | reflexivity + | (exists eq_refl) | apply @UnderLets.wf_splice with (P:=fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) + /\ expr.wf G'' v1 v2) | progress intros ]. lazymatch goal with | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ] @@ -223,8 +223,8 @@ Module Compilers. all: repeat first [ 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 + | erewrite -> expr.wf_reflect_list in H' by eassumption ]; + exfalso; clear -H H'; congruence | [ |- UnderLets.wf _ _ _ _ ] => constructor end | progress expr.invert_subst @@ -235,9 +235,9 @@ Module Compilers. | solve [ auto ] | progress subst | apply @UnderLets.wf_splice with (P:=fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) + /\ expr.wf G'' v1 v2) | progress intros | wf_safe_t_step | progress type.inversion_type @@ -248,28 +248,27 @@ Module Compilers. N1 N2 C1 C2 ls1 ls2 G (Hwf : expr.wf G ls1 ls2) (HN : UnderLets.wf (fun G' x1 x2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> Compile.wf_anyexpr G'' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) G N1 N2) + /\ Compile.wf_anyexpr G'' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) G N1 N2) (HC : forall G' x xs y ys rec1 rec2, (exists seg, G' = (seg ++ G)%list) -> expr.wf G x y -> expr.wf G (reify_list xs) (reify_list ys) - -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' rec1 rec2) + -> (exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' rec1 rec2) -> UnderLets.wf (fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) + /\ expr.wf G'' v1 v2) G' (C1 x xs rec1) (C2 y ys rec2)) : option_eq (UnderLets.wf (fun G' v1 v2 - => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P), - forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' - (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) - (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) + => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P) G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' + (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) + (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) G) (@rlist_rect_cast var1 A A' P (@Compile.value _ ident var1) N1 C1 ls1 _ id) (@rlist_rect_cast var2 A A' P (@Compile.value _ ident var2) N2 C2 ls2 _ id). @@ -280,7 +279,8 @@ Module Compilers. apply wf_rlist_rectv; auto. eapply UnderLets.wf_Proper_list_impl; [ | | eassumption ]; trivial; cbn; intros ? ? ? H. repeat let x := fresh in intro x; specialize (H x). - inversion H; inversion_sigma; type.inversion_type; subst; assumption. + destruct H as [? [H0 H1] ]. + inversion H1; inversion_sigma; type.inversion_type; subst; eauto. Qed. @@ -394,16 +394,6 @@ Module Compilers. eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto). Qed. - (** TODO: MOVE ME *) - Lemma combine_repeat {A B} (a : A) (b : B) n : combine (repeat a n) (repeat b n) = repeat (a, b) n. - Proof. induction n; cbn; congruence. Qed. - Lemma combine_rev_rev_samelength {A B} ls1 ls2 : length ls1 = length ls2 -> @combine A B (rev ls1) (rev ls2) = rev (combine ls1 ls2). - Proof. - revert ls2; induction ls1 as [|? ? IHls1], ls2; cbn in *; try congruence; intros. - rewrite combine_app_samelength, IHls1 by (rewrite ?rev_length; congruence); cbn [combine]. - reflexivity. - Qed. - Local Ltac start_good cps_id rewrite_rules := split; [ reflexivity | ]; repeat apply conj; try solve [ eapply cps_id ]; []; @@ -547,6 +537,13 @@ Module Compilers. => is_evar R; revert H; instantiate (1:=fun G' => expr.wf G'); solve [ auto ] | [ H : expr.wf ?G ?a ?b |- ?R ?G ?a ?b ] => is_evar R; instantiate (1:=fun G' => expr.wf G'); solve [ auto ] + | [ |- (forall t v1 v2, In _ _ -> _) /\ expr.wf _ _ _ ] => apply conj; revgoals + | [ |- (forall t v1 v2, In _ _ -> _) /\ Compile.wf_anyexpr _ _ _ _ ] => apply conj; revgoals + | [ H : expr.wf _ ?x ?y |- Compile.wf_value _ ?x ?y ] => hnf + | [ |- Compile.wf_value _ ?x ?y ] => eapply Compile.wf_value'_Proper_list; [ | solve [ cbv [Compile.wf_value] in *; eauto ] ]; solve [ wf_t ] + | [ |- In ?x ?ls ] => is_evar ls; refine (or_introl eq_refl : In x (x :: _)); shelve + | [ |- or (_ = _) ?G ] => first [ left; reflexivity | has_evar G; right ] + | [ H : @In ?A _ ?ls |- _ ] => is_evar ls; unify ls (@nil A); cbn [In] in H end | progress expr.invert_subst | solve [ wf_t ] @@ -557,12 +554,9 @@ Module Compilers. Lemma nbe_rewrite_rules_good : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules. Proof. - (*Time start_good (@nbe_cps_id) (@nbe_rewrite_rules). - Set Ltac Profiling. - Time all: try solve [ repeat repeat good_t_step ]. - Show Ltac Profile. - (*start_good (@nbe_cps_id) (@nbe_rewrite_rules). - all: repeat good_t_step.*) + (* + Time start_good (@nbe_cps_id) (@nbe_rewrite_rules). + Time all: repeat repeat good_t_step. *) Admitted. diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 0cbaaaacf..06c71e480 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -623,12 +623,11 @@ Module Compilers. | true, true => UnderLets.wf (fun G' v1 v2 - => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t), - forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2') - -> expr.wf G'' - (rew [fun t : base.type => expr t] pf1 in unwrap v1) - (rew [fun t : base.type => expr t] pf2 in unwrap v2)) + => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t) G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2') + /\ expr.wf G'' + (rew [fun t : base.type => expr t] pf1 in unwrap v1) + (rew [fun t : base.type => expr t] pf2 in unwrap v2)) G | false, false => UnderLets.wf (fun G' => wf_anyexpr G' t) G diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v index bdad9d840..5d1bae6e4 100644 --- a/src/Experiments/NewPipeline/RewriterWf2.v +++ b/src/Experiments/NewPipeline/RewriterWf2.v @@ -484,7 +484,7 @@ Module Compilers. (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t)) (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t)) (wf_do_again : forall G (t : base.type) e1 e2, - expr.wf nil e1 e2 + (exists G', (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) /\ expr.wf G' e1 e2) -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)) (d : @decision_tree pident) (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) @@ -757,8 +757,9 @@ Module Compilers. (Hrew : rewrite_rules_goodT rew1 rew2) (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t)) (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t)) - (wf_do_again : forall G (t : base.type) e1 e2, - expr.wf nil e1 e2 + (wf_do_again : forall G G' (t : base.type) e1 e2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) + -> expr.wf G' e1 e2 -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)). Local Notation assemble_identifier_rewriters' var := (@assemble_identifier_rewriters' ident var pident full_types invert_bind_args type_of_pident pident_to_typed of_typed_ident arg_types bind_args try_make_transport_ident_cps dtree). @@ -776,7 +777,8 @@ Module Compilers. Proof. revert dependent G; revert dependent re1; revert dependent re2; induction t as [t|s IHs d IHd]; intros; cbn [assemble_identifier_rewriters']. - { rewrite HK1, HK2; apply wf_eval_rewrite_rules; assumption. } + { rewrite HK1, HK2; apply wf_eval_rewrite_rules; try assumption. + intros; destruct_head'_ex; destruct_head'_and; eauto. } { hnf; intros; subst. unshelve eapply IHd; cbn [type_of_rawexpr]; [ shelve | shelve | constructor | cbn; reflexivity | cbn; reflexivity ]. all: rewrite ?HK1, ?HK2. @@ -903,9 +905,10 @@ Module Compilers. do_again1 do_again2 (wf_do_again - : forall (t : base.type) e1 e2, - expr.wf nil e1 e2 - -> UnderLets.wf (fun G' => expr.wf G') nil (do_again1 t e1) (do_again2 t e2)) + : forall G G' (t : base.type) e1 e2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) + -> expr.wf G' e1 e2 + -> UnderLets.wf (fun G' => expr.wf G') G (do_again1 t e1) (do_again2 t e2)) t (idc : ident t), wf_value_with_lets nil (rewrite_head var1 do_again1 t idc) (rewrite_head var2 do_again2 t idc)) fuel {t} (e : Expr t) (Hwf : Wf e) @@ -913,7 +916,6 @@ Module Compilers. Proof. intros var1 var2; cbv [Rewrite]; eapply wf_rewrite with (G:=nil); [ | apply Hwf | wf_t ]. intros; subst; eapply wf_value'_Proper_list; [ | eapply wf_rewrite_head ]; wf_t. - eapply wf_do_again; [ | eassumption ]; wf_t. Qed. End Compile. End RewriteRules. -- cgit v1.2.3