diff options
Diffstat (limited to 'src/RewriterProofs.v')
-rw-r--r-- | src/RewriterProofs.v | 206 |
1 files changed, 18 insertions, 188 deletions
diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v index 2d45a6271..c2a891de1 100644 --- a/src/RewriterProofs.v +++ b/src/RewriterProofs.v @@ -1,194 +1,24 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Language. -Require Import Crypto.LanguageInversion. -Require Import Crypto.LanguageWf. -Require Import Crypto.UnderLetsProofs. -Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Rewriter. -Require Import Crypto.RewriterFull. -Require Import Crypto.RewriterWf1. -Require Import Crypto.RewriterWf2. -Require Import Crypto.RewriterInterpProofs1. -Require Import Crypto.RewriterRulesProofs. -Require Import Crypto.RewriterRulesGood. -Require Import Crypto.RewriterRulesInterpGood. -Import Coq.Lists.List ListNotations. Local Open Scope list_scope. -Local Open Scope Z_scope. +Require Import Crypto.Rewriter.NBE. +Require Import Crypto.Rewriter.Arith. +Require Import Crypto.Rewriter.ArithWithCasts. +Require Import Crypto.Rewriter.StripLiteralCasts. +Require Import Crypto.Rewriter.ToFancy. +Require Import Crypto.Rewriter.ToFancyWithCasts. -Import EqNotations. Module Compilers. - Import Language.Compilers. - Import LanguageInversion.Compilers. - Import LanguageWf.Compilers. - Import UnderLetsProofs.Compilers. - Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. - Import Rewriter.Compilers. - Import RewriterFull.Compilers. - Import RewriterWf1.Compilers. - Import RewriterWf2.Compilers. - Import RewriterInterpProofs1.Compilers. - Import RewriterRulesGood.Compilers. - Import RewriterRulesInterpGood.Compilers. - Import expr.Notations. - Import defaults. - Import Rewriter.Compilers.RewriteRules. - Import RewriterFull.Compilers.RewriteRules. - Import RewriterWf1.Compilers.RewriteRules. - Import RewriterWf2.Compilers.RewriteRules. - Import RewriterInterpProofs1.Compilers.RewriteRules. - Import RewriterRulesGood.Compilers.RewriteRules. - Import RewriterRulesInterpGood.Compilers.RewriteRules. - Import RewriterWf1.Compilers.RewriteRules.GoalType. - Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. - Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. - Import RewriterWf1.Compilers.RewriteRules.GoalType. - Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. - Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. + Export NBE.Compilers. + Export Arith.Compilers. + Export ArithWithCasts.Compilers. + Export StripLiteralCasts.Compilers. + Export ToFancy.Compilers. + Export ToFancyWithCasts.Compilers. Module Import RewriteRules. - Module Export Tactics. - Definition VerifiedRewriter_of_Rewriter - (R : RewriterT) - (RWf : Wf_GoalT R) - (RInterp : Interp_GoalT R) - (RProofs : PrimitiveHList.hlist - (@snd bool Prop) - (List.skipn (dummy_count (Rewriter_data R)) (rewrite_rules_specs (Rewriter_data R)))) - : VerifiedRewriter. - Proof. - simple refine - (let HWf := _ in - let HInterp_gen := _ in - @Build_VerifiedRewriter R RWf RInterp HWf HInterp_gen (HInterp_gen _)); - [ | clear HWf ]; intros. - all: abstract ( - rewrite Rewrite_eq; cbv [Make.Rewrite]; rewrite rewrite_head_eq, all_rewrite_rules_eq; - first [ apply Compile.Wf_Rewrite; [ | assumption ]; - let wf_do_again := fresh "wf_do_again" in - (intros ? ? ? ? wf_do_again ? ?); - eapply @Compile.wf_assemble_identifier_rewriters; - eauto using - pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct - with nocore; - try reflexivity - | eapply Compile.InterpRewrite; [ | assumption ]; - intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); - eauto using - pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed, - @ident.gen_interp_Proper, eq_refl - with nocore ]). - Defined. - End Tactics. - - Definition VerifiedRewriterNBE : VerifiedRewriter - := @VerifiedRewriter_of_Rewriter RewriterNBE RewriterRulesNBEWf RewriterRulesNBEInterp nbe_rewrite_rules_proofs. - Definition VerifiedRewriterArith (max_const_val : Z) : VerifiedRewriter - := @VerifiedRewriter_of_Rewriter (RewriterArith max_const_val) (RewriterRulesArithWf max_const_val) (RewriterRulesArithInterp max_const_val) (arith_rewrite_rules_proofs max_const_val). - Definition VerifiedRewriterArithWithCasts : VerifiedRewriter - := @VerifiedRewriter_of_Rewriter RewriterArithWithCasts RewriterRulesArithWithCastsWf RewriterRulesArithWithCastsInterp arith_with_casts_rewrite_rules_proofs. - Definition VerifiedRewriterStripLiteralCasts : VerifiedRewriter - := @VerifiedRewriter_of_Rewriter RewriterStripLiteralCasts RewriterRulesStripLiteralCastsWf RewriterRulesStripLiteralCastsInterp strip_literal_casts_rewrite_rules_proofs. - Definition VerifiedRewriterToFancy (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)) - : VerifiedRewriter - := @VerifiedRewriter_of_Rewriter (RewriterToFancy invert_low invert_high) (RewriterRulesToFancyWf invert_low invert_high Hlow Hhigh) (RewriterRulesToFancyInterp invert_low invert_high Hlow Hhigh) fancy_rewrite_rules_proofs. - Definition VerifiedRewriterToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z) - (value_range flag_range : ZRange.zrange) - (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)) - : VerifiedRewriter - := @VerifiedRewriter_of_Rewriter (RewriterToFancyWithCasts invert_low invert_high value_range flag_range) (RewriterRulesToFancyWithCastsWf invert_low invert_high value_range flag_range Hlow Hhigh) (RewriterRulesToFancyWithCastsInterp invert_low invert_high value_range flag_range Hlow Hhigh) (fancy_with_casts_rewrite_rules_proofs invert_low invert_high value_range flag_range Hlow Hhigh). - - Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e). - Proof. now apply VerifiedRewriterNBE. Qed. - Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e). - Proof. now apply VerifiedRewriterArith. Qed. - Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e). - Proof. now apply VerifiedRewriterArithWithCasts. Qed. - Lemma Wf_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Wf (@RewriteStripLiteralCasts t e). - Proof. now apply VerifiedRewriterStripLiteralCasts. Qed. - Lemma Wf_RewriteToFancy (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)) - {t} e (Hwf : Wf e) : Wf (@RewriteToFancy invert_low invert_high t e). - Proof. unshelve eapply VerifiedRewriterToFancy; multimatch goal with H : _ |- _ => refine H end. Qed. - Lemma Wf_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z) - (value_range flag_range : ZRange.zrange) - (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)) - {t} e (Hwf : Wf e) : Wf (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e). - Proof. now unshelve eapply VerifiedRewriterToFancyWithCasts. Qed. - - Lemma Interp_gen_RewriteNBE {cast_outside_of_range t} e (Hwf : Wf e) - : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteNBE t e) - == expr.Interp (@ident.gen_interp cast_outside_of_range) e. - Proof. now apply VerifiedRewriterNBE. Qed. - Lemma Interp_gen_RewriteArith {cast_outside_of_range} (max_const_val : Z) {t} e (Hwf : Wf e) - : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArith max_const_val t e) - == expr.Interp (@ident.gen_interp cast_outside_of_range) e. - Proof. now apply VerifiedRewriterArith. Qed. - Lemma Interp_gen_RewriteArithWithCasts {cast_outside_of_range} {t} e (Hwf : Wf e) - : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArithWithCasts t e) - == expr.Interp (@ident.gen_interp cast_outside_of_range) e. - Proof. now apply VerifiedRewriterArithWithCasts. Qed. - Lemma Interp_gen_RewriteStripLiteralCasts {cast_outside_of_range} {t} e (Hwf : Wf e) - : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteStripLiteralCasts t e) - == expr.Interp (@ident.gen_interp cast_outside_of_range) e. - Proof. now apply VerifiedRewriterStripLiteralCasts. Qed. - Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (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)) - {t} e (Hwf : Wf e) - : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancy invert_low invert_high t e) - == expr.Interp (@ident.gen_interp cast_outside_of_range) e. - Proof. unshelve eapply VerifiedRewriterToFancy; multimatch goal with H : _ |- _ => refine H end. Qed. - Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) - (value_range flag_range : ZRange.zrange) - (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)) - {t} e (Hwf : Wf e) - : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e) - == expr.Interp (@ident.gen_interp cast_outside_of_range) e. - Proof. now unshelve eapply VerifiedRewriterToFancyWithCasts. Qed. - - Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. - Proof. apply Interp_gen_RewriteNBE; assumption. Qed. - Lemma Interp_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) - : Interp (@RewriteArith max_const_val t e) == Interp e. - Proof. apply Interp_gen_RewriteArith; assumption. Qed. - Lemma Interp_RewriteArithWithCasts {t} e (Hwf : Wf e) - : Interp (@RewriteArithWithCasts t e) == Interp e. - Proof. apply Interp_gen_RewriteArithWithCasts; assumption. Qed. - Lemma Interp_RewriteStripLiteralCasts {t} e (Hwf : Wf e) - : Interp (@RewriteStripLiteralCasts t e) == Interp e. - Proof. apply Interp_gen_RewriteStripLiteralCasts; assumption. Qed. - Lemma Interp_RewriteToFancy (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)) - {t} e (Hwf : Wf e) - : Interp (@RewriteToFancy invert_low invert_high t e) == Interp e. - Proof. apply Interp_gen_RewriteToFancy; assumption. Qed. - Lemma Interp_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z) - (value_range flag_range : ZRange.zrange) - (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)) - {t} e (Hwf : Wf e) - : Interp (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e) == Interp e. - Proof. apply Interp_gen_RewriteToFancyWithCasts; assumption. Qed. + Export NBE.Compilers.RewriteRules. + Export Arith.Compilers.RewriteRules. + Export ArithWithCasts.Compilers.RewriteRules. + Export StripLiteralCasts.Compilers.RewriteRules. + Export ToFancy.Compilers.RewriteRules. + Export ToFancyWithCasts.Compilers.RewriteRules. End RewriteRules. - - Lemma Wf_PartialEvaluate {t} e (Hwf : Wf e) : Wf (@PartialEvaluate t e). - Proof. apply Wf_RewriteNBE, Hwf. Qed. - - Lemma Interp_gen_PartialEvaluate {cast_outside_of_range} {t} e (Hwf : Wf e) - : expr.Interp (@ident.gen_interp cast_outside_of_range) (@PartialEvaluate t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. - Proof. apply Interp_gen_RewriteNBE, Hwf. Qed. - - Lemma Interp_PartialEvaluate {t} e (Hwf : Wf e) - : Interp (@PartialEvaluate t e) == Interp e. - Proof. apply Interp_gen_PartialEvaluate; assumption. Qed. - - Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy Wf_RewriteArithWithCasts Wf_RewriteStripLiteralCasts Wf_RewriteToFancyWithCasts : wf. - Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_gen_RewriteArithWithCasts @Interp_gen_RewriteStripLiteralCasts @Interp_gen_RewriteToFancyWithCasts @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy @Interp_RewriteArithWithCasts @Interp_RewriteStripLiteralCasts @Interp_RewriteToFancyWithCasts : interp. End Compilers. |