Push back admits in interp lemmas

Also, we now pull bounds out of the initial expression, rather than the
final expression, because it makes the proofs easier.  (It means we only
have to run bounds analysis with one var type, not talk about its
relatedness with multiple var types.)

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
17m52.60s | Total                                                                | 17m53.17s || -0m00.57s | -0.05%
--------------------------------------------------------------------------------------------------------------------
5m55.17s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m55.71s  || -0m00.53s | -0.15%
4m33.38s  | Experiments/NewPipeline/Toplevel1                                    | 4m33.93s  || -0m00.55s | -0.20%
1m36.04s  | Experiments/NewPipeline/Toplevel2                                    | 1m35.94s  || +0m00.09s | +0.10%
0m38.56s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m38.44s  || +0m00.12s | +0.31%
0m38.50s  | p521_32.c                                                            | 0m38.63s  || -0m00.13s | -0.33%
0m37.71s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.22s  || +0m00.49s | +1.31%
0m35.06s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.71s  || +0m00.35s | +1.00%
0m31.97s  | p521_64.c                                                            | 0m32.06s  || -0m00.09s | -0.28%
0m23.81s  | p384_32.c                                                            | 0m23.59s  || +0m00.21s | +0.93%
0m20.73s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.94s  || -0m00.21s | -1.00%
0m18.80s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.85s  || -0m00.05s | -0.26%
0m13.79s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m14.00s  || -0m00.21s | -1.50%
0m12.56s  | Experiments/NewPipeline/CStringification                             | 0m12.59s  || -0m00.02s | -0.23%
0m10.52s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.49s  || +0m00.02s | +0.28%
0m08.64s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.49s  || +0m00.15s | +1.76%
0m08.45s  | p384_64.c                                                            | 0m08.51s  || -0m00.06s | -0.70%
0m05.48s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.50s  || -0m00.01s | -0.36%
0m05.36s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.55s  || -0m00.18s | -3.42%
0m04.06s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.10s  || -0m00.04s | -0.97%
0m03.92s  | secp256k1_32.c                                                       | 0m03.78s  || +0m00.14s | +3.70%
0m03.84s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.81s  || +0m00.02s | +0.78%
0m03.76s  | p256_32.c                                                            | 0m03.87s  || -0m00.11s | -2.84%
0m03.29s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.25s  || +0m00.04s | +1.23%
0m03.09s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m03.11s  || -0m00.02s | -0.64%
0m02.22s  | p224_32.c                                                            | 0m02.24s  || -0m00.02s | -0.89%
0m02.03s  | curve25519_32.c                                                      | 0m02.05s  || -0m00.02s | -0.97%
0m01.54s  | p224_64.c                                                            | 0m01.54s  || +0m00.00s | +0.00%
0m01.53s  | p256_64.c                                                            | 0m01.55s  || -0m00.02s | -1.29%
0m01.52s  | secp256k1_64.c                                                       | 0m01.51s  || +0m00.01s | +0.66%
0m01.38s  | curve25519_64.c                                                      | 0m01.39s  || -0m00.01s | -0.71%
0m01.31s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.22s  || +0m00.09s | +7.37%
0m01.27s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.27s  || +0m00.00s | +0.00%
0m01.26s  | Experiments/NewPipeline/CLI                                          | 0m01.25s  || +0m00.01s | +0.80%
0m01.04s  | Experiments/NewPipeline/CompilersTestCases                           | 0m00.97s  || +0m00.07s | +7.21%
0m01.02s  | Experiments/NewPipeline/AbstractInterpretation                       | 0m01.12s  || -0m00.10s | -8.92%

1 files changed, 4 insertions, 15 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 4d9673eb1..10590c02b 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -1058,18 +1058,6 @@ Module Compilers.
     : Expr t
     := partial.EtaExpandWithListInfoFromBound (GeneralizeVar.GeneralizeVar (e _)) bound.
 
-  Definition CheckPartialEvaluateWithBounds
-             {A}
-             (relax_zrange : zrange -> option zrange)
-             {t} (E : Expr t)
-             (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
-             (b_out : ZRange.type.base.option.interp (type.final_codomain t))
-    : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + A)
-    := let b_computed := partial.Extract E b_in in
-       if ZRange.type.base.option.is_tighter_than b_computed b_out
-       then @inl (Expr t) _ (RelaxZRange.expr.Relax relax_zrange E)
-       else inr (@inl (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) _ (b_computed, E)).
-
   Definition CheckedPartialEvaluateWithBounds
              (relax_zrange : zrange -> option zrange)
              {t} (E : Expr t)
@@ -1078,11 +1066,12 @@ Module Compilers.
     : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + list { t : _ & ident t })
     := dlet_nd e := GeneralizeVar.ToFlat E in
        let E := GeneralizeVar.FromFlat e in
+       let b_computed := partial.Extract E b_in in
        match CheckCasts.GetUnsupportedCasts E with
        | nil => (let E := PartialEvaluateWithBounds E b_in in
-                 dlet_nd e := GeneralizeVar.ToFlat E in
-                 let E := GeneralizeVar.FromFlat e in
-                 CheckPartialEvaluateWithBounds relax_zrange E b_in b_out)
+                if ZRange.type.base.option.is_tighter_than b_computed b_out
+                then @inl (Expr t) _ (RelaxZRange.expr.Relax relax_zrange E)
+                else inr (@inl (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) _ (b_computed, E)))
        | unsupported_casts => inr (inr unsupported_casts)
        end.
 End Compilers.