aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross <jgross@mit.edu>2019-04-08 15:41:53 -0400
committerJason Gross <jasongross9@gmail.com>2019-04-11 11:01:29 -0400
commit301af21a0d908762a83ebbd9c009bcd8d3af3100 (patch)
tree1fcfd7a1c07c48b0f19b1c2b33110f441853ea12
parentad3f1343356b2ac60da964922459105e3329af0e (diff)
Make a single tactic to build the rewriter
Parallelize across different rewriters, rather than across different parts of the rewriter. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 20m38.03s | Total | 20m17.67s || +0m20.36s | +1.67% ----------------------------------------------------------------------------------------------- N/A | RewriterFull.vo | 1m11.76s || -1m11.76s | -100.00% 0m56.15s | Rewriter/ToFancyWithCasts.vo | N/A || +0m56.14s | ∞ N/A | RewriterRulesInterpGood.vo | 0m51.06s || -0m51.06s | -100.00% 0m45.62s | Rewriter/NBE.vo | N/A || +0m45.61s | ∞ 0m44.32s | Rewriter/ArithWithCasts.vo | N/A || +0m44.32s | ∞ 0m24.56s | Rewriter/Arith.vo | N/A || +0m24.55s | ∞ N/A | RewriterRulesGood.vo | 0m21.60s || -0m21.60s | -100.00% 1m34.27s | RewriterWf2.vo | 1m43.16s || -0m08.88s | -8.61% 3m21.20s | p384_32.c | 3m28.08s || -0m06.87s | -3.30% 1m40.72s | Fancy/Barrett256.vo | 1m43.94s || -0m03.21s | -3.09% 0m41.11s | p521_64.c | 0m38.11s || +0m03.00s | +7.87% 0m47.88s | p521_32.c | 0m44.98s || +0m02.90s | +6.44% 0m23.68s | ExtractionOCaml/word_by_word_montgomery | 0m21.56s || +0m02.12s | +9.83% 0m58.92s | ExtractionHaskell/word_by_word_montgomery | 0m57.87s || +0m01.05s | +1.81% 0m20.05s | p448_solinas_64.c | 0m18.72s || +0m01.33s | +7.10% 0m15.19s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.76s || +0m01.42s | +10.39% 0m14.64s | ExtractionOCaml/unsaturated_solinas | 0m13.55s || +0m01.08s | +8.04% 0m09.19s | ExtractionOCaml/saturated_solinas | 0m10.69s || -0m01.50s | -14.03% 0m08.65s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.85s || -0m01.19s | -12.18% 0m07.71s | ExtractionOCaml/saturated_solinas.ml | 0m06.26s || +0m01.45s | +23.16% 0m05.93s | ExtractionHaskell/saturated_solinas.hs | 0m04.71s || +0m01.21s | +25.90% 0m01.16s | Rewriter/StripLiteralCasts.vo | N/A || +0m01.15s | ∞ 0m01.14s | Rewriter/ToFancy.vo | N/A || +0m01.13s | ∞ 0m44.44s | RewriterInterpProofs1.vo | 0m45.18s || -0m00.74s | -1.63% 0m39.85s | ExtractionHaskell/unsaturated_solinas | 0m40.68s || -0m00.82s | -2.04% 0m36.42s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.44s || -0m00.01s | -0.05% 0m36.21s | RewriterWf1.vo | 0m36.91s || -0m00.69s | -1.89% 0m34.81s | Fancy/Montgomery256.vo | 0m34.38s || +0m00.42s | +1.25% 0m30.85s | ExtractionHaskell/saturated_solinas | 0m31.77s || -0m00.91s | -2.89% 0m27.26s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.09s || +0m00.17s | +0.62% 0m26.88s | SlowPrimeSynthesisExamples.vo | 0m27.32s || -0m00.44s | -1.61% 0m20.88s | PushButtonSynthesis/BarrettReduction.vo | 0m21.17s || -0m00.29s | -1.36% 0m18.08s | secp256k1_32.c | 0m18.44s || -0m00.36s | -1.95% 0m17.39s | p256_32.c | 0m17.74s || -0m00.34s | -1.97% 0m15.12s | p434_64.c | 0m14.68s || +0m00.43s | +2.99% 0m09.02s | p224_32.c | 0m08.11s || +0m00.91s | +11.22% 0m07.91s | p384_64.c | 0m07.92s || -0m00.00s | -0.12% 0m07.89s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.50s || +0m00.38s | +5.19% 0m07.02s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.60s || -0m00.58s | -7.63% 0m06.91s | BoundsPipeline.vo | 0m06.92s || -0m00.00s | -0.14% 0m03.56s | PushButtonSynthesis/Primitives.vo | 0m03.53s || +0m00.03s | +0.84% 0m03.39s | PushButtonSynthesis/SmallExamples.vo | 0m03.25s || +0m00.14s | +4.30% 0m03.32s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.14s || +0m00.17s | +5.73% 0m02.83s | curve25519_32.c | 0m02.41s || +0m00.41s | +17.42% 0m02.72s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.62s || +0m00.10s | +3.81% 0m01.91s | secp256k1_64.c | 0m01.89s || +0m00.02s | +1.05% 0m01.75s | curve25519_64.c | 0m02.14s || -0m00.39s | -18.22% 0m01.60s | p224_64.c | 0m01.60s || +0m00.00s | +0.00% 0m01.43s | p256_64.c | 0m01.82s || -0m00.39s | -21.42% 0m01.30s | CLI.vo | 0m01.35s || -0m00.05s | -3.70% 0m01.22s | StandaloneOCamlMain.vo | 0m01.07s || +0m00.14s | +14.01% 0m01.18s | CompilersTestCases.vo | 0m01.14s || +0m00.04s | +3.50% 0m01.12s | StandaloneHaskellMain.vo | 0m01.14s || -0m00.01s | -1.75% 0m00.84s | RewriterProofsTactics.vo | N/A || +0m00.84s | ∞ 0m00.83s | RewriterProofs.vo | 0m01.06s || -0m00.23s | -21.69%
-rw-r--r--_CoqProject10
-rw-r--r--src/BoundsPipeline.v3
-rw-r--r--src/CompilersTestCases.v4
-rw-r--r--src/Rewriter/Arith.v40
-rw-r--r--src/Rewriter/ArithWithCasts.v37
-rw-r--r--src/Rewriter/NBE.v50
-rw-r--r--src/Rewriter/StripLiteralCasts.v37
-rw-r--r--src/Rewriter/ToFancy.v45
-rw-r--r--src/Rewriter/ToFancyWithCasts.v47
-rw-r--r--src/RewriterFull.v49
-rw-r--r--src/RewriterProofs.v206
-rw-r--r--src/RewriterProofsTactics.v107
-rw-r--r--src/RewriterRulesGood.v42
-rw-r--r--src/RewriterRulesInterpGood.v42
-rw-r--r--src/RewriterWf1.v10
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.