Finish relax interp proofs

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
17m50.60s | Total                                                                | 17m59.23s || -0m08.63s | -0.80%
--------------------------------------------------------------------------------------------------------------------
0m02.92s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m07.06s  || -0m04.13s | -58.64%
5m55.40s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m56.43s  || -0m01.03s | -0.28%
0m38.25s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m40.00s  || -0m01.75s | -4.37%
0m23.76s  | p384_32.c                                                            | 0m25.24s  || -0m01.47s | -5.86%
4m32.74s  | Experiments/NewPipeline/Toplevel1                                    | 4m31.77s  || +0m00.97s | +0.35%
1m36.34s  | Experiments/NewPipeline/Toplevel2                                    | 1m35.98s  || +0m00.36s | +0.37%
0m38.76s  | p521_32.c                                                            | 0m38.53s  || +0m00.22s | +0.59%
0m37.08s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.15s  || -0m00.07s | -0.18%
0m35.15s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.38s  || +0m00.76s | +2.23%
0m32.29s  | p521_64.c                                                            | 0m32.14s  || +0m00.14s | +0.46%
0m20.50s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.86s  || -0m00.35s | -1.72%
0m18.69s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.91s  || -0m00.21s | -1.16%
0m13.51s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.95s  || -0m00.43s | -3.15%
0m12.46s  | Experiments/NewPipeline/CStringification                             | 0m12.60s  || -0m00.13s | -1.11%
0m10.36s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.52s  || -0m00.16s | -1.52%
0m08.55s  | p384_64.c                                                            | 0m08.77s  || -0m00.21s | -2.50%
0m08.52s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.83s  || -0m00.31s | -3.51%
0m05.38s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.43s  || -0m00.04s | -0.92%
0m05.34s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.42s  || -0m00.08s | -1.47%
0m04.01s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.85s  || +0m00.15s | +4.15%
0m03.88s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.08s  || -0m00.20s | -4.90%
0m03.77s  | secp256k1_32.c                                                       | 0m03.83s  || -0m00.06s | -1.56%
0m03.76s  | p256_32.c                                                            | 0m03.80s  || -0m00.04s | -1.05%
0m03.18s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.25s  || -0m00.06s | -2.15%
0m02.10s  | p224_32.c                                                            | 0m02.14s  || -0m00.04s | -1.86%
0m02.03s  | curve25519_32.c                                                      | 0m02.06s  || -0m00.03s | -1.45%
0m01.60s  | p256_64.c                                                            | 0m01.67s  || -0m00.06s | -4.19%
0m01.59s  | p224_64.c                                                            | 0m01.58s  || +0m00.01s | +0.63%
0m01.53s  | secp256k1_64.c                                                       | 0m01.68s  || -0m00.14s | -8.92%
0m01.42s  | Experiments/NewPipeline/CLI                                          | 0m01.38s  || +0m00.04s | +2.89%
0m01.38s  | curve25519_64.c                                                      | 0m01.39s  || -0m00.01s | -0.71%
0m01.16s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.21s  || -0m00.05s | -4.13%
0m01.16s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.25s  || -0m00.09s | -7.20%
0m01.02s  | Experiments/NewPipeline/CompilersTestCases                           | 0m01.03s  || -0m00.01s | -0.97%
0m01.01s  | Experiments/NewPipeline/AbstractInterpretation                       | 0m01.07s  || -0m00.06s | -5.60%

4 files changed, 293 insertions, 154 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 9d07eb1c4..4d9673eb1 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -987,24 +987,40 @@ Module Compilers.
         := @partial.ident.extract abstract_domain' abstract_interp_ident t (e _) bound.
     End specialized.
   End partial.
-
   Import defaults.
 
+  Module Import CheckCasts.
+    Fixpoint get_casts {t} (e : expr t) : list { t : _ & ident t }
+      := match e with
+         | expr.Ident t idc => if partial.is_annotation _ idc then [existT _ t idc] else nil
+         | expr.Var t v => v
+         | expr.Abs s d f => @get_casts _ (f nil)
+         | expr.App s d f x => @get_casts _ f ++ @get_casts _ x
+         | expr.LetIn A B x f => @get_casts _ x ++ @get_casts _ (f nil)
+         end%list.
+
+    Definition GetUnsupportedCasts {t} (e : Expr t) : list { t : _ & ident t }
+      := get_casts (e _).
+  End CheckCasts.
+
   Module RelaxZRange.
     Module ident.
       Section relax.
         Context (relax_zrange : zrange -> option zrange).
 
-        Definition relax {t} (idc : ident t) : option (ident t)
-          := match idc in ident.ident t return option (ident t) with
+        Let always_relax_zrange : zrange -> zrange
+          := fun range => match relax_zrange range with
+                          | Some r => r
+                          | None => range
+                          end.
+
+        Definition relax {t} (idc : ident t) : ident t
+          := match idc in ident.ident t return ident t with
              | ident.Z_cast range
-               => (r <- relax_zrange range;
-                    Some (ident.Z_cast r))
+               => ident.Z_cast (always_relax_zrange range)
              | ident.Z_cast2 (r1, r2)
-               => (r1 <- relax_zrange r1;
-                    r2 <- relax_zrange r2;
-                    Some (ident.Z_cast2 (r1, r2)))
-             | _ => None
+               => ident.Z_cast2 (always_relax_zrange r1, always_relax_zrange r2)
+             | idc => idc
              end%option.
       End relax.
     End ident.
@@ -1018,24 +1034,12 @@ Module Compilers.
           Fixpoint relax {t} (e : @expr var t) : @expr var t
             := match e with
                | expr.Var _ _ as e
-               | expr.Ident _ _ as e
                  => e
+               | expr.Ident t idc
+                 => expr.Ident (ident.relax relax_zrange idc)
                | expr.Abs s d f => expr.Abs (fun v => @relax d (f v))
                | expr.LetIn tx tC ex eC => expr.LetIn (@relax tx ex) (fun v => @relax tC (eC v))
-               | expr.App s d f x
-                 => let f' := @relax _ f in
-                    let x' := @relax _ x in
-                    match s, d return expr (s -> d) -> expr s -> expr d with
-                    | type.base base.type.Z, type.base base.type.Z
-                    | type.base (base.type.Z * base.type.Z)%etype, type.base (base.type.Z * base.type.Z)%etype
-                      => fun f x
-                         => match option_map (ident.relax relax_zrange)
-                                             (invert_Ident f) with
-                            | Some (Some idc) => expr.App (expr.Ident idc) x
-                            | _ => expr.App f x
-                            end
-                    | _, _ => expr.App
-                    end f' x'
+               | expr.App s d f x => expr.App (@relax _ f) (@relax _ x)
                end.
         End with_var.
 
@@ -1055,24 +1059,30 @@ Module Compilers.
     := partial.EtaExpandWithListInfoFromBound (GeneralizeVar.GeneralizeVar (e _)) bound.
 
   Definition CheckPartialEvaluateWithBounds
+             {A}
              (relax_zrange : zrange -> option zrange)
              {t} (E : Expr t)
              (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
              (b_out : ZRange.type.base.option.interp (type.final_codomain t))
-    : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t)
+    : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + A)
     := let b_computed := partial.Extract E b_in in
        if ZRange.type.base.option.is_tighter_than b_computed b_out
        then @inl (Expr t) _ (RelaxZRange.expr.Relax relax_zrange E)
-       else @inr _ (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) (b_computed, E).
+       else inr (@inl (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) _ (b_computed, E)).
 
   Definition CheckedPartialEvaluateWithBounds
              (relax_zrange : zrange -> option zrange)
              {t} (E : Expr t)
              (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
              (b_out : ZRange.type.base.option.interp (type.final_codomain t))
-    : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t)
-    := let E := PartialEvaluateWithBounds E b_in in
-       dlet_nd e := GeneralizeVar.ToFlat E in
-             let E := GeneralizeVar.FromFlat e in
-             CheckPartialEvaluateWithBounds relax_zrange E b_in b_out.
+    : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + list { t : _ & ident t })
+    := dlet_nd e := GeneralizeVar.ToFlat E in
+       let E := GeneralizeVar.FromFlat e in
+       match CheckCasts.GetUnsupportedCasts E with
+       | nil => (let E := PartialEvaluateWithBounds E b_in in
+                 dlet_nd e := GeneralizeVar.ToFlat E in
+                 let E := GeneralizeVar.FromFlat e in
+                 CheckPartialEvaluateWithBounds relax_zrange E b_in b_out)
+       | unsupported_casts => inr (inr unsupported_casts)
+       end.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index b50064e9c..66ed19540 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -18,6 +18,7 @@ Require Import Crypto.Util.Tactics.SplitInContext.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.SpecializeAllWays.
+Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Experiments.NewPipeline.Language.
 Require Import Crypto.Experiments.NewPipeline.LanguageInversion.
 Require Import Crypto.Experiments.NewPipeline.LanguageWf.
@@ -45,19 +46,147 @@ Module Compilers.
       Let type_base (x : base_type) : type := type.base x.
       Local Coercion type_base : base_type >-> type.
       Context {ident : type -> Type}.
-      Local Notation expr := (@expr base_type ident).
       Local Notation Expr := (@expr.Expr base_type ident).
-      Local Notation UnderLets := (@UnderLets base_type ident).
-      Context (abstract_domain' : base_type -> Type)
+      Context (abstract_domain' base_interp : base_type -> Type)
+              (abstraction_relation' : forall t, abstract_domain' t -> base_interp t -> Prop)
               (bottom' : forall A, abstract_domain' A)
+              (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v)
               (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
-              (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop)
-              {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)}.
+              (interp_ident : forall t, ident t -> type.interp base_interp t)
+              (interp_ident_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (interp_ident t idc)).
       Local Notation abstract_domain := (@abstract_domain base_type abstract_domain').
+      Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop
+        := type.related_hetero (@abstraction_relation').
       Local Notation bottom := (@bottom base_type abstract_domain' (@bottom')).
       Local Notation bottom_for_each_lhs_of_arrow := (@bottom_for_each_lhs_of_arrow base_type abstract_domain' (@bottom')).
-      Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R).
+      Local Notation var := (type.interp base_interp).
+      Local Notation expr := (@expr base_type ident var).
+      Local Notation UnderLets := (@UnderLets base_type ident var).
+      Local Notation value := (@value base_type ident var abstract_domain').
+      Local Notation value_with_lets := (@value_with_lets base_type ident var abstract_domain').
+      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 t -> UnderLets (expr t)).
+      (*
+      Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom').
+      Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom').
+      Local Notation reflect1 := (@reflect base_type ident var1 abstract_domain' annotate1 bottom').
+      Local Notation reflect2 := (@reflect base_type ident var2 abstract_domain' annotate2 bottom').
+      Local Notation interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
+      Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
+      Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
+      Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
+      Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
+      Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
+      Local Notation eta_expand_with_bound'1 := (@eta_expand_with_bound' base_type ident var1 abstract_domain' annotate1 bottom').
+      Local Notation eta_expand_with_bound'2 := (@eta_expand_with_bound' base_type ident var2 abstract_domain' annotate2 bottom').
+*)
+(*
+
+      Fixpoint value (t : type)
+        := (abstract_domain t
+            * match t return Type (* COQBUG(https://github.com/coq/coq/issues/7727) *) with
+              | type.base t
+                => @expr var t
+              | type.arrow s d
+                => value s -> UnderLets (value d)
+              end)%type.
+
+      Definition value_with_lets (t : type)
+        := UnderLets (value t).
+
+
+      Fixpoint bottom {t} : abstract_domain t
+        := match t with
+           | type.base t => bottom' t
+           | type.arrow s d => fun _ => @bottom d
+           end.
+
+      Fixpoint bottom_for_each_lhs_of_arrow {t} : type.for_each_lhs_of_arrow abstract_domain t
+        := match t return type.for_each_lhs_of_arrow abstract_domain t with
+           | type.base t => tt
+           | type.arrow s d => (bottom, @bottom_for_each_lhs_of_arrow d)
+           end.
+
+      Definition state_of_value {t} : value t -> abstract_domain t
+        := match t return value t -> abstract_domain t with
+           | type.base t => fun '(st, v) => st
+           | type.arrow s d => fun '(st, v) => st
+           end.
+
+      Fixpoint reify (is_let_bound : bool) {t} : value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t)
+        := match t return value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) with
+           | type.base t
+             => fun '(st, v) 'tt
+                => annotate is_let_bound t st v
+           | type.arrow s d
+             => fun '(f_st, f_e) '(sv, dv)
+                => Base
+                     (λ x , (UnderLets.to_expr
+                               (fx <-- f_e (@reflect _ (expr.Var x) sv);
+                                  @reify false _ fx dv)))
+           end%core%expr
+      with reflect {t} : @expr var t -> abstract_domain t -> value t
+           := match t return @expr var t -> abstract_domain t -> value t with
+              | type.base t
+                => fun e st => (st, e)
+              | type.arrow s d
+                => fun e absf
+                   => (absf,
+                       (fun v
+                        => let stv := state_of_value v in
+                           (rv <-- (@reify false s v bottom_for_each_lhs_of_arrow);
+                              Base (@reflect d (e @ rv) (absf stv))%expr)))
+              end%under_lets.
+
+      (* N.B. Because the [App] case only looks at the second argument
+              of arrow-values, we are free to set the state of [Abs]
+              nodes to [bottom], because for any [Abs] nodes which are
+              actually applied (here and in places where we don't
+              rewrite), we just drop it. *)
+      Fixpoint interp {t} (e : @expr value_with_lets t) : value_with_lets t
+        := match e in expr.expr t return value_with_lets t with
+           | expr.Ident t idc => interp_ident _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*)
+           | expr.Var t v => v
+           | expr.Abs s d f => Base (bottom, fun x => @interp d (f (Base x)))
+           | expr.App s d f x
+             => (x' <-- @interp s x;
+                   f' <-- @interp (s -> d)%etype f;
+                   snd f' x')
+           | expr.LetIn (type.arrow _ _) B x f
+             => (x' <-- @interp _ x;
+                   @interp _ (f (Base x')))
+           | expr.LetIn (type.base A) B x f
+             => (x' <-- @interp _ x;
+                   x'' <-- reify true (* this forces a let-binder here *) x' tt;
+                   @interp _ (f (Base (reflect x'' (state_of_value x')))))
+           end%under_lets.
+
+      Definition eval_with_bound' {t} (e : @expr value_with_lets t)
+                 (st : type.for_each_lhs_of_arrow abstract_domain t)
+        : expr t
+        := UnderLets.to_expr (e' <-- interp e; reify false e' st).
+
+      Definition eval' {t} (e : @expr value_with_lets t) : expr t
+        := eval_with_bound' e bottom_for_each_lhs_of_arrow.
+
+      Definition eta_expand_with_bound' {t} (e : @expr var t)
+                 (st : type.for_each_lhs_of_arrow abstract_domain t)
+        : expr t
+        := UnderLets.to_expr (reify false (reflect e bottom) st).
+
+      Section extract.
+        Context (ident_extract : forall t, ident t -> abstract_domain t).
+
+        Definition extract' {t} (e : @expr abstract_domain t) : abstract_domain t
+          := expr.interp (@ident_extract) e.
+
+        Definition extract_gen {t} (e : @expr abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t)
+          : abstract_domain' (type.final_codomain t)
+          := type.app_curried (extract' e) bound.
+      End extract.
+    End with_var.
+
+
 
       Section extract.
         Context (ident_extract : forall t, ident t -> abstract_domain t)
@@ -82,8 +211,9 @@ Module Compilers.
           eapply extract'_Proper; eassumption.
         Qed.
       End extract.
+*)
     End with_type.
-
+(*
     Module ident.
       Import defaults.
       Local Notation UnderLets := (@UnderLets base.type ident).
@@ -118,7 +248,7 @@ Module Compilers.
         End extract.
       End with_type.
     End ident.
-
+*)
     Section specialized.
       Import defaults.
       Local Notation abstract_domain' := ZRange.type.base.option.interp (only parsing).
@@ -201,58 +331,91 @@ Module Compilers.
   End partial.
   Import defaults.
 
+  Module Import CheckCasts.
+    Module ident.
+      Lemma interp_eqv_without_casts t idc
+            cast_outside_of_range1 cast_outside_of_range2
+            (Hc : partial.is_annotation t idc = false)
+      : ident.gen_interp cast_outside_of_range1 idc
+        == ident.gen_interp cast_outside_of_range2 idc.
+      Proof.
+        generalize (@ident.gen_interp_Proper cast_outside_of_range1 t idc idc eq_refl);
+          destruct idc; try exact id; cbn in Hc; discriminate.
+      Qed.
+    End ident.
+
+    Lemma interp_eqv_without_casts
+          cast_outside_of_range1 cast_outside_of_range2
+          G {t} e1 e2 e3
+          (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G -> v2 == v3)
+          (Hwf : expr.wf3 G e1 e2 e3)
+          (Hc : @CheckCasts.get_casts t e1 = nil)
+    : expr.interp (@ident.gen_interp cast_outside_of_range1) e2
+      == expr.interp (@ident.gen_interp cast_outside_of_range2) e3.
+    Proof.
+      induction Hwf;
+        repeat first [ progress cbn [CheckCasts.get_casts] in *
+                     | discriminate
+                     | match goal with
+                       | [ H : (_ ++ _)%list = nil |- _ ] => apply List.app_eq_nil in H
+                       end
+                     | progress destruct_head'_and
+                     | progress break_innermost_match_hyps
+                     | progress interp_safe_t
+                     | solve [ eauto using ident.interp_eqv_without_casts ] ].
+    Qed.
+
+    Lemma Interp_WithoutUnsupportedCasts {t} (e : Expr t)
+          (Hc : CheckCasts.GetUnsupportedCasts e = nil)
+          (Hwf : expr.Wf3 e)
+          cast_outside_of_range1 cast_outside_of_range2
+      : expr.Interp (@ident.gen_interp cast_outside_of_range1) e
+        == expr.Interp (@ident.gen_interp cast_outside_of_range2) e.
+    Proof. eapply interp_eqv_without_casts with (G:=nil); wf_safe_t. Qed.
+  End CheckCasts.
+
   Module RelaxZRange.
+    Definition relaxed_cast_outside_of_range
+               (relax_zrange : zrange -> option zrange)
+               (cast_outside_of_range : zrange -> Z -> Z)
+    : zrange -> Z -> Z
+      := fun r v
+         => match relax_zrange r with
+            | Some r' => ident.cast cast_outside_of_range r' v
+            | None => cast_outside_of_range r v
+            end.
+
     Module ident.
       Section relax.
         Context (relax_zrange : zrange -> option zrange)
+                (cast_outside_of_range : zrange -> Z -> Z)
                 (Hrelax : forall r r' z, is_tighter_than_bool z r = true
                                          -> relax_zrange r = Some r'
                                          -> is_tighter_than_bool z r' = true).
 
-        Lemma interp_relax {t} (idc idc' : ident t)
-              (Hidc : @RelaxZRange.ident.relax relax_zrange t idc = Some idc')
-              v
-              (Hinterp : forall cast_outside_of_range, type.app_curried (ident.gen_interp cast_outside_of_range idc) v = type.app_curried (ident.interp idc) v)
-          : forall cast_outside_of_range, type.app_curried (ident.gen_interp cast_outside_of_range idc') v = type.app_curried (ident.interp idc) v.
+        Local Notation relaxed_cast_outside_of_range := (@relaxed_cast_outside_of_range relax_zrange cast_outside_of_range).
+
+        Lemma interp_relax {t} (idc : ident t)
+          : ident.gen_interp cast_outside_of_range (@RelaxZRange.ident.relax relax_zrange t idc)
+            == ident.gen_interp relaxed_cast_outside_of_range idc.
         Proof.
-          intro cast_outside_of_range.
-          pose proof (Hinterp (fun _ => id)).
-          pose proof (fun myrange => Hinterp (fun _ => cast_outside_of_range myrange)).
-          destruct idc; cbv [RelaxZRange.ident.relax Option.bind] in *; inversion_option; break_innermost_match_hyps; inversion_option; subst;
-            repeat match goal with
-                   | [ H : relax_zrange _ = Some _ |- _ ] => unique pose proof (fun zl zu pf => Hrelax _ _ (Build_zrange zl zu) pf H)
-                   end;
-            repeat first [ reflexivity
+          pose proof (@ident.gen_interp_Proper cast_outside_of_range t idc idc eq_refl) as Hp.
+          destruct idc; cbn [type.related] in *; repeat (let x := fresh "x" in intro x; specialize (Hp x));
+            repeat first [ assumption
+                         | reflexivity
                          | discriminate
                          | congruence
-                         | progress cbv [RelaxZRange.ident.relax Option.bind id ident.cast is_tighter_than_bool] in *
-                         | progress cbn [fst snd] in *
                          | progress subst
-                         | progress inversion_option
-                         | progress inversion_prod
+                         | progress cbv [relaxed_cast_outside_of_range RelaxZRange.ident.relax Option.bind ident.cast respectful is_tighter_than_bool id] in *
+                         | progress cbn [ident.gen_interp type.related type.interp base.interp upper lower] in *
                          | progress destruct_head'_prod
-                         | progress destruct_head'_and
-                         | progress cbn in *
-                         | progress Bool.split_andb
-                         | progress intros
+                         | progress specialize_by (exact eq_refl)
+                         | break_match_step ltac:(fun x => let h := head x in constr_eq h relax_zrange)
                          | match goal with
-                           | [ H : forall x, (_, _) = (_, _) |- _ ]
-                             => pose proof (fun x => f_equal (@fst _ _) (H x));
-                               pose proof (fun x => f_equal (@snd _ _) (H x));
-                               clear H
-                           | [ H : context[andb _ _ = true] |- _ ] => rewrite Bool.andb_true_iff in H || setoid_rewrite Bool.andb_true_iff in H
-                           | [ H : context[Z.leb _ _ = true] |- _ ] => rewrite Z.leb_le in H || setoid_rewrite Z.leb_le in H
-                           | [ H : forall a b, and (Z.le ?x a) (Z.le b ?y) -> _ /\ _, H' : Z.le ?x _, H'' : Z.le _ ?y |- _ ]
-                             => unique pose proof (proj1 (H _ _ (conj H' H'')));
-                                unique pose proof (proj2 (H _ _ (conj H' H'')))
+                           | [ H : relax_zrange ?r = Some ?r' |- context[Z.leb (lower ?r) ?v] ]
+                             => pose proof (fun pf => Hrelax _ _ (Build_zrange v v) pf H); clear H
                            end
-                         | progress rewrite ?Bool.andb_false_iff in *
-                         | progress destruct_head'_or
-                         | progress break_innermost_match_hyps
-                         | progress break_innermost_match
-                         | progress Z.ltb_to_lt
-                         | apply (f_equal2 (@pair _ _))
-                         | lia ].
+                         | break_innermost_match_step ].
         Qed.
       End relax.
     End ident.
@@ -262,63 +425,27 @@ Module Compilers.
         Context (relax_zrange : zrange -> option zrange)
                 (Hrelax : forall r r' z, is_tighter_than_bool z r = true
                                          -> relax_zrange r = Some r'
-                                         -> is_tighter_than_bool z r' = true).
-        Lemma interp_relax {t} (e : expr t)
-              v
-              (Hinterp : forall cast_outside_of_range, type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e) v
-                                                  = type.app_curried (defaults.interp e) v)
-          : forall cast_outside_of_range, type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.relax relax_zrange e)) v
-                                     = type.app_curried (defaults.interp e) v.
+                                         -> is_tighter_than_bool z r' = true)
+                (cast_outside_of_range : zrange -> Z -> Z).
+
+        Local Notation relaxed_cast_outside_of_range := (@relaxed_cast_outside_of_range relax_zrange cast_outside_of_range).
+
+        Lemma interp_relax G {t} (e1 e2 : expr t)
+              (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2)
+              (Hwf : expr.wf G e1 e2)
+          : expr.interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.relax relax_zrange e1)
+            == expr.interp (@ident.gen_interp relaxed_cast_outside_of_range) e2.
         Proof.
-          intro cast_outside_of_range; rewrite <- (Hinterp cast_outside_of_range); pose proof (Hinterp cast_outside_of_range).
-          induction e; cbn -[RelaxZRange.ident.relax] in *; interp_safe_t; cbv [option_map] in *;
+          induction Hwf; cbn -[RelaxZRange.ident.relax] in *; interp_safe_t; cbv [option_map] in *;
             break_innermost_match; cbn -[RelaxZRange.ident.relax] in *; interp_safe_t;
-              eauto using tt.
-          all: repeat first [ reflexivity
-                            | progress intros
-                            | progress specialize_by_assumption
-                            | progress cbn -[RelaxZRange.ident.relax] in *
-                            | match goal with
-                              | [ H : unit -> ?T |- _ ] => specialize (H tt)
-                              | [ H : forall x : _ * _, _ |- _ ] => specialize (fun a b => H (a, b))
-                              | [ e : expr (type.base (base.type.type_base base.type.unit)) |- _ ]
-                                => match goal with
-                                  | [ |- context[expr.interp ?ii e] ] => destruct (expr.interp ii e)
-                                  | [ H : context[expr.interp ?ii e] |- _ ] => destruct (expr.interp ii e)
-                                  end
-                              end
-                            | progress cbn [fst snd] in *
-                            | match goal with
-                              | [ H : _ |- _ ] => rewrite H
-                              end ].
-          all: specialize_all_ways.
-          all: repeat first [ reflexivity
-                            | progress intros
-                            | progress specialize_by_assumption
-                            | progress cbn -[RelaxZRange.ident.relax] in *
-                            | match goal with
-                              | [ H : unit -> ?T |- _ ] => specialize (H tt)
-                              | [ H : forall x : _ * _, _ |- _ ] => specialize (fun a b => H (a, b))
-                              | [ e : expr (type.base (base.type.type_base base.type.unit)) |- _ ]
-                                => match goal with
-                                  | [ |- context[expr.interp ?ii e] ] => destruct (expr.interp ii e)
-                                  | [ H : context[expr.interp ?ii e] |- _ ] => destruct (expr.interp ii e)
-                                  end
-                              end
-                            | progress cbn [fst snd] in *
-                            | match goal with
-                              | [ H : _ |- _ ] => rewrite H
-                              end ].
-        Admitted.
+              eauto using tt, @ident.interp_relax.
+        Qed.
 
         Lemma Interp_Relax {t} (e : Expr t)
-              (Hwf : expr.Wf3 e)
-              v
-              (Hinterp : forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) e) v
-                                                  = type.app_curried (defaults.Interp e) v)
-          : forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.Relax relax_zrange e)) v
-                                     = type.app_curried (defaults.Interp e) v.
-        Proof. eapply @interp_relax; try assumption. Qed.
+              (Hwf : Wf e)
+          : expr.Interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.Relax relax_zrange e)
+            == expr.Interp (@ident.gen_interp relaxed_cast_outside_of_range) e.
+        Proof. apply interp_relax with (G:=nil); wf_safe_t. Qed.
       End relax.
     End expr.
   End RelaxZRange.
@@ -336,11 +463,12 @@ Module Compilers.
         (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
         (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
       type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1
-      = type.app_curried (Interp E) arg2.
+      = type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) E) arg2.
   Proof.
   Admitted.
 
   Lemma Interp_PartialEvaluateWithBounds_bounded
+        cast_outside_of_range
         {t} (E : Expr t)
         (Hwf : Wf E)
         (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
@@ -348,7 +476,7 @@ Module Compilers.
         (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
       ZRange.type.base.option.is_bounded_by
         (partial.Extract (PartialEvaluateWithBounds E b_in) b_in)
-        (type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds E b_in)) arg1)
+        (type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1)
       = true.
   Proof.
   Admitted.
@@ -362,6 +490,7 @@ Module Compilers.
         (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
       type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds E b_in)) arg1 = type.app_curried (Interp E) arg2.
   Proof.
+    cbv [PartialEvaluateWithListInfoFromBounds].
   Admitted.
 
   Theorem CheckedPartialEvaluateWithBounds_Correct
@@ -385,6 +514,14 @@ Module Compilers.
   Proof.
     cbv [CheckedPartialEvaluateWithBounds CheckPartialEvaluateWithBounds Let_In] in *;
       break_innermost_match_hyps; inversion_sum; subst.
+    let H := lazymatch goal with H : _ = nil |- _ => H end in
+    pose proof (@Interp_WithoutUnsupportedCasts _ _ H ltac:(solve [ auto with wf ])) as H'; clear H;
+      assert (forall cast_outside_of_range1 cast_outside_of_range2,
+                 expr.Interp (@ident.gen_interp cast_outside_of_range1) E == expr.Interp (@ident.gen_interp cast_outside_of_range2) E)
+      by (intros c1 c2; specialize (H' c1 c2);
+          rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat in H' by eauto with wf typeclass_instances;
+          assumption).
+    clear H'.
     split.
     { intros arg1 arg2 Harg12 Harg1.
       assert (arg1_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg1)
@@ -398,6 +535,8 @@ Module Compilers.
                         | rewrite RelaxZRange.expr.Interp_Relax; eauto
                         | erewrite !Interp_PartialEvaluateWithBounds
                         | solve [ eauto with wf ]
+                        | apply type.app_curried_Proper
+                        | apply expr.Wf_Interp_Proper_gen
                         | progress intros ]. }
     { auto with wf. }
   Qed.
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationWf.v b/src/Experiments/NewPipeline/AbstractInterpretationWf.v
index 69844c8ef..c0938e7d5 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationWf.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationWf.v
@@ -777,23 +777,6 @@ Module Compilers.
           Proof using Type.
             clear -Hwf.
             induction Hwf; wf_safe_t.
-            cbn [RelaxZRange.expr.relax]; cbv [option_map] in *.
-            break_innermost_match;
-              repeat first [ progress wf_safe_t
-                           | progress expr.invert_subst
-                           | progress expr.inversion_wf_constr
-                           | progress destruct_head' False
-                           | progress inversion_option
-                           | progress cbn [invert_Ident invert_Var invert_Abs invert_App invert_LetIn] in *
-                           | match goal with
-                             | [ H : context[RelaxZRange.expr.relax ?r ?x], H' : RelaxZRange.expr.relax ?r ?x = _ |- _ ]
-                               => rewrite H' in H
-                             | [ H : context[match RelaxZRange.expr.relax ?r ?x with _ => _ end] |- _ ]
-                               => remember (RelaxZRange.expr.relax r x) in *; progress expr.invert_match
-                             | [ H : ?x = Some ?a, H' : context[?x] |- _ ] => rewrite H in H'
-                             | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H'
-                             end
-                           | progress expr.inversion_wf_one_constr ].
           Qed.
         End with_var2.
 
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index e896e495f..626fb04f1 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -541,6 +541,7 @@ Module Pipeline.
   | Values_not_provably_distinctZ (descr : string) (lhs rhs : Z)
   | Values_not_provably_equalZ (descr : string) (lhs rhs : Z)
   | Values_not_provably_equal_listZ (descr : string) (lhs rhs : list Z)
+  | Unsupported_casts_in_input {t} (e : @Compilers.defaults.Expr t) (ls : list { t : _ & ident t })
   | Stringification_failed {t} (e : @Compilers.defaults.Expr t) (err : string)
   | Invalid_argument (msg : string).
 
@@ -647,6 +648,10 @@ Module Pipeline.
               | Values_not_provably_equalZ descr lhs rhs
               | Values_not_provably_equal_listZ descr lhs rhs
                 => ["Values not provably equal (" ++ descr ++ ") : expected " ++ show true lhs ++ " = " ++ show true rhs]
+              | Unsupported_casts_in_input t e ls
+                => ["Unsupported casts in input syntax tree:"]
+                     ++ show_lines false e
+                     ++ ["Unsupported casts: " ++ @show_list _ (fun p v => show p (projT2 v)) false ls]
               | Stringification_failed t e err => ["Stringification failed on the syntax tree:"] ++ show_lines false e ++ [err]
               | Invalid_argument msg
                 => ["Invalid argument:" ++ msg]%string
@@ -699,11 +704,13 @@ Module Pipeline.
                end in
       dlet_nd e := ToFlat E in
       let E := FromFlat e in
-      let E := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in
-      match E with
+      let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in
+      match E' with
       | inl E => Success E
-      | inr (b, E)
+      | inr (inl (b, E))
         => Error (Computed_bounds_are_not_tight_enough b out_bounds E arg_bounds)
+      | inr (inr unsupported_casts)
+        => Error (Unsupported_casts_in_input E unsupported_casts)
       end.
 
   Definition BoundsPipelineToStrings
@@ -807,7 +814,7 @@ Module Pipeline.
     cbv [BoundsPipeline Let_In bounds_goodT] in *;
       repeat match goal with
              | [ H : match ?x with _ => _ end = Success _ |- _ ]
-               => destruct x eqn:?; cbv beta iota in H; [ | destruct_head'_prod; congruence ];
+               => destruct x eqn:?; cbv beta iota in H; [ | break_innermost_match_hyps; congruence ];
                     let H' := fresh in
                     inversion H as [H']; clear H; rename H' into H
              end.
@@ -820,7 +827,7 @@ Module Pipeline.
                [ destruct H' as [H01 Hwf'] | .. ]
         end;
         [
-        | match goal with
+        | lazymatch goal with
           | [ |- Wf _ ] => idtac
           | _ => eassumption || reflexivity
           end.. ].