Insert casts before literals during bounds analysis

Unless we explicitly say not to.  The ability to explicitly say not to
is required for, e.g., eta-expansion where we want to replace variable
lists of known length with with cons cells indexing into the variable
list, but don't want to pollute the code with casts.

Uniformity in this way allows rewrite rules to not blow up exponentially
(in the number of wildcards); we previously required a separate rewrite
rule for each way of choosing between wildcard and literal.

To preserve output of the pipeline, we add another pass that just strips
the casts off of literals at the end.

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
20m27.24s | Total                                        | 22m39.70s || -2m12.46s | -9.74%
--------------------------------------------------------------------------------------------
0m44.27s  | Rewriter.vo                                  | 2m11.58s  || -1m27.31s | -66.35%
1m15.23s  | RewriterRulesInterpGood.vo                   | 1m50.28s  || -0m35.04s | -31.78%
1m40.19s  | RewriterRulesGood.vo                         | 1m58.05s  || -0m17.85s | -15.12%
0m26.99s  | AbstractInterpretationProofs.vo              | 0m16.91s  || +0m10.07s | +59.60%
3m15.98s  | p384_32.c                                    | 3m07.78s  || +0m08.19s | +4.36%
0m42.52s  | ExtractionHaskell/word_by_word_montgomery    | 0m44.60s  || -0m02.07s | -4.66%
0m28.63s  | ExtractionHaskell/unsaturated_solinas        | 0m31.38s  || -0m02.75s | -8.76%
0m21.76s  | ExtractionHaskell/saturated_solinas          | 0m24.56s  || -0m02.79s | -11.40%
0m09.87s  | ExtractionOCaml/unsaturated_solinas          | 0m11.28s  || -0m01.41s | -12.50%
1m59.22s  | RewriterWf2.vo                               | 2m00.09s  || -0m00.87s | -0.72%
1m07.03s  | Fancy/Montgomery256.vo                       | 1m07.31s  || -0m00.28s | -0.41%
0m52.60s  | Fancy/Barrett256.vo                          | 0m53.16s  || -0m00.55s | -1.05%
0m48.17s  | RewriterInterpProofs1.vo                     | 0m48.72s  || -0m00.54s | -1.12%
0m40.16s  | AbstractInterpretationWf.vo                  | 0m40.23s  || -0m00.07s | -0.17%
0m38.35s  | p521_32.c                                    | 0m38.26s  || +0m00.09s | +0.23%
0m31.56s  | p521_64.c                                    | 0m31.53s  || +0m00.02s | +0.09%
0m24.64s  | RewriterWf1.vo                               | 0m24.01s  || +0m00.62s | +2.62%
0m23.54s  | AbstractInterpretationZRangeProofs.vo        | 0m23.64s  || -0m00.10s | -0.42%
0m23.48s  | PushButtonSynthesis/WordByWordMontgomery.vo  | 0m23.26s  || +0m00.21s | +0.94%
0m20.92s  | SlowPrimeSynthesisExamples.vo                | 0m20.62s  || +0m00.30s | +1.45%
0m19.92s  | PushButtonSynthesis/UnsaturatedSolinas.vo    | 0m19.80s  || +0m00.12s | +0.60%
0m16.60s  | ExtractionOCaml/word_by_word_montgomery      | 0m17.56s  || -0m00.95s | -5.46%
0m14.72s  | p448_solinas_64.c                            | 0m14.66s  || +0m00.06s | +0.40%
0m13.70s  | secp256k1_32.c                               | 0m13.45s  || +0m00.25s | +1.85%
0m13.68s  | p256_32.c                                    | 0m13.33s  || +0m00.34s | +2.62%
0m13.28s  | CStringification.vo                          | 0m13.26s  || +0m00.01s | +0.15%
0m11.88s  | p484_64.c                                    | 0m11.74s  || +0m00.14s | +1.19%
0m09.96s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m10.24s  || -0m00.27s | -2.73%
0m07.47s  | ExtractionOCaml/saturated_solinas            | 0m07.93s  || -0m00.46s | -5.80%
0m06.78s  | BoundsPipeline.vo                            | 0m05.96s  || +0m00.82s | +13.75%
0m06.72s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m07.03s  || -0m00.31s | -4.40%
0m06.38s  | p224_32.c                                    | 0m06.54s  || -0m00.16s | -2.44%
0m06.21s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s  || -0m00.12s | -2.05%
0m05.45s  | p384_64.c                                    | 0m05.18s  || +0m00.27s | +5.21%
0m04.82s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m04.84s  || -0m00.01s | -0.41%
0m04.80s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.07s  || -0m00.27s | -5.32%
0m03.83s  | ExtractionHaskell/saturated_solinas.hs       | 0m04.07s  || -0m00.24s | -5.89%
0m03.30s  | PushButtonSynthesis/Primitives.vo            | 0m03.31s  || -0m00.01s | -0.30%
0m03.26s  | PushButtonSynthesis/SmallExamples.vo         | 0m03.24s  || +0m00.01s | +0.61%
0m03.08s  | PushButtonSynthesis/SaturatedSolinas.vo      | 0m02.96s  || +0m00.12s | +4.05%
0m02.16s  | curve25519_32.c                              | 0m02.16s  || +0m00.00s | +0.00%
0m01.57s  | curve25519_64.c                              | 0m01.47s  || +0m00.10s | +6.80%
0m01.40s  | CLI.vo                                       | 0m01.32s  || +0m00.07s | +6.06%
0m01.27s  | PushButtonSynthesis/MontgomeryReduction.vo   | 0m01.19s  || +0m00.08s | +6.72%
0m01.26s  | StandaloneHaskellMain.vo                     | 0m01.18s  || +0m00.08s | +6.77%
0m01.22s  | PushButtonSynthesis/BarrettReduction.vo      | 0m01.29s  || -0m00.07s | -5.42%
0m01.13s  | RewriterProofs.vo                            | 0m01.10s  || +0m00.02s | +2.72%
0m01.10s  | secp256k1_64.c                               | 0m01.01s  || +0m00.09s | +8.91%
0m01.08s  | StandaloneOCamlMain.vo                       | 0m01.13s  || -0m00.04s | -4.42%
0m01.06s  | p256_64.c                                    | 0m01.02s  || +0m00.04s | +3.92%
0m01.05s  | AbstractInterpretation.vo                    | 0m01.00s  || +0m00.05s | +5.00%
0m01.00s  | CompilersTestCases.vo                        | 0m01.08s  || -0m00.08s | -7.40%
0m01.00s  | p224_64.c                                    | 0m01.00s  || +0m00.00s | +0.00%

1 files changed, 18 insertions, 2 deletions

diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v
index c18527305..e4ac4afda 100644
--- a/src/RewriterProofs.v
+++ b/src/RewriterProofs.v
@@ -94,6 +94,11 @@ Module Compilers.
       start_Wf_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_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).
+      apply strip_literal_casts_rewrite_rules_good.
+    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))
@@ -136,6 +141,14 @@ Module Compilers.
       apply arith_with_casts_rewrite_rules_interp_good.
     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.
+    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))
@@ -167,6 +180,9 @@ Module Compilers.
     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))
@@ -193,6 +209,6 @@ Module Compilers.
     : 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_RewriteToFancyWithCasts : wf.
-  Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_gen_RewriteArithWithCasts @Interp_gen_RewriteToFancyWithCasts @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy @Interp_RewriteArithWithCasts @Interp_RewriteToFancyWithCasts : interp.
+  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.