Add a rewrite rule to collapse constant casts

If, e.g., we know from bounds analysis that the result of an operation
fits in the range r[0~>0], we now just replace it with the literal
constant.

Fixes #493

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
21m22.14s | Total                                        | 21m22.79s || -0m00.65s | -0.05%
--------------------------------------------------------------------------------------------
4m09.97s  | PushButtonSynthesis.vo                       | 4m10.56s  || -0m00.59s | -0.23%
3m09.12s  | p384_32.c                                    | 3m08.91s  || +0m00.21s | +0.11%
2m05.94s  | Rewriter.vo                                  | 2m06.30s  || -0m00.35s | -0.28%
1m56.58s  | RewriterWf2.vo                               | 1m56.09s  || +0m00.48s | +0.42%
1m52.39s  | RewriterRulesGood.vo                         | 1m52.04s  || +0m00.35s | +0.31%
1m46.01s  | RewriterRulesInterpGood.vo                   | 1m45.79s  || +0m00.21s | +0.20%
0m46.44s  | RewriterInterpProofs1.vo                     | 0m46.47s  || -0m00.03s | -0.06%
0m44.96s  | ExtractionHaskell/word_by_word_montgomery    | 0m45.59s  || -0m00.63s | -1.38%
0m39.18s  | p521_32.c                                    | 0m39.33s  || -0m00.14s | -0.38%
0m32.41s  | p521_64.c                                    | 0m32.54s  || -0m00.13s | -0.39%
0m30.87s  | ExtractionHaskell/unsaturated_solinas        | 0m30.67s  || +0m00.19s | +0.65%
0m24.32s  | ExtractionHaskell/saturated_solinas          | 0m24.44s  || -0m00.12s | -0.49%
0m23.59s  | RewriterWf1.vo                               | 0m24.10s  || -0m00.51s | -2.11%
0m17.01s  | ExtractionOCaml/word_by_word_montgomery      | 0m17.14s  || -0m00.12s | -0.75%
0m13.48s  | secp256k1_32.c                               | 0m13.30s  || +0m00.17s | +1.35%
0m13.11s  | p256_32.c                                    | 0m13.37s  || -0m00.25s | -1.94%
0m11.34s  | p484_64.c                                    | 0m11.34s  || +0m00.00s | +0.00%
0m10.78s  | ExtractionOCaml/unsaturated_solinas          | 0m10.79s  || -0m00.00s | -0.09%
0m10.27s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m10.06s  || +0m00.20s | +2.08%
0m08.11s  | ExtractionOCaml/saturated_solinas            | 0m07.92s  || +0m00.18s | +2.39%
0m06.92s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m07.02s  || -0m00.09s | -1.42%
0m06.18s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s  || -0m00.10s | -1.59%
0m06.13s  | BoundsPipeline.vo                            | 0m05.98s  || +0m00.14s | +2.50%
0m05.90s  | p224_32.c                                    | 0m05.92s  || -0m00.01s | -0.33%
0m05.29s  | p384_64.c                                    | 0m05.33s  || -0m00.04s | -0.75%
0m05.17s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.20s  || -0m00.03s | -0.57%
0m04.91s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m04.93s  || -0m00.01s | -0.40%
0m04.06s  | ExtractionHaskell/saturated_solinas.hs       | 0m04.00s  || +0m00.05s | +1.49%
0m02.21s  | curve25519_32.c                              | 0m02.22s  || -0m00.01s | -0.45%
0m01.52s  | curve25519_64.c                              | 0m01.50s  || +0m00.02s | +1.33%
0m01.38s  | CLI.vo                                       | 0m01.42s  || -0m00.04s | -2.81%
0m01.14s  | RewriterProofs.vo                            | 0m01.13s  || +0m00.01s | +0.88%
0m01.14s  | StandaloneOCamlMain.vo                       | 0m00.96s  || +0m00.17s | +18.74%
0m01.12s  | StandaloneHaskellMain.vo                     | 0m01.03s  || +0m00.09s | +8.73%
0m01.12s  | secp256k1_64.c                               | 0m01.00s  || +0m00.12s | +12.00%
0m01.05s  | p256_64.c                                    | 0m00.98s  || +0m00.07s | +7.14%
0m01.03s  | p224_64.c                                    | 0m01.15s  || -0m00.11s | -10.43%

1 files changed, 21 insertions, 9 deletions

diff --git a/src/PushButtonSynthesis.v b/src/PushButtonSynthesis.v
index 0c7f0c994..e20904f63 100644
--- a/src/PushButtonSynthesis.v
+++ b/src/PushButtonSynthesis.v
@@ -212,11 +212,13 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
     Definition saturated_bounds : ZRange.type.option.interp (base.type.list (base.type.Z))
       := Some saturated_bounds_list.
 
+    (* We include [0], so that even after bounds relaxation, we can
+       notice where the constant 0s are, and remove them. *)
     Definition possible_values_of_machine_wordsize
-      := [machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; machine_wordsize; 2 * machine_wordsize]%Z.
 
     Definition possible_values_of_machine_wordsize_with_bytes
-      := [1; 8; machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z.
 
     Let possible_values := possible_values_of_machine_wordsize.
     Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes.
@@ -600,11 +602,13 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
     Definition m_enc : list Z
       := encode (weight (Qnum limbwidth) (Qden limbwidth)) n s c m.
 
+    (* We include [0], so that even after bounds relaxation, we can
+       notice where the constant 0s are, and remove them. *)
     Definition possible_values_of_machine_wordsize
-      := [machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; machine_wordsize; 2 * machine_wordsize]%Z.
 
     Definition possible_values_of_machine_wordsize_with_bytes
-      := [1; 8; machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z.
 
     Let possible_values := possible_values_of_machine_wordsize.
     Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes.
@@ -1131,8 +1135,10 @@ Module SaturatedSolinas.
             (c : list (Z * Z))
             (machine_wordsize : Z).
 
+    (* We include [0], so that even after bounds relaxation, we can
+       notice where the constant 0s are, and remove them. *)
     Definition possible_values_of_machine_wordsize
-      := [1; machine_wordsize]%Z.
+      := [0; 1; machine_wordsize]%Z.
 
     Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)).
     Let m := s - Associational.eval c.
@@ -1518,11 +1524,13 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
     Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize).
     Local Notation saturated_bounds := (saturated_bounds n machine_wordsize).
 
+    (* We include [0], so that even after bounds relaxation, we can
+       notice where the constant 0s are, and remove them. *)
     Definition possible_values_of_machine_wordsize
-      := [1; machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; 1; machine_wordsize; 2 * machine_wordsize]%Z.
 
     Definition possible_values_of_machine_wordsize_with_bytes
-      := [1; 8; machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z.
 
     Let possible_values := possible_values_of_machine_wordsize.
     Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes.
@@ -2825,8 +2833,10 @@ Module BarrettReduction.
     Let muLow := mu mod (2 ^ machine_wordsize).
     Let consts_list := [M; muLow].
 
+    (* We include [0], so that even after bounds relaxation, we can
+       notice where the constant 0s are, and remove them. *)
     Definition possible_values_of_machine_wordsize
-      := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; 1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z.
     Let possible_values := possible_values_of_machine_wordsize.
 
     Definition check_args {T} (res : Pipeline.ErrorT T)
@@ -3026,8 +3036,10 @@ Module MontgomeryReduction.
     Let bound := Some value_range.
     Let consts_list := [N; N'].
 
+    (* We include [0], so that even after bounds relaxation, we can
+       notice where the constant 0s are, and remove them. *)
     Definition possible_values_of_machine_wordsize
-      := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z.
+      := [0; 1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z.
     Local Arguments possible_values_of_machine_wordsize / .
 
     Let possible_values := possible_values_of_machine_wordsize.