From 067d1f14b03d83dcb1c0a60808919ceff6205836 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 3 Apr 2019 16:43:48 -0400 Subject: Automate more of the rewriter reification, proof Now we actually make use of the rewrite-rule-specific proofs, rather than duplicating them inline. We now support reifying `ident.gets_inlined` to `SubstVarLike.is_var_fst_snd_pair_opp_cast`. We also now fix a bug where we previously incorrectly substituted context variables when reifying side conditions (needed for correct reification of split-mul things, coming up soon). Things are unfortunately a bit slow. I'm not sure what's up with my proof of `reflect_ident_iota_interp_related`; it seems more complicated than it should be (maybe partly due to funext concerns). Next up is to split out the rewrite rule generation bits into separate files and have a single tactic that builds the entire package for us (in prep for making the rewriter builder a vernacular). After that I want to more fully parameterize things over `ident`, and then also over the non-container base-types (which will require some reworking of how we handle special identifiers). Additionally, I want to make the rewrite rule definitions not depend on Language.v. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 20m50.18s | Total | 23m01.24s || -2m11.06s | -9.48% ----------------------------------------------------------------------------------------------- 0m27.24s | RewriterRulesGood.vo | 1m34.94s || -1m07.70s | -71.30% 0m54.89s | RewriterRulesInterpGood.vo | 1m57.72s || -1m02.82s | -53.37% 1m37.88s | RewriterWf2.vo | 1m47.69s || -0m09.81s | -9.10% 1m16.71s | Rewriter.vo | 1m12.61s || +0m04.10s | +5.64% 0m37.14s | ExtractionHaskell/unsaturated_solinas | 0m40.06s || -0m02.92s | -7.28% 0m36.10s | RewriterWf1.vo | 0m33.12s || +0m02.98s | +8.99% 0m18.31s | p256_32.c | 0m20.70s || -0m02.39s | -11.54% 1m43.31s | Fancy/Barrett256.vo | 1m42.09s || +0m01.21s | +1.19% 0m32.46s | ExtractionHaskell/saturated_solinas | 0m30.92s || +0m01.53s | +4.98% 0m23.44s | ExtractionOCaml/word_by_word_montgomery | 0m22.26s || +0m01.17s | +5.30% 0m12.17s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.58s || -0m01.41s | -10.38% 0m10.04s | p224_32.c | 0m08.20s || +0m01.83s | +22.43% 0m09.98s | ExtractionOCaml/saturated_solinas | 0m11.67s || -0m01.68s | -14.48% 0m07.80s | ExtractionOCaml/saturated_solinas.ml | 0m06.16s || +0m01.63s | +26.62% 0m06.87s | ExtractionHaskell/saturated_solinas.hs | 0m04.98s || +0m01.88s | +37.95% 3m23.11s | p384_32.c | 3m22.61s || +0m00.50s | +0.24% 0m59.32s | ExtractionHaskell/word_by_word_montgomery | 0m58.76s || +0m00.56s | +0.95% 0m46.19s | p521_32.c | 0m47.16s || -0m00.96s | -2.05% 0m45.26s | RewriterInterpProofs1.vo | 0m45.64s || -0m00.38s | -0.83% 0m39.50s | p521_64.c | 0m38.97s || +0m00.53s | +1.36% 0m36.38s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.00s || +0m00.38s | +1.05% 0m34.40s | Fancy/Montgomery256.vo | 0m34.63s || -0m00.23s | -0.66% 0m26.95s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.44s || +0m00.50s | +1.92% 0m25.62s | SlowPrimeSynthesisExamples.vo | 0m26.04s || -0m00.41s | -1.61% 0m24.39s | RewriterRulesProofs.vo | 0m24.18s || +0m00.21s | +0.86% 0m20.49s | PushButtonSynthesis/BarrettReduction.vo | 0m20.62s || -0m00.13s | -0.63% 0m18.54s | p448_solinas_64.c | 0m19.15s || -0m00.60s | -3.18% 0m17.37s | secp256k1_32.c | 0m17.70s || -0m00.32s | -1.86% 0m14.80s | p434_64.c | 0m14.16s || +0m00.64s | +4.51% 0m14.05s | ExtractionOCaml/unsaturated_solinas | 0m14.28s || -0m00.22s | -1.61% 0m09.17s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.58s || -0m00.41s | -4.27% 0m08.47s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.22s || +0m00.25s | +3.04% 0m07.69s | p384_64.c | 0m07.72s || -0m00.02s | -0.38% 0m06.80s | BoundsPipeline.vo | 0m06.65s || +0m00.14s | +2.25% 0m06.49s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.59s || +0m00.90s | +16.10% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.08s | +2.31% 0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.36s || -0m00.00s | -0.29% 0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.15s || +0m00.04s | +1.26% 0m02.79s | curve25519_32.c | 0m03.32s || -0m00.52s | -15.96% 0m02.66s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.73s || -0m00.06s | -2.56% 0m02.55s | RewriterRules.vo | 0m02.52s || +0m00.02s | +1.19% 0m01.98s | curve25519_64.c | 0m01.57s || +0m00.40s | +26.11% 0m01.78s | p224_64.c | 0m01.30s || +0m00.48s | +36.92% 0m01.60s | secp256k1_64.c | 0m01.74s || -0m00.13s | -8.04% 0m01.45s | p256_64.c | 0m01.55s || -0m00.10s | -6.45% 0m01.34s | RewriterProofs.vo | 0m01.16s || +0m00.18s | +15.51% 0m01.33s | CLI.vo | 0m01.40s || -0m00.06s | -4.99% 0m01.12s | StandaloneOCamlMain.vo | 0m01.09s || +0m00.03s | +2.75% 0m01.10s | CompilersTestCases.vo | 0m01.08s || +0m00.02s | +1.85% 0m01.08s | StandaloneHaskellMain.vo | 0m01.02s || +0m00.06s | +5.88% --- src/RewriterRulesGood.v | 199 +++++++++--------------------------------------- 1 file changed, 36 insertions(+), 163 deletions(-) (limited to 'src/RewriterRulesGood.v') diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index c4486ef67..c05bcc23e 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -44,151 +44,11 @@ Module Compilers. Module Import RewriteRules. Import Rewriter.Compilers.RewriteRules. - Lemma nbe_rewrite_head_eq : @nbe_rewrite_head = @nbe_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma fancy_rewrite_head_eq - : (fun var do_again => @fancy_rewrite_head var) - = @fancy_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma arith_rewrite_head_eq max_const_val : (fun var do_again => @arith_rewrite_head max_const_val var) = (fun var => @arith_rewrite_head0 var max_const_val). - Proof. reflexivity. Qed. - - Lemma fancy_with_casts_rewrite_head_eq invert_low invert_high value_range flag_range - : (fun var do_again => @fancy_with_casts_rewrite_head invert_low invert_high value_range flag_range var) - = (fun var => @fancy_with_casts_rewrite_head0 var invert_low invert_high value_range flag_range). - Proof. reflexivity. Qed. - - Lemma arith_with_casts_rewrite_head_eq : @arith_with_casts_rewrite_head = @arith_with_casts_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma strip_literal_casts_rewrite_head_eq : (fun var do_again => @strip_literal_casts_rewrite_head var) = @strip_literal_casts_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma nbe_all_rewrite_rules_eq : @nbe_all_rewrite_rules = @nbe_rewrite_rules. - Proof. reflexivity. Qed. - - Lemma fancy_all_rewrite_rules_eq : @fancy_all_rewrite_rules = @fancy_rewrite_rules. - Proof. reflexivity. Qed. - - Lemma arith_all_rewrite_rules_eq : @arith_all_rewrite_rules = @arith_rewrite_rules. - Proof. reflexivity. Qed. - - Lemma fancy_with_casts_all_rewrite_rules_eq : @fancy_with_casts_all_rewrite_rules = @fancy_with_casts_rewrite_rules. - Proof. reflexivity. Qed. - - Lemma arith_with_casts_all_rewrite_rules_eq : @arith_with_casts_all_rewrite_rules = @arith_with_casts_rewrite_rules. - Proof. reflexivity. Qed. - - Lemma strip_literal_casts_all_rewrite_rules_eq : @strip_literal_casts_all_rewrite_rules = @strip_literal_casts_rewrite_rules. - Proof. reflexivity. Qed. - Section good. Context {var1 var2 : type -> Type}. Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) var1 var2). - Lemma wf_rlist_rect_gen - {ivar1 ivar2 A P} - Q - N1 N2 C1 C2 ls1 ls2 G - (Hwf : expr.wf G ls1 ls2) - (HN : UnderLets.wf Q 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) - -> Q G' rec1 rec2 - -> UnderLets.wf Q G' (C1 x xs rec1) (C2 y ys rec2)) - : option_eq (UnderLets.wf Q G) - (@rlist_rect var1 A P ivar1 N1 C1 ls1) - (@rlist_rect var2 A P ivar2 N2 C2 ls2). - Proof using Type. - cbv [rlist_rect]. - cbv [Compile.option_bind' Option.bind]. - break_innermost_match. - 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 - | [ |- UnderLets.wf _ _ _ _ ] => constructor - end - | progress expr.invert_subst - | progress cbn [sequence_return option_eq] - | assumption - | reflexivity - | apply @UnderLets.wf_splice with (P:=fun G' => expr.wf G') - | progress intros ]. - lazymatch goal with - | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ] - => revert dependent l'; intro l2; revert dependent l; intro l1 - end. - revert l2; induction l1 as [|l1 ls1 IHls1], l2; cbn [list_rect]; - rewrite ?expr.reify_list_cons, ?expr.reify_list_nil; - intros; expr.inversion_wf_constr; [ assumption | ]. - 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 - | [ |- UnderLets.wf _ _ _ _ ] => constructor - end - | progress expr.invert_subst - | progress cbn [sequence_return option_eq] - | assumption - | reflexivity - | solve [ auto ] - | progress subst - | apply @UnderLets.wf_splice with (P:=Q) - | progress intros - | wf_safe_t_step - | progress type.inversion_type - | progress expr.inversion_wf_constr ]. - Qed. - Lemma wf_rlist_rect {A P} - N1 N2 C1 C2 ls1 ls2 G - (Hwf : expr.wf G ls1 ls2) - (HN : UnderLets.wf (fun G' => expr.wf G') 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) - -> expr.wf G' rec1 rec2 - -> UnderLets.wf (fun G'' => expr.wf G'') G' (C1 x xs rec1) (C2 y ys rec2)) - : option_eq (UnderLets.wf (fun G' => expr.wf G') G) - (@rlist_rect var1 A P var1 N1 C1 ls1) - (@rlist_rect var2 A P var2 N2 C2 ls2). - Proof using Type. apply wf_rlist_rect_gen; assumption. Qed. - Lemma wf_rlist_rectv {A P} - N1 N2 C1 C2 ls1 ls2 G - (Hwf : expr.wf G ls1 ls2) - (HN : UnderLets.wf (fun G' v1 v2 - => 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) - (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) - -> (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 - => 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 G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - /\ expr.wf G'' v1 v2) - G) - (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1) - (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2). - Proof using Type. apply wf_rlist_rect_gen; assumption. Qed. - Lemma wf_list_rect {T A} G N1 N2 C1 C2 ls1 ls2 (HN : Compile.wf_value G N1 N2) @@ -222,22 +82,29 @@ Module Compilers. (nat_rect (fun _ => @Compile.value_with_lets base.type ident var2 A) O2 S2 n). Proof. induction n; cbn [nat_rect]; try eapply HS; eauto using (ex_intro _ nil). Qed. + Global Strategy -100 [rewrite_rules Compile.rewrite_rules_goodT_curried_cps]. + Local Ltac start_good := - apply Compile.rewrite_rules_goodT_by_curried; - split; [ reflexivity | ]; - lazymatch goal with - | [ |- forall x p x' p', In (@existT ?A ?P x p, @existT ?A' ?P' x' p') ?ls -> @?Q x x' p p' ] - => apply (@forall_In_pair_existT A A' P P' Q ls); cbn [projT1 projT2 fst snd]; cbv [id] - end; - (exists eq_refl); - cbn [eq_rect]; - cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data_curried Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen_curried Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default pattern.base.lookup_default PositiveSet.rev PositiveMap.empty Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.maybe_option_eq]; - cbn [List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb]; - repeat first [ progress intros - | match goal with - | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl) - end - | progress cbn [eq_rect] in * ]. + match goal with + | [ |- rewrite_rules_goodT ?rew1 ?rew2 ] + => let H := fresh in + pose proof (@Compile.rewrite_rules_goodT_by_curried _ _ _ _ _ rew1 rew2 eq_refl) as H; + let data := lazymatch rew1 with rewrite_rules ?data _ => data end in + let h := head data in + cbv [h rewrite_rules] in H; + let h' := lazymatch type of H with + | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => head rew1 + end in + let pident_arg_types + := lazymatch type of H with + | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => pident_arg_types + end in + cbv [h' pident_arg_types Compile.rewrite_rules_goodT_curried_cps] in H; + (* make [Qed] not take forever by explicitly recording a cast node *) + let H' := fresh in + pose proof H as H'; clear H; + apply H'; clear H'; intros + end. Local Ltac fin_wf := repeat first [ progress intros @@ -286,15 +153,16 @@ Module Compilers. | progress intros | progress fin_wf ]. + Local Notation nbe_rewrite_rules := (rewrite_rules nbe_rewriter_data _). Lemma nbe_rewrite_rules_good : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules. Proof using Type. Time start_good. - Time all: handle_reified_rewrite_rules; handle_extra_nbe. + Time all: abstract (handle_reified_rewrite_rules; handle_extra_nbe). Qed. Local Ltac handle_extra_arith_rules := - repeat first [ progress cbv [rwhenl option_eq SubstVarLike.is_var_fst_snd_pair_opp_cast] + repeat first [ progress cbv [option_eq SubstVarLike.is_var_fst_snd_pair_opp_cast] in * | break_innermost_match_step | match goal with | [ Hwf : Compile.wf_value _ ?x _, H : context[SubstVarLike.is_recursively_var_or_ident _ ?x] |- _ ] => erewrite SubstVarLike.wfT_is_recursively_var_or_ident in H by exact Hwf @@ -302,37 +170,42 @@ Module Compilers. | congruence | progress fin_wf ]. + Local Notation arith_rewrite_rules max_const := (rewrite_rules (arith_rewriter_data max_const) _). Lemma arith_rewrite_rules_good max_const : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const). Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules; handle_extra_arith_rules. - Qed. + Time Qed. + Local Notation arith_with_casts_rewrite_rules := (rewrite_rules arith_with_casts_rewriter_data _). Lemma arith_with_casts_rewrite_rules_good : rewrite_rules_goodT arith_with_casts_rewrite_rules arith_with_casts_rewrite_rules. Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules. - Qed. + Time Qed. + Local Notation strip_literal_casts_rewrite_rules := (rewrite_rules strip_literal_casts_rewriter_data _). Lemma strip_literal_casts_rewrite_rules_good : rewrite_rules_goodT strip_literal_casts_rewrite_rules strip_literal_casts_rewrite_rules. Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules. - Qed. + Time Qed. + Local Notation fancy_rewrite_rules invert_low invert_high := (rewrite_rules (fancy_rewriter_data invert_low invert_high) _). Lemma fancy_rewrite_rules_good (invert_low invert_high : Z -> Z -> option Z) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) - : rewrite_rules_goodT fancy_rewrite_rules fancy_rewrite_rules. + : rewrite_rules_goodT (fancy_rewrite_rules invert_low invert_high) (fancy_rewrite_rules invert_low invert_high). Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules. - Qed. + Time Qed. + Local Notation fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range := (rewrite_rules (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range) _). Lemma fancy_with_casts_rewrite_rules_good (invert_low invert_high : Z -> Z -> option Z) (value_range flag_range : ZRange.zrange) @@ -342,7 +215,7 @@ Module Compilers. Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules. - Qed. + Time Qed. End good. End RewriteRules. End Compilers. -- cgit v1.2.3