Split up rewrite rules proofs into multiple files

This may help with travis timing, and should help with local build-times
too, a bit.

After     | File Name                                                            | Before    || Change     | % Change
---------------------------------------------------------------------------------------------------------------------
27m47.33s | Total                                                                | 27m47.30s || +0m00.02s  | +0.00%
---------------------------------------------------------------------------------------------------------------------
0m00.96s  | Experiments/NewPipeline/RewriterProofs                               | 10m55.28s || -10m54.31s | -99.85%
9m36.19s  | Experiments/NewPipeline/RewriterRulesGood                            |    N/A    || +9m36.19s  | ∞
1m12.65s  | Experiments/NewPipeline/RewriterWf2                                  |    N/A    || +1m12.65s  | ∞
0m04.35s  | Experiments/NewPipeline/RewriterWf1                                  |    N/A    || +0m04.34s  | ∞
5m55.46s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m55.87s  || -0m00.41s  | -0.11%
4m32.42s  | Experiments/NewPipeline/Toplevel1                                    | 4m31.54s  || +0m00.87s  | +0.32%
1m38.81s  | Experiments/NewPipeline/Toplevel2                                    | 1m39.00s  || -0m00.18s  | -0.19%
0m38.16s  | p521_32.c                                                            | 0m38.11s  || +0m00.04s  | +0.13%
0m37.22s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.41s  || -0m00.18s  | -0.50%
0m34.44s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.37s  || +0m00.07s  | +0.20%
0m31.84s  | p521_64.c                                                            | 0m31.70s  || +0m00.14s  | +0.44%
0m21.46s  | p384_32.c                                                            | 0m21.46s  || +0m00.00s  | +0.00%
0m21.02s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.67s  || +0m00.34s  | +1.69%
0m18.81s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.92s  || -0m00.11s  | -0.58%
0m13.83s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.95s  || -0m00.11s  | -0.86%
0m10.56s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.55s  || +0m00.00s  | +0.09%
0m08.57s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.51s  || +0m00.06s  | +0.70%
0m08.14s  | p384_64.c                                                            | 0m08.14s  || +0m00.00s  | +0.00%
0m05.53s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.49s  || +0m00.04s  | +0.72%
0m05.46s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.34s  || +0m00.12s  | +2.24%
0m04.05s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.06s  || -0m00.00s  | -0.24%
0m03.88s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.84s  || +0m00.04s  | +1.04%
0m03.40s  | secp256k1_32.c                                                       | 0m03.22s  || +0m00.17s  | +5.59%
0m03.31s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.34s  || -0m00.02s  | -0.89%
0m03.24s  | p256_32.c                                                            | 0m03.20s  || +0m00.04s  | +1.25%
0m02.09s  | curve25519_32.c                                                      | 0m01.95s  || +0m00.13s  | +7.17%
0m01.91s  | p224_32.c                                                            | 0m01.92s  || -0m00.01s  | -0.52%
0m01.57s  | p224_64.c                                                            | 0m01.42s  || +0m00.15s  | +10.56%
0m01.44s  | p256_64.c                                                            | 0m01.41s  || +0m00.03s  | +2.12%
0m01.39s  | Experiments/NewPipeline/CLI                                          | 0m01.42s  || -0m00.03s  | -2.11%
0m01.38s  | secp256k1_64.c                                                       | 0m01.38s  || +0m00.00s  | +0.00%
0m01.33s  | curve25519_64.c                                                      | 0m01.34s  || -0m00.01s  | -0.74%
0m01.26s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.26s  || +0m00.00s  | +0.00%
0m01.20s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.24s  || -0m00.04s  | -3.22%

1 files changed, 207 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
new file mode 100644
index 000000000..03502fb9c
--- /dev/null
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -0,0 +1,207 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.MSets.MSetPositive.
+Require Import Coq.FSets.FMapPositive.
+Require Import Crypto.Experiments.NewPipeline.Language.
+Require Import Crypto.Experiments.NewPipeline.LanguageInversion.
+Require Import Crypto.Experiments.NewPipeline.LanguageWf.
+Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs.
+Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs.
+Require Import Crypto.Experiments.NewPipeline.Rewriter.
+Require Import Crypto.Experiments.NewPipeline.RewriterWf1.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.SpecializeAllWays.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.CPSNotations.
+Require Import Crypto.Util.HProp.
+Require Import Crypto.Util.Decidable.
+Import ListNotations. Local Open Scope list_scope.
+Local Open Scope Z_scope.
+
+Import EqNotations.
+Module Compilers.
+  Import Language.Compilers.
+  Import LanguageInversion.Compilers.
+  Import LanguageWf.Compilers.
+  Import UnderLetsProofs.Compilers.
+  Import GENERATEDIdentifiersWithoutTypesProofs.Compilers.
+  Import Rewriter.Compilers.
+  Import RewriterWf1.Compilers.
+  Import expr.Notations.
+  Import RewriterWf1.Compilers.RewriteRules.
+  Import defaults.
+
+  Module Import RewriteRules.
+    Import Rewriter.Compilers.RewriteRules.
+
+    Lemma nbe_rewrite_head_eq : @nbe_rewrite_head = @nbe_rewrite_head0.
+    Proof. reflexivity. Qed.
+
+    Lemma fancy_rewrite_head_eq invert_low invert_high
+      : (fun var do_again => @fancy_rewrite_head invert_low invert_high var)
+        = (fun var => @fancy_rewrite_head0 var invert_low invert_high).
+    Proof. reflexivity. Qed.
+
+    Lemma arith_rewrite_head_eq max_const_val : @arith_rewrite_head max_const_val = (fun var => @arith_rewrite_head0 var max_const_val).
+    Proof. reflexivity. Qed.
+
+    Lemma nbe_all_rewrite_rules_eq : @nbe_all_rewrite_rules = @nbe_rewrite_rules.
+    Proof. reflexivity. Qed.
+
+    Lemma fancy_all_rewrite_rules_eq : @fancy_all_rewrite_rules = @fancy_rewrite_rules.
+    Proof. reflexivity. Qed.
+
+    Lemma arith_all_rewrite_rules_eq : @arith_all_rewrite_rules = @arith_rewrite_rules.
+    Proof. reflexivity. Qed.
+
+    Section good.
+      Context {var1 var2 : type -> Type}.
+
+      Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident pattern.ident.arg_types var1 var2).
+
+      Lemma rlist_rect_cps_id {var} A P {ivar} N_case C_case ls T k
+        : @rlist_rect var A P ivar N_case C_case ls T k = k (@rlist_rect var A P ivar N_case C_case ls _ id).
+      Proof.
+        cbv [rlist_rect id Compile.option_bind']; rewrite !expr.reflect_list_cps_id.
+        destruct (invert_expr.reflect_list ls) eqn:?; cbn [Option.bind Option.sequence_return]; reflexivity.
+      Qed.
+      Lemma rlist_rect_cast_cps_id {var} A A' P {ivar} N_case C_case ls T k
+        : @rlist_rect_cast var A A' P ivar N_case C_case ls T k = k (@rlist_rect_cast var A A' P ivar N_case C_case ls _ id).
+      Proof.
+        cbv [rlist_rect_cast Compile.castbe Compile.castb id Compile.option_bind']; rewrite_type_transport_correct;
+          break_innermost_match; type_beq_to_eq; subst; cbn [eq_rect Option.bind Option.sequence_return]; [ | reflexivity ].
+        apply rlist_rect_cps_id.
+      Qed.
+
+      Local Ltac start_cps_id :=
+        lazymatch goal with
+        | [ |- In _ ?rewr -> _ ] => let h := head rewr in cbv [h]
+        end;
+        cbn [In combine]; intros; destruct_head'_or; inversion_sigma; subst; try reflexivity; destruct_head' False.
+
+      Local Ltac cps_id_step :=
+        first [ reflexivity
+              | progress destruct_head' False
+              | progress subst
+              | progress inversion_option
+              | progress cbv [id Compile.binding_dataT pattern.ident.arg_types Compile.ptype_interp Compile.ptype_interp_cps Compile.pbase_type_interp_cps Compile.value Compile.value' Compile.app_binding_data Compile.app_ptype_interp_cps Compile.app_pbase_type_interp_cps Compile.lift_with_bindings Compile.lift_ptype_interp_cps Compile.lift_pbase_type_interp_cps cpsbind cpscall cpsreturn cps_option_bind type_base rwhen] in *
+              | progress cbn [UnderLets.splice eq_rect projT1 projT2 Option.bind Option.sequence Option.sequence_return] in *
+              | progress type_beq_to_eq
+              | progress rewrite_type_transport_correct
+              | progress cbv [Compile.option_bind' Compile.castbe Compile.castb Compile.castv] in *
+              | progress break_innermost_match
+              | progress destruct_head'_sigT
+              | rewrite !expr.reflect_list_cps_id
+              | match goal with
+                | [ |- context[@rlist_rect_cast ?var ?A ?A' ?P ?ivar ?N_case ?C_case ?ls ?T ?k] ]
+                  => (tryif (let __ := constr:(eq_refl : k = (fun x => x)) in idtac)
+                       then fail
+                       else rewrite (@rlist_rect_cast_cps_id var A A' P ivar N_case C_case ls T k))
+                | [ |- context[@rlist_rect ?var ?A ?P ?ivar ?N_case ?C_case ?ls ?T ?k] ]
+                  => (tryif (let __ := constr:(eq_refl : k = (fun x => x)) in idtac)
+                       then fail
+                       else rewrite (@rlist_rect_cps_id var A P ivar N_case C_case ls T k))
+                end
+              | progress cbv [Option.bind] in *
+              | break_match_step ltac:(fun _ => idtac) ].
+
+      Local Ltac cps_id_t := start_cps_id; repeat cps_id_step.
+
+      Lemma nbe_cps_id {var} p r
+        : In (existT _ p r) (@nbe_rewrite_rules var)
+          -> forall v T k, r v T k = k (r v _ id).
+      Proof. cps_id_t. Qed.
+
+      Lemma arith_cps_id max_const {var} p r
+        : In (existT _ p r) (@arith_rewrite_rules var max_const)
+          -> forall v T k, r v T k = k (r v _ id).
+      Proof. cps_id_t. Qed.
+
+      Lemma fancy_cps_id invert_low invert_high {var} p r
+        : In (existT _ p r) (@fancy_rewrite_rules var invert_low invert_high)
+          -> forall v T k, r v T k = k (r v _ id).
+      Proof. cps_id_t. Qed.
+
+      Local Ltac start_good cps_id rewrite_rules :=
+        split; [ reflexivity | ];
+          repeat apply conj; try solve [ eapply cps_id ]; [];
+            cbv [rewrite_rules]; cbn [In combine];
+              intros; destruct_head'_or; inversion_prod; inversion_sigma; subst; destruct_head' False;
+              (split; [ reflexivity | ]).
+
+      Local Ltac good_t_step :=
+        first [ progress subst
+              | progress cbv [id Compile.binding_dataT pattern.ident.arg_types Compile.ptype_interp Compile.ptype_interp_cps Compile.pbase_type_interp_cps Compile.value Compile.value' Compile.app_binding_data Compile.app_ptype_interp_cps Compile.app_pbase_type_interp_cps Compile.lift_with_bindings Compile.lift_ptype_interp_cps Compile.lift_pbase_type_interp_cps cpsbind cpscall cpsreturn cps_option_bind type_base Compile.wf_binding_dataT Compile.wf_ptype_interp_id Compile.wf_ptype_interp_cps Compile.wf_pbase_type_interp_cps ident.smart_Literal rwhen AnyExpr.unwrap] in *
+              | progress destruct_head'_sig
+              | progress cbn [eq_rect option_eq projT1 projT2 fst snd base.interp In combine Option.bind Option.sequence Option.sequence_return UnderLets.splice] in *
+              | progress destruct_head'_prod
+              | progress destruct_head'_sigT
+              | progress intros
+              | progress eliminate_hprop_eq
+              | progress cbv [Compile.option_bind' Compile.castbe Compile.castb Compile.castv] in *
+              | progress type_beq_to_eq
+              | progress rewrite_type_transport_correct
+              | break_innermost_match_step
+              | wf_safe_t_step
+              | rewrite !expr.reflect_list_cps_id
+              | congruence
+              | match goal with
+                | [ |- expr.wf _ (reify_list _) (reify_list _) ] => rewrite expr.wf_reify_list
+                | [ |- context[length ?ls] ] => tryif is_var ls then fail else (progress autorewrite with distr_length)
+                | [ |- ex _ ] => eexists
+                | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice
+                | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor
+                | [ H : Compile.wf_value ?G ?e1 ?e2 |- UnderLets.wf _ ?G (?e1 _) (?e2 _) ] => eapply (H nil)
+                | [ H : Compile.wf_value ?G ?e1 ?e2 |- UnderLets.wf _ ?G (?e1 _ _) (?e2 _ _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | ] ]; revgoals
+                | [ |- context[@rlist_rect_cast ?var ?A ?A' ?P ?ivar ?N_case ?C_case ?ls ?T ?k] ]
+                  => (tryif (let __ := constr:(eq_refl : k = (fun x => x)) in idtac)
+                       then fail
+                       else rewrite (@rlist_rect_cast_cps_id var A A' P ivar N_case C_case ls T k))
+                | [ |- context[@rlist_rect ?var ?A ?P ?ivar ?N_case ?C_case ?ls ?T ?k] ]
+                  => (tryif (let __ := constr:(eq_refl : k = (fun x => x)) in idtac)
+                       then fail
+                       else rewrite (@rlist_rect_cps_id var A P ivar N_case C_case ls T k))
+                | [ |- ?x = ?x /\ _ ] => split; [ reflexivity | ]
+                end
+              | solve [ wf_t ]
+(*| progress cbv [Option.bind]
+                          | break_match_step ltac:(fun _ => idtac)*) ].
+
+      Lemma nbe_rewrite_rules_good
+        : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules.
+      Proof.
+        start_good (@nbe_cps_id) (@nbe_rewrite_rules).
+        all: repeat good_t_step.
+      Admitted.
+
+      Lemma arith_rewrite_rules_good max_const
+        : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const).
+      Proof.
+        start_good (@arith_cps_id) (@arith_rewrite_rules).
+        all: repeat good_t_step.
+      Admitted.
+
+      Lemma fancy_rewrite_rules_good
+            (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))
+        : rewrite_rules_goodT (fancy_rewrite_rules invert_low invert_high) (fancy_rewrite_rules invert_low invert_high).
+      Proof.
+        start_good (@fancy_cps_id) (@fancy_rewrite_rules).
+        all: repeat good_t_step.
+        all: cbv [Option.bind].
+        all: repeat good_t_step.
+      Qed.
+    End good.
+  End RewriteRules.
+End Compilers.