Add placeholder rewrite rules for rewriting after bounds

Currently, there aren't any interesting rewrite rules in the lists, but
this allows us to move rewrite rules that depend on cast behavior to
after bounds analysis.

Unfortunately, it takes a lot of time to build from Rewriter.v to the
standalone binaries, so it'll probably make sense to inline some stuff
for more rapid development.

Note that we also now have a tactic that does all of the evaluation for
rewrite rules (assuming the right [Arguments] commands have been
issued).

6 files changed, 326 insertions, 265 deletions

diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 5ace04e08..476612aef 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -320,6 +320,11 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         break_innermost_match; split_andb; Z.ltb_to_lt; intro H';
           rewrite ?H' by lia; Z.rewrite_mod_small; reflexivity.
       Qed.
+
+      Lemma cast_normalize r v : cast (ZRange.normalize r) v = cast r v.
+      Proof.
+        cbv [cast]; rewrite ZRange.normalize_idempotent; reflexivity.
+      Qed.
     End with_cast.
 
     Lemma cast_idempotent_gen {cast_outside_of_range1 cast_outside_of_range2}
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 0713ea83a..6c0572ea4 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -5,6 +5,8 @@ Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.CPSNotations.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
 Require Crypto.Util.PrimitiveProd.
 Require Crypto.Util.PrimitiveHList.
 Require Import Crypto.Experiments.NewPipeline.Language.
@@ -1854,17 +1856,29 @@ Module Compilers.
             ; make_rewriteol (-??) (fun e => (llet v := e in -$v)  when  negb (SubstVarLike.is_var_fst_snd_pair_opp e)) (* inline negation when the rewriter wouldn't already inline it *)
            ].
 
+      Definition arith_with_casts_rewrite_rules : rewrite_rulesT
+        := [make_rewrite (#(@pattern.ident.fst '1 '2) @ (??, ??)) (fun _ _ x y => x)
+            ; make_rewrite (#(@pattern.ident.snd '1 '2) @ (??, ??)) (fun _ x _ y => y)
+            ; make_rewriteo
+                (#pattern.ident.Z_cast @ (#pattern.ident.Z_cast @ ??))
+                (fun r1 r2 x => #(ident.Z_cast r2) @ x  when  ZRange.is_tighter_than_bool (ZRange.normalize r2) (ZRange.normalize r1))].
+
       Definition nbe_dtree'
         := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 nbe_rewrite_rules.
       Definition arith_dtree'
         := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 (arith_rewrite_rules 0%Z (* dummy val *)).
+      Definition arith_with_casts_dtree'
+        := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 arith_with_casts_rewrite_rules.
       Definition nbe_dtree : decision_tree
         := Eval compute in invert_Some nbe_dtree'.
       Definition arith_dtree : decision_tree
         := Eval compute in invert_Some arith_dtree'.
+      Definition arith_with_casts_dtree : decision_tree
+        := Eval compute in invert_Some arith_with_casts_dtree'.
 
       Definition nbe_default_fuel := Eval compute in List.length nbe_rewrite_rules.
       Definition arith_default_fuel := Eval compute in List.length (arith_rewrite_rules 0%Z (* dummy val *)).
+      Definition arith_with_casts_default_fuel := Eval compute in List.length arith_with_casts_rewrite_rules.
 
       Import PrimitiveHList.
       (* N.B. The [combine_hlist] call MUST eta-expand
@@ -1888,10 +1902,16 @@ Module Compilers.
       Definition arith_pr1_rewrite_rules max_const_val := Eval hnf in projT1 (arith_split_rewrite_rules max_const_val).
       Definition arith_pr2_rewrite_rules max_const_val := Eval hnf in projT2 (arith_split_rewrite_rules max_const_val).
       Definition arith_all_rewrite_rules max_const_val := combine_hlist (P:=rewrite_ruleTP) (arith_pr1_rewrite_rules max_const_val) (arith_pr2_rewrite_rules max_const_val).
+      Definition arith_with_casts_split_rewrite_rules := Eval cbv [split_list projT1 projT2 arith_with_casts_rewrite_rules] in split_list arith_with_casts_rewrite_rules.
+      Definition arith_with_casts_pr1_rewrite_rules := Eval hnf in projT1 arith_with_casts_split_rewrite_rules.
+      Definition arith_with_casts_pr2_rewrite_rules := Eval hnf in projT2 arith_with_casts_split_rewrite_rules.
+      Definition arith_with_casts_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) (arith_with_casts_pr1_rewrite_rules) arith_with_casts_pr2_rewrite_rules.
       Definition nbe_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t
         := @assemble_identifier_rewriters nbe_dtree nbe_all_rewrite_rules do_again t idc.
       Definition arith_rewrite_head0 max_const_val do_again {t} (idc : ident t) : value_with_lets t
         := @assemble_identifier_rewriters arith_dtree (arith_all_rewrite_rules max_const_val) do_again t idc.
+      Definition arith_with_casts_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t
+        := @assemble_identifier_rewriters arith_with_casts_dtree arith_with_casts_all_rewrite_rules do_again t idc.
 
       Section fancy.
         Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z).
@@ -2067,18 +2087,32 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
                   ((#pattern.ident.Z_shiftr @ ?? @ #?ℤ) * (#pattern.ident.Z_shiftr @ ?? @ #?ℤ))
                   (fun x offset1 y offset2 => let s := (2*offset1)%Z in #(ident.fancy_mulhh s) @ (x, y)  when  offset1 =? offset2)
             ].
+        Definition fancy_with_casts_rewrite_rules : rewrite_rulesT
+          := [].
+
         Definition fancy_dtree'
           := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_rewrite_rules.
         Definition fancy_dtree : decision_tree
           := Eval compute in invert_Some fancy_dtree'.
+        Definition fancy_with_casts_dtree'
+          := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_with_casts_rewrite_rules.
+        Definition fancy_with_casts_dtree : decision_tree
+          := Eval compute in invert_Some fancy_with_casts_dtree'.
         Definition fancy_default_fuel := Eval compute in List.length fancy_rewrite_rules.
+        Definition fancy_with_casts_default_fuel := Eval compute in List.length fancy_with_casts_rewrite_rules.
         Import PrimitiveHList.
         Definition fancy_split_rewrite_rules := Eval cbv [split_list projT1 projT2 fancy_rewrite_rules] in split_list fancy_rewrite_rules.
         Definition fancy_pr1_rewrite_rules := Eval hnf in projT1 fancy_split_rewrite_rules.
         Definition fancy_pr2_rewrite_rules := Eval hnf in projT2 fancy_split_rewrite_rules.
         Definition fancy_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) fancy_pr1_rewrite_rules fancy_pr2_rewrite_rules.
+        Definition fancy_with_casts_split_rewrite_rules := Eval cbv [split_list projT1 projT2 fancy_with_casts_rewrite_rules] in split_list fancy_with_casts_rewrite_rules.
+        Definition fancy_with_casts_pr1_rewrite_rules := Eval hnf in projT1 fancy_with_casts_split_rewrite_rules.
+        Definition fancy_with_casts_pr2_rewrite_rules := Eval hnf in projT2 fancy_with_casts_split_rewrite_rules.
+        Definition fancy_with_casts_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) fancy_with_casts_pr1_rewrite_rules fancy_with_casts_pr2_rewrite_rules.
         Definition fancy_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t
           := @assemble_identifier_rewriters fancy_dtree fancy_all_rewrite_rules do_again t idc.
+        Definition fancy_with_casts_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t
+          := @assemble_identifier_rewriters fancy_with_casts_dtree fancy_with_casts_all_rewrite_rules do_again t idc.
       End fancy.
     End with_var.
     Module RewriterPrintingNotations.
@@ -2103,193 +2137,150 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
       Notation "x <- 'type.try_make_transport_cps' t1 t2 ; f" := (type.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x  <-  'type.try_make_transport_cps'  t1  t2 ; '/' f ']'").
       Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x  <-  'base.try_make_transport_cps'  t1  t2 ; '/' f ']'").
     End RewriterPrintingNotations.
+
+    Ltac make_rewrite_head1 rewrite_head0 pr2_rewrite_rules :=
+      (eval cbv -[pr2_rewrite_rules
+                    base.interp base.try_make_transport_cps
+                    type.try_make_transport_cps type.try_transport_cps
+                    pattern.type.unify_extracted_cps
+                    Let_In Option.sequence Option.sequence_return
+                    UnderLets.splice UnderLets.to_expr
+                    Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
+                    Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps
+                    Compile.value'
+                    SubstVarLike.is_var_fst_snd_pair_opp
+                 ] in rewrite_head0).
+    Ltac timed_make_rewrite_head1 rewrite_head0 pr2_rewrite_rules :=
+      constr:(ltac:(time (idtac; let v := make_rewrite_head1 rewrite_head0 pr2_rewrite_rules in exact v))).
+    Ltac make_rewrite_head2 rewrite_head1 pr2_rewrite_rules :=
+      (eval cbv [id
+                   pr2_rewrite_rules
+                   projT1 projT2
+                   cpsbind cpscall cps_option_bind cpsreturn
+                   PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd
+                   pattern.ident.arg_types
+                   Compile.eval_decision_tree
+                   Compile.eval_rewrite_rules
+                   Compile.expr_of_rawexpr
+                   Compile.normalize_deep_rewrite_rule
+                   Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
+                   (*Compile.reflect*)
+                   (*Compile.reify*)
+                   Compile.reveal_rawexpr_cps
+                   Compile.reveal_rawexpr_cps_gen
+                   Compile.rew_should_do_again
+                   Compile.rew_with_opt
+                   Compile.rew_under_lets
+                   Compile.rew_replacement
+                   Compile.rew_is_cps
+                   Compile.rValueOrExpr
+                   Compile.swap_list
+                   Compile.type_of_rawexpr
+                   Compile.value
+                   (*Compile.value'*)
+                   Compile.value_of_rawexpr
+                   Compile.value_with_lets
+                   ident.smart_Literal
+                   type.try_transport_cps
+                   rlist_rect rwhen rwhenl
+                ] in rewrite_head1).
+    Ltac timed_make_rewrite_head2 rewrite_head1 pr2_rewrite_rules :=
+      constr:(ltac:(time (idtac; let v := make_rewrite_head2 rewrite_head1 pr2_rewrite_rules in exact v))).
+    Ltac make_rewrite_head3 rewrite_head2 :=
+      (eval cbn [id
+                   cpsbind cpscall cps_option_bind cpsreturn
+                   Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value'
+                   Option.sequence Option.sequence_return Option.bind
+                   UnderLets.reify_and_let_binds_base_cps
+                   UnderLets.splice UnderLets.splice_list UnderLets.to_expr
+                   base.interp base.base_interp
+                   base.type.base_beq
+                   type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps
+                   Datatypes.fst Datatypes.snd
+                ] in rewrite_head2).
+    Ltac timed_make_rewrite_head3 rewrite_head2 :=
+      constr:(ltac:(time (idtac; let v := make_rewrite_head3 rewrite_head2 in exact v))).
+    Ltac make_rewrite_head rewrite_head0 pr2_rewrite_rules :=
+      let rewrite_head1 := make_rewrite_head1 rewrite_head0 pr2_rewrite_rules in
+      let rewrite_head2 := make_rewrite_head2 rewrite_head1 pr2_rewrite_rules in
+      let rewrite_head3 := make_rewrite_head3 rewrite_head2 in
+      rewrite_head3.
+    Ltac timed_make_rewrite_head rewrite_head0 pr2_rewrite_rules :=
+      let rewrite_head1 := timed_make_rewrite_head1 rewrite_head0 pr2_rewrite_rules in
+      let rewrite_head2 := timed_make_rewrite_head2 rewrite_head1 pr2_rewrite_rules in
+      let rewrite_head3 := timed_make_rewrite_head3 rewrite_head2 in
+      rewrite_head3.
+    Notation make_rewrite_head rewrite_head0 pr2_rewrite_rules
+      := (ltac:(let v := timed_make_rewrite_head rewrite_head0 pr2_rewrite_rules in
+                exact v)) (only parsing).
+
+    (* For reduction *)
+    Local Arguments base.try_make_base_transport_cps _ !_ !_.
+    Local Arguments base.try_make_transport_cps _ !_ !_.
+    Local Arguments type.try_make_transport_cps _ _ _ !_ !_.
+    Local Arguments Option.sequence {A} !v1 v2.
+    Local Arguments Option.sequence_return {A} !v1 v2.
+    Local Arguments Option.bind {A B} !_ _.
+    Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_.
+    Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _.
+    Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _.
+    Local Arguments base.type.base_beq !_ !_.
+    Local Arguments id / .
+    (* For printing *)
+    Local Arguments option {_}.
+    Local Arguments UnderLets.UnderLets {_ _ _}.
+    Local Arguments expr.expr {_ _ _}.
+    Local Notation ℤ := base.type.Z.
+    Local Notation ℕ := base.type.nat.
+    Local Notation bool := base.type.bool.
+    Local Notation unit := base.type.unit.
+    Local Notation list := base.type.list.
+    Local Notation "x" := (type.base x) (only printing, at level 9).
+
     Section red_fancy.
-      Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z)
+      Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
               {var : type.type base.type -> Type}
               (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t)
-                                                -> UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
+                                                -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
               {t} (idc : ident t).
-      Time Let rewrite_head1
-        := Eval cbv -[fancy_pr2_rewrite_rules
-                        base.interp base.try_make_transport_cps
-                        type.try_make_transport_cps type.try_transport_cps
-                        pattern.type.unify_extracted_cps
-                        Let_In Option.sequence Option.sequence_return
-                        UnderLets.splice UnderLets.to_expr
-                        Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
-                        Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps
-                        Compile.value'
-                        SubstVarLike.is_var_fst_snd_pair_opp
-                     ] in @fancy_rewrite_head0 var invert_low invert_high do_again t idc.
-      (* Finished transaction in 3.395 secs (3.395u,0.s) (successful) *)
-
-      Time Local Definition fancy_rewrite_head2
-        := Eval cbv [id
-                       rewrite_head1 fancy_pr2_rewrite_rules
-                       projT1 projT2
-                       cpsbind cpscall cps_option_bind cpsreturn
-                       PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd
-                       pattern.ident.arg_types
-                       Compile.eval_decision_tree
-                       Compile.eval_rewrite_rules
-                       Compile.expr_of_rawexpr
-                       Compile.normalize_deep_rewrite_rule
-                       Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
-                       (*Compile.reflect*)
-                       (*Compile.reify*)
-                       Compile.reveal_rawexpr_cps
-                       Compile.reveal_rawexpr_cps_gen
-                       Compile.rew_should_do_again
-                       Compile.rew_with_opt
-                       Compile.rew_under_lets
-                       Compile.rew_replacement
-                       Compile.rew_is_cps
-                       Compile.rValueOrExpr
-                       Compile.swap_list
-                       Compile.type_of_rawexpr
-                       Compile.value
-                       (*Compile.value'*)
-                       Compile.value_of_rawexpr
-                       Compile.value_with_lets
-                       ident.smart_Literal
-                       type.try_transport_cps
-                       rlist_rect rwhen rwhenl
-                    ] in rewrite_head1.
-      (* Finished transaction in 10.793 secs (10.796u,0.s) (successful) *)
-
-      Local Arguments base.try_make_base_transport_cps _ !_ !_.
-      Local Arguments base.try_make_transport_cps _ !_ !_.
-      Local Arguments type.try_make_transport_cps _ _ _ !_ !_.
-      Local Arguments Option.sequence {A} !v1 v2.
-      Local Arguments Option.sequence_return {A} !v1 v2.
-      Local Arguments Option.bind {A B} !_ _.
-      Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_.
-      Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _.
-      Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _.
-      Local Arguments base.type.base_beq !_ !_.
-      Local Arguments option {_}.
-      Local Arguments id / .
-      Local Arguments fancy_rewrite_head2 / .
-      Local Arguments UnderLets.UnderLets {_ _ _}.
-      Local Arguments expr.expr {_ _ _}.
-      Local Notation ℤ := base.type.Z.
-      Local Notation ℕ := base.type.nat.
-      Local Notation bool := base.type.bool.
-      Local Notation unit := base.type.unit.
-      Local Notation list := base.type.list.
-      Local Notation "x" := (type.base x) (only printing, at level 9).
 
       Time Definition fancy_rewrite_head
-        := Eval cbn [id
-                       fancy_rewrite_head2
-                       cpsbind cpscall cps_option_bind cpsreturn
-                       Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value'
-                       Option.sequence Option.sequence_return Option.bind
-                       UnderLets.reify_and_let_binds_base_cps
-                       UnderLets.splice UnderLets.splice_list UnderLets.to_expr
-                       base.interp base.base_interp
-                       base.type.base_beq
-                       type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps
-                       Datatypes.fst Datatypes.snd
-                    ] in fancy_rewrite_head2.
-      (* Finished transaction in 1.892 secs (1.891u,0.s) (successful) *)
+        := make_rewrite_head (@fancy_rewrite_head0 var invert_low invert_high do_again t idc) (@fancy_pr2_rewrite_rules).
+      (* Tactic call ran for 0.19 secs (0.187u,0.s) (success)
+         Tactic call ran for 10.297 secs (10.3u,0.s) (success)
+         Tactic call ran for 1.746 secs (1.747u,0.s) (success)
+         Finished transaction in 12.402 secs (12.4u,0.s) (successful) *)
 
       Local Set Printing Depth 1000000.
       Local Set Printing Width 200.
       Import RewriterPrintingNotations.
       (* Redirect "/tmp/fancy_rewrite_head" Print fancy_rewrite_head. *)
     End red_fancy.
+    Section red_fancy_with_casts.
+      Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
+              {var : type.type base.type -> Type}
+              (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t)
+                                                -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
+              {t} (idc : ident t).
+      Time Definition fancy_with_casts_rewrite_head
+        := make_rewrite_head (@fancy_with_casts_rewrite_head0 var (*invert_low invert_high*) do_again t idc) (@fancy_with_casts_pr2_rewrite_rules).
 
+      Local Set Printing Depth 1000000.
+      Local Set Printing Width 200.
+      Import RewriterPrintingNotations.
+      (* Redirect "/tmp/fancy_with_casts_rewrite_head" Print fancy_with_casts_rewrite_head. *)
+    End red_fancy_with_casts.
     Section red_nbe.
       Context {var : type.type base.type -> Type}
               (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t)
-                                                -> UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
+                                                -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
               {t} (idc : ident t).
-
-      Time Let rewrite_head1
-        := Eval cbv -[nbe_pr2_rewrite_rules
-                        base.interp base.try_make_transport_cps
-                        type.try_make_transport_cps type.try_transport_cps
-                        pattern.type.unify_extracted_cps
-                        Let_In Option.sequence Option.sequence_return
-                        UnderLets.splice UnderLets.to_expr
-                        Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
-                        Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps
-                        Compile.value'
-                        SubstVarLike.is_var_fst_snd_pair_opp
-                     ] in @nbe_rewrite_head0 var do_again t idc.
-      (* Finished transaction in 7.035 secs (7.036u,0.s) (successful) *)
-
-      Time Local Definition nbe_rewrite_head2
-        := Eval cbv [id
-                       rewrite_head1 nbe_pr2_rewrite_rules
-                       projT1 projT2
-                       cpsbind cpscall cps_option_bind cpsreturn
-                       PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd
-                       pattern.ident.arg_types
-                       Compile.eval_decision_tree
-                       Compile.eval_rewrite_rules
-                       Compile.expr_of_rawexpr
-                       Compile.normalize_deep_rewrite_rule
-                       Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
-                       (*Compile.reflect*)
-                       (*Compile.reify*)
-                       Compile.reveal_rawexpr_cps
-                       Compile.reveal_rawexpr_cps_gen
-                       Compile.rew_should_do_again
-                       Compile.rew_with_opt
-                       Compile.rew_under_lets
-                       Compile.rew_replacement
-                       Compile.rew_is_cps
-                       Compile.rValueOrExpr
-                       Compile.swap_list
-                       Compile.type_of_rawexpr
-                       Compile.value
-                       (*Compile.value'*)
-                       Compile.value_of_rawexpr
-                       Compile.value_with_lets
-                       ident.smart_Literal
-                       type.try_transport_cps
-                       rlist_rect rwhen rwhenl
-                    ] in rewrite_head1.
-      (* Finished transaction in 29.297 secs (29.284u,0.016s) (successful) *)
-
-      Local Arguments base.try_make_base_transport_cps _ !_ !_.
-      Local Arguments base.try_make_transport_cps _ !_ !_.
-      Local Arguments type.try_make_transport_cps _ _ _ !_ !_.
-      Local Arguments Option.sequence {A} !v1 v2.
-      Local Arguments Option.sequence_return {A} !v1 v2.
-      Local Arguments Option.bind {A B} !_ _.
-      Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_.
-      Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _.
-      Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _.
-      Local Arguments base.type.base_beq !_ !_.
-      Local Arguments option {_}.
-      Local Arguments id / .
-      Local Arguments nbe_rewrite_head2 / .
-      Local Arguments UnderLets.UnderLets {_ _ _}.
-      Local Arguments expr.expr {_ _ _}.
-      Local Notation ℤ := base.type.Z.
-      Local Notation ℕ := base.type.nat.
-      Local Notation bool := base.type.bool.
-      Local Notation unit := base.type.unit.
-      Local Notation list := base.type.list.
-      Local Notation "x" := (type.base x) (only printing, at level 9).
-
       Time Definition nbe_rewrite_head
-        := Eval cbn [id
-                       nbe_rewrite_head2
-                       cpsbind cpscall cps_option_bind cpsreturn
-                       Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value'
-                       Option.sequence Option.sequence_return Option.bind
-                       UnderLets.reify_and_let_binds_base_cps
-                       UnderLets.splice UnderLets.splice_list UnderLets.to_expr
-                       base.interp base.base_interp
-                       base.type.base_beq
-                       type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps
-                       PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd Datatypes.fst Datatypes.snd
-                    ] in nbe_rewrite_head2.
-      (* Finished transaction in 1.998 secs (2.u,0.s) (successful) *)
+        := make_rewrite_head (@nbe_rewrite_head0 var do_again t idc) (@nbe_pr2_rewrite_rules).
+      (* Tactic call ran for 0.232 secs (0.235u,0.s) (success)
+         Tactic call ran for 29.061 secs (29.04u,0.004s) (success)
+         Tactic call ran for 1.605 secs (1.604u,0.s) (success)
+         Finished transaction in 31.203 secs (31.183u,0.004s) (successful) *)
 
       Local Set Printing Depth 1000000.
       Local Set Printing Width 200.
@@ -2301,93 +2292,15 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
       Context (max_const_val : Z)
               {var : type.type base.type -> Type}
               (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t)
-                                                -> UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
+                                                -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
               {t} (idc : ident t).
 
-      Time Let rewrite_head1
-        := Eval cbv -[arith_pr2_rewrite_rules
-                        base.interp base.try_make_transport_cps
-                        type.try_make_transport_cps type.try_transport_cps
-                        pattern.type.unify_extracted_cps
-                        Let_In Option.sequence Option.sequence_return
-                        UnderLets.splice UnderLets.to_expr
-                        Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
-                        Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps
-                        Compile.value'
-                        SubstVarLike.is_var_fst_snd_pair_opp
-                     ] in @arith_rewrite_head0 var max_const_val do_again t idc.
-      (* Finished transaction in 15.381 secs (15.379u,0.s) (successful) *)
-
-      Time Local Definition arith_rewrite_head2
-        := Eval cbv [id
-                       rewrite_head1 arith_pr2_rewrite_rules
-                       projT1 projT2
-                       cpsbind cpscall cps_option_bind cpsreturn
-                       PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd
-                       pattern.ident.arg_types
-                       Compile.eval_decision_tree
-                       Compile.eval_rewrite_rules
-                       Compile.expr_of_rawexpr
-                       Compile.normalize_deep_rewrite_rule
-                       Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
-                       (*Compile.reflect*)
-                       (*Compile.reify*)
-                       Compile.reveal_rawexpr_cps
-                       Compile.reveal_rawexpr_cps_gen
-                       Compile.rew_should_do_again
-                       Compile.rew_with_opt
-                       Compile.rew_under_lets
-                       Compile.rew_replacement
-                       Compile.rew_is_cps
-                       Compile.rValueOrExpr
-                       Compile.swap_list
-                       Compile.type_of_rawexpr
-                       Compile.value
-                       (*Compile.value'*)
-                       Compile.value_of_rawexpr
-                       Compile.value_with_lets
-                       ident.smart_Literal
-                       type.try_transport_cps
-                       rlist_rect rwhen rwhenl
-                    ] in rewrite_head1.
-      (* Finished transaction in 83.667 secs (83.564u,0.115s) (successful) *)
-
-      Local Arguments base.try_make_base_transport_cps _ !_ !_.
-      Local Arguments base.try_make_transport_cps _ !_ !_.
-      Local Arguments type.try_make_transport_cps _ _ _ !_ !_.
-      Local Arguments Option.sequence {A} !v1 v2.
-      Local Arguments Option.sequence_return {A} !v1 v2.
-      Local Arguments Option.bind {A B} !_ _.
-      Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_.
-      Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _.
-      Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _.
-      Local Arguments base.type.base_beq !_ !_.
-      Local Arguments option {_}.
-      Local Arguments id / .
-      Local Arguments arith_rewrite_head2 / .
-      Local Arguments UnderLets.UnderLets {_ _ _}.
-      Local Arguments expr.expr {_ _ _}.
-      Local Notation ℤ := base.type.Z.
-      Local Notation ℕ := base.type.nat.
-      Local Notation bool := base.type.bool.
-      Local Notation unit := base.type.unit.
-      Local Notation list := base.type.list.
-      Local Notation "x" := (type.base x) (only printing, at level 9).
-
       Time Definition arith_rewrite_head
-        := Eval cbn [id
-                       arith_rewrite_head2
-                       cpsbind cpscall cps_option_bind cpsreturn
-                       Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value'
-                       Option.sequence Option.sequence_return Option.bind
-                       UnderLets.reify_and_let_binds_base_cps
-                       UnderLets.splice UnderLets.splice_list UnderLets.to_expr
-                       base.interp base.base_interp
-                       base.type.base_beq
-                       type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps
-                       PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd Datatypes.fst Datatypes.snd
-                    ] in arith_rewrite_head2.
-      (* Finished transaction in 3.967 secs (3.968u,0.s) (successful) *)
+        := make_rewrite_head (@arith_rewrite_head0 var max_const_val do_again t idc) (@arith_pr2_rewrite_rules).
+      (* Tactic call ran for 0.283 secs (0.284u,0.s) (success)
+         Tactic call ran for 79.61 secs (79.612u,0.008s) (success)
+         Tactic call ran for 3.574 secs (3.576u,0.s) (success)
+         Finished transaction in 83.677 secs (83.68u,0.008s) (successful) *)
 
       Local Set Printing Depth 1000000.
       Local Set Printing Width 200.
@@ -2395,14 +2308,35 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
       (* Redirect "/tmp/arith_rewrite_head" Print arith_rewrite_head. *)
     End red_arith.
 
+    Section red_arith_with_casts.
+      Context {var : type.type base.type -> Type}
+              (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t)
+                                                -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t)))
+              {t} (idc : ident t).
+
+      Time Definition arith_with_casts_rewrite_head
+        := make_rewrite_head (@arith_with_casts_rewrite_head0 var do_again t idc) (@arith_with_casts_pr2_rewrite_rules).
+
+      Local Set Printing Depth 1000000.
+      Local Set Printing Width 200.
+      Import RewriterPrintingNotations.
+      (* Redirect "/tmp/arith_with_casts_rewrite_head" Print arith_with_casts_rewrite_head. *)
+    End red_arith_with_casts.
+
     Definition RewriteNBE {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t
       := @Compile.Rewrite (@nbe_rewrite_head) nbe_default_fuel t e.
     Definition RewriteArith (max_const_val : Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t
       := @Compile.Rewrite (@arith_rewrite_head max_const_val) arith_default_fuel t e.
+    Definition RewriteArithWithCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t
+      := @Compile.Rewrite (fun var do_again => @arith_with_casts_rewrite_head var) arith_with_casts_default_fuel t e.
     Definition RewriteToFancy
-               (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z)
+               (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
                {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t
       := @Compile.Rewrite (fun var _ => @fancy_rewrite_head invert_low invert_high var) fancy_default_fuel t e.
+    Definition RewriteToFancyWithCasts
+               (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
+               {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t
+      := @Compile.Rewrite (fun var _ => @fancy_with_casts_rewrite_head (*invert_low invert_high*) var) fancy_with_casts_default_fuel t e.
   End RewriteRules.
 
   Import defaults.
diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v
index eddd3585f..df51ea28d 100644
--- a/src/Experiments/NewPipeline/RewriterProofs.v
+++ b/src/Experiments/NewPipeline/RewriterProofs.v
@@ -77,6 +77,11 @@ Module Compilers.
       start_Wf_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0).
       apply arith_rewrite_rules_good.
     Qed.
+    Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e).
+    Proof.
+      start_Wf_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0).
+      apply arith_with_casts_rewrite_rules_good.
+    Qed.
     Lemma Wf_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))
@@ -86,6 +91,15 @@ Module Compilers.
       apply fancy_rewrite_rules_good; assumption.
     Qed.
 
+    Lemma Wf_RewriteToFancyWithCasts (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) : Wf (@RewriteToFancyWithCasts invert_low invert_high t e).
+    Proof.
+      start_Wf_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0).
+      eapply fancy_with_casts_rewrite_rules_good; eassumption.
+    Qed.
+
     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.
@@ -99,6 +113,13 @@ Module Compilers.
       start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0).
     Admitted.
 
+    Lemma Interp_gen_RewriteArithWithCasts {cast_outside_of_range} {t} e (Hwf : Wf e)
+      : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArithWithCasts t e)
+        == expr.Interp (@ident.gen_interp cast_outside_of_range) e.
+    Proof.
+      start_Interp_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0).
+    Admitted.
+
     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))
@@ -109,17 +130,36 @@ Module Compilers.
       start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0).
     Admitted.
 
+    Lemma Interp_gen_RewriteToFancyWithCasts {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)
+      : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts invert_low invert_high t e)
+        == expr.Interp (@ident.gen_interp cast_outside_of_range) e.
+    Proof.
+      start_Interp_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_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_RewriteArithWithCasts {t} e (Hwf : Wf e)
+      : Interp (@RewriteArithWithCasts t e) == Interp e.
+    Proof. apply Interp_gen_RewriteArithWithCasts; 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.
+    Lemma Interp_RewriteToFancyWithCasts (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 (@RewriteToFancyWithCasts invert_low invert_high t e) == Interp e.
+    Proof. apply Interp_gen_RewriteToFancyWithCasts; assumption. Qed.
   End RewriteRules.
 
   Lemma Wf_PartialEvaluate {t} e (Hwf : Wf e) : Wf (@PartialEvaluate t e).
@@ -133,6 +173,6 @@ Module Compilers.
     : 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_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy : interp.
+  Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy Wf_RewriteArithWithCasts Wf_RewriteToFancyWithCasts : wf.
+  Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_gen_RewriteArithWithCasts @Interp_gen_RewriteToFancyWithCasts @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy @Interp_RewriteArithWithCasts @Interp_RewriteToFancyWithCasts : interp.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index 978c49189..04e65dee3 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -54,6 +54,14 @@ Module Compilers.
     Lemma arith_rewrite_head_eq max_const_val : @arith_rewrite_head max_const_val = (fun var => @arith_rewrite_head0 var max_const_val).
     Proof. reflexivity. Qed.
 
+    Lemma fancy_with_casts_rewrite_head_eq (*invert_low invert_high*)
+      : (fun var do_again => @fancy_with_casts_rewrite_head (*invert_low invert_high*) var)
+        = (fun var => @fancy_with_casts_rewrite_head0 var (*invert_low invert_high*)).
+    Proof. reflexivity. Qed.
+
+    Lemma arith_with_casts_rewrite_head_eq : (fun var _ => @arith_with_casts_rewrite_head var) = @arith_with_casts_rewrite_head0.
+    Proof. reflexivity. Qed.
+
     Lemma nbe_all_rewrite_rules_eq : @nbe_all_rewrite_rules = @nbe_rewrite_rules.
     Proof. reflexivity. Qed.
 
@@ -63,6 +71,12 @@ Module Compilers.
     Lemma arith_all_rewrite_rules_eq : @arith_all_rewrite_rules = @arith_rewrite_rules.
     Proof. reflexivity. Qed.
 
+    Lemma fancy_with_casts_all_rewrite_rules_eq : @fancy_with_casts_all_rewrite_rules = @fancy_with_casts_rewrite_rules.
+    Proof. reflexivity. Qed.
+
+    Lemma arith_with_casts_all_rewrite_rules_eq : @arith_with_casts_all_rewrite_rules = @arith_with_casts_rewrite_rules.
+    Proof. reflexivity. Qed.
+
     Section good.
       Context {var1 var2 : type -> Type}.
 
@@ -336,6 +350,13 @@ Module Compilers.
         Time all: repeat good_t_step.
       Qed.
 
+      Lemma arith_with_casts_rewrite_rules_good
+        : rewrite_rules_goodT arith_with_casts_rewrite_rules arith_with_casts_rewrite_rules.
+      Proof using Type.
+        Time start_good.
+        Time all: repeat good_t_step.
+      Qed.
+
       Lemma fancy_rewrite_rules_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))
@@ -347,6 +368,18 @@ Module Compilers.
         all: cbv [Option.bind].
         Time all: repeat good_t_step.
       Qed.
+
+      Lemma fancy_with_casts_rewrite_rules_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_goodT (fancy_with_casts_rewrite_rules (*invert_low invert_high*)) (fancy_with_casts_rewrite_rules (*invert_low invert_high*)).
+      Proof using Type.
+        Time start_good.
+        Time all: repeat good_t_step.
+        all: cbv [Option.bind].
+        Time all: repeat good_t_step.
+      Qed.
     End good.
   End RewriteRules.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index df35ffd40..3a7bef3e7 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -24,6 +24,8 @@ 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.ZRange.Operations.
+Require Import Crypto.Util.ZRange.BasicLemmas.
 Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SplitInContext.
@@ -128,6 +130,7 @@ Module Compilers.
               | match goal with
                 | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
                 | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand
+                | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence
                 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 *
@@ -160,10 +163,19 @@ Module Compilers.
                   => 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)
+                | [ H : context[ZRange.normalize (ZRange.normalize _)] |- _ ]
+                  => rewrite ZRange.normalize_idempotent in H
+                | [ |- context[ZRange.normalize (ZRange.normalize _)] ]
+                  => rewrite ZRange.normalize_idempotent
+                | [ |- context[ident.cast (ZRange.normalize ?r)] ]
+                  => rewrite ident.cast_normalize
+                | [ H : context[ident.cast (ZRange.normalize ?r)] |- _ ]
+                  => rewrite ident.cast_normalize in H
                 end
               | progress intros
               | progress subst
               | progress inversion_option
+              | progress destruct_head'_and
               | progress Z.ltb_to_lt
               | progress split_andb
               | match goal with
@@ -279,6 +291,19 @@ Module Compilers.
                 end
               | break_innermost_match_step
               | break_innermost_match_hyps_step
+              | progress destruct_head'_or
+              | match goal with
+                | [ |- context[ident.cast ?coor ?r ?v] ]
+                  => is_var v;
+                     pose proof (@ident.cast_always_bounded coor r v);
+                     generalize dependent (ident.cast coor r v); clear v; intro v; intros
+                | [ |- context[ident.cast ?coor ?r ?v] ]
+                  => is_var v; is_var coor;
+                     pose proof (@ident.cast_cases coor r v);
+                     generalize dependent (ident.cast coor r v); intros
+                | [ H : is_bounded_by_bool ?v ?r = true, H' : is_tighter_than_bool ?r ?r' = true |- _ ]
+                  => unique assert (is_bounded_by_bool v r' = true) by (eauto 2 using ZRange.is_bounded_by_of_is_tighter_than)
+                end
               | match goal with
                 | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))]
                     |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ]
@@ -433,6 +458,13 @@ subgoal 9 (ID 33473) is:
         1-9: exact admit.
       Qed.
 
+      Lemma arith_with_casts_rewrite_rules_interp_good
+        : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules.
+      Proof using Type.
+        Time start_interp_good.
+        Time all: try solve [ repeat interp_good_t_step; (lia + nia) ].
+      Qed.
+
       Local Ltac fancy_local_t :=
         repeat first [ match goal with
                        | [ H : forall s v v', ?invert_low s v = Some v' -> v = _,
@@ -524,6 +556,16 @@ subgoal 16 (ID 105431) is:
          *)
         1-16: exact admit.
       Qed.
+
+      Lemma fancy_with_casts_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_with_casts_rewrite_rules (*invert_low invert_high*)).
+      Proof using Type.
+        Time start_interp_good.
+        Time all: repeat interp_good_t_step.
+      Qed.
     End with_cast.
   End RewriteRules.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 74370aaea..59ce4a33e 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -713,7 +713,13 @@ Module Pipeline.
       let E := FromFlat e in
       let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in
       match E' with
-      | inl E => Success E
+      | inl E
+        => let E := RewriteRules.RewriteArithWithCasts E in
+           let E := match translate_to_fancy with
+                    | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancyWithCasts invert_low invert_high E
+                    | None => E
+                    end in
+           Success E
       | inr (inl (b, E))
         => Error (Computed_bounds_are_not_tight_enough b out_bounds E arg_bounds)
       | inr (inr unsupported_casts)
@@ -844,15 +850,16 @@ Module Pipeline.
           | [ |- Wf _ ] => idtac
           | _ => eassumption || reflexivity
           end.. ].
-      { subst; split; [ | assumption ].
+      { subst; split; [ | solve [ wf_interp_t ] ].
         split_and; simpl in *.
-        split; [ solve [ eauto with nocore ] | ].
-        { intros; match goal with H : context[type.app_curried _ _ = _] |- _ => erewrite H; clear H end; eauto.
-          transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1).
-          { apply type.app_curried_Proper; [ | symmetry; eassumption ].
-            clear dependent arg1; clear dependent arg2; clear dependent out_bounds.
-            wf_interp_t. }
-          { apply Interp_PartialEvaluateWithListInfoFromBounds; auto. } } }
+        split; [ solve [ wf_interp_t; eauto with nocore ] | ].
+        intros; break_innermost_match; autorewrite with interp; try solve [ wf_interp_t ]; [ | ].
+        all: match goal with H : context[type.app_curried _ _ = _] |- _ => erewrite H; clear H end; eauto.
+        all: transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1);
+          [ | apply Interp_PartialEvaluateWithListInfoFromBounds; auto ].
+        all: apply type.app_curried_Proper; [ | symmetry; eassumption ].
+        all: clear dependent arg1; clear dependent arg2; clear dependent out_bounds.
+        all: wf_interp_t. }
       { wf_interp_t. } }
   Qed.