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, 42 insertions, 48 deletions

diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v
index a2ba63c01..a6a2d8d6b 100644
--- a/src/AbstractInterpretationWf.v
+++ b/src/AbstractInterpretationWf.v
@@ -171,23 +171,23 @@ Module Compilers.
                          | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ].
         Qed.
 
-        Fixpoint wf_reify (is_let_bound : bool) G {t}
+        Fixpoint wf_reify (annotate_with_state : bool) (is_let_bound : bool) G {t}
           : forall v1 v2 (Hv : @wf_value G t v1 v2)
               s1 s2 (Hs : type.and_for_each_lhs_of_arrow (@abstract_domain_R) s1 s2),
-            UnderLets.wf (fun G' => expr.wf G') G (@reify1 is_let_bound t v1 s1) (@reify2 is_let_bound t v2 s2)
-        with wf_reflect G {t}
+            UnderLets.wf (fun G' => expr.wf G') G (@reify1 annotate_with_state is_let_bound t v1 s1) (@reify2 annotate_with_state is_let_bound t v2 s2)
+        with wf_reflect (annotate_with_state : bool) G {t}
              : forall e1 e2 (He : expr.wf G e1 e2)
                  s1 s2 (Hs : abstract_domain_R s1 s2),
-            @wf_value G t (@reflect1 t e1 s1) (@reflect2 t e2 s2).
+            @wf_value G t (@reflect1 annotate_with_state t e1 s1) (@reflect2 annotate_with_state t e2 s2).
         Proof using annotate_Proper bottom'_Proper.
           all: clear -wf_reflect wf_reify annotate_Proper type_base bottom'_Proper.
           all: pose proof (@bottom_for_each_lhs_of_arrow_Proper); cbv [Proper abstract_domain_R] in *.
           all: destruct t as [t|s d];
             [ clear wf_reify wf_reflect
-            | pose proof (fun G => wf_reflect G s) as wf_reflect_s;
-              pose proof (fun G => wf_reflect G d) as wf_reflect_d;
-              pose proof (fun G => wf_reify false G s) as wf_reify_s;
-              pose proof (fun G => wf_reify false G d) as wf_reify_d;
+            | pose proof (fun G => wf_reflect annotate_with_state G s) as wf_reflect_s;
+              pose proof (fun G => wf_reflect annotate_with_state G d) as wf_reflect_d;
+              pose proof (fun G => wf_reify annotate_with_state false G s) as wf_reify_s;
+              pose proof (fun G => wf_reify annotate_with_state false G d) as wf_reify_d;
               pose proof (@bottom_Proper s);
               clear wf_reify wf_reflect ].
           all: cbn [reify reflect] in *.
@@ -208,9 +208,9 @@ Module Compilers.
                               | [ |- expr.wf _ _ _ ] => constructor
                               | [ He : forall seg G' sv1 sv2, G' = (seg ++ ?G)%list -> _ |- UnderLets.wf _ (?v :: ?G) (UnderLets.splice _ _) (UnderLets.splice _ _) ]
                                 => eapply UnderLets.wf_splice; [ apply (He (cons v nil)) | ]
-                              | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _) _) (UnderLets.splice (reify2 _ _ _) _) ]
+                              | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _ _) _) (UnderLets.splice (reify2 _ _ _ _) _) ]
                                 => eapply UnderLets.wf_splice; [ apply wf_reify_s || apply wf_reify_d | ]
-                              | [ |- wf_value _ (reflect1 _ _) (reflect2 _ _) ] => apply wf_reflect_s || apply wf_reflect_d
+                              | [ |- wf_value _ (reflect1 _ _ _) (reflect2 _ _ _) ] => apply wf_reflect_s || apply wf_reflect_d
                               | [ H : wf_value _ ?x ?y |- wf_value _ ?x ?y ]
                                 => eapply wf_value_Proper_list; [ | eassumption ]
                               | [ H : forall x y, ?R x y -> ?R' (?f x) (?g y) |- ?R' (?f _) (?g _) ]
@@ -259,10 +259,10 @@ Module Compilers.
                          end
                        | break_innermost_match_step ].
 
-        Lemma wf_interp G G' {t} (e1 : @expr (@value_with_lets1) t) (e2 : @expr (@value_with_lets2) t)
+        Lemma wf_interp (annotate_with_state : bool) G G' {t} (e1 : @expr (@value_with_lets1) t) (e2 : @expr (@value_with_lets2) t)
               (Hwf : expr.wf G e1 e2)
               (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-          : wf_value_with_lets G' (interp1 e1) (interp2 e2).
+          : wf_value_with_lets G' (interp1 annotate_with_state e1) (interp2 annotate_with_state e2).
         Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
           revert dependent G'; induction Hwf; intros; cbn [interp];
             try solve [ apply interp_ident_Proper; auto
@@ -270,9 +270,9 @@ Module Compilers.
             wf_interp_t.
         Qed.
 
-        Lemma wf_eval_with_bound' G G' {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+        Lemma wf_eval_with_bound' (annotate_with_state : bool) G G' {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
               (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-          : expr.wf G' (@eval_with_bound'1 t e1 st1) (@eval_with_bound'2 t e2 st2).
+          : expr.wf G' (@eval_with_bound'1 annotate_with_state t e1 st1) (@eval_with_bound'2 annotate_with_state t e2 st2).
         Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
           eapply UnderLets.wf_to_expr, UnderLets.wf_splice.
           { eapply wf_interp; solve [ eauto ]. }
@@ -303,7 +303,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).
         Context (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop).
@@ -311,7 +310,6 @@ Module Compilers.
         Context {annotate_ident_Proper : forall t, Proper (abstract_domain'_R t ==> eq) (annotate_ident t)}
                 {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}
                 {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}
-                {update_literal_with_state_Proper : forall t, Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t)}
                 {is_annotated_for_Proper : forall t t', Proper (eq ==> abstract_domain'_R _ ==> eq) (@is_annotated_for t t')}
                 (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2))
                 (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2).
@@ -325,14 +323,14 @@ Module Compilers.
 
           Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident is_annotated_for).
           Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident is_annotated_for).
-          Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-          Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-          Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident update_literal_with_state is_annotated_for).
-          Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident update_literal_with_state is_annotated_for).
+          Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident is_annotated_for).
+          Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident is_annotated_for).
           Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident is_annotated_for).
           Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident is_annotated_for).
-          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
+          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
           Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom').
           Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom').
 
@@ -382,7 +380,7 @@ Module Compilers.
                 v1 v2 (Hv : abstract_domain'_R t v1 v2)
                 e1 e2 (He : expr.wf G e1 e2)
             : UnderLets.wf (fun G' => expr.wf G') G (@annotate_base1 is_let_bound t v1 e1) (@annotate_base2 is_let_bound t v2 e2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper update_literal_with_state_Proper is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper is_annotated_for_Proper.
             cbv [ident.annotate_base];
               repeat first [ apply wf_annotate_with_ident
                            | break_innermost_match_step
@@ -409,7 +407,7 @@ Module Compilers.
                 v1 v2 (Hv : abstract_domain'_R t v1 v2)
                 e1 e2 (He : expr.wf G e1 e2)
             : UnderLets.wf (fun G' => expr.wf G') G (@annotate1 is_let_bound t v1 e1) (@annotate2 is_let_bound t v2 e2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
             revert dependent G; induction t; intros;
               cbn [ident.annotate]; try apply wf_annotate_base; trivial.
             all: repeat first [ lazymatch goal with
@@ -491,9 +489,9 @@ Module Compilers.
                 let b' := type_of_value b in
                 constr:(type.arrow a' b')
             end.
-          Lemma wf_interp_ident_nth_default G T
-            : wf_value_with_lets G (@interp_ident1 _ (@ident.List_nth_default T)) (@interp_ident2 _ (@ident.List_nth_default T)).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper.
+          Lemma wf_interp_ident_nth_default (annotate_with_state : bool) G T
+            : wf_value_with_lets G (@interp_ident1 annotate_with_state _ (@ident.List_nth_default T)) (@interp_ident2 annotate_with_state _ (@ident.List_nth_default T)).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
             cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain].
             { intros; subst.
               destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *.
@@ -599,9 +597,9 @@ Module Compilers.
                              end ]. }
           Qed.
 
-          Lemma wf_interp_ident_not_nth_default G {t} (idc : ident t)
-            : wf_value_with_lets G (Base (reflect1 (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 (###idc)%expr (abstract_interp_ident _ idc))).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper.
+          Lemma wf_interp_ident_not_nth_default (annotate_with_state : bool) G {t} (idc : ident t)
+            : wf_value_with_lets G (Base (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
             constructor; eapply wf_reflect;
               solve [ apply bottom'_Proper
                     | apply wf_annotate
@@ -609,43 +607,43 @@ Module Compilers.
                     | apply abstract_interp_ident_Proper; reflexivity ].
           Qed.
 
-          Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2)
-            : wf_value_with_lets G (@interp_ident1 t idc1) (@interp_ident2 t idc2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper.
+          Lemma wf_interp_ident (annotate_with_state : bool) G {t} idc1 idc2 (Hidc : idc1 = idc2)
+            : wf_value_with_lets G (@interp_ident1 annotate_with_state t idc1) (@interp_ident2 annotate_with_state t idc2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
             cbv [wf_value_with_lets ident.interp_ident]; subst idc2; destruct idc1;
               first [ apply wf_interp_ident_nth_default
                     | apply wf_interp_ident_not_nth_default ].
           Qed.
 
-          Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-          Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-          Lemma wf_eval_with_bound {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+          Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Lemma wf_eval_with_bound (annotate_with_state : bool) {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
                 (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-            : expr.wf G' (@eval_with_bound1 t e1 st1) (@eval_with_bound2 t e2 st2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper.
+            : expr.wf G' (@eval_with_bound1 annotate_with_state t e1 st1) (@eval_with_bound2 annotate_with_state t e2 st2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
             eapply wf_eval_with_bound';
               solve [ eassumption
                     | eapply wf_annotate
                     | eapply wf_interp_ident ].
           Qed.
 
-          Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-          Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
+          Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
           Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2)
                 (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
             : expr.wf G' (@eval1 t e1) (@eval2 t e2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
             eapply wf_eval';
               solve [ eassumption
                     | eapply wf_annotate
                     | eapply wf_interp_ident ].
           Qed.
 
-          Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
-          Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
+          Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
           Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
             : expr.wf G (@eta_expand_with_bound1 t e1 st1) (@eta_expand_with_bound2 t e2 st2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
             eapply wf_eta_expand_with_bound';
               solve [ eassumption
                     | eapply wf_annotate
@@ -697,10 +695,6 @@ Module Compilers.
                          end ].
       Qed.
 
-      Global Instance update_literal_with_state_Proper {t}
-        : Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t).
-      Proof. repeat intro; congruence. Qed.
-
       Global Instance extract_list_state_Proper {t}
         : Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t)))
                  (extract_list_state t).