diff options
Diffstat (limited to 'src/Rewriter')
| -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 |
6 files changed, 256 insertions, 0 deletions
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. |