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, 37 insertions, 53 deletions

diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 4d82b869a..75ce71eff 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -732,11 +732,15 @@ Module Compilers.
            end%under_lets.
 
       (** We drop the state of higher-order arrows *)
-      Fixpoint reify (is_let_bound : bool) {t} : value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t)
+      Fixpoint reify (annotate_with_state : bool) (is_let_bound : bool) {t} : value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t)
         := match t return value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) with
            | type.base t
              => fun '(st, v) 'tt
-                => annotate is_let_bound t st v
+                => if annotate_with_state
+                   then annotate is_let_bound t st v
+                   else if is_let_bound
+                        then UnderLets.UnderLet v (fun v' => UnderLets.Base ($v'))
+                        else UnderLets.Base v
            | type.arrow s d
              => fun f_e '(sv, dv)
                => let sv := match s with
@@ -745,10 +749,10 @@ Module Compilers.
                            end in
                  Base
                    (λ x , (UnderLets.to_expr
-                             (fx <-- f_e (@reflect _ (expr.Var x) sv);
-                                @reify false _ fx dv)))
+                             (fx <-- f_e (@reflect annotate_with_state _ (expr.Var x) sv);
+                                @reify annotate_with_state false _ fx dv)))
            end%core%expr
-      with reflect {t} : @expr var t -> abstract_domain t -> value t
+      with reflect (annotate_with_state : bool) {t} : @expr var t -> abstract_domain t -> value t
            := match t return @expr var t -> abstract_domain t -> value t with
               | type.base t
                 => fun e st => (st, e)
@@ -756,45 +760,45 @@ Module Compilers.
                 => fun e absf
                    => (fun v
                        => let stv := state_of_value v in
-                          (rv <-- (@reify false s v bottom_for_each_lhs_of_arrow);
-                             Base (@reflect d (e @ rv) (absf stv))%expr))
+                          (rv <-- (@reify annotate_with_state false s v bottom_for_each_lhs_of_arrow);
+                             Base (@reflect annotate_with_state d (e @ rv) (absf stv))%expr))
               end%under_lets.
 
-      Fixpoint interp {t} (e : @expr value_with_lets t) : value_with_lets t
+      Fixpoint interp (annotate_with_state : bool) {t} (e : @expr value_with_lets t) : value_with_lets t
         := match e in expr.expr t return value_with_lets t with
            | expr.Ident t idc => interp_ident _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*)
            | expr.Var t v => v
-           | expr.Abs s d f => Base (fun x => @interp d (f (Base x)))
+           | expr.Abs s d f => Base (fun x => @interp annotate_with_state d (f (Base x)))
            | expr.App (type.base s) d f x
-             => (x' <-- @interp _ x;
-                   f' <-- @interp (_ -> d)%etype f;
+             => (x' <-- @interp annotate_with_state _ x;
+                   f' <-- @interp annotate_with_state (_ -> d)%etype f;
                    f' x')
            | expr.App (type.arrow s' d') d f x
-             => (x' <-- @interp (s' -> d')%etype x;
+             => (x' <-- @interp annotate_with_state (s' -> d')%etype x;
                    x'' <-- bottomify x';
-                   f' <-- @interp (_ -> d)%etype f;
+                   f' <-- @interp annotate_with_state (_ -> d)%etype f;
                    f' x'')
            | expr.LetIn (type.arrow _ _) B x f
-             => (x' <-- @interp _ x;
-                   @interp _ (f (Base x')))
+             => (x' <-- @interp annotate_with_state _ x;
+                   @interp annotate_with_state _ (f (Base x')))
            | expr.LetIn (type.base A) B x f
-             => (x' <-- @interp _ x;
-                   x'' <-- reify true (* this forces a let-binder here *) x' tt;
-                   @interp _ (f (Base (reflect x'' (state_of_value x')))))
+             => (x' <-- @interp annotate_with_state _ x;
+                   x'' <-- reify annotate_with_state true (* this forces a let-binder here *) x' tt;
+                   @interp annotate_with_state _ (f (Base (reflect annotate_with_state x'' (state_of_value x')))))
            end%under_lets.
 
-      Definition eval_with_bound' {t} (e : @expr value_with_lets t)
+      Definition eval_with_bound' (annotate_with_state : bool) {t} (e : @expr value_with_lets t)
                  (st : type.for_each_lhs_of_arrow abstract_domain t)
         : expr t
-        := UnderLets.to_expr (e' <-- interp e; reify false e' st).
+        := UnderLets.to_expr (e' <-- interp annotate_with_state e; reify annotate_with_state false e' st).
 
       Definition eval' {t} (e : @expr value_with_lets t) : expr t
-        := eval_with_bound' e bottom_for_each_lhs_of_arrow.
+        := eval_with_bound' false e bottom_for_each_lhs_of_arrow.
 
       Definition eta_expand_with_bound' {t} (e : @expr var t)
                  (st : type.for_each_lhs_of_arrow abstract_domain t)
         : expr t
-        := UnderLets.to_expr (reify false (reflect e bottom) st).
+        := UnderLets.to_expr (reify true false (reflect true e bottom) st).
 
       Section extract.
         Context (ident_extract : forall t, ident t -> abstract_domain t).
@@ -832,7 +836,6 @@ Module Compilers.
         Context (annotate_ident : forall t, abstract_domain' t -> option (ident (t -> t)))
                 (bottom' : forall A, abstract_domain' A)
                 (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
-                (update_literal_with_state : forall A : base.type.base, abstract_domain' A -> base.interp A -> base.interp A)
                 (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A)))
                 (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool).
 
@@ -861,10 +864,7 @@ Module Compilers.
         Definition annotate_base (is_let_bound : bool) {t : base.type.base}
                    (st : abstract_domain' t) (e : @expr var t)
           : UnderLets (@expr var t)
-          := match invert_Literal e with
-             | Some v => Base ##(update_literal_with_state _ st v)
-             | None => annotate_with_ident is_let_bound st e
-             end%expr.
+          := annotate_with_ident is_let_bound st e.
 
         Fixpoint annotate (is_let_bound : bool) {t : base.type} : abstract_domain' t -> @expr var t -> UnderLets (@expr var t)
           := match t return abstract_domain' t -> @expr var t -> UnderLets (@expr var t) with
@@ -904,10 +904,10 @@ Module Compilers.
         Local Notation reflect := (@reflect base.type ident var abstract_domain' annotate bottom').
 
         (** We manually rewrite with the rule for [nth_default], as the eliminator for eta-expanding lists in the input *)
-        Definition interp_ident {t} (idc : ident t) : value_with_lets t
+        Definition interp_ident (annotate_with_state : bool) {t} (idc : ident t) : value_with_lets t
           := match idc in ident t return value_with_lets t with
              | ident.List_nth_default T as idc
-               => let default := reflect (###idc) (abstract_interp_ident _ idc) in
+               => let default := reflect annotate_with_state (###idc) (abstract_interp_ident _ idc) in
                   Base
                     (fun default_arg
                      => default <-- default default_arg;
@@ -917,7 +917,7 @@ Module Compilers.
                                   Base
                                     (fun n_arg
                                      => default <-- default n_arg;
-                                          ls' <-- @reify false (base.type.list T) ls_arg tt;
+                                          ls' <-- @reify annotate_with_state false (base.type.list T) ls_arg tt;
                                           Base
                                             (fst default,
                                              match reflect_list ls', invert_Literal (snd n_arg) with
@@ -925,16 +925,16 @@ Module Compilers.
                                                => nth_default (snd default_arg) ls n
                                              | _, _ => snd default
                                              end))))
-             | idc => Base (reflect (###idc) (abstract_interp_ident _ idc))
+             | idc => Base (reflect annotate_with_state (###idc) (abstract_interp_ident _ idc))
              end%core%under_lets%expr.
 
-        Definition eval_with_bound {t} (e : @expr value_with_lets t)
+        Definition eval_with_bound (annotate_with_state : bool) {t} (e : @expr value_with_lets t)
                    (st : type.for_each_lhs_of_arrow abstract_domain t)
           : @expr var t
-          := @eval_with_bound' base.type ident var abstract_domain' annotate bottom' (@interp_ident) t e st.
+          := @eval_with_bound' base.type ident var abstract_domain' annotate bottom' (@interp_ident annotate_with_state) annotate_with_state t e st.
 
         Definition eval {t} (e : @expr value_with_lets t) : @expr var t
-          := @eval' base.type ident var abstract_domain' annotate bottom' (@interp_ident) t e.
+          := @eval' base.type ident var abstract_domain' annotate bottom' (@interp_ident false) t e.
 
         Definition eta_expand_with_bound {t} (e : @expr var t)
                    (st : type.for_each_lhs_of_arrow abstract_domain t)
@@ -999,32 +999,16 @@ Module Compilers.
           := ZRange.type.base.option.None.
         Definition abstract_interp_ident t (idc : ident t) : type.interp abstract_domain' t
           := ZRange.ident.option.interp idc.
-        Definition update_Z_literal_with_state : abstract_domain' base.type.Z -> Z -> Z
-          := fun r n
-             => match r with
-                | Some r => if ZRange.type.base.is_bounded_by (t:=base.type.Z) r n
-                            then n
-                            else ident.cast_outside_of_range r n
-                | None => n
-                end.
-        Definition update_literal_with_state (t : base.type.base) : abstract_domain' t -> base.interp t -> base.interp t
-          := match t with
-             | base.type.Z => update_Z_literal_with_state
-             | base.type.unit
-             | base.type.bool
-             | base.type.nat
-               => fun _ => id
-             end.
         Definition extract_list_state A (st : abstract_domain' (base.type.list A)) : option (list (abstract_domain' A))
           := st.
 
         Definition eval_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
           := (@partial.ident.eval_with_bound)
-               var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for t e bound.
+               var abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for true t e bound.
 
         Definition eta_expand_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
           := (@partial.ident.eta_expand_with_bound)
-               var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for t e bound.
+               var abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for t e bound.
 
         Definition EvalWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
           := fun var => eval_with_bound (e _) bound.
@@ -1034,7 +1018,7 @@ Module Compilers.
 
       Definition eval {var} {t} (e : @expr _ t) : expr t
         := (@partial.ident.eval)
-             var abstract_domain' (annotate_ident default_relax_zrange) bottom' abstract_interp_ident update_literal_with_state extract_list_state (is_annotated_for default_relax_zrange) t e.
+             var abstract_domain' (annotate_ident default_relax_zrange) bottom' abstract_interp_ident extract_list_state (is_annotated_for default_relax_zrange) t e.
       Definition Eval {t} (e : Expr t) : Expr t
         := fun var => eval (e _).
       Definition EtaExpandWithListInfoFromBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t