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, 73 insertions, 75 deletions

diff --git a/curve25519_32.c b/curve25519_32.c
index 5366ec40c..508141786 100644
--- a/curve25519_32.c
+++ b/curve25519_32.c
@@ -748,43 +748,42 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) {
   uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff));
   uint8_t x82 = (uint8_t)(x80 >> 8);
   uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff));
-  fiat_25519_uint1 x84 = (fiat_25519_uint1)(x82 >> 8);
-  uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff));
-  uint32_t x86 = (x84 + x32);
-  uint32_t x87 = (x86 >> 8);
-  uint8_t x88 = (uint8_t)(x86 & UINT8_C(0xff));
-  uint32_t x89 = (x87 >> 8);
-  uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff));
-  fiat_25519_uint1 x91 = (fiat_25519_uint1)(x89 >> 8);
-  uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff));
-  uint32_t x93 = (x91 + x45);
-  uint32_t x94 = (x93 >> 8);
-  uint8_t x95 = (uint8_t)(x93 & UINT8_C(0xff));
-  uint32_t x96 = (x94 >> 8);
-  uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff));
-  uint8_t x98 = (uint8_t)(x96 >> 8);
-  uint8_t x99 = (uint8_t)(x96 & UINT8_C(0xff));
-  uint32_t x100 = (x98 + x44);
-  uint32_t x101 = (x100 >> 8);
-  uint8_t x102 = (uint8_t)(x100 & UINT8_C(0xff));
-  uint32_t x103 = (x101 >> 8);
-  uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff));
-  uint8_t x105 = (uint8_t)(x103 >> 8);
-  uint8_t x106 = (uint8_t)(x103 & UINT8_C(0xff));
-  uint32_t x107 = (x105 + x43);
-  uint32_t x108 = (x107 >> 8);
-  uint8_t x109 = (uint8_t)(x107 & UINT8_C(0xff));
-  uint32_t x110 = (x108 >> 8);
-  uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff));
-  uint8_t x112 = (uint8_t)(x110 >> 8);
-  uint8_t x113 = (uint8_t)(x110 & UINT8_C(0xff));
-  uint32_t x114 = (x112 + x42);
-  uint32_t x115 = (x114 >> 8);
-  uint8_t x116 = (uint8_t)(x114 & UINT8_C(0xff));
-  uint32_t x117 = (x115 >> 8);
-  uint8_t x118 = (uint8_t)(x115 & UINT8_C(0xff));
-  uint8_t x119 = (uint8_t)(x117 >> 8);
-  uint8_t x120 = (uint8_t)(x117 & UINT8_C(0xff));
+  uint8_t x84 = (uint8_t)(x82 & UINT8_C(0xff));
+  uint32_t x85 = (0x0 + x32);
+  uint32_t x86 = (x85 >> 8);
+  uint8_t x87 = (uint8_t)(x85 & UINT8_C(0xff));
+  uint32_t x88 = (x86 >> 8);
+  uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff));
+  fiat_25519_uint1 x90 = (fiat_25519_uint1)(x88 >> 8);
+  uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff));
+  uint32_t x92 = (x90 + x45);
+  uint32_t x93 = (x92 >> 8);
+  uint8_t x94 = (uint8_t)(x92 & UINT8_C(0xff));
+  uint32_t x95 = (x93 >> 8);
+  uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff));
+  uint8_t x97 = (uint8_t)(x95 >> 8);
+  uint8_t x98 = (uint8_t)(x95 & UINT8_C(0xff));
+  uint32_t x99 = (x97 + x44);
+  uint32_t x100 = (x99 >> 8);
+  uint8_t x101 = (uint8_t)(x99 & UINT8_C(0xff));
+  uint32_t x102 = (x100 >> 8);
+  uint8_t x103 = (uint8_t)(x100 & UINT8_C(0xff));
+  uint8_t x104 = (uint8_t)(x102 >> 8);
+  uint8_t x105 = (uint8_t)(x102 & UINT8_C(0xff));
+  uint32_t x106 = (x104 + x43);
+  uint32_t x107 = (x106 >> 8);
+  uint8_t x108 = (uint8_t)(x106 & UINT8_C(0xff));
+  uint32_t x109 = (x107 >> 8);
+  uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff));
+  uint8_t x111 = (uint8_t)(x109 >> 8);
+  uint8_t x112 = (uint8_t)(x109 & UINT8_C(0xff));
+  uint32_t x113 = (x111 + x42);
+  uint32_t x114 = (x113 >> 8);
+  uint8_t x115 = (uint8_t)(x113 & UINT8_C(0xff));
+  uint32_t x116 = (x114 >> 8);
+  uint8_t x117 = (uint8_t)(x114 & UINT8_C(0xff));
+  uint8_t x118 = (uint8_t)(x116 >> 8);
+  uint8_t x119 = (uint8_t)(x116 & UINT8_C(0xff));
   out1[0] = x51;
   out1[1] = x53;
   out1[2] = x55;
@@ -800,23 +799,23 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) {
   out1[12] = x79;
   out1[13] = x81;
   out1[14] = x83;
-  out1[15] = x85;
-  out1[16] = x88;
-  out1[17] = x90;
-  out1[18] = x92;
-  out1[19] = x95;
-  out1[20] = x97;
-  out1[21] = x99;
-  out1[22] = x102;
-  out1[23] = x104;
-  out1[24] = x106;
-  out1[25] = x109;
-  out1[26] = x111;
-  out1[27] = x113;
-  out1[28] = x116;
-  out1[29] = x118;
-  out1[30] = x120;
-  out1[31] = x119;
+  out1[15] = x84;
+  out1[16] = x87;
+  out1[17] = x89;
+  out1[18] = x91;
+  out1[19] = x94;
+  out1[20] = x96;
+  out1[21] = x98;
+  out1[22] = x101;
+  out1[23] = x103;
+  out1[24] = x105;
+  out1[25] = x108;
+  out1[26] = x110;
+  out1[27] = x112;
+  out1[28] = x115;
+  out1[29] = x117;
+  out1[30] = x119;
+  out1[31] = x118;
 }
 
 /*
@@ -880,30 +879,29 @@ static void fiat_25519_from_bytes(uint32_t out1[10], const uint8_t arg1[32]) {
   uint8_t x52 = (uint8_t)(x51 >> 25);
   uint32_t x53 = (x51 & UINT32_C(0x1ffffff));
   uint32_t x54 = (x52 + x41);
-  fiat_25519_uint1 x55 = (fiat_25519_uint1)(x54 >> 26);
-  uint32_t x56 = (x54 & UINT32_C(0x3ffffff));
-  uint32_t x57 = (x55 + x40);
-  uint8_t x58 = (uint8_t)(x57 >> 25);
-  uint32_t x59 = (x57 & UINT32_C(0x1ffffff));
-  uint32_t x60 = (x58 + x39);
-  uint8_t x61 = (uint8_t)(x60 >> 26);
-  uint32_t x62 = (x60 & UINT32_C(0x3ffffff));
-  uint32_t x63 = (x61 + x38);
-  uint8_t x64 = (uint8_t)(x63 >> 25);
-  uint32_t x65 = (x63 & UINT32_C(0x1ffffff));
-  uint32_t x66 = (x64 + x37);
-  uint8_t x67 = (uint8_t)(x66 >> 26);
-  uint32_t x68 = (x66 & UINT32_C(0x3ffffff));
-  uint32_t x69 = (x67 + x36);
+  uint32_t x55 = (x54 & UINT32_C(0x3ffffff));
+  uint32_t x56 = (0x0 + x40);
+  uint8_t x57 = (uint8_t)(x56 >> 25);
+  uint32_t x58 = (x56 & UINT32_C(0x1ffffff));
+  uint32_t x59 = (x57 + x39);
+  uint8_t x60 = (uint8_t)(x59 >> 26);
+  uint32_t x61 = (x59 & UINT32_C(0x3ffffff));
+  uint32_t x62 = (x60 + x38);
+  uint8_t x63 = (uint8_t)(x62 >> 25);
+  uint32_t x64 = (x62 & UINT32_C(0x1ffffff));
+  uint32_t x65 = (x63 + x37);
+  uint8_t x66 = (uint8_t)(x65 >> 26);
+  uint32_t x67 = (x65 & UINT32_C(0x3ffffff));
+  uint32_t x68 = (x66 + x36);
   out1[0] = x35;
   out1[1] = x47;
   out1[2] = x50;
   out1[3] = x53;
-  out1[4] = x56;
-  out1[5] = x59;
-  out1[6] = x62;
-  out1[7] = x65;
-  out1[8] = x68;
-  out1[9] = x69;
+  out1[4] = x55;
+  out1[5] = x58;
+  out1[6] = x61;
+  out1[7] = x64;
+  out1[8] = x67;
+  out1[9] = x68;
 }