Don't guarantee anything about casting outside of range

We used to claim that casts brought values into the intersection of the
known range and the casted range.  This is absurd, in the same way that
it's absurd to claim that attempting to dereference a pointer guarantees
that it's non-null.  Instead, we pass through bounds that fit soundly
within the casted range, and otherwise guarantee nothing about the
bounds of the resulting code.

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
17m52.74s | Total                                                                | 17m53.29s || -0m00.55s | -0.05%
--------------------------------------------------------------------------------------------------------------------
4m33.01s  | Experiments/NewPipeline/Toplevel1                                    | 4m31.90s  || +0m01.11s | +0.40%
5m55.30s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m55.05s  || +0m00.25s | +0.07%
1m36.16s  | Experiments/NewPipeline/Toplevel2                                    | 1m35.88s  || +0m00.28s | +0.29%
0m38.71s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m39.10s  || -0m00.39s | -0.99%
0m38.52s  | p521_32.c                                                            | 0m39.13s  || -0m00.60s | -1.55%
0m37.12s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.32s  || -0m00.20s | -0.53%
0m34.93s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.65s  || +0m00.28s | +0.80%
0m32.10s  | p521_64.c                                                            | 0m32.70s  || -0m00.60s | -1.83%
0m23.76s  | p384_32.c                                                            | 0m23.69s  || +0m00.07s | +0.29%
0m20.25s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.70s  || -0m00.44s | -2.17%
0m18.64s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.99s  || -0m00.34s | -1.84%
0m13.72s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.78s  || -0m00.05s | -0.43%
0m12.55s  | Experiments/NewPipeline/CStringification                             | 0m12.58s  || -0m00.02s | -0.23%
0m10.42s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.56s  || -0m00.14s | -1.32%
0m08.64s  | p384_64.c                                                            | 0m08.44s  || +0m00.20s | +2.36%
0m08.59s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.51s  || +0m00.08s | +0.94%
0m05.52s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.32s  || +0m00.19s | +3.75%
0m05.34s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.47s  || -0m00.12s | -2.37%
0m04.04s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m04.02s  || +0m00.02s | +0.49%
0m04.00s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.84s  || +0m00.16s | +4.16%
0m03.99s  | secp256k1_32.c                                                       | 0m03.82s  || +0m00.17s | +4.45%
0m03.89s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.02s  || -0m00.12s | -3.23%
0m03.81s  | p256_32.c                                                            | 0m03.83s  || -0m00.02s | -0.52%
0m03.21s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.30s  || -0m00.08s | -2.72%
0m02.14s  | p224_32.c                                                            | 0m02.26s  || -0m00.11s | -5.30%
0m02.11s  | curve25519_32.c                                                      | 0m02.09s  || +0m00.02s | +0.95%
0m01.73s  | p224_64.c                                                            | 0m01.54s  || +0m00.18s | +12.33%
0m01.66s  | secp256k1_64.c                                                       | 0m01.64s  || +0m00.02s | +1.21%
0m01.58s  | p256_64.c                                                            | 0m01.68s  || -0m00.09s | -5.95%
0m01.38s  | curve25519_64.c                                                      | 0m01.47s  || -0m00.09s | -6.12%
0m01.37s  | Experiments/NewPipeline/CLI                                          | 0m01.45s  || -0m00.07s | -5.51%
0m01.25s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.20s  || +0m00.05s | +4.16%
0m01.21s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.28s  || -0m00.07s | -5.46%
0m01.06s  | Experiments/NewPipeline/CompilersTestCases                           | 0m01.07s  || -0m00.01s | -0.93%
0m01.04s  | Experiments/NewPipeline/AbstractInterpretation                       | 0m01.02s  || +0m00.02s | +1.96%

1 files changed, 10 insertions, 12 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index b673d630f..72a94e54c 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -353,6 +353,14 @@ Module Compilers.
                (only parsing).
         (** do bounds analysis on identifiers; take in optional bounds
             on arguments, return optional bounds on outputs. *)
+        (** Casts are like assertions; we only guarantee anything when they're true *)
+        Definition interp_Z_cast (r : zrange) (v : option zrange) : option zrange
+          := match v with
+             | Some v => if is_tighter_than_bool v r (* the value is definitely inside the range *)
+                         then Some v
+                         else None
+             | None => None
+             end.
         Definition interp {t} (idc : ident t) : type.option.interp t
           := match idc in ident.ident t return type.option.interp t with
              | ident.Literal _ v => of_literal v
@@ -589,20 +597,10 @@ Module Compilers.
                                                     x y m)))
              | ident.Z_cast range
                => fun r : option zrange
-                 => Some match r with
-                        | Some r => ZRange.intersection r range
-                        | None => range
-                        end
+                  => interp_Z_cast range r
              | ident.Z_cast2 (r1, r2)
                => fun '((r1', r2') : option zrange * option zrange)
-                 => (Some match r1' with
-                         | Some r => ZRange.intersection r r1
-                         | None => r1
-                         end,
-                    Some match r2' with
-                         | Some r => ZRange.intersection r r2
-                         | None => r2
-                         end)
+                  => (interp_Z_cast r1 r1', interp_Z_cast r2 r2')
              (** TODO(jadep): fill in fancy bounds analysis rules *)
              | ident.fancy_add log2wordmax _
              | ident.fancy_sub log2wordmax _