Don't fuse annotations

It was causing issues with proving things, and isn't really needed.

Instead, we just check if the current annotation is exactly the state
we're attempting to annotate with; if it is, then we don't double up on
identical annotations.

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
17m54.46s | Total                                                                | 17m52.24s || +0m02.21s | +0.20%
--------------------------------------------------------------------------------------------------------------------
5m55.78s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m55.41s  || +0m00.37s | +0.10%
4m32.97s  | Experiments/NewPipeline/Toplevel1                                    | 4m33.59s  || -0m00.62s | -0.22%
1m35.89s  | Experiments/NewPipeline/Toplevel2                                    | 1m35.77s  || +0m00.11s | +0.12%
0m39.24s  | p521_32.c                                                            | 0m38.50s  || +0m00.74s | +1.92%
0m38.16s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m38.52s  || -0m00.36s | -0.93%
0m37.42s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.34s  || +0m00.07s | +0.21%
0m34.59s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.58s  || +0m00.01s | +0.02%
0m32.58s  | p521_64.c                                                            | 0m31.97s  || +0m00.60s | +1.90%
0m23.66s  | p384_32.c                                                            | 0m23.63s  || +0m00.03s | +0.12%
0m21.02s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.88s  || +0m00.14s | +0.67%
0m18.92s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.84s  || +0m00.08s | +0.42%
0m13.91s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.99s  || -0m00.08s | -0.57%
0m12.56s  | Experiments/NewPipeline/CStringification                             | 0m12.61s  || -0m00.04s | -0.39%
0m10.51s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.66s  || -0m00.15s | -1.40%
0m08.55s  | p384_64.c                                                            | 0m08.46s  || +0m00.08s | +1.06%
0m08.51s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.61s  || -0m00.09s | -1.16%
0m05.59s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.56s  || +0m00.03s | +0.53%
0m05.43s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.34s  || +0m00.08s | +1.68%
0m04.00s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m03.07s  || +0m00.93s | +30.29%
0m04.00s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.04s  || -0m00.04s | -0.99%
0m03.91s  | secp256k1_32.c                                                       | 0m03.93s  || -0m00.02s | -0.50%
0m03.87s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.84s  || +0m00.03s | +0.78%
0m03.84s  | p256_32.c                                                            | 0m03.78s  || +0m00.06s | +1.58%
0m03.33s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.32s  || +0m00.01s | +0.30%
0m02.12s  | p224_32.c                                                            | 0m02.10s  || +0m00.02s | +0.95%
0m02.11s  | curve25519_32.c                                                      | 0m02.03s  || +0m00.08s | +3.94%
0m01.56s  | p256_64.c                                                            | 0m01.55s  || +0m00.01s | +0.64%
0m01.53s  | p224_64.c                                                            | 0m01.55s  || -0m00.02s | -1.29%
0m01.50s  | secp256k1_64.c                                                       | 0m01.51s  || -0m00.01s | -0.66%
0m01.44s  | curve25519_64.c                                                      | 0m01.51s  || -0m00.07s | -4.63%
0m01.38s  | Experiments/NewPipeline/CLI                                          | 0m01.22s  || +0m00.15s | +13.11%
0m01.30s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.16s  || +0m00.14s | +12.06%
0m01.25s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.25s  || +0m00.00s | +0.00%
0m01.04s  | Experiments/NewPipeline/CompilersTestCases                           | 0m01.08s  || -0m00.04s | -3.70%
0m01.00s  | Experiments/NewPipeline/AbstractInterpretation                       | 0m01.05s  || -0m00.05s | -4.76%

3 files changed, 197 insertions, 73 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 10590c02b..b673d630f 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -790,31 +790,18 @@ Module Compilers.
                 (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_annotation : forall t, ident t -> bool)
-        (*(do_again : forall t : base.type, @expr var t -> UnderLets (@expr var t))*).
+                (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool).
 
         (** TODO: Is it okay to commute annotations? *)
         Definition update_annotation {t} (st : abstract_domain' t) (e : @expr var t) : @expr var t
-          := match e with
-             | (#cst' @ e')
-               => if is_annotation _ cst'
-                 then match type.try_transport base.try_make_transport_cps ident _ (t -> t) cst', type.try_transport base.try_make_transport_cps _ _ _ e' with
-                      | Some cst'', Some e''
-                        => match annotate_ident _ (abstract_interp_ident _ cst'' st) with
-                          | Some cst''' => ###cst''' @ e''
-                          | None => e
-                          end%expr
-                      | _, _ => e
-                      end
-                 else match annotate_ident _ st with
-                      | Some cst => ###cst @ e
-                      | None => e
-                      end%expr
-             | _ => match annotate_ident _ st with
-                   | Some cst => ###cst @ e
-                   | None => e
-                   end%expr
-             end%expr_pat.
+          := match e, annotate_ident _ st with
+             | (#cst' @ e'), Some cst
+               => if is_annotated_for _ _ cst' st
+                  then e
+                  else ###cst @ e
+             | _, Some cst => ###cst @ e
+             | _, None => e
+             end%expr_pat%expr.
 
         Definition annotate_with_ident (is_let_bound : bool) {t}
                    (st : abstract_domain' t) (e : @expr var t)
@@ -934,6 +921,22 @@ Module Compilers.
              => fun '(sta, stb) => sta' <- sta; stb' <- stb; Some (ident.Z_cast2 (sta', stb'))
            | _ => fun _ => None
            end%option%etype.
+      Definition is_annotated_for t t' (idc : ident t) : abstract_domain' t' -> bool
+        := match idc, t' with
+           | ident.Z_cast r, base.type.type_base base.type.Z
+             => fun r'
+                => match r' with
+                   | Some r' => zrange_beq r r'
+                   | None => false
+                   end
+           | ident.Z_cast2 (r1, r2), base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)
+             => fun '(r1', r2')
+                => match r1', r2' with
+                   | Some r1', Some r2' => zrange_beq r1 r1' && zrange_beq r2 r2'
+                   | _, _ => false
+                   end
+           | _, _ => fun _ => false
+           end.
       Definition is_annotation t (idc : ident t) : bool
         := match idc with
            | ident.Z_cast _
@@ -966,13 +969,13 @@ Module Compilers.
 
       Definition eval {var} {t} (e : @expr _ t) : expr t
         := (@partial.ident.eval)
-             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation t e.
+             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for t e.
       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_annotation t e bound.
+             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for 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_annotation t e bound.
+             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for t e bound.
       Definition Eval {t} (e : Expr t) : Expr t
         := fun var => eval (e _).
       Definition EvalWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index 341448363..69d1985b2 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -12,6 +12,7 @@ Require Import Crypto.Util.Option.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SplitInContext.
@@ -86,11 +87,18 @@ Module Compilers.
       Local Notation state_of_value := (@state_of_value base_type ident var abstract_domain').
       Context (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> @expr var t -> @UnderLets var (@expr var t))
               (interp_ident : forall t, ident t -> value_with_lets t)
-              (ident_extract : forall t, ident t -> abstract_domain t).
+              (ident_extract : forall t, ident t -> abstract_domain t)
+              (interp_annotate
+               : forall is_let_bound t st e
+                   (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).
       Local Notation eta_expand_with_bound' := (@eta_expand_with_bound' base_type ident _ abstract_domain' annotate bottom').
       Local Notation eval_with_bound' := (@partial.eval_with_bound' base_type ident _ abstract_domain' annotate bottom' interp_ident).
       Local Notation extract' := (@extract' base_type ident abstract_domain' ident_extract).
       Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract).
+      Local Notation reify := (@reify base_type ident _ abstract_domain' annotate bottom').
+      Local Notation reflect := (@reflect base_type ident _ abstract_domain' annotate bottom').
       (*
       Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom').
       Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom').
@@ -252,9 +260,9 @@ Module Compilers.
                    _
                    (extract_gen e_st st)
                    (type.app_curried (expr.interp ident_interp (eval_with_bound' e1 st)) arg1)).
-      Proof using Type.
-        cbv [extract_gen extract'].
-        cbv [eval_with_bound'].
+      Proof using interp_annotate.
+        cbv [extract_gen extract' eval_with_bound'].
+        split; intros; rewrite UnderLets.interp_to_expr, UnderLets.interp_splice.
       Admitted.
 
       Lemma interp_eta_expand_with_bound'
@@ -265,8 +273,9 @@ Module Compilers.
             (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 (eta_expand_with_bound' e1 b_in)) arg1 = type.app_curried (expr.interp ident_interp e2) arg2.
-      Proof using Type.
+      Proof using interp_annotate.
         cbv [eta_expand_with_bound'].
+        intros; rewrite UnderLets.interp_to_expr.
       Admitted.
 
 
@@ -298,10 +307,108 @@ Module Compilers.
                 (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_annotation : forall t, ident t -> bool).
-        Context (abstraction_relation' : forall t, abstract_domain' t -> base.interp t -> Prop).
-        Context (cast_outside_of_range : zrange -> Z -> Z).
+                (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool)
+                (is_annotation : forall t, ident t -> bool)
+                (abstraction_relation' : forall t, abstract_domain' t -> base.interp t -> Prop)
+                (cast_outside_of_range : zrange -> Z -> Z).
         Local Notation abstraction_relation := (@abstraction_relation base.type abstract_domain' base.interp abstraction_relation').
+        Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
+        Context (interp_annotate_ident
+                 : forall t st idc,
+                    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)
+                (*is_annotation_abstraction_relation_weaken
+                 : forall t st idc v,
+                    is_annotation _ idc = true
+                    -> abstraction_relation' _ st v
+                    -> abstraction_relation' _ (abstract_interp_ident (type.base t -> type.base t)%etype idc st) v*)
+                (*interp_annotate_ident_commute
+                 : forall t st v cst0 cst1,
+                    is_annotation (type.base t -> type.base t) cst0 = true ->
+                    annotate_ident t (abstract_interp_ident (type.base t -> type.base t) cst0 st) = Some cst1 ->
+                    abstraction_relation' t st (ident_interp cst0 v) -> ident_interp cst1 v = ident_interp cst0 v)*)
+                (abstract_interp_ident_Proper
+                 : forall t idc, is_annotation _ idc = false -> type.related_hetero (@abstraction_relation') (abstract_interp_ident t idc) (ident_interp idc))
+                (fst_is_not_annotation : forall A B, is_annotation _ (@ident.fst A B) = false)
+                (snd_is_not_annotation : forall A B, is_annotation _ (@ident.snd A B) = false).
+
+        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).
+
+        Lemma interp_update_annotation t st e
+              (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e))
+          : expr.interp (@ident_interp) (@update_annotation t st e)
+            = expr.interp (@ident_interp) e.
+        Proof using interp_annotate_ident.
+          cbv [update_annotation];
+            repeat first [ reflexivity
+                         | progress subst
+                         | progress eliminate_hprop_eq
+                         | progress cbn [expr.interp eq_rect] in *
+                         | erewrite interp_annotate_ident by eassumption
+                         | progress expr.invert_match
+                         | progress type_beq_to_eq
+                         | progress rewrite_type_transport_correct
+                         | progress break_innermost_match_step ].
+        Qed.
+
+        Lemma interp_annotate_with_ident is_let_bound t st e
+              (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e))
+          : expr.interp (@ident_interp) (UnderLets.interp (@ident_interp) (@annotate_with_ident is_let_bound t st e))
+            = expr.interp (@ident_interp) e.
+        Proof using interp_annotate_ident.
+          cbv [annotate_with_ident]; break_innermost_match; cbn [expr.interp UnderLets.interp];
+            apply interp_update_annotation; assumption.
+        Qed.
+
+        Lemma interp_annotate_base is_let_bound (t : base.type.base) st e
+              (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.
+          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.
+
+        Lemma interp_annotate is_let_bound (t : base.type) st e
+              (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.
+          induction t; cbn [annotate]; auto using interp_annotate_base.
+          all: repeat first [ reflexivity
+                            | progress break_innermost_match
+                            | progress expr.invert_subst
+                            | progress cbn [fst snd UnderLets.interp expr.interp ident_interp] in *
+                            | rewrite !UnderLets.interp_splice
+                            | rewrite !UnderLets.interp_splice_list
+                            | rewrite !List.map_map
+                            | rewrite expr.interp_reify_list
+                            | apply interp_annotate_with_ident; assumption
+                            | progress intros
+                            | match goal with
+                              | [ H : context[expr.interp _ (reify_list _)] |- _ ] => rewrite expr.interp_reify_list in H
+                              | [ H : abstraction_relation' (_ * _) _ (_, _) |- _ ]
+                                => pose proof (abstract_interp_ident_Proper _ ident.fst ltac:(auto) _ _ H);
+                                  pose proof (abstract_interp_ident_Proper _ ident.snd ltac:(auto)_ _ H);
+                                  clear H
+                              | [ H : context[_ = _] |- _ = _ ] => rewrite H by assumption
+                              | [ |- List.map ?f (List.combine ?l1 ?l2) = List.map ?g ?l2 ]
+                                => transitivity (List.map g (List.map (@snd _ _) (List.combine l1 l2)));
+                                  [ rewrite List.map_map; apply List.map_ext_in
+                                  | rewrite map_snd_combine, List.firstn_all2; [ reflexivity | ] ]
+                              end ].
+          apply IHt.
+        Admitted.
+
+
         (*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)}
@@ -309,8 +416,8 @@ Module Compilers.
                 (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).
          *)
-        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_annotation).
-        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_annotation).
+        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 extract := (@ident.extract abstract_domain' abstract_interp_ident).
 
         Lemma interp_eval_with_bound
@@ -320,15 +427,15 @@ 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.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1
-                = type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e2) arg2)
+                type.app_curried (expr.interp (@ident_interp) (eval_with_bound 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),
                    abstraction_relation'
                      _
                      (extract e_st st)
-                     (type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1)).
-        Proof using Type. cbv [extract eval_with_bound]; apply interp_eval_with_bound'; assumption. Qed.
+                     (type.app_curried (expr.interp (@ident_interp) (eval_with_bound e1 st)) arg1)).
+        Proof. cbv [extract eval_with_bound]; apply interp_eval_with_bound'; auto using interp_annotate. Qed.
 
         Lemma interp_eta_expand_with_bound
               {t} (e1 e2 : expr t)
@@ -337,8 +444,8 @@ 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) b_in arg1),
-            type.app_curried (interp (eta_expand_with_bound e1 b_in)) arg1 = type.app_curried (interp e2) arg2.
-        Proof. cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto. Qed.
+            type.app_curried (expr.interp (@ident_interp) (eta_expand_with_bound e1 b_in)) arg1 = type.app_curried (expr.interp (@ident_interp) e2) arg2.
+        Proof. cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto using interp_annotate. Qed.
 
 (*
         Definition eval {t} (e : @expr value_with_lets t) : @expr var t
@@ -393,10 +500,17 @@ Module Compilers.
         rewrite Bool.andb_true_iff; split; auto.
       Qed.
 
-      Lemma abstract_interp_ident_related {t} (idc : ident t)
-        : type.related_hetero (@abstraction_relation') (@abstract_interp_ident t idc) (ident.interp idc).
+      Lemma invert_is_annotation t idc
+        : is_annotation t idc = true
+          -> (exists r, existT _ t idc = existT _ (base.type.Z -> base.type.Z)%etype (ident.Z_cast r))
+            \/ (exists r, existT _ t idc = existT _ (base.type.Z * base.type.Z -> base.type.Z * base.type.Z)%etype (ident.Z_cast2 r)).
+      Proof. destruct idc; cbn [is_annotation]; try discriminate; eauto. Qed.
+
+      Lemma abstract_interp_ident_related cast_outside_of_range {t} (idc : ident t)
+            (not_cast : is_annotation _ idc = false)
+        : type.related_hetero (@abstraction_relation') (@abstract_interp_ident t idc) (@ident.gen_interp cast_outside_of_range _ idc).
       Proof.
-        destruct idc; cbv [abstract_interp_ident abstraction_relation'].
+        destruct idc; cbv [abstract_interp_ident abstraction_relation']; cbn [is_annotation] in *; try discriminate.
         all: cbv [type.related_hetero ZRange.ident.option.interp ident.interp ident.gen_interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some].
       Admitted.
 
@@ -449,6 +563,7 @@ Module Compilers.
         := @partial.ident.extract abstract_domain' abstract_interp_ident t (e _) bound.
        *)
 
+      Local Hint Resolve interp_annotate_ident interp_update_literal_with_state abstract_interp_ident_related.
 
       Lemma interp_eval_with_bound
             cast_outside_of_range
@@ -484,7 +599,7 @@ Module Compilers.
       Proof.
         cbv [partial.eta_expand_with_bound]; intros arg1 arg2 Harg12 Harg1.
         eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1.
-        { apply ident.interp_eta_expand_with_bound with (abstraction_relation':=@abstraction_relation'); eauto. }
+        { apply ident.interp_eta_expand_with_bound with (is_annotation:=is_annotation) (abstraction_relation':=@abstraction_relation'); eauto. }
         { apply ZRange.type.option.is_bounded_by_impl_related_hetero. }
       Qed.
 
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationWf.v b/src/Experiments/NewPipeline/AbstractInterpretationWf.v
index c0938e7d5..5478fb14e 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationWf.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationWf.v
@@ -282,13 +282,14 @@ Module Compilers.
                 (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_annotation : forall t, ident t -> bool).
+                (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).
         Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R).
         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).
 
@@ -299,22 +300,22 @@ Module Compilers.
         Section with_var2.
           Context {var1 var2 : type -> Type}.
 
-          Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation).
-          Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation).
-          Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          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 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 reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom').
           Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom').
 
           Lemma wf_update_annotation G {t} st1 st2 (Hst : abstract_domain'_R t st1 st2) e1 e2 (He : expr.wf G e1 e2)
             : expr.wf G (@update_annotation1 t st1 e1) (@update_annotation2 t st2 e2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper is_annotated_for_Proper.
             cbv [ident.update_annotation];
               repeat first [ progress subst
                            | progress expr.invert_subst
@@ -335,8 +336,10 @@ Module Compilers.
                            | progress type_beq_to_eq
                            | progress type.inversion_type
                            | progress base.type.inversion_type
+                           | discriminate
                            | match goal with
-                             | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H; clear dependent x
+                             | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H
+                             | [ H : abstract_domain'_R _ ?x _, H' : context[?x] |- _ ] => rewrite !H in H'
                              end
                            | progress wf_safe_t
                            | break_innermost_match_step ].
@@ -347,7 +350,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_with_ident1 is_let_bound t v1 e1) (@annotate_with_ident2 is_let_bound t v2 e2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper is_annotated_for_Proper.
             cbv [ident.annotate_with_ident]; break_innermost_match; repeat constructor; apply wf_update_annotation; assumption.
           Qed.
 
@@ -356,7 +359,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.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper update_literal_with_state_Proper is_annotated_for_Proper.
             cbv [ident.annotate_base];
               repeat first [ apply wf_annotate_with_ident
                            | break_innermost_match_step
@@ -383,7 +386,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.
+          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.
             revert dependent G; induction t; intros;
               cbn [ident.annotate]; try apply wf_annotate_base; trivial.
             all: repeat first [ lazymatch goal with
@@ -459,7 +462,7 @@ Module Compilers.
 
           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.
+          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.
             cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain].
             split.
             { exact (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl). }
@@ -565,7 +568,7 @@ Module Compilers.
 
           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.
+          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.
             constructor; eapply wf_reflect;
               solve [ apply bottom'_Proper
                     | apply wf_annotate
@@ -575,41 +578,41 @@ Module Compilers.
 
           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.
+          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.
             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_annotation).
-          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_annotation).
+          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)
                 (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.
+          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.
             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_annotation).
-          Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          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).
           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.
+          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.
             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_annotation).
-          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_annotation).
+          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).
           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.
+          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.
             eapply wf_eta_expand_with_bound';
               solve [ eassumption
                     | eapply wf_annotate
@@ -672,6 +675,9 @@ Module Compilers.
         intros st st' ?; subst st'; cbv [option_eq extract_list_state]; break_innermost_match; reflexivity.
       Qed.
 
+      Global Instance is_annotated_for_Proper {t t'} : Proper (eq ==> abstract_domain'_R _ ==> eq) (@is_annotated_for t t') | 10.
+      Proof. repeat intro; subst; reflexivity. Qed.
+
       Lemma 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).
       Proof.