diff options
| -rw-r--r-- | _CoqProject | 10 | ||||
| -rw-r--r-- | src/BoundsPipeline.v | 3 | ||||
| -rw-r--r-- | src/CompilersTestCases.v | 4 | ||||
| -rw-r--r-- | src/Rewriter/Arith.v | 40 | ||||
| -rw-r--r-- | src/Rewriter/ArithWithCasts.v | 37 | ||||
| -rw-r--r-- | src/Rewriter/NBE.v | 50 | ||||
| -rw-r--r-- | src/Rewriter/StripLiteralCasts.v | 37 | ||||
| -rw-r--r-- | src/Rewriter/ToFancy.v | 45 | ||||
| -rw-r--r-- | src/Rewriter/ToFancyWithCasts.v | 47 | ||||
| -rw-r--r-- | src/RewriterFull.v | 49 | ||||
| -rw-r--r-- | src/RewriterProofs.v | 206 | ||||
| -rw-r--r-- | src/RewriterProofsTactics.v | 107 | ||||
| -rw-r--r-- | src/RewriterRulesGood.v | 42 | ||||
| -rw-r--r-- | src/RewriterRulesInterpGood.v | 42 | ||||
| -rw-r--r-- | src/RewriterWf1.v | 10 |
15 files changed, 394 insertions, 335 deletions
diff --git a/_CoqProject b/_CoqProject index 9f5a239e1..2ca7a4b89 100644 --- a/_CoqProject +++ b/_CoqProject @@ -35,12 +35,10 @@ src/MiscCompilerPasses.v src/MiscCompilerPassesProofs.v src/PreLanguage.v src/Rewriter.v -src/RewriterFull.v src/RewriterInterpProofs1.v src/RewriterProofs.v +src/RewriterProofsTactics.v src/RewriterRules.v -src/RewriterRulesGood.v -src/RewriterRulesInterpGood.v src/RewriterRulesProofs.v src/RewriterWf1.v src/RewriterWf2.v @@ -121,6 +119,12 @@ src/PushButtonSynthesis/UnsaturatedSolinas.v src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v src/PushButtonSynthesis/WordByWordMontgomery.v src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v +src/Rewriter/Arith.v +src/Rewriter/ArithWithCasts.v +src/Rewriter/NBE.v +src/Rewriter/StripLiteralCasts.v +src/Rewriter/ToFancy.v +src/Rewriter/ToFancyWithCasts.v src/Spec/CompleteEdwardsCurve.v src/Spec/Ed25519.v src/Spec/EdDSA.v diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index af25f223e..f0c161dc2 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -24,7 +24,6 @@ Require Crypto.Language. Require Crypto.UnderLets. Require Crypto.AbstractInterpretation. Require Crypto.Rewriter. -Require Crypto.RewriterFull. Require Crypto.MiscCompilerPasses. Require Crypto.CStringification. Require Crypto.LanguageWf. @@ -47,7 +46,6 @@ Import Crypto.UnderLets Crypto.AbstractInterpretation Crypto.Rewriter - Crypto.RewriterFull Crypto.MiscCompilerPasses Crypto.CStringification. @@ -62,7 +60,6 @@ Import UnderLets.Compilers AbstractInterpretation.Compilers Rewriter.Compilers - RewriterFull.Compilers MiscCompilerPasses.Compilers CStringification.Compilers. diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v index 19fcf1588..2ed149cdd 100644 --- a/src/CompilersTestCases.v +++ b/src/CompilersTestCases.v @@ -5,7 +5,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Language. Require Import Crypto.UnderLets. Require Import Crypto.AbstractInterpretation. -Require Import Crypto.RewriterFull. +Require Import Crypto.RewriterProofs. Require Import Crypto.MiscCompilerPasses. Require Import Crypto.CStringification. Import ListNotations. Local Open Scope Z_scope. @@ -13,7 +13,7 @@ Import ListNotations. Local Open Scope Z_scope. Import Language.Compilers. Import UnderLets.Compilers. Import AbstractInterpretation.Compilers. -Import RewriterFull.Compilers. +Import RewriterProofs.Compilers. Import MiscCompilerPasses.Compilers. Import CStringification.Compilers. Local Coercion Z.of_nat : nat >-> Z. diff --git a/src/Rewriter/Arith.v b/src/Rewriter/Arith.v new file mode 100644 index 000000000..cae1526d2 --- /dev/null +++ b/src/Rewriter/Arith.v @@ -0,0 +1,40 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. +Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterRulesProofs. + +Module Compilers. + Import Language.Compilers. + Import Language.Compilers.defaults. + Import LanguageWf.Compilers. + Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. + Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + + Module Import RewriteRules. + Section __. + Context (max_const_val : Z). + + Definition VerifiedRewriterArith : VerifiedRewriter. + Proof using All. make_rewriter false (arith_rewrite_rules_proofs max_const_val). Defined. + + Definition RewriteArith {t} := Eval hnf in @Rewrite VerifiedRewriterArith t. + + Lemma Wf_RewriteArith {t} e (Hwf : Wf e) : Wf (@RewriteArith t e). + Proof. now apply VerifiedRewriterArith. Qed. + + Lemma Interp_gen_RewriteArith {cast_outside_of_range t} e (Hwf : Wf e) + : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArith t e) + == expr.Interp (@ident.gen_interp cast_outside_of_range) e. + Proof. now apply VerifiedRewriterArith. Qed. + + Lemma Interp_RewriteArith {t} e (Hwf : Wf e) : Interp (@RewriteArith t e) == Interp e. + Proof. apply Interp_gen_RewriteArith; assumption. Qed. + End __. + End RewriteRules. + + Module Export Hints. + Hint Resolve Wf_RewriteArith : wf. + Hint Rewrite @Interp_gen_RewriteArith @Interp_RewriteArith : interp. + End Hints. +End Compilers. diff --git a/src/Rewriter/ArithWithCasts.v b/src/Rewriter/ArithWithCasts.v new file mode 100644 index 000000000..de17f207e --- /dev/null +++ b/src/Rewriter/ArithWithCasts.v @@ -0,0 +1,37 @@ +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. +Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterRulesProofs. + +Module Compilers. + Import Language.Compilers. + Import Language.Compilers.defaults. + Import LanguageWf.Compilers. + Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. + Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + + Module Import RewriteRules. + Section __. + Definition VerifiedRewriterArithWithCasts : VerifiedRewriter. + Proof using All. make_rewriter false arith_with_casts_rewrite_rules_proofs. Defined. + + Definition RewriteArithWithCasts {t} := Eval hnf in @Rewrite VerifiedRewriterArithWithCasts t. + + Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e). + Proof. now apply VerifiedRewriterArithWithCasts. 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_RewriteArithWithCasts {t} e (Hwf : Wf e) : Interp (@RewriteArithWithCasts t e) == Interp e. + Proof. apply Interp_gen_RewriteArithWithCasts; assumption. Qed. + End __. + End RewriteRules. + + Module Export Hints. + Hint Resolve Wf_RewriteArithWithCasts : wf. + Hint Rewrite @Interp_gen_RewriteArithWithCasts @Interp_RewriteArithWithCasts : interp. + End Hints. +End Compilers. diff --git a/src/Rewriter/NBE.v b/src/Rewriter/NBE.v new file mode 100644 index 000000000..64e38a38d --- /dev/null +++ b/src/Rewriter/NBE.v @@ -0,0 +1,50 @@ +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. +Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterRulesProofs. + +Module Compilers. + Import Language.Compilers. + Import Language.Compilers.defaults. + Import LanguageWf.Compilers. + Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. + Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + + Module Import RewriteRules. + Section __. + Definition VerifiedRewriterNBE : VerifiedRewriter. + Proof using All. make_rewriter true nbe_rewrite_rules_proofs. Defined. + + Definition RewriteNBE {t} := Eval hnf in @Rewrite VerifiedRewriterNBE t. + + Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e). + Proof. now apply VerifiedRewriterNBE. 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_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. + Proof. apply Interp_gen_RewriteNBE; assumption. Qed. + End __. + End RewriteRules. + + Definition PartialEvaluate {t} (e : Expr t) : Expr t := RewriteRules.RewriteNBE e. + + 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. + + Module Export Hints. + Hint Resolve Wf_PartialEvaluate Wf_RewriteNBE : wf. + Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteNBE @Interp_PartialEvaluate @Interp_RewriteNBE : interp. + End Hints. +End Compilers. diff --git a/src/Rewriter/StripLiteralCasts.v b/src/Rewriter/StripLiteralCasts.v new file mode 100644 index 000000000..0f35dfed6 --- /dev/null +++ b/src/Rewriter/StripLiteralCasts.v @@ -0,0 +1,37 @@ +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. +Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterRulesProofs. + +Module Compilers. + Import Language.Compilers. + Import Language.Compilers.defaults. + Import LanguageWf.Compilers. + Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. + Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + + Module Import RewriteRules. + Section __. + Definition VerifiedRewriterStripLiteralCasts : VerifiedRewriter. + Proof using All. make_rewriter false strip_literal_casts_rewrite_rules_proofs. Defined. + + Definition RewriteStripLiteralCasts {t} := Eval hnf in @Rewrite VerifiedRewriterStripLiteralCasts t. + + Lemma Wf_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Wf (@RewriteStripLiteralCasts t e). + Proof. now apply VerifiedRewriterStripLiteralCasts. 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_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Interp (@RewriteStripLiteralCasts t e) == Interp e. + Proof. apply Interp_gen_RewriteStripLiteralCasts; assumption. Qed. + End __. + End RewriteRules. + + Module Export Hints. + Hint Resolve Wf_RewriteStripLiteralCasts : wf. + Hint Rewrite @Interp_gen_RewriteStripLiteralCasts @Interp_RewriteStripLiteralCasts : interp. + End Hints. +End Compilers. diff --git a/src/Rewriter/ToFancy.v b/src/Rewriter/ToFancy.v new file mode 100644 index 000000000..da18848ba --- /dev/null +++ b/src/Rewriter/ToFancy.v @@ -0,0 +1,45 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. +Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterRulesProofs. + +Module Compilers. + Import Language.Compilers. + Import Language.Compilers.defaults. + Import LanguageWf.Compilers. + Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. + Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + + Module Import RewriteRules. + Section __. + Context (invert_low invert_high : Z (*log2wordmax*) -> 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)). + + Definition VerifiedRewriterToFancy : VerifiedRewriter. + Proof using All. make_rewriter false fancy_rewrite_rules_proofs. Defined. + + Definition RewriteToFancy {t} : Expr t -> Expr t. + Proof using invert_low invert_high. + let v := (eval hnf in (@Rewrite VerifiedRewriterToFancy t)) in exact v. + Defined. + + Lemma Wf_RewriteToFancy {t} e (Hwf : Wf e) : Wf (@RewriteToFancy t e). + Proof using All. now apply VerifiedRewriterToFancy. Qed. + + Lemma Interp_gen_RewriteToFancy {cast_outside_of_range t} e (Hwf : Wf e) + : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancy t e) + == expr.Interp (@ident.gen_interp cast_outside_of_range) e. + Proof using All. now apply VerifiedRewriterToFancy. Qed. + + Lemma Interp_RewriteToFancy {t} e (Hwf : Wf e) : Interp (@RewriteToFancy t e) == Interp e. + Proof using All. apply Interp_gen_RewriteToFancy; assumption. Qed. + End __. + End RewriteRules. + + Module Export Hints. + Hint Resolve Wf_RewriteToFancy : wf. + Hint Rewrite @Interp_gen_RewriteToFancy @Interp_RewriteToFancy : interp. + End Hints. +End Compilers. diff --git a/src/Rewriter/ToFancyWithCasts.v b/src/Rewriter/ToFancyWithCasts.v new file mode 100644 index 000000000..714ea071e --- /dev/null +++ b/src/Rewriter/ToFancyWithCasts.v @@ -0,0 +1,47 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. +Require Import Crypto.Util.ZRange. +Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterRulesProofs. + +Module Compilers. + Import Language.Compilers. + Import Language.Compilers.defaults. + Import LanguageWf.Compilers. + Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. + Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + + Module Import RewriteRules. + Section __. + Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + (value_range flag_range : 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)). + + Definition VerifiedRewriterToFancyWithCasts : VerifiedRewriter. + Proof using All. make_rewriter false (@fancy_with_casts_rewrite_rules_proofs invert_low invert_high value_range flag_range Hlow Hhigh). Defined. + + Definition RewriteToFancyWithCasts {t} : Expr t -> Expr t. + Proof using invert_low invert_high value_range flag_range. + let v := (eval hnf in (@Rewrite VerifiedRewriterToFancyWithCasts t)) in exact v. + Defined. + + Lemma Wf_RewriteToFancyWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteToFancyWithCasts t e). + Proof using All. now apply VerifiedRewriterToFancyWithCasts. Qed. + + Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range t} e (Hwf : Wf e) + : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts t e) + == expr.Interp (@ident.gen_interp cast_outside_of_range) e. + Proof using All. now apply VerifiedRewriterToFancyWithCasts. Qed. + + Lemma Interp_RewriteToFancyWithCasts {t} e (Hwf : Wf e) : Interp (@RewriteToFancyWithCasts t e) == Interp e. + Proof using All. apply Interp_gen_RewriteToFancyWithCasts; assumption. Qed. + End __. + End RewriteRules. + + Module Export Hints. + Hint Resolve Wf_RewriteToFancyWithCasts : wf. + Hint Rewrite @Interp_gen_RewriteToFancyWithCasts @Interp_RewriteToFancyWithCasts : interp. + End Hints. +End Compilers. diff --git a/src/RewriterFull.v b/src/RewriterFull.v deleted file mode 100644 index 772732442..000000000 --- a/src/RewriterFull.v +++ /dev/null @@ -1,49 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZRange. -Require Import Crypto.RewriterRules. -Require Import Crypto.Rewriter. -Local Open Scope Z_scope. - -Import Compilers.RewriteRules.GoalType. -Import Compilers.RewriteRules.Tactic. - -Module Compilers. - Module RewriteRules. - Definition RewriterNBE : RewriterT. - Proof. make_Rewriter true nbe_rewrite_rulesT. Defined. - - Definition RewriterArith (max_const_val : Z) : RewriterT. - Proof. make_Rewriter false (arith_rewrite_rulesT max_const_val). Defined. - - Definition RewriterArithWithCasts : RewriterT. - Proof. make_Rewriter false arith_with_casts_rewrite_rulesT. Defined. - - Definition RewriterStripLiteralCasts : RewriterT. - Proof. make_Rewriter false strip_literal_casts_rewrite_rulesT. Defined. - - Definition RewriterToFancy - (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) - : RewriterT. - Proof. make_Rewriter false fancy_rewrite_rulesT. Defined. - - Definition RewriterToFancyWithCasts - (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) - (value_range flag_range : zrange) - : RewriterT. - Proof. make_Rewriter false (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). Defined. - - Definition RewriteNBE {t} := Eval hnf in @Rewrite RewriterNBE t. - Definition RewriteArith max_const_val {t} := Eval hnf in @Rewrite (RewriterArith max_const_val) t. - Definition RewriteArithWithCasts {t} := Eval hnf in @Rewrite RewriterArithWithCasts t. - Definition RewriteStripLiteralCasts {t} := Eval hnf in @Rewrite RewriterStripLiteralCasts t. - Definition RewriteToFancy invert_low invert_high {t} - := Eval hnf in @Rewrite (RewriterToFancy invert_low invert_high) t. - Definition RewriteToFancyWithCasts invert_low invert_high value_range flag_range {t} - := Eval hnf in @Rewrite (RewriterToFancyWithCasts invert_low invert_high value_range flag_range) t. - End RewriteRules. - - Import Language.Compilers.defaults. - - Definition PartialEvaluate {t} (e : Expr t) : Expr t - := RewriteRules.RewriteNBE e. -End Compilers. 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. diff --git a/src/RewriterProofsTactics.v b/src/RewriterProofsTactics.v new file mode 100644 index 000000000..22fd16cbb --- /dev/null +++ b/src/RewriterProofsTactics.v @@ -0,0 +1,107 @@ +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.RewriterWf1. +Require Import Crypto.RewriterWf2. +Require Import Crypto.RewriterInterpProofs1. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Import Crypto.Util.Tactics.ConstrFail. + +Module Compilers. + Import LanguageWf.Compilers. + Import GENERATEDIdentifiersWithoutTypes.Compilers. + Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. + Import Rewriter.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules. + Import RewriterWf2.Compilers.RewriteRules. + Import RewriterInterpProofs1.Compilers.RewriteRules. + Import Rewriter.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. + + Module Import RewriteRules. + 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 (@Rewriter.Compilers.RewriteRules.GoalType.Rewrite R) 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. + + Ltac make_VerifiedRewriter R RWf RInterp RProofs := + let res := (eval hnf in (@VerifiedRewriter_of_Rewriter R RWf RInterp RProofs)) in + let res := lazymatch res with + | context Res[@Build_VerifiedRewriter ?R] + => let t := fresh "t" in + let R' := fresh in + let R' := constr:(fun t + => match R t return _ with + | R' => ltac:(let v := (eval hnf in R') in exact v) + end) in + context Res[@Build_VerifiedRewriter R'] + end in + res. + + Ltac Build_Rewriter include_interp specs_proofs := + let specs := lazymatch type of specs_proofs with + | PrimitiveHList.hlist (@snd bool Prop) ?specs => specs + | ?T + => let expected_type := uconstr:(PrimitiveHList.hlist (@snd bool Prop) ?[specs]) in + constr_fail_with ltac:(fun _ => fail 1 "Invalid type for specs_proofs:" T "Expected:" expected_type) + end in + let R_name := fresh "Rewriter_data" in + let R := Build_RewriterT include_interp specs in + let R := cache_term R R_name in + let Rwf := fresh "Rewriter_Wf" in + let Rwf := cache_proof_with_type_by (Wf_GoalT R) ltac:(idtac; prove_good ()) Rwf in + let RInterp := fresh "Rewriter_Interp" in + let RInterp := cache_proof_with_type_by (Interp_GoalT R) ltac:(idtac; prove_interp_good ()) RInterp in + make_VerifiedRewriter R Rwf RInterp specs_proofs. + + Module Export GoalType. + Export RewriterWf1.Compilers.RewriteRules.GoalType. + End GoalType. + + Module Export Tactic. + Module Export Settings. + Export Rewriter.Compilers.RewriteRules.Tactic.Settings. + End Settings. + + Ltac make_rewriter include_interp specs_proofs := + let res := Build_Rewriter include_interp specs_proofs in refine res. + + Tactic Notation "make_rewriter" constr(include_interp) constr(specs_proofs) := + make_rewriter include_interp specs_proofs. + End Tactic. + End RewriteRules. +End Compilers. diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v deleted file mode 100644 index 2d3ed96e2..000000000 --- a/src/RewriterRulesGood.v +++ /dev/null @@ -1,42 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.RewriterFull. -Require Import Crypto.RewriterWf1. -Local Open Scope Z_scope. - -Module Compilers. - Import RewriterFull.Compilers. - Import RewriterWf1.Compilers. - - Module Import RewriteRules. - Import RewriterFull.Compilers.RewriteRules. - Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. - Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. - - Lemma RewriterRulesNBEWf : Wf_GoalT RewriterNBE. - Proof. prove_good (). Qed. - - Lemma RewriterRulesArithWf max_const : Wf_GoalT (RewriterArith max_const). - Proof. prove_good (). Qed. - - Lemma RewriterRulesArithWithCastsWf : Wf_GoalT RewriterArithWithCasts. - Proof. prove_good (). Qed. - - Lemma RewriterRulesStripLiteralCastsWf : Wf_GoalT RewriterStripLiteralCasts. - Proof. prove_good (). Qed. - - Lemma RewriterRulesToFancyWf - (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)) - : Wf_GoalT (RewriterToFancy invert_low invert_high). - Proof. prove_good (). Qed. - - Lemma RewriterRulesToFancyWithCastsWf - (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)) - : Wf_GoalT (RewriterToFancyWithCasts invert_low invert_high value_range flag_range). - Proof. prove_good (). Qed. - End RewriteRules. -End Compilers. diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v deleted file mode 100644 index 095719421..000000000 --- a/src/RewriterRulesInterpGood.v +++ /dev/null @@ -1,42 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.RewriterFull. -Require Import Crypto.RewriterWf1. -Local Open Scope Z_scope. - -Module Compilers. - Import RewriterFull.Compilers. - Import RewriterWf1.Compilers. - - Module Import RewriteRules. - Import RewriterFull.Compilers.RewriteRules. - Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. - Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. - - Lemma RewriterRulesNBEInterp : Interp_GoalT RewriterNBE. - Proof. prove_interp_good (). Qed. - - Lemma RewriterRulesArithInterp max_const : Interp_GoalT (RewriterArith max_const). - Proof. prove_interp_good (). Qed. - - Lemma RewriterRulesArithWithCastsInterp : Interp_GoalT RewriterArithWithCasts. - Proof. prove_interp_good (). Qed. - - Lemma RewriterRulesStripLiteralCastsInterp : Interp_GoalT RewriterStripLiteralCasts. - Proof. prove_interp_good (). Qed. - - Lemma RewriterRulesToFancyInterp - (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)) - : Interp_GoalT (RewriterToFancy invert_low invert_high). - Proof. prove_interp_good (). Qed. - - Lemma RewriterRulesToFancyWithCastsInterp - (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)) - : Interp_GoalT (RewriterToFancyWithCasts invert_low invert_high value_range flag_range). - Proof. prove_interp_good (). Qed. - End RewriteRules. -End Compilers. diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index d9e1f6293..2788d7444 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -3716,16 +3716,14 @@ Module Compilers. Module GoalType. Record VerifiedRewriter := { - Rewriter : RewriterT; - RewriterRulesWf : WfTactics.GoalType.Wf_GoalT Rewriter; - RewriterRulesInterp : InterpTactics.GoalType.Interp_GoalT Rewriter; - Wf_Rewrite : forall {t} e (Hwf : Wf e), Wf (@Rewrite Rewriter t e); + Rewrite : forall {t} (e : expr.Expr (ident:=ident) t), expr.Expr (ident:=ident) t; + Wf_Rewrite : forall {t} e (Hwf : Wf e), Wf (@Rewrite t e); Interp_gen_Rewrite : forall {cast_outside_of_range t} e (Hwf : Wf e), - expr.Interp (@ident.gen_interp cast_outside_of_range) (@Rewrite Rewriter t e) + expr.Interp (@ident.gen_interp cast_outside_of_range) (@Rewrite t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e; Interp_Rewrite - : forall {t} e (Hwf : Wf e), Interp (@Rewrite Rewriter t e) == Interp e + : forall {t} e (Hwf : Wf e), Interp (@Rewrite t e) == Interp e }. End GoalType. End RewriteRules. |