Automate more of the rewriter reification, proof

Now we actually make use of the rewrite-rule-specific proofs, rather
than duplicating them inline.

We now support reifying `ident.gets_inlined` to
`SubstVarLike.is_var_fst_snd_pair_opp_cast`.

We also now fix a bug where we previously incorrectly substituted
context variables when reifying side conditions (needed for correct
reification of split-mul things, coming up soon).

Things are unfortunately a bit slow.

I'm not sure what's up with my proof of
`reflect_ident_iota_interp_related`; it seems more complicated than it
should be (maybe partly due to funext concerns).

Next up is to split out the rewrite rule generation bits into separate
files and have a single tactic that builds the entire package for us (in
prep for making the rewriter builder a vernacular).  After that I want
to more fully parameterize things over `ident`, and then also over the
non-container base-types (which will require some reworking of how we
handle special identifiers).  Additionally, I want to make the rewrite
rule definitions not depend on Language.v.

After     | File Name                                       | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------
20m50.18s | Total                                           | 23m01.24s || -2m11.06s | -9.48%
-----------------------------------------------------------------------------------------------
0m27.24s  | RewriterRulesGood.vo                            | 1m34.94s  || -1m07.70s | -71.30%
0m54.89s  | RewriterRulesInterpGood.vo                      | 1m57.72s  || -1m02.82s | -53.37%
1m37.88s  | RewriterWf2.vo                                  | 1m47.69s  || -0m09.81s | -9.10%
1m16.71s  | Rewriter.vo                                     | 1m12.61s  || +0m04.10s | +5.64%
0m37.14s  | ExtractionHaskell/unsaturated_solinas           | 0m40.06s  || -0m02.92s | -7.28%
0m36.10s  | RewriterWf1.vo                                  | 0m33.12s  || +0m02.98s | +8.99%
0m18.31s  | p256_32.c                                       | 0m20.70s  || -0m02.39s | -11.54%
1m43.31s  | Fancy/Barrett256.vo                             | 1m42.09s  || +0m01.21s | +1.19%
0m32.46s  | ExtractionHaskell/saturated_solinas             | 0m30.92s  || +0m01.53s | +4.98%
0m23.44s  | ExtractionOCaml/word_by_word_montgomery         | 0m22.26s  || +0m01.17s | +5.30%
0m12.17s  | ExtractionOCaml/word_by_word_montgomery.ml      | 0m13.58s  || -0m01.41s | -10.38%
0m10.04s  | p224_32.c                                       | 0m08.20s  || +0m01.83s | +22.43%
0m09.98s  | ExtractionOCaml/saturated_solinas               | 0m11.67s  || -0m01.68s | -14.48%
0m07.80s  | ExtractionOCaml/saturated_solinas.ml            | 0m06.16s  || +0m01.63s | +26.62%
0m06.87s  | ExtractionHaskell/saturated_solinas.hs          | 0m04.98s  || +0m01.88s | +37.95%
3m23.11s  | p384_32.c                                       | 3m22.61s  || +0m00.50s | +0.24%
0m59.32s  | ExtractionHaskell/word_by_word_montgomery       | 0m58.76s  || +0m00.56s | +0.95%
0m46.19s  | p521_32.c                                       | 0m47.16s  || -0m00.96s | -2.05%
0m45.26s  | RewriterInterpProofs1.vo                        | 0m45.64s  || -0m00.38s | -0.83%
0m39.50s  | p521_64.c                                       | 0m38.97s  || +0m00.53s | +1.36%
0m36.38s  | PushButtonSynthesis/UnsaturatedSolinas.vo       | 0m36.00s  || +0m00.38s | +1.05%
0m34.40s  | Fancy/Montgomery256.vo                          | 0m34.63s  || -0m00.23s | -0.66%
0m26.95s  | PushButtonSynthesis/WordByWordMontgomery.vo     | 0m26.44s  || +0m00.50s | +1.92%
0m25.62s  | SlowPrimeSynthesisExamples.vo                   | 0m26.04s  || -0m00.41s | -1.61%
0m24.39s  | RewriterRulesProofs.vo                          | 0m24.18s  || +0m00.21s | +0.86%
0m20.49s  | PushButtonSynthesis/BarrettReduction.vo         | 0m20.62s  || -0m00.13s | -0.63%
0m18.54s  | p448_solinas_64.c                               | 0m19.15s  || -0m00.60s | -3.18%
0m17.37s  | secp256k1_32.c                                  | 0m17.70s  || -0m00.32s | -1.86%
0m14.80s  | p434_64.c                                       | 0m14.16s  || +0m00.64s | +4.51%
0m14.05s  | ExtractionOCaml/unsaturated_solinas             | 0m14.28s  || -0m00.22s | -1.61%
0m09.17s  | ExtractionOCaml/unsaturated_solinas.ml          | 0m09.58s  || -0m00.41s | -4.27%
0m08.47s  | ExtractionHaskell/word_by_word_montgomery.hs    | 0m08.22s  || +0m00.25s | +3.04%
0m07.69s  | p384_64.c                                       | 0m07.72s  || -0m00.02s | -0.38%
0m06.80s  | BoundsPipeline.vo                               | 0m06.65s  || +0m00.14s | +2.25%
0m06.49s  | ExtractionHaskell/unsaturated_solinas.hs        | 0m05.59s  || +0m00.90s | +16.10%
0m03.54s  | PushButtonSynthesis/Primitives.vo               | 0m03.46s  || +0m00.08s | +2.31%
0m03.35s  | PushButtonSynthesis/SmallExamples.vo            | 0m03.36s  || -0m00.00s | -0.29%
0m03.19s  | PushButtonSynthesis/SaturatedSolinas.vo         | 0m03.15s  || +0m00.04s | +1.26%
0m02.79s  | curve25519_32.c                                 | 0m03.32s  || -0m00.52s | -15.96%
0m02.66s  | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.73s  || -0m00.06s | -2.56%
0m02.55s  | RewriterRules.vo                                | 0m02.52s  || +0m00.02s | +1.19%
0m01.98s  | curve25519_64.c                                 | 0m01.57s  || +0m00.40s | +26.11%
0m01.78s  | p224_64.c                                       | 0m01.30s  || +0m00.48s | +36.92%
0m01.60s  | secp256k1_64.c                                  | 0m01.74s  || -0m00.13s | -8.04%
0m01.45s  | p256_64.c                                       | 0m01.55s  || -0m00.10s | -6.45%
0m01.34s  | RewriterProofs.vo                               | 0m01.16s  || +0m00.18s | +15.51%
0m01.33s  | CLI.vo                                          | 0m01.40s  || -0m00.06s | -4.99%
0m01.12s  | StandaloneOCamlMain.vo                          | 0m01.09s  || +0m00.03s | +2.75%
0m01.10s  | CompilersTestCases.vo                           | 0m01.08s  || +0m00.02s | +1.85%
0m01.08s  | StandaloneHaskellMain.vo                        | 0m01.02s  || +0m00.06s | +5.88%

1 files changed, 38 insertions, 26 deletions

diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v
index 0587aec51..6da5a9e47 100644
--- a/src/RewriterProofs.v
+++ b/src/RewriterProofs.v
@@ -13,6 +13,7 @@ Require Import Crypto.Rewriter.
 Require Import Crypto.RewriterWf1.
 Require Import Crypto.RewriterWf2.
 Require Import Crypto.RewriterInterpProofs1.
+Require Import Crypto.RewriterRulesProofs.
 Require Import Crypto.RewriterRulesGood.
 Require Import Crypto.RewriterRulesInterpGood.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -54,14 +55,25 @@ Module Compilers.
 
   Module Import RewriteRules.
 
-    Local Ltac start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
+    Local Ltac start_Wf_or_interp_proof Rewrite_folded :=
       let Rewrite := lazymatch goal with
                      | [ |- Wf ?e ] => head e
                      | [ |- expr.Interp _ ?e == _ ] => head e
                      end in
-      cbv [Rewrite]; rewrite rewrite_head_eq; cbv [rewrite_head0]; rewrite all_rewrite_rules_eq.
-    Local Ltac start_Wf_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
-      start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0;
+      progress change Rewrite with Rewrite_folded; cbv [Rewrite_folded];
+      let data := lazymatch goal with |- context[Make.Rewrite ?data] => data end in
+      let data_head := head data in
+      cbv [Make.Rewrite];
+      rewrite (rewrite_head_eq data);
+      let lem := fresh in
+      pose proof (all_rewrite_rules_eq data) as lem;
+      cbv [data_head rewrite_head0 default_fuel all_rewrite_rules rewrite_rules];
+      unfold data_head at 1 in lem;
+      cbv [all_rewrite_rules] in lem;
+      let h := lazymatch goal with |- context[Compile.Rewrite ?rewrite_head] => head rewrite_head end in
+      cbv [h]; rewrite lem; clear lem.
+    Local Ltac start_Wf_proof Rewrite_folded :=
+      start_Wf_or_interp_proof Rewrite_folded;
       apply Compile.Wf_Rewrite; [ | assumption ];
       let wf_do_again := fresh "wf_do_again" in
       (intros ? ? ? ? wf_do_again ? ?);
@@ -70,8 +82,8 @@ Module Compilers.
             pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct
         with nocore;
       try reflexivity.
-    Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
-      start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0;
+    Local Ltac start_Interp_proof Rewrite_folded :=
+      start_Wf_or_interp_proof Rewrite_folded;
       eapply Compile.InterpRewrite; [ | assumption ];
       intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed);
       eauto using
@@ -81,22 +93,22 @@ Module Compilers.
 
     Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e).
     Proof.
-      start_Wf_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0).
+      start_Wf_proof RewriteNBE_folded.
       apply nbe_rewrite_rules_good.
     Qed.
     Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e).
     Proof.
-      start_Wf_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0).
+      start_Wf_proof RewriteArith_folded.
       apply arith_rewrite_rules_good.
     Qed.
     Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e).
     Proof.
-      start_Wf_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0).
+      start_Wf_proof RewriteArithWithCasts_folded.
       apply arith_with_casts_rewrite_rules_good.
     Qed.
     Lemma Wf_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Wf (@RewriteStripLiteralCasts t e).
     Proof.
-      start_Wf_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0).
+      start_Wf_proof RewriteStripLiteralCasts_folded.
       apply strip_literal_casts_rewrite_rules_good.
     Qed.
     Lemma Wf_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z)
@@ -104,8 +116,8 @@ Module Compilers.
             (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.
-      start_Wf_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0).
-      eapply fancy_rewrite_rules_good; eassumption.
+      start_Wf_proof RewriteToFancy_folded.
+      apply fancy_rewrite_rules_good; assumption.
     Qed.
 
     Lemma Wf_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z)
@@ -114,39 +126,39 @@ Module Compilers.
             (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.
-      start_Wf_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0).
-      eapply fancy_with_casts_rewrite_rules_good; eassumption.
+      start_Wf_proof RewriteToFancyWithCasts_folded.
+      apply fancy_with_casts_rewrite_rules_good; assumption.
     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.
-      start_Interp_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0).
-      apply nbe_rewrite_rules_interp_good.
+      start_Interp_proof RewriteNBE_folded.
+      apply nbe_rewrite_rules_interp_good, nbe_rewrite_rules_proofs.
     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.
-      start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0).
-      apply arith_rewrite_rules_interp_good.
+      start_Interp_proof RewriteArith_folded.
+      apply arith_rewrite_rules_interp_good, arith_rewrite_rules_proofs.
     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.
-      start_Interp_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0).
-      apply arith_with_casts_rewrite_rules_interp_good.
+      start_Interp_proof RewriteArithWithCasts_folded.
+      apply arith_with_casts_rewrite_rules_interp_good, arith_with_casts_rewrite_rules_proofs.
     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.
-      start_Interp_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0).
-      apply strip_literal_casts_rewrite_rules_interp_good.
+      start_Interp_proof RewriteStripLiteralCasts_folded.
+      apply strip_literal_casts_rewrite_rules_interp_good, strip_literal_casts_rewrite_rules_proofs.
     Qed.
 
     Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z)
@@ -156,8 +168,8 @@ Module Compilers.
       : 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.
-      start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0).
-      eapply fancy_rewrite_rules_interp_good; eassumption.
+      start_Interp_proof RewriteToFancy_folded.
+      apply fancy_rewrite_rules_interp_good; try assumption; apply fancy_rewrite_rules_proofs; assumption.
     Qed.
 
     Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z)
@@ -168,8 +180,8 @@ Module Compilers.
       : 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.
-      start_Interp_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0).
-      eapply fancy_with_casts_rewrite_rules_interp_good; eassumption.
+      start_Interp_proof RewriteToFancyWithCasts_folded.
+      apply fancy_with_casts_rewrite_rules_interp_good; try assumption; apply fancy_with_casts_rewrite_rules_proofs; assumption.
     Qed.
 
     Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e.