Parameterize rewriter proofs over cast-outside-of-range behavior

5 files changed, 397 insertions, 387 deletions

diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index b9f217c42..6102a97cc 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -1591,24 +1591,6 @@ Module Compilers.
 
   Notation reify_list := ident.reify_list.
 
-  Lemma interp_reify_list {t} ls
-    : interp (@reify_list _ t ls) = List.map interp ls.
-  Proof.
-    unfold reify_list.
-    induction ls as [|x xs IHxs]; cbn in *; [ reflexivity | ].
-    rewrite IHxs; reflexivity.
-  Qed.
-
-  Lemma interp_smart_Literal {t} v : expr.interp (@ident.interp) (@ident.smart_Literal _ t v) = v.
-  Proof.
-    cbv [ident.interp]; induction t; cbn [ident.smart_Literal expr.interp ident.gen_interp];
-      break_innermost_match; cbn [expr.interp ident.gen_interp].
-    { reflexivity. }
-    { apply f_equal2; auto. }
-    { etransitivity; [ rewrite interp_reify_list, map_map | apply map_id ].
-      apply map_ext; auto. }
-  Qed.
-
   Module GallinaReify.
     Module base.
       Section reify.
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 77561f246..36ffba237 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -714,6 +714,16 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
               reflexivity.
         Qed.
 
+        Lemma interp_smart_Literal {t} v : interp (@ident.smart_Literal _ t v) = v.
+        Proof.
+          cbv [ident.interp]; induction t; cbn [ident.smart_Literal expr.interp ident.gen_interp];
+            break_innermost_match; cbn [expr.interp ident.gen_interp].
+          { reflexivity. }
+          { apply f_equal2; auto. }
+          { etransitivity; [ rewrite interp_reify_list, map_map | apply map_id ].
+            apply map_ext; auto. }
+        Qed.
+
         Lemma interp_reify {t} v : interp (GallinaReify.base.reify (t:=t) v) = v.
         Proof.
           induction t; cbn [GallinaReify.base.reify]; break_innermost_match; cbn; f_equal;
diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v
index 650842f75..eddd3585f 100644
--- a/src/Experiments/NewPipeline/RewriterProofs.v
+++ b/src/Experiments/NewPipeline/RewriterProofs.v
@@ -51,7 +51,7 @@ Module Compilers.
     Local Ltac start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
       let Rewrite := lazymatch goal with
                      | [ |- Wf ?e ] => head e
-                     | [ |- Interp ?e == _ ] => head e
+                     | [ |- expr.Interp _ ?e == _ ] => head e
                      end in
       cbv [Rewrite]; rewrite rewrite_head_eq; cbv [rewrite_head0]; rewrite all_rewrite_rules_eq.
     Local Ltac start_Wf_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
@@ -86,32 +86,53 @@ Module Compilers.
       apply fancy_rewrite_rules_good; assumption.
     Qed.
 
-    Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e.
+    Lemma Interp_gen_RewriteNBE {cast_outside_of_range t} e (Hwf : Wf e)
+      : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteNBE t e)
+        == expr.Interp (@ident.gen_interp cast_outside_of_range) e.
     Proof.
       start_Interp_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0).
     Admitted.
-    Lemma Interp_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Interp (@RewriteArith max_const_val t e) == Interp e.
+    Lemma Interp_gen_RewriteArith {cast_outside_of_range} (max_const_val : Z) {t} e (Hwf : Wf e)
+      : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArith max_const_val t e)
+        == expr.Interp (@ident.gen_interp cast_outside_of_range) e.
     Proof.
       start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0).
     Admitted.
 
-    Lemma Interp_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z)
+    Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z)
           (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
           (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
           {t} e (Hwf : Wf e)
-      : Interp (@RewriteToFancy invert_low invert_high t e) == Interp e.
+      : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancy invert_low invert_high t e)
+        == expr.Interp (@ident.gen_interp cast_outside_of_range) e.
     Proof.
       start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0).
     Admitted.
+
+    Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e.
+    Proof. apply Interp_gen_RewriteNBE; assumption. Qed.
+    Lemma Interp_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e)
+      : Interp (@RewriteArith max_const_val t e) == Interp e.
+    Proof. apply Interp_gen_RewriteArith; assumption. Qed.
+    Lemma Interp_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z)
+          (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
+          (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
+          {t} e (Hwf : Wf e)
+      : Interp (@RewriteToFancy invert_low invert_high t e) == Interp e.
+    Proof. apply Interp_gen_RewriteToFancy; assumption. Qed.
   End RewriteRules.
 
   Lemma Wf_PartialEvaluate {t} e (Hwf : Wf e) : Wf (@PartialEvaluate t e).
   Proof. apply Wf_RewriteNBE, Hwf. Qed.
 
-  Lemma Interp_PartialEvaluate {t} e (Hwf : Wf e) : Interp (@PartialEvaluate t e) == Interp e.
-  Proof. apply Interp_RewriteNBE, Hwf. Qed.
+  Lemma Interp_gen_PartialEvaluate {cast_outside_of_range} {t} e (Hwf : Wf e)
+    : expr.Interp (@ident.gen_interp cast_outside_of_range) (@PartialEvaluate t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e.
+  Proof. apply Interp_gen_RewriteNBE, Hwf. Qed.
 
+  Lemma Interp_PartialEvaluate {t} e (Hwf : Wf e)
+    : Interp (@PartialEvaluate t e) == Interp e.
+  Proof. apply Interp_gen_PartialEvaluate; assumption. Qed.
 
   Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy : wf.
-  Hint Rewrite @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy : interp.
+  Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy : interp.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 7647b1f06..df35ffd40 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -23,6 +23,7 @@ Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.AddGetCarry.
 Require Import Crypto.Util.ZUtil.MulSplit.
 Require Import Crypto.Util.ZUtil.Zselect.
+Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SplitInContext.
@@ -57,274 +58,279 @@ Module Compilers.
 
   Module Import RewriteRules.
     Import Rewriter.Compilers.RewriteRules.
+    Section with_cast.
+      Context {cast_outside_of_range : zrange -> Z -> Z}.
 
-    Local Lemma rlist_rect_eq {var A P ivar} Pnil Pcons ls
-      : @rlist_rect var A P ivar Pnil Pcons ls
-        = match invert_expr.reflect_list ls with
-          | Some ls
-            => Some (list_rect
-                       (fun _ => _)
-                       Pnil
-                       (fun x xs rec => rec' <-- rec; Pcons x xs rec')
-                       ls)%under_lets
-          | None => None
-          end.
-    Proof. cbv [rlist_rect Compile.option_bind' Option.bind]; reflexivity. Qed.
+      Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
 
-    Local Lemma UnderLets_interp_list_rect {A P} Pnil Pcons ls
-      : UnderLets.interp
-          (@ident.interp)
-          (list_rect
-             (fun _ : list A => UnderLets.UnderLets base.type ident _ P)
-             Pnil
-             (fun x xs rec => rec' <-- rec; Pcons x xs rec')
-             ls)%under_lets
-        = list_rect
-            (fun _ => P)
-            (UnderLets.interp (@ident.interp) Pnil)
-            (fun x xs rec => UnderLets.interp (@ident.interp) (Pcons x xs rec))
-            ls.
-    Proof.
-      induction ls as [|x xs IHxs]; cbn [list_rect]; [ reflexivity | ].
-      rewrite UnderLets.interp_splice, IHxs; reflexivity.
-    Qed.
+      Local Lemma rlist_rect_eq {var A P ivar} Pnil Pcons ls
+        : @rlist_rect var A P ivar Pnil Pcons ls
+          = match invert_expr.reflect_list ls with
+            | Some ls
+              => Some (list_rect
+                         (fun _ => _)
+                         Pnil
+                         (fun x xs rec => rec' <-- rec; Pcons x xs rec')
+                         ls)%under_lets
+            | None => None
+            end.
+      Proof. cbv [rlist_rect Compile.option_bind' Option.bind]; reflexivity. Qed.
 
-    Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) (@pattern.ident.to_typed) (@ident.interp)).
+      Local Lemma UnderLets_interp_list_rect {A P} Pnil Pcons ls
+        : UnderLets.interp
+            (@ident_interp)
+            (list_rect
+               (fun _ : list A => UnderLets.UnderLets base.type ident _ P)
+               Pnil
+               (fun x xs rec => rec' <-- rec; Pcons x xs rec')
+               ls)%under_lets
+          = list_rect
+              (fun _ => P)
+              (UnderLets.interp (@ident_interp) Pnil)
+              (fun x xs rec => UnderLets.interp (@ident_interp) (Pcons x xs rec))
+              ls.
+      Proof.
+        induction ls as [|x xs IHxs]; cbn [list_rect]; [ reflexivity | ].
+        rewrite UnderLets.interp_splice, IHxs; reflexivity.
+      Qed.
 
-    Local Ltac do_cbv0 :=
-      cbv [id
-             Compile.rewrite_rules_interp_goodT
-             Compile.rewrite_rule_data_interp_goodT Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT' Compile.pattern_default_interp pattern.type.under_forall_vars_relation Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.forall2_type_of_list_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule_cps_id_hypsT Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related Compile.value'_interp_related].
-    Local Ltac do_cbv :=
-      do_cbv0;
-      cbv [List.map List.fold_right List.rev list_rect orb List.app].
+      Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) (@pattern.ident.to_typed) (@ident_interp)).
 
-    Local Ltac start_interp_good :=
-      do_cbv;
-      lazymatch goal with
-      | [ |- forall x p, In (@existT ?A ?P x p) ?ls -> @?Q x p ]
-        => let Q' := fresh in
-           pose Q as Q';
-           change (forall x p, In (@existT A P x p) ls -> Q' x p);
-           apply (@forall_In_existT A P Q' ls); cbn [projT1 projT2]; cbv [id];
-           subst Q'; cbn [projT1 projT2]
-      end;
-      do_cbv0;
-      repeat first [ progress intros
-                   | match goal with
-                     | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl)
-                     | [ |- True /\ _ ] => split; [ exact I | ]
-                     end
-                   | progress cbn [eq_rect] in * ];
-      cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.interp ident.gen_interp] in *.
+      Local Ltac do_cbv0 :=
+        cbv [id
+               Compile.rewrite_rules_interp_goodT
+               Compile.rewrite_rule_data_interp_goodT Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT' Compile.pattern_default_interp pattern.type.under_forall_vars_relation Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.forall2_type_of_list_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule_cps_id_hypsT Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related Compile.value'_interp_related].
+      Local Ltac do_cbv :=
+        do_cbv0;
+        cbv [List.map List.fold_right List.rev list_rect orb List.app].
 
-    Local Ltac interp_good_t_step :=
-      first [ reflexivity
-            | match goal with
-              | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
-              | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand
-              end
-            | progress cbn [expr.interp ident.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr] in *
-            | progress cbv [Compile.option_bind' respectful] in *
-            | progress fold (@type.interp _ base.interp)
-            | progress fold (@base.interp)
-            | match goal with
-              | [ |- context[List.map _ (Lists.List.repeat _ _)] ] => rewrite map_repeat
-              | [ |- context[List.map _ (List.map _ _)] ] => rewrite map_map
-              | [ |- context[List.map (fun x => x) _] ] => rewrite map_id
-              | [ |- context[List.map _ (List.rev _)] ] => rewrite map_rev
-              | [ |- context[List.map _ (firstn _ _)] ] => rewrite <- firstn_map
-              | [ |- context[List.map _ (skipn _ _)] ] => rewrite <- skipn_map
-              | [ |- context[List.length (List.map _ _)] ] => rewrite map_length
-              | [ |- context[List.combine (List.map _ _) _] ] => rewrite combine_map_l
-              | [ |- context[List.combine _ (List.map _ _)] ] => rewrite combine_map_r
-              | [ |- context[expr.interp _ (reify_list _)] ] => rewrite interp_reify_list
-              | [ |- context[expr.interp _ (UnderLets.to_expr ?e)] ] => rewrite UnderLets.interp_to_expr
-              | [ |- context[UnderLets.interp _ (UnderLets.splice_list _ _)] ] => rewrite UnderLets.interp_splice_list
-              | [ |- context[rlist_rect] ] => rewrite rlist_rect_eq
-              | [ |- context[UnderLets.interp _ (list_rect _ _ _ _)] ] => rewrite UnderLets_interp_list_rect
-              | [ |- context[UnderLets.interp _ (UnderLets.splice _ _)] ] => rewrite UnderLets.interp_splice
-              | [ |- context[list_rect _ _ _ (List.map _ _)] ] => rewrite list_rect_map
-              | [ |- list_rect _ _ _ _ = List.app ?ls1 ?ls2 ]
-                =>  rewrite (eq_app_list_rect ls1 ls2)
-              | [ |- list_rect _ _ _ _ = @flat_map ?A ?B ?f ?ls ]
-                =>  rewrite (@eq_flat_map_list_rect A B f ls)
-              | [ |- list_rect _ _ _ _ = @partition ?A ?f ?ls ]
-                =>  rewrite (@eq_partition_list_rect A f ls)
-              | [ |- list_rect _ _ _ _ = @List.map ?A ?B ?f ?ls ]
-                => rewrite (@eq_map_list_rect A B f ls)
-              | [ |- _ = @fold_right ?A ?B ?f ?v ?ls ]
-                =>  rewrite (@eq_fold_right_list_rect A B f v ls)
-              end
-            | progress intros
-            | progress subst
-            | progress inversion_option
-            | progress Z.ltb_to_lt
-            | progress split_andb
-            | match goal with
-              | [ |- Lists.List.repeat _ _ = Lists.List.repeat _ _ ] => apply f_equal2
-              | [ |- firstn _ _ = firstn _ _ ] => apply f_equal2
-              | [ |- skipn _ _ = skipn _ _ ] => apply f_equal2
-              | [ |- rev _ = rev _ ] => apply f_equal
-              | [ |- List.app ?l1 ?l2 = List.app ?l1' ?l2 ] => apply f_equal2
-              | [ |- List.app ?l1 ?l2 = List.app ?l1 ?l2' ] => apply f_equal2
-              | [ |- cons _ _ = cons _ _ ] => apply f_equal2
-              | [ |- list_rect _ ?Pnil ?Pcons ?ls = list_rect _ ?Pnil ?Pcons' ?ls ]
-                => apply list_rect_Proper; [ reflexivity | repeat intro | reflexivity ]
-              | [ |- bool_rect _ ?x ?y ?b = bool_rect _ ?x ?y ?b' ]
-                => apply f_equal3; [ reflexivity | reflexivity | solve [ repeat interp_good_t_step ] ]
-              | [ H : expr.wf _ ?v1 ?v2 |- expr.interp _ ?v1 = expr.interp _ ?v2 ]
-                => apply (expr.wf_interp_Proper _ _ _ H ltac:(assumption))
-              | [ |- ?R (?f (?g (if ?b then ?x else ?y))) (bool_rect ?A ?B ?C ?D) ]
-                => rewrite <- (@Bool.pull_bool_if _ _ g b), <- (@Bool.pull_bool_if _ _ f b);
-                   change (R (bool_rect _ (f (g x)) (f (g y)) b) (bool_rect A B C D))
-              | [ |- context[invert_expr.reflect_list ?ls] ]
-                => destruct (invert_expr.reflect_list ls) eqn:?; expr.invert_subst
-              | [ |- ?f (nth_default _ _ _) = _ ]
-                => rewrite <- (@map_nth_default_always _ _ f)
-              | [ |- map ?f ?ls = map ?g ?ls ] => apply map_ext_in
-              | [ |- List.map _ (update_nth _ _ _) = update_nth _ _ _ ] => apply map_update_nth_ext
-              | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
-              | [ H : forall v : unit, _ |- _ ] => specialize (H tt)
-              | [ H : _ = expr.interp ?ii ?v |- _ ] => is_var v; generalize dependent (expr.interp ii v); clear v
-              | [ |- bool_rect _ _ _ ?b = bool_rect _ _ _ ?b ]
-                => is_var b; destruct b; cbv [bool_rect]
-              | [ H : (forall x y, _ -> expr.interp _ (UnderLets.interp _ (?f1 x)) = expr.interp _ (UnderLets.interp _ (?f2 y)))
-                  |- expr.interp _ (UnderLets.interp _ (?f1 ?x1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2)) ]
-                => apply H
-              | [ H : (forall x y, _ -> forall x' y', _ -> expr.interp _ (UnderLets.interp _ (?f1 x x')) = expr.interp _ (UnderLets.interp _ (?f2 y y')))
-                  |- expr.interp _ (UnderLets.interp _ (?f1 ?x1 ?y1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2 ?y2)) ]
-                => apply H
-              | [ |- context G[rwhen ?v ?b] ]
-                => let c := constr:(rwhen v b) in
-                   let c := (eval cbv [rwhen] in c) in
-                   let G' := context G[c] in
-                   change G';
-                   destruct b eqn:?
-              | [ |- context G[rwhenl ?v ?b] ]
-                => let c := constr:(rwhenl v b) in
-                   let c := (eval cbv [rwhenl] in c) in
-                   let G' := context G[c] in
-                   change G';
-                   destruct b eqn:?
-              | [ H : negb ?b = true |- _ ] => rewrite (@Bool.negb_true_iff b) in H
-              | [ |- context[expr.interp ?ii ?v] ]
-                => is_var v; generalize dependent (expr.interp ii v); clear v; intro v
-              | [ |- context[Z.mul_split ?a ?b ?c] ]
-                => rewrite (surjective_pairing (Z.mul_split a b c)), Z.mul_split_div, Z.mul_split_mod
-              | [ |- context[Z.zselect] ] => rewrite Z.zselect_correct
-              | [ |- context[Z.sub_get_borrow_full ?a ?b ?c] ]
-                => rewrite (surjective_pairing (Z.sub_get_borrow_full a b c)), Z.sub_get_borrow_full_div, Z.sub_get_borrow_full_mod
-              | [ |- context[Z.sub_with_get_borrow_full ?a ?b ?c ?d] ]
-                => rewrite (surjective_pairing (Z.sub_with_get_borrow_full a b c d)), Z.sub_with_get_borrow_full_div, Z.sub_with_get_borrow_full_mod
-              | [ |- context[Z.add_get_carry_full ?a ?b ?c] ]
-                => rewrite (surjective_pairing (Z.add_get_carry_full a b c)), Z.add_get_carry_full_div, Z.add_get_carry_full_mod
-              | [ |- context[Z.add_with_get_carry_full ?a ?b ?c ?d] ]
-                => rewrite (surjective_pairing (Z.add_with_get_carry_full a b c d)), Z.add_with_get_carry_full_div, Z.add_with_get_carry_full_mod
-              | [ |- pair _ _ = pair _ _ ] => apply f_equal2
-              | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia
-              | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia
-              | [ |- Z.opp _ = Z.opp _ ] => apply f_equal
-              end
-            | match goal with
-              | [ |- context[?f (list_rect _ _ _ _)] ]
-                => match f with
-                   | expr.interp _ => idtac
-                   | Compile.reify_expr => idtac
-                   end;
-                   erewrite (@push_f_list_rect _ _ f)
-                     by (intros;
-                         repeat first [ progress cbn [expr.interp ident.interp ident.gen_interp UnderLets.interp Compile.reify_expr]
-                                      | rewrite UnderLets.interp_splice ];
-                         match goal with
-                         | [ |- ?LHS = ?Pcons' ?x ?xs ?rec ]
-                           => let LHS' := match (eval pattern x, xs, rec in LHS) with ?f _ _ _ => f end in
-                              unify Pcons' LHS'; reflexivity
-                         end)
-              | [ |- context[?f (nat_rect _ _ _ _)] ]
-                => match f with
-                   | expr.interp _ => idtac
-                   | UnderLets.interp _ => idtac
-                   | Compile.reify_expr => idtac
-                   end;
-                   erewrite (@push_f_nat_rect _ _ f)
-                     by (intros;
-                         repeat first [ progress cbn [expr.interp ident.interp ident.gen_interp UnderLets.interp Compile.reify_expr]
-                                      | rewrite UnderLets.interp_splice ];
-                         match goal with
-                         | [ |- ?LHS = ?PS' ?x ?rec ]
-                           => let LHS' := match (eval pattern x, rec in LHS) with ?f _ _ => f end in
-                              unify PS' LHS'; reflexivity
-                         end)
-              | [ |- ?f (list_rect _ _ _ _) = list_rect _ _ _ _ ]
-                => match f with
-                   | expr.interp _ => idtac
-                   | Compile.reify_expr => idtac
-                   end;
-                   erewrite (@push_f_list_rect _ _ f);
-                   [ apply list_rect_Proper; repeat intro; try reflexivity | ]
-              | [ |- ?f (nat_rect _ _ _ _) = nat_rect _ _ _ _ ]
-                => match f with
-                   | expr.interp _ => idtac
-                   | UnderLets.interp _ => idtac
-                   | Compile.reify_expr => idtac
-                   end;
-                   erewrite (@push_f_nat_rect _ _ f);
-                   [ apply nat_rect_Proper_nondep; repeat intro; try reflexivity | ]
-              end
-            | break_innermost_match_step
-            | break_innermost_match_hyps_step
-            | match goal with
-              | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))]
-                  |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ]
-                => apply H
-              | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith
-              | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith
-              | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r
-              | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H
-              | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ]
-                => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith
-              | [ |- _ = _ :> BinInt.Z ] => progress normalize_commutative_identifier Z.land Z.land_comm
-              | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => exfalso; apply H', H
-              | [ H : ?x = 2^Z.log2_up ?x - 1 |- context[2^Z.log2_up ?x - 1] ] => rewrite <- H
-              | [ H : ?x = 2^Z.log2 ?x, H' : context[2^Z.log2 ?x] |- _ = _ :> BinInt.Z ]
-                => rewrite <- H in H'
-              | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const
-              | [ |- ?f (?g (nat_rect _ _ _ ?n ?v)) = nat_rect _ _ _ ?n _ ]
-                => revert v; is_var n; induction n; intro v; cbn [nat_rect]
-              | [ |- _ mod ?x = _ mod ?x ]
-                => progress (push_Zmod; pull_Zmod)
-              | [ |- _ mod ?x = _ mod ?x ]
-                => apply f_equal2; (lia + nia)
-              | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast
-              end ].
+      Local Ltac start_interp_good :=
+        do_cbv;
+        lazymatch goal with
+        | [ |- forall x p, In (@existT ?A ?P x p) ?ls -> @?Q x p ]
+          => let Q' := fresh in
+             pose Q as Q';
+             change (forall x p, In (@existT A P x p) ls -> Q' x p);
+             apply (@forall_In_existT A P Q' ls); cbn [projT1 projT2]; cbv [id];
+             subst Q'; cbn [projT1 projT2]
+        end;
+        do_cbv0;
+        repeat first [ progress intros
+                     | match goal with
+                       | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl)
+                       | [ |- True /\ _ ] => split; [ exact I | ]
+                       end
+                     | progress cbn [eq_rect] in * ];
+        cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp] in *.
 
-    Lemma nbe_rewrite_rules_interp_good
-      : rewrite_rules_interp_goodT nbe_rewrite_rules.
-    Proof using Type.
-      Time start_interp_good.
-      Time all: repeat interp_good_t_step.
-    Qed.
+      Local Ltac interp_good_t_step :=
+        first [ reflexivity
+              | match goal with
+                | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
+                | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand
+                end
+              | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr] in *
+              | progress cbv [Compile.option_bind' respectful] in *
+              | progress fold (@type.interp _ base.interp)
+              | progress fold (@base.interp)
+              | match goal with
+                | [ |- context[List.map _ (Lists.List.repeat _ _)] ] => rewrite map_repeat
+                | [ |- context[List.map _ (List.map _ _)] ] => rewrite map_map
+                | [ |- context[List.map (fun x => x) _] ] => rewrite map_id
+                | [ |- context[List.map _ (List.rev _)] ] => rewrite map_rev
+                | [ |- context[List.map _ (firstn _ _)] ] => rewrite <- firstn_map
+                | [ |- context[List.map _ (skipn _ _)] ] => rewrite <- skipn_map
+                | [ |- context[List.length (List.map _ _)] ] => rewrite map_length
+                | [ |- context[List.combine (List.map _ _) _] ] => rewrite combine_map_l
+                | [ |- context[List.combine _ (List.map _ _)] ] => rewrite combine_map_r
+                | [ |- context[expr.interp _ (reify_list _)] ] => rewrite expr.interp_reify_list
+                | [ |- context[expr.interp _ (UnderLets.to_expr ?e)] ] => rewrite UnderLets.interp_to_expr
+                | [ |- context[UnderLets.interp _ (UnderLets.splice_list _ _)] ] => rewrite UnderLets.interp_splice_list
+                | [ |- context[rlist_rect] ] => rewrite rlist_rect_eq
+                | [ |- context[UnderLets.interp _ (list_rect _ _ _ _)] ] => rewrite UnderLets_interp_list_rect
+                | [ |- context[UnderLets.interp _ (UnderLets.splice _ _)] ] => rewrite UnderLets.interp_splice
+                | [ |- context[list_rect _ _ _ (List.map _ _)] ] => rewrite list_rect_map
+                | [ |- list_rect _ _ _ _ = List.app ?ls1 ?ls2 ]
+                  =>  rewrite (eq_app_list_rect ls1 ls2)
+                | [ |- list_rect _ _ _ _ = @flat_map ?A ?B ?f ?ls ]
+                  =>  rewrite (@eq_flat_map_list_rect A B f ls)
+                | [ |- list_rect _ _ _ _ = @partition ?A ?f ?ls ]
+                  =>  rewrite (@eq_partition_list_rect A f ls)
+                | [ |- list_rect _ _ _ _ = @List.map ?A ?B ?f ?ls ]
+                  => rewrite (@eq_map_list_rect A B f ls)
+                | [ |- _ = @fold_right ?A ?B ?f ?v ?ls ]
+                  =>  rewrite (@eq_fold_right_list_rect A B f v ls)
+                end
+              | progress intros
+              | progress subst
+              | progress inversion_option
+              | progress Z.ltb_to_lt
+              | progress split_andb
+              | match goal with
+                | [ |- Lists.List.repeat _ _ = Lists.List.repeat _ _ ] => apply f_equal2
+                | [ |- firstn _ _ = firstn _ _ ] => apply f_equal2
+                | [ |- skipn _ _ = skipn _ _ ] => apply f_equal2
+                | [ |- rev _ = rev _ ] => apply f_equal
+                | [ |- List.app ?l1 ?l2 = List.app ?l1' ?l2 ] => apply f_equal2
+                | [ |- List.app ?l1 ?l2 = List.app ?l1 ?l2' ] => apply f_equal2
+                | [ |- cons _ _ = cons _ _ ] => apply f_equal2
+                | [ |- list_rect _ ?Pnil ?Pcons ?ls = list_rect _ ?Pnil ?Pcons' ?ls ]
+                  => apply list_rect_Proper; [ reflexivity | repeat intro | reflexivity ]
+                | [ |- bool_rect _ ?x ?y ?b = bool_rect _ ?x ?y ?b' ]
+                  => apply f_equal3; [ reflexivity | reflexivity | solve [ repeat interp_good_t_step ] ]
+                | [ H : expr.wf _ ?v1 ?v2 |- expr.interp _ ?v1 = expr.interp _ ?v2 ]
+                  => apply (expr.wf_interp_Proper _ _ _ H ltac:(assumption))
+                | [ |- ?R (?f (?g (if ?b then ?x else ?y))) (bool_rect ?A ?B ?C ?D) ]
+                  => rewrite <- (@Bool.pull_bool_if _ _ g b), <- (@Bool.pull_bool_if _ _ f b);
+                     change (R (bool_rect _ (f (g x)) (f (g y)) b) (bool_rect A B C D))
+                | [ |- context[invert_expr.reflect_list ?ls] ]
+                  => destruct (invert_expr.reflect_list ls) eqn:?; expr.invert_subst
+                | [ |- ?f (nth_default _ _ _) = _ ]
+                  => rewrite <- (@map_nth_default_always _ _ f)
+                | [ |- map ?f ?ls = map ?g ?ls ] => apply map_ext_in
+                | [ |- List.map _ (update_nth _ _ _) = update_nth _ _ _ ] => apply map_update_nth_ext
+                | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
+                | [ H : forall v : unit, _ |- _ ] => specialize (H tt)
+                | [ H : _ = expr.interp ?ii ?v |- _ ] => is_var v; generalize dependent (expr.interp ii v); clear v
+                | [ |- bool_rect _ _ _ ?b = bool_rect _ _ _ ?b ]
+                  => is_var b; destruct b; cbv [bool_rect]
+                | [ H : (forall x y, _ -> expr.interp _ (UnderLets.interp _ (?f1 x)) = expr.interp _ (UnderLets.interp _ (?f2 y)))
+                    |- expr.interp _ (UnderLets.interp _ (?f1 ?x1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2)) ]
+                  => apply H
+                | [ H : (forall x y, _ -> forall x' y', _ -> expr.interp _ (UnderLets.interp _ (?f1 x x')) = expr.interp _ (UnderLets.interp _ (?f2 y y')))
+                    |- expr.interp _ (UnderLets.interp _ (?f1 ?x1 ?y1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2 ?y2)) ]
+                  => apply H
+                | [ |- context G[rwhen ?v ?b] ]
+                  => let c := constr:(rwhen v b) in
+                     let c := (eval cbv [rwhen] in c) in
+                     let G' := context G[c] in
+                     change G';
+                     destruct b eqn:?
+                | [ |- context G[rwhenl ?v ?b] ]
+                  => let c := constr:(rwhenl v b) in
+                     let c := (eval cbv [rwhenl] in c) in
+                     let G' := context G[c] in
+                     change G';
+                     destruct b eqn:?
+                | [ H : negb ?b = true |- _ ] => rewrite (@Bool.negb_true_iff b) in H
+                | [ |- context[expr.interp ?ii ?v] ]
+                  => is_var v; generalize dependent (expr.interp ii v); clear v; intro v
+                | [ |- context[Z.mul_split ?a ?b ?c] ]
+                  => rewrite (surjective_pairing (Z.mul_split a b c)), Z.mul_split_div, Z.mul_split_mod
+                | [ |- context[Z.zselect] ] => rewrite Z.zselect_correct
+                | [ |- context[Z.sub_get_borrow_full ?a ?b ?c] ]
+                  => rewrite (surjective_pairing (Z.sub_get_borrow_full a b c)), Z.sub_get_borrow_full_div, Z.sub_get_borrow_full_mod
+                | [ |- context[Z.sub_with_get_borrow_full ?a ?b ?c ?d] ]
+                  => rewrite (surjective_pairing (Z.sub_with_get_borrow_full a b c d)), Z.sub_with_get_borrow_full_div, Z.sub_with_get_borrow_full_mod
+                | [ |- context[Z.add_get_carry_full ?a ?b ?c] ]
+                  => rewrite (surjective_pairing (Z.add_get_carry_full a b c)), Z.add_get_carry_full_div, Z.add_get_carry_full_mod
+                | [ |- context[Z.add_with_get_carry_full ?a ?b ?c ?d] ]
+                  => rewrite (surjective_pairing (Z.add_with_get_carry_full a b c d)), Z.add_with_get_carry_full_div, Z.add_with_get_carry_full_mod
+                | [ |- pair _ _ = pair _ _ ] => apply f_equal2
+                | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia
+                | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia
+                | [ |- Z.opp _ = Z.opp _ ] => apply f_equal
+                end
+              | match goal with
+                | [ |- context[?f (list_rect _ _ _ _)] ]
+                  => match f with
+                     | expr.interp _ => idtac
+                     | Compile.reify_expr => idtac
+                     end;
+                     erewrite (@push_f_list_rect _ _ f)
+                       by (intros;
+                           repeat first [ progress cbn [expr.interp ident.gen_interp UnderLets.interp Compile.reify_expr]
+                                        | rewrite UnderLets.interp_splice ];
+                           match goal with
+                           | [ |- ?LHS = ?Pcons' ?x ?xs ?rec ]
+                             => let LHS' := match (eval pattern x, xs, rec in LHS) with ?f _ _ _ => f end in
+                                unify Pcons' LHS'; reflexivity
+                           end)
+                | [ |- context[?f (nat_rect _ _ _ _)] ]
+                  => match f with
+                     | expr.interp _ => idtac
+                     | UnderLets.interp _ => idtac
+                     | Compile.reify_expr => idtac
+                     end;
+                     erewrite (@push_f_nat_rect _ _ f)
+                       by (intros;
+                           repeat first [ progress cbn [expr.interp ident.gen_interp UnderLets.interp Compile.reify_expr]
+                                        | rewrite UnderLets.interp_splice ];
+                           match goal with
+                           | [ |- ?LHS = ?PS' ?x ?rec ]
+                             => let LHS' := match (eval pattern x, rec in LHS) with ?f _ _ => f end in
+                                unify PS' LHS'; reflexivity
+                           end)
+                | [ |- ?f (list_rect _ _ _ _) = list_rect _ _ _ _ ]
+                  => match f with
+                     | expr.interp _ => idtac
+                     | Compile.reify_expr => idtac
+                     end;
+                     erewrite (@push_f_list_rect _ _ f);
+                     [ apply list_rect_Proper; repeat intro; try reflexivity | ]
+                | [ |- ?f (nat_rect _ _ _ _) = nat_rect _ _ _ _ ]
+                  => match f with
+                     | expr.interp _ => idtac
+                     | UnderLets.interp _ => idtac
+                     | Compile.reify_expr => idtac
+                     end;
+                     erewrite (@push_f_nat_rect _ _ f);
+                     [ apply nat_rect_Proper_nondep; repeat intro; try reflexivity | ]
+                end
+              | break_innermost_match_step
+              | break_innermost_match_hyps_step
+              | match goal with
+                | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))]
+                    |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ]
+                  => apply H
+                | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith
+                | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith
+                | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r
+                | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H
+                | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ]
+                  => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith
+                | [ |- _ = _ :> BinInt.Z ] => progress normalize_commutative_identifier Z.land Z.land_comm
+                | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => exfalso; apply H', H
+                | [ H : ?x = 2^Z.log2_up ?x - 1 |- context[2^Z.log2_up ?x - 1] ] => rewrite <- H
+                | [ H : ?x = 2^Z.log2 ?x, H' : context[2^Z.log2 ?x] |- _ = _ :> BinInt.Z ]
+                  => rewrite <- H in H'
+                | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const
+                | [ |- ?f (?g (nat_rect _ _ _ ?n ?v)) = nat_rect _ _ _ ?n _ ]
+                  => revert v; is_var n; induction n; intro v; cbn [nat_rect]
+                | [ |- _ mod ?x = _ mod ?x ]
+                  => progress (push_Zmod; pull_Zmod)
+                | [ |- _ mod ?x = _ mod ?x ]
+                  => apply f_equal2; (lia + nia)
+                | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast
+                end ].
 
-    Axiom proof_admitted : False.
-    Local Notation admit := (match proof_admitted with end).
+      Lemma nbe_rewrite_rules_interp_good
+        : rewrite_rules_interp_goodT nbe_rewrite_rules.
+      Proof using Type.
+        Time start_interp_good.
+        Time all: repeat interp_good_t_step.
+      Qed.
 
-    Lemma arith_rewrite_rules_interp_good max_const
-      : rewrite_rules_interp_goodT (arith_rewrite_rules max_const).
-    Proof using Type.
-      Time start_interp_good.
-      Time all: try solve [ repeat interp_good_t_step; (lia + nia) ].
-      (* This is mainly for display *)
-      all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
-                        | progress subst
-                        | match goal with
-                          | [ H : context[expr.interp ?ii ?v] |- _ ]
-                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
-                          | [ |- context[expr.interp ?ii ?v] ]
-                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
-                          end ].
-      (* 9 subgoals (ID 30397)
+      Axiom proof_admitted : False.
+      Local Notation admit := (match proof_admitted with end).
 
+      Lemma arith_rewrite_rules_interp_good max_const
+        : rewrite_rules_interp_goodT (arith_rewrite_rules max_const).
+      Proof using Type.
+        Time start_interp_good.
+        Time all: try solve [ repeat interp_good_t_step; (lia + nia) ].
+        (* This is mainly for display *)
+        all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
+                          | progress subst
+                          | match goal with
+                            | [ H : context[expr.interp ?ii ?v] |- _ ]
+                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                            | [ |- context[expr.interp ?ii ?v] ]
+                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                            end ].
+        (* 9 subgoals (ID 32915)
+
+  cast_outside_of_range : zrange -> Z -> Z
   max_const, x, x0 : Z
   v1 : expr (type.base base.type.Z)
   ============================
@@ -333,200 +339,191 @@ Module Compilers.
      Some (UnderLets.Base x1))%option
   with
   | Some v0 =>
-      expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
-      Z.mul_split x x0 (expr.interp (@ident.interp) v1)
+      expr.interp ident_interp (UnderLets.interp ident_interp v0) =
+      Z.mul_split x x0 (expr.interp ident_interp v1)
   | None => True
   end
 
-subgoal 2 (ID 30445) is:
+subgoal 2 (ID 32967) is:
  match
    (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1);
     Some (UnderLets.Base x1))%option
  with
  | Some v0 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
-     Z.mul_split x (expr.interp (@ident.interp) v1) x0
+     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
+     Z.mul_split x (expr.interp ident_interp v1) x0
  | None => True
  end
-subgoal 3 (ID 30493) is:
+subgoal 3 (ID 33019) is:
  match
    (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1);
     Some (UnderLets.Base x1))%option
  with
  | Some v0 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
-     Z.mul_split x x0 (expr.interp (@ident.interp) v1)
+     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
+     Z.mul_split x x0 (expr.interp ident_interp v1)
  | None => True
  end
-subgoal 4 (ID 30541) is:
+subgoal 4 (ID 33071) is:
  match
    (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1);
     Some (UnderLets.Base x1))%option
  with
  | Some v0 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
-     Z.mul_split x (expr.interp (@ident.interp) v1) x0
+     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
+     Z.mul_split x (expr.interp ident_interp v1) x0
  | None => True
  end
-subgoal 5 (ID 30631) is:
+subgoal 5 (ID 33168) is:
  match
    (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0);
     Some (UnderLets.Base x0))%option
  with
  | Some v1 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v1) =
-     Z.add_get_carry_full v2 x (expr.interp (@ident.interp) v0)
+     expr.interp ident_interp (UnderLets.interp ident_interp v1) =
+     Z.add_get_carry_full v2 x (expr.interp ident_interp v0)
  | None => True
  end
-subgoal 6 (ID 30721) is:
+subgoal 6 (ID 33265) is:
  match
    (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0);
     Some (UnderLets.Base x0))%option
  with
  | Some v1 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v1) =
-     Z.add_get_carry_full v2 (expr.interp (@ident.interp) v0) x
+     expr.interp ident_interp (UnderLets.interp ident_interp v1) =
+     Z.add_get_carry_full v2 (expr.interp ident_interp v0) x
  | None => True
  end
-subgoal 7 (ID 30772) is:
+subgoal 7 (ID 33320) is:
  match
    (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0));
     Some (UnderLets.Base x2))%option
  with
  | Some v0 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
-     Z.add_with_get_carry_full x x0 x1 (expr.interp (@ident.interp) v1)
+     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
+     Z.add_with_get_carry_full x x0 x1 (expr.interp ident_interp v1)
  | None => True
  end
-subgoal 8 (ID 30824) is:
+subgoal 8 (ID 33376) is:
  match
    (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0));
     Some (UnderLets.Base x2))%option
  with
  | Some v0 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
-     Z.add_with_get_carry_full x x0 (expr.interp (@ident.interp) v1) x1
+     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
+     Z.add_with_get_carry_full x x0 (expr.interp ident_interp v1) x1
  | None => True
  end
-subgoal 9 (ID 30915) is:
+subgoal 9 (ID 33473) is:
  match
    rwhenl
      (Some
         (UnderLets.UnderLet
-           (#(ident.Z_add_with_get_carry)%expr @ v1 @ v0 @ (##x)%expr @
-            (##x0)%expr)%expr_pat
+           (#(ident.Z_add_with_get_carry)%expr @ v1 @ v0 @ (##x)%expr @ (##x0)%expr)%expr_pat
            (fun vc : Z * Z =>
             UnderLets.Base (#(ident.fst)%expr @ ($vc)%expr, (##0)%expr)%expr_pat)))
      ((x =? 0) && (x0 =? 0))
  with
  | Some v2 =>
-     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v2) =
-     Z.add_with_get_carry_full (expr.interp (@ident.interp) v1)
-       (expr.interp (@ident.interp) v0) x x0
+     expr.interp ident_interp (UnderLets.interp ident_interp v2) =
+     Z.add_with_get_carry_full (expr.interp ident_interp v1) (expr.interp ident_interp v0) x x0
  | None => True
  end
-*)
-      1-9: exact admit.
-    Qed.
+         *)
+        1-9: exact admit.
+      Qed.
 
-    Local Ltac fancy_local_t :=
-      repeat first [ match goal with
-                     | [ H : forall s v v', ?invert_low s v = Some v' -> v = _,
-                           H' : ?invert_low _ _ = Some _ |- _ ] => apply H in H'
-                     end
-                   | progress autorewrite with zsimplify in * ].
+      Local Ltac fancy_local_t :=
+        repeat first [ match goal with
+                       | [ H : forall s v v', ?invert_low s v = Some v' -> v = _,
+                             H' : ?invert_low _ _ = Some _ |- _ ] => apply H in H'
+                       end
+                     | progress autorewrite with zsimplify in * ].
 
-    Lemma fancy_rewrite_rules_interp_good
+      Lemma fancy_rewrite_rules_interp_good
             (invert_low invert_high : Z -> Z -> option Z)
             (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
             (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
-      : rewrite_rules_interp_goodT (fancy_rewrite_rules invert_low invert_high).
-    Proof using Type.
-      Time start_interp_good.
-      Time all: try solve [
-                      repeat interp_good_t_step;
-                        cbv [Option.bind] in *;
+        : rewrite_rules_interp_goodT (fancy_rewrite_rules invert_low invert_high).
+      Proof using Type.
+        Time start_interp_good.
+        Time all: try solve [
                         repeat interp_good_t_step;
-                        fancy_local_t;
-                        repeat interp_good_t_step ].
-      Time all: repeat interp_good_t_step.
-      Time all: cbv [Option.bind] in *.
-      Time all: repeat interp_good_t_step.
-      Time all: fancy_local_t.
-      Time all: repeat interp_good_t_step.
-      all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
-                        | progress subst
-                        | match goal with
-                          | [ H : context[expr.interp ?ii ?v] |- _ ]
-                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
-                          | [ |- context[expr.interp ?ii ?v] ]
-                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
-                          end ].
-      all: repeat match goal with
-                  | [ H : _ = _ :> BinInt.Z |- _ ] => revert H
-                  | [ v : BinInt.Z |- _ ] => clear v || revert v
-                  end.
-      (* 16 subgoals (ID 100240)
+                          cbv [Option.bind] in *;
+                          repeat interp_good_t_step;
+                          fancy_local_t;
+                          repeat interp_good_t_step ].
+        Time all: repeat interp_good_t_step.
+        Time all: cbv [Option.bind] in *.
+        Time all: repeat interp_good_t_step.
+        Time all: fancy_local_t.
+        Time all: repeat interp_good_t_step.
+        all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
+                          | progress subst
+                          | match goal with
+                            | [ H : context[expr.interp ?ii ?v] |- _ ]
+                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                            | [ |- context[expr.interp ?ii ?v] ]
+                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                            end ].
+        all: repeat match goal with
+                    | [ H : _ = _ :> BinInt.Z |- _ ] => revert H
+                    | [ v : BinInt.Z |- _ ] => clear v || revert v
+                    end.
+        (* 16 subgoals (ID 105273)
 
+  cast_outside_of_range : zrange -> Z -> Z
   invert_low, invert_high : Z -> Z -> option Z
-  Hlow : forall s v v' : Z,
-         invert_low s v = Some v' -> v = Z.land v' (2 ^ (s / 2) - 1)
+  Hlow : forall s v v' : Z, invert_low s v = Some v' -> v = Z.land v' (2 ^ (s / 2) - 1)
   Hhigh : forall s v v' : Z, invert_high s v = Some v' -> v = Z.shiftr v' (s / 2)
   ============================
   forall x x0 v1 v0 : Z,
   x = 2 ^ Z.log2 x -> (v1 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0) / x
 
-subgoal 2 (ID 100250) is:
+subgoal 2 (ID 105283) is:
  forall x x0 v0 v1 : Z,
  x = 2 ^ Z.log2 x -> (v0 + Z.shiftl v1 x0 mod x) / x = (Z.shiftl v1 x0 + v0) / x
-subgoal 3 (ID 100260) is:
+subgoal 3 (ID 105293) is:
  forall x x0 v1 v0 : Z,
  x = 2 ^ Z.log2 x -> (v1 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0) / x
-subgoal 4 (ID 100270) is:
+subgoal 4 (ID 105303) is:
  forall x x0 v0 v1 : Z,
  x = 2 ^ Z.log2 x -> (v0 + Z.shiftr v1 x0 mod x) / x = (Z.shiftr v1 x0 + v0) / x
-subgoal 5 (ID 100278) is:
+subgoal 5 (ID 105311) is:
  forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 + v0 mod x) / x = (v1 + v0) / x
-subgoal 6 (ID 100290) is:
+subgoal 6 (ID 105323) is:
  forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x ->
- (v1 + v0 + Z.shiftl v4 x0 mod x) / x = (v1 + v0 + Z.shiftl v4 x0) / x
-subgoal 7 (ID 100302) is:
+ x = 2 ^ Z.log2 x -> (v1 + v0 + Z.shiftl v4 x0 mod x) / x = (v1 + v0 + Z.shiftl v4 x0) / x
+subgoal 7 (ID 105335) is:
  forall x x0 v1 v4 v0 : Z,
- x = 2 ^ Z.log2 x ->
- (v1 + v4 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0 + v4) / x
-subgoal 8 (ID 100314) is:
+ x = 2 ^ Z.log2 x -> (v1 + v4 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0 + v4) / x
+subgoal 8 (ID 105347) is:
  forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x ->
- (v1 + v0 + Z.shiftr v4 x0 mod x) / x = (v1 + v0 + Z.shiftr v4 x0) / x
-subgoal 9 (ID 100326) is:
+ x = 2 ^ Z.log2 x -> (v1 + v0 + Z.shiftr v4 x0 mod x) / x = (v1 + v0 + Z.shiftr v4 x0) / x
+subgoal 9 (ID 105359) is:
  forall x x0 v1 v4 v0 : Z,
- x = 2 ^ Z.log2 x ->
- (v1 + v4 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0 + v4) / x
-subgoal 10 (ID 100336) is:
- forall x v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x -> (v1 + v0 + v4 mod x) / x = (v1 + v0 + v4) / x
-subgoal 11 (ID 100346) is:
+ x = 2 ^ Z.log2 x -> (v1 + v4 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0 + v4) / x
+subgoal 10 (ID 105369) is:
+ forall x v1 v0 v4 : Z, x = 2 ^ Z.log2 x -> (v1 + v0 + v4 mod x) / x = (v1 + v0 + v4) / x
+subgoal 11 (ID 105379) is:
  forall x x0 v1 v0 : Z,
  x = 2 ^ Z.log2 x -> (v1 - Z.shiftl v0 x0 mod x) / x = (v1 - Z.shiftl v0 x0) / x
-subgoal 12 (ID 100356) is:
+subgoal 12 (ID 105389) is:
  forall x x0 v1 v0 : Z,
  x = 2 ^ Z.log2 x -> (v1 - Z.shiftr v0 x0 mod x) / x = (v1 - Z.shiftr v0 x0) / x
-subgoal 13 (ID 100364) is:
+subgoal 13 (ID 105397) is:
  forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 - v0 mod x) / x = (v1 - v0) / x
-subgoal 14 (ID 100376) is:
+subgoal 14 (ID 105409) is:
  forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x ->
- (v0 - Z.shiftl v4 x0 mod x - v1) / x = (v0 - Z.shiftl v4 x0 - v1) / x
-subgoal 15 (ID 100388) is:
+ x = 2 ^ Z.log2 x -> (v0 - Z.shiftl v4 x0 mod x - v1) / x = (v0 - Z.shiftl v4 x0 - v1) / x
+subgoal 15 (ID 105421) is:
  forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x ->
- (v0 - Z.shiftr v4 x0 mod x - v1) / x = (v0 - Z.shiftr v4 x0 - v1) / x
-subgoal 16 (ID 100398) is:
- forall x v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x -> (v0 - v4 mod x - v1) / x = (v0 - v4 - v1) / x
-*)
-      all: exact admit.
-    Qed.
+ x = 2 ^ Z.log2 x -> (v0 - Z.shiftr v4 x0 mod x - v1) / x = (v0 - Z.shiftr v4 x0 - v1) / x
+subgoal 16 (ID 105431) is:
+ forall x v1 v0 v4 : Z, x = 2 ^ Z.log2 x -> (v0 - v4 mod x - v1) / x = (v0 - v4 - v1) / x
+         *)
+        1-16: exact admit.
+      Qed.
+    End with_cast.
   End RewriteRules.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 8dd20fd85..74370aaea 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -1679,7 +1679,7 @@ Module Import UnsaturatedSolinas.
                      | progress rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *
                      | reflexivity
                      | lia
-                     | rewrite interp_reify_list, ?map_map
+                     | rewrite expr.interp_reify_list, ?map_map
                      | rewrite map_ext with (g:=id), map_id
                      | progress distr_length
                      | progress cbv [Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *
@@ -2803,7 +2803,7 @@ Module WordByWordMontgomery.
                      | progress rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *
                      | reflexivity
                      | lia
-                     | rewrite interp_reify_list, ?map_map
+                     | rewrite expr.interp_reify_list, ?map_map
                      | rewrite map_ext with (g:=id), map_id
                      | progress distr_length
                      | progress cbv [Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *