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%

1 files changed, 18 insertions, 188 deletions

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