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, 68 insertions, 56 deletions

diff --git a/src/AbstractInterpretationProofs.v b/src/AbstractInterpretationProofs.v
index 6bf479dfe..c0f20474d 100644
--- a/src/AbstractInterpretationProofs.v
+++ b/src/AbstractInterpretationProofs.v
@@ -335,14 +335,29 @@ Module Compilers.
         { assumption. }
       Qed.
 
+      Lemma related_bounded_value_Proper_eq {t}
+        : Proper (eq ==> eq ==> eq ==> Basics.impl) (@related_bounded_value t).
+      Proof using Type.
+        repeat intro; subst; assumption.
+      Qed.
+
+      Lemma related_bounded_value_Proper_interp_eq_base {t}
+        : Proper (eq ==> RelProd eq (fun x y => expr.interp ident_interp x = expr.interp ident_interp y) ==> eq ==> Basics.impl) (@related_bounded_value (type.base t)).
+      Proof using Type.
+        repeat intro; subst.
+        cbv [value RelProd relation_conjunction predicate_intersection pointwise_extension RelCompFun] in *.
+        destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *; subst.
+        cbv [related_bounded_value] in *; destruct_head'_and; repeat apply conj; subst; (idtac + symmetry); assumption.
+      Qed.
+
       Fixpoint interp_reify
-               is_let_bound {t} st e v b_in
+               annotate_with_state is_let_bound {t} st e v b_in
                (Hb : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in)
                (H : related_bounded_value st e v) {struct t}
         : (forall arg1 arg2
                   (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                   (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
-              type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify is_let_bound t e b_in))) arg1
+              type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1
               = type.app_curried v arg2)
           /\ (forall arg1
                      (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1)
@@ -350,30 +365,31 @@ Module Compilers.
                  abstraction_relation'
                    _
                    (type.app_curried (fill_in_bottom_for_arrows st) b_in)
-                   (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify is_let_bound t e b_in))) arg1))
+                   (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1))
       with interp_reflect
-             {t} st e v
+             annotate_with_state {t} st e v
              (Hst_Proper : Proper abstract_domain_R st)
              (H_val : expr.interp ident_interp e == v)
              (Hst1 : abstraction_relation (fill_in_bottom_for_arrows st) (expr.interp ident_interp e))
              {struct t}
            : related_bounded_value
                st
-               (@reflect t e st)
+               (@reflect annotate_with_state t e st)
                v.
       Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
         all: destruct t as [t|s d];
           [ clear interp_reify interp_reflect
-          | pose proof (fun is_let_bound => interp_reify is_let_bound s) as interp_reify_s;
-            pose proof (fun is_let_bound => interp_reify is_let_bound d) as interp_reify_d;
-            pose proof (interp_reflect s) as interp_reflect_s;
-            pose proof (interp_reflect d) as interp_reflect_d;
+          | pose proof (fun is_let_bound => interp_reify annotate_with_state is_let_bound s) as interp_reify_s;
+            pose proof (fun is_let_bound => interp_reify annotate_with_state is_let_bound d) as interp_reify_d;
+            pose proof (interp_reflect annotate_with_state s) as interp_reflect_s;
+            pose proof (interp_reflect annotate_with_state d) as interp_reflect_d;
             clear interp_reify interp_reflect;
             pose proof (@abstract_domain_R_bottom_fill_arrows s);
             pose proof (@abstract_domain_R_bottom_fill_arrows d) ].
         all: cbn [reify reflect] in *; fold (@reify) (@reflect) in *.
         all: cbn [related_bounded_value type.related type.app_curried] in *.
         all: cbn [UnderLets.interp expr.interp type.final_codomain type.andb_each_lhs_of_arrow type.is_base fst snd fill_in_bottom_for_arrows type.map_for_each_lhs_of_arrow type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow partial.bottom_for_each_lhs_of_arrow partial.bottom] in *.
+        all: destruct annotate_with_state; try destruct is_let_bound.
         all: repeat first [ reflexivity
                           | progress eta_expand
                           | progress cbv [type.is_not_higher_order] in *
@@ -408,7 +424,7 @@ Module Compilers.
                             try assumption; auto; []
                           | match goal with
                             | [ |- Proper ?R _ ] => (eapply PER_valid_l + eapply PER_valid_r); eassumption
-                            | [ |- @related_bounded_value ?t ?st1 (reflect _ ?st2) _ ]
+                            | [ |- @related_bounded_value ?t ?st1 (reflect _ _ ?st2) _ ]
                               => (tryif first [ constr_eq st1 st2 | has_evar st1 | has_evar st2 ]
                                   then fail
                                   else (eapply (@related_bounded_value_Proper1 t st2 st1);
@@ -427,7 +443,7 @@ Module Compilers.
                             end
                           | progress fold (@reify) (@reflect) (@type.interp) (@type.related) (@type.related_hetero) in *
                           | match goal with
-                            | [ |- type.related _ (expr.interp _ (UnderLets.interp _ (reify _ _ _))) _ ]
+                            | [ |- type.related _ (expr.interp _ (UnderLets.interp _ (reify _ _ _ _))) _ ]
                               => rewrite type.related_iff_app_curried
                             | [ |- type.related_hetero _ (@state_of_value ?t _) _ ]
                               => is_var t; destruct t; cbv [state_of_value]; [ cbn | apply bottom_related ]
@@ -435,14 +451,14 @@ Module Compilers.
       Qed.
 
       Lemma interp_reify_first_order
-               is_let_bound {t} st e v b_in
+               annotate_with_state is_let_bound {t} st e v b_in
                (Ht : type.is_not_higher_order t = true)
                (Hb : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in)
                (H : related_bounded_value st e v)
         : (forall arg1 arg2
                   (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                   (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
-              type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify is_let_bound t e b_in))) arg1
+              type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1
               = type.app_curried v arg2)
           /\ (forall arg1
                      (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1)
@@ -450,21 +466,21 @@ Module Compilers.
                  abstraction_relation'
                    _
                    (type.app_curried st b_in)
-                   (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify is_let_bound t e b_in))) arg1)).
+                   (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1)).
       Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
         rewrite first_order_app_curried_fill_in_bottom_for_arrows_eq by assumption.
         apply interp_reify; assumption.
       Qed.
 
       Lemma interp_reflect_first_order
-             {t} st e v
+             annotate_with_state {t} st e v
              (Ht : type.is_not_higher_order t = true)
              (Hst_Proper : Proper abstract_domain_R st)
              (H_val : expr.interp ident_interp e == v)
              (Hst : abstraction_relation st (expr.interp ident_interp e))
         : related_bounded_value
             st
-            (@reflect t e st)
+            (@reflect annotate_with_state t e st)
             v.
       Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
         rewrite first_order_abstraction_relation_fill_in_bottom_for_arrows_iff in Hst by assumption.
@@ -507,7 +523,7 @@ Module Compilers.
                   related_bounded_value (ident_extract t idc) (UnderLets.interp ident_interp (interp_ident t idc)) (ident_interp t idc)).
 
       Lemma interp_interp
-            G G' {t} (e_st e1 e2 e3 : expr t)
+            annotate_with_state G G' {t} (e_st e1 e2 e3 : expr t)
             (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G
                                      -> related_bounded_value_with_lets v1 v2 v3)
             (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> v1 == v2)
@@ -515,13 +531,14 @@ Module Compilers.
             (Hwf' : expr.wf G' e2 e3)
         : related_bounded_value_with_lets
             (extract' e_st)
-            (interp e1)
+            (interp annotate_with_state e1)
             (expr.interp (@ident_interp) e2).
       Proof using interp_ident_Proper interp_annotate abstraction_relation'_Proper ident_interp_Proper' abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper bottom'_related.
         clear -ident_interp_Proper' interp_ident_Proper interp_annotate abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper bottom'_related HG HG' Hwf Hwf'.
         cbv [related_bounded_value_with_lets] in *;
           revert dependent G'; induction Hwf; intros;
-            cbn [extract' interp expr.interp UnderLets.interp List.In related_bounded_value reify reflect] in *.
+            cbn [extract' interp expr.interp UnderLets.interp List.In related_bounded_value reify reflect] in *; cbv [Let_In] in *.
+        all: destruct annotate_with_state eqn:?.
         all: repeat first [ progress intros
                           | progress subst
                           | progress inversion_sigma
@@ -538,8 +555,8 @@ Module Compilers.
                           | rewrite interp_annotate
                           | solve [ cbv [Proper respectful Basics.impl] in *; eauto using related_of_related_bounded_value, related_bounded_value_bottomify ]
                           | progress specialize_by_assumption
-                          | progress cbv [Let_In extract'] in *
-                          | progress cbn [state_of_value] in *
+                          | progress cbv [Let_In] in *
+                          | progress cbn [state_of_value extract'] in *
                           | progress expr.invert_subst
                           | match goal with
                             | [ |- abstract_domain ?t ] => exact (@bottom t)
@@ -553,6 +570,11 @@ Module Compilers.
                             | [ |- related_bounded_value _ (fst _, UnderLets.interp _ (annotate _ _ _ _)) _ ]
                               => apply related_bounded_value_annotate_base
                             | [ H : context[match ?v with None => _ | _ => _ end] |- _ ] => destruct v eqn:?
+                            | [ H : context[@related_bounded_value (type.base ?t) ?x _ ?y]
+                                |- @related_bounded_value (type.base ?t) ?x _ ?y ]
+                              => eapply related_bounded_value_Proper_interp_eq_base; [ reflexivity | split; hnf | reflexivity | eapply H ];
+                                 cbn [fst snd expr.interp];
+                                 [ reflexivity | reflexivity | .. ]
                             end
                           | apply conj
                           | match goal with
@@ -578,7 +600,7 @@ Module Compilers.
       Qed.
 
       Lemma interp_eval_with_bound'
-            {t} (e_st e1 e2 : expr t)
+            annotate_with_state {t} (e_st e1 e2 : expr t)
             (Hwf : expr.wf3 nil e_st e1 e2)
             (Hwf' : expr.wf nil e2 e2)
             (Ht : type.is_not_higher_order t = true)
@@ -587,7 +609,7 @@ Module Compilers.
         : (forall arg1 arg2
                   (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                   (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
-              type.app_curried (expr.interp ident_interp (eval_with_bound' e1 st)) arg1
+              type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e1 st)) arg1
               = type.app_curried (expr.interp ident_interp e2) arg2)
           /\ (forall arg1
                      (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1)
@@ -595,7 +617,7 @@ Module Compilers.
                  abstraction_relation'
                    _
                    (extract_gen e_st st)
-                   (type.app_curried (expr.interp ident_interp (eval_with_bound' e1 st)) arg1)).
+                   (type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e1 st)) arg1)).
       Proof using interp_annotate abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_related interp_ident_Proper bottom'_Proper ident_interp_Proper'.
         cbv [extract_gen extract' eval_with_bound'].
         split; intros; rewrite UnderLets.interp_to_expr, UnderLets.interp_splice.
@@ -678,9 +700,6 @@ Module Compilers.
                     annotate_ident t st = Some idc
                     -> forall v, abstraction_relation' _ st v
                            -> ident_interp idc v = v)
-                (interp_update_literal_with_state
-                 : forall (t : base.type.base) (st : abstract_domain' t) (v : base.interp t),
-                    abstraction_relation' t st v -> update_literal_with_state t st v = v)
                 (abstract_interp_ident_Proper'
                  : forall t idc, type.related_hetero (@abstraction_relation') (abstract_interp_ident t idc) (ident_interp idc))
                 (extract_list_state_related
@@ -697,9 +716,9 @@ Module Compilers.
 
         Local Notation update_annotation := (@ident.update_annotation _ abstract_domain' annotate_ident is_annotated_for).
         Local Notation annotate_with_ident := (@ident.annotate_with_ident _ abstract_domain' annotate_ident is_annotated_for).
-        Local Notation annotate_base := (@ident.annotate_base _ abstract_domain' annotate_ident update_literal_with_state is_annotated_for).
-        Local Notation annotate := (@ident.annotate _ abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-        Local Notation interp_ident := (@ident.interp_ident _ abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
+        Local Notation annotate_base := (@ident.annotate_base _ abstract_domain' annotate_ident is_annotated_for).
+        Local Notation annotate := (@ident.annotate _ abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for).
+        Local Notation interp_ident := (@ident.interp_ident _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
         Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' bottom' abstract_domain'_R).
         Local Notation reify := (@reify base.type ident _ abstract_domain' annotate bottom').
         Local Notation reflect := (@reflect base.type ident _ abstract_domain' annotate bottom').
@@ -746,9 +765,8 @@ Module Compilers.
               (He : abstraction_relation' t st (expr.interp (t:=type.base (base.type.type_base t)) (@ident_interp) e))
           : expr.interp (@ident_interp) (UnderLets.interp (@ident_interp) (@annotate_base is_let_bound t st e))
             = expr.interp (@ident_interp) e.
-        Proof using interp_annotate_ident interp_update_literal_with_state.
+        Proof using interp_annotate_ident.
           cbv [annotate_base]; break_innermost_match; expr.invert_subst; cbv beta iota in *; subst.
-          { cbn [expr.interp UnderLets.interp ident.smart_Literal ident_interp] in *; eauto. }
           { apply interp_annotate_with_ident; assumption. }
         Qed.
 
@@ -756,7 +774,7 @@ Module Compilers.
               (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e))
           : expr.interp (@ident_interp) (UnderLets.interp (@ident_interp) (@annotate is_let_bound t st e))
             = expr.interp (@ident_interp) e.
-        Proof using interp_update_literal_with_state interp_annotate_ident abstract_interp_ident_Proper' extract_list_state_related extract_list_state_length_good bottom'_related.
+        Proof using interp_annotate_ident abstract_interp_ident_Proper' extract_list_state_related extract_list_state_length_good bottom'_related.
           induction t; cbn [annotate]; auto using interp_annotate_base.
           all: repeat first [ reflexivity
                             | progress subst
@@ -824,9 +842,9 @@ Module Compilers.
                               end ].
         Qed.
 
-        Lemma interp_ident_Proper_not_nth_default t idc
-          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (Base (reflect (expr.Ident idc) (abstract_interp_ident _ idc)))) (ident_interp idc).
-        Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related interp_annotate_ident interp_update_literal_with_state abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
+        Lemma interp_ident_Proper_not_nth_default annotate_with_state t idc
+          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (Base (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)))) (ident_interp idc).
+        Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related interp_annotate_ident abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
           cbn [UnderLets.interp].
           eapply interp_reflect;
             try first [ apply ident.gen_interp_Proper
@@ -836,9 +854,9 @@ Module Compilers.
             eauto.
         Qed.
 
-        Lemma interp_ident_Proper_nth_default T (idc:=@ident.List_nth_default T)
-          : related_bounded_value (abstract_interp_ident _ idc) (UnderLets.interp (@ident_interp) (interp_ident idc)) (ident_interp idc).
-        Proof using abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper extract_list_state_length_good extract_list_state_related interp_annotate_ident interp_update_literal_with_state bottom'_related.
+        Lemma interp_ident_Proper_nth_default annotate_with_state T (idc:=@ident.List_nth_default T)
+          : related_bounded_value (abstract_interp_ident _ idc) (UnderLets.interp (@ident_interp) (interp_ident annotate_with_state idc)) (ident_interp idc).
+        Proof using abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper extract_list_state_length_good extract_list_state_related interp_annotate_ident bottom'_related.
           subst idc; cbn [interp_ident reify reflect fst snd UnderLets.interp ident_interp related_bounded_value abstract_domain value].
           cbv [abstract_domain]; cbn [type.interp bottom_for_each_lhs_of_arrow state_of_value fst snd].
           repeat first [ progress intros
@@ -858,6 +876,7 @@ Module Compilers.
                        | apply (@abstract_interp_ident_Proper'' _ (@ident.List_nth_default T))
                        | apply conj
                        | rewrite map_nth_default_always
+                       | rewrite expr.interp_reify_list
                        | match goal with
                          | [ H : context[expr.interp _ (UnderLets.interp _ (annotate _ _ _))] |- _ ]
                            => rewrite interp_annotate in H
@@ -869,20 +888,20 @@ Module Compilers.
                          end ].
         Qed.
 
-        Lemma interp_ident_Proper t idc
-          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (interp_ident idc)) (ident_interp idc).
+        Lemma interp_ident_Proper annotate_with_state t idc
+          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (interp_ident annotate_with_state idc)) (ident_interp idc).
         Proof.
           pose idc as idc'.
-          destruct idc; first [ refine (@interp_ident_Proper_not_nth_default _ idc')
-                              | refine (@interp_ident_Proper_nth_default _) ].
+          destruct idc; first [ refine (@interp_ident_Proper_not_nth_default _ _ idc')
+                              | refine (@interp_ident_Proper_nth_default _ _) ].
         Qed.
 
-        Local Notation eval_with_bound := (@partial.ident.eval_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-        Local Notation eta_expand_with_bound := (@partial.ident.eta_expand_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
+        Local Notation eval_with_bound := (@partial.ident.eval_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+        Local Notation eta_expand_with_bound := (@partial.ident.eta_expand_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
         Local Notation extract := (@ident.extract abstract_domain' bottom' abstract_interp_ident).
 
         Lemma interp_eval_with_bound
-              {t} (e_st e1 e2 : expr t)
+              annotate_with_state {t} (e_st e1 e2 : expr t)
               (Hwf : expr.wf3 nil e_st e1 e2)
               (Hwf' : expr.wf nil e2 e2)
               (Ht : type.is_not_higher_order t = true)
@@ -891,7 +910,7 @@ Module Compilers.
           : (forall arg1 arg2
                     (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
-                type.app_curried (expr.interp (@ident_interp) (eval_with_bound e1 st)) arg1
+                type.app_curried (expr.interp (@ident_interp) (eval_with_bound annotate_with_state e1 st)) arg1
                 = type.app_curried (expr.interp (@ident_interp) e2) arg2)
             /\ (forall arg1
                        (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1)
@@ -899,7 +918,7 @@ Module Compilers.
                    abstraction_relation'
                      _
                      (extract e_st st)
-                     (type.app_curried (expr.interp (@ident_interp) (eval_with_bound e1 st)) arg1)).
+                     (type.app_curried (expr.interp (@ident_interp) (eval_with_bound annotate_with_state e1 st)) arg1)).
         Proof. cbv [extract eval_with_bound]; apply @interp_eval_with_bound' with (abstract_domain'_R:=abstract_domain'_R); auto using interp_annotate, interp_ident_Proper, ident.gen_interp_Proper. Qed.
 
         Lemma interp_eta_expand_with_bound
@@ -951,13 +970,6 @@ Module Compilers.
         : type.related_hetero (@abstraction_relation') (@abstract_interp_ident t idc) (@ident.gen_interp cast_outside_of_range _ idc).
       Proof using Type. apply ZRange.ident.option.interp_related. Qed.
 
-      Lemma interp_update_literal_with_state {t : base.type.base} st v
-        : @abstraction_relation' t st v -> @update_literal_with_state t st v = v.
-      Proof using Type.
-        cbv [abstraction_relation' update_literal_with_state update_Z_literal_with_state ZRange.type.base.option.is_bounded_by];
-          break_innermost_match; try congruence; reflexivity.
-      Qed.
-
       Lemma extract_list_state_related {t} st v ls
         : @abstraction_relation' _ st v
           -> @extract_list_state t st = Some ls
@@ -1034,7 +1046,7 @@ Module Compilers.
           : @annotate_ident relax_zrange t st1 = @annotate_ident relax_zrange t st2.
         Proof using Type. congruence. Qed.
 
-        Local Hint Resolve interp_annotate_ident interp_update_literal_with_state abstract_interp_ident_related.
+        Local Hint Resolve interp_annotate_ident abstract_interp_ident_related.
 
         Lemma interp_eval_with_bound
               cast_outside_of_range