move src/Experiments/NewPipeline/ to src/

1 files changed, 648 insertions, 0 deletions

diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v
new file mode 100644
index 000000000..2b74545f3
--- /dev/null
+++ b/src/BoundsPipeline.v
@@ -0,0 +1,648 @@
+(** * BoundsPipeline *)
+(** This file assembles the various compiler stages together into a
+    composed pipeline.  It is the final interface for the compiler,
+    right before integration with Arithmetic. *)
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.QArith.QArith_base.
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ErrorT.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Strings.Show.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Show.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.HasBody.
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Crypto.Language.
+Require Crypto.UnderLets.
+Require Crypto.AbstractInterpretation.
+Require Crypto.Rewriter.
+Require Crypto.MiscCompilerPasses.
+Require Crypto.CStringification.
+Require Crypto.LanguageWf.
+Require Crypto.UnderLetsProofs.
+Require Crypto.MiscCompilerPassesProofs.
+Require Crypto.RewriterProofs.
+Require Crypto.AbstractInterpretationWf.
+Require Crypto.AbstractInterpretationProofs.
+Require Import Crypto.Util.Notations.
+Import ListNotations. Local Open Scope Z_scope.
+
+Import
+  Crypto.LanguageWf
+  Crypto.UnderLetsProofs
+  Crypto.MiscCompilerPassesProofs
+  Crypto.RewriterProofs
+  Crypto.AbstractInterpretationWf
+  Crypto.AbstractInterpretationProofs
+  Crypto.Language
+  Crypto.UnderLets
+  Crypto.AbstractInterpretation
+  Crypto.Rewriter
+  Crypto.MiscCompilerPasses
+  Crypto.CStringification.
+
+Import
+  LanguageWf.Compilers
+  UnderLetsProofs.Compilers
+  MiscCompilerPassesProofs.Compilers
+  RewriterProofs.Compilers
+  AbstractInterpretationWf.Compilers
+  AbstractInterpretationProofs.Compilers
+  Language.Compilers
+  UnderLets.Compilers
+  AbstractInterpretation.Compilers
+  Rewriter.Compilers
+  MiscCompilerPasses.Compilers
+  CStringification.Compilers.
+
+Import Compilers.defaults.
+
+Definition round_up_bitwidth_gen (possible_values : list Z) (bitwidth : Z) : option Z
+  := List.fold_right
+       (fun allowed cur
+        => if bitwidth <=? allowed
+           then Some allowed
+           else cur)
+       None
+       possible_values.
+
+Lemma round_up_bitwidth_gen_le possible_values bitwidth v
+  : round_up_bitwidth_gen possible_values bitwidth = Some v
+    -> bitwidth <= v.
+Proof.
+  cbv [round_up_bitwidth_gen].
+  induction possible_values as [|x xs IHxs]; cbn; intros; inversion_option.
+  break_innermost_match_hyps; Z.ltb_to_lt; inversion_option; subst; trivial.
+  specialize_by_assumption; omega.
+Qed.
+
+Definition relax_zrange_gen (possible_values : list Z) : zrange -> option zrange
+  := (fun '(r[ l ~> u ])
+      => if (0 <=? l)%Z
+         then option_map (fun u => r[0~>2^u-1])
+                         (round_up_bitwidth_gen possible_values (Z.log2_up (u+1)))
+        else None)%zrange.
+
+Lemma relax_zrange_gen_good
+      (possible_values : list Z)
+  : forall r r' z : zrange,
+    (z <=? r)%zrange = true -> relax_zrange_gen possible_values r = Some r' -> (z <=? r')%zrange = true.
+Proof.
+  cbv [is_tighter_than_bool relax_zrange_gen]; intros *.
+  pose proof (Z.log2_up_nonneg (upper r + 1)).
+  rewrite !Bool.andb_true_iff; destruct_head' zrange; cbn [ZRange.lower ZRange.upper] in *.
+  cbv [List.fold_right option_map].
+  break_innermost_match; intros; destruct_head'_and;
+    try match goal with
+        | [ H : _ |- _ ] => apply round_up_bitwidth_gen_le in H
+        end;
+    inversion_option; inversion_zrange;
+      subst;
+      repeat apply conj;
+      Z.ltb_to_lt; try omega;
+        try (rewrite <- Z.log2_up_le_pow2_full in *; omega).
+Qed.
+
+Module Pipeline.
+  Import GeneralizeVar.
+  Inductive ErrorMessage :=
+  | Computed_bounds_are_not_tight_enough
+      {t} (computed_bounds expected_bounds : ZRange.type.base.option.interp (type.final_codomain t))
+      (syntax_tree : Expr t) (arg_bounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+  | No_modular_inverse (descr : string) (v : Z) (m : Z)
+  | Value_not_leZ (descr : string) (lhs rhs : Z)
+  | Value_not_leQ (descr : string) (lhs rhs : Q)
+  | Value_not_ltZ (descr : string) (lhs rhs : Z)
+  | Value_not_lt_listZ (descr : string) (lhs rhs : list Z)
+  | Value_not_le_listZ (descr : string) (lhs rhs : list Z)
+  | Values_not_provably_distinctZ (descr : string) (lhs rhs : Z)
+  | Values_not_provably_equalZ (descr : string) (lhs rhs : Z)
+  | Values_not_provably_equal_listZ (descr : string) (lhs rhs : list Z)
+  | Unsupported_casts_in_input {t} (e : @Compilers.defaults.Expr t) (ls : list { t : _ & ident t })
+  | Stringification_failed {t} (e : @Compilers.defaults.Expr t) (err : string)
+  | Invalid_argument (msg : string).
+
+  Notation ErrorT := (ErrorT ErrorMessage).
+
+  Section show.
+    Local Open Scope string_scope.
+    Fixpoint find_too_loose_base_bounds {t}
+      : ZRange.type.base.option.interp t -> ZRange.type.base.option.interp t-> bool * list (nat * nat) * list (zrange * zrange)
+      := match t return ZRange.type.base.option.interp t -> ZRange.type.option.interp t-> bool * list (nat * nat) * list (zrange * zrange) with
+         | base.type.unit
+           => fun 'tt 'tt => (false, nil, nil)
+         | base.type.nat
+         | base.type.bool
+           => fun _ _ => (false, nil, nil)
+         | base.type.Z
+           => fun a b
+              => match a, b with
+                 | None, None => (false, nil, nil)
+                 | Some _, None => (false, nil, nil)
+                 | None, Some _ => (true, nil, nil)
+                 | Some a, Some b
+                   => if is_tighter_than_bool a b
+                      then (false, nil, nil)
+                      else (false, nil, ((a, b)::nil))
+                 end
+         | base.type.prod A B
+           => fun '(ra, rb) '(ra', rb')
+              => let '(b1, lens1, ls1) := @find_too_loose_base_bounds A ra ra' in
+                 let '(b2, lens2, ls2) := @find_too_loose_base_bounds B rb rb' in
+                 (orb b1 b2, lens1 ++ lens2, ls1 ++ ls2)%list
+         | base.type.list A
+           => fun ls1 ls2
+              => match ls1, ls2 with
+                 | None, None
+                 | Some _, None
+                   => (false, nil, nil)
+                 | None, Some _
+                   => (true, nil, nil)
+                 | Some ls1, Some ls2
+                   => List.fold_right
+                        (fun '(b, len, err) '(bs, lens, errs)
+                         => (orb b bs, len ++ lens, err ++ errs)%list)
+                        (false,
+                         (if (List.length ls1 =? List.length ls2)%nat
+                          then nil
+                          else ((List.length ls1, List.length ls2)::nil)),
+                         nil)
+                        (List.map
+                           (fun '(a, b) => @find_too_loose_base_bounds A a b)
+                           (List.combine ls1 ls2))
+                 end
+         end.
+
+    Definition find_too_loose_bounds {t}
+      : ZRange.type.option.interp t -> ZRange.type.option.interp t-> bool * list (nat * nat) * list (zrange * zrange)
+      := match t with
+         | type.arrow s d => fun _ _ => (false, nil, nil)
+         | type.base t => @find_too_loose_base_bounds t
+         end.
+    Definition explain_too_loose_bounds {t} (b1 b2 : ZRange.type.option.interp t)
+      : string
+      := let '(none_some, lens, bs) := find_too_loose_bounds b1 b2 in
+         String.concat
+           String.NewLine
+           ((if none_some then "Found None where Some was expected"::nil else nil)
+              ++ (List.map
+                    (A:=nat*nat)
+                    (fun '(l1, l2) => "Found a list of length " ++ show false l1 ++ " where a list of length " ++ show false l2 ++ " was expected.")
+                    lens)
+              ++ (List.map
+                    (A:=zrange*zrange)
+                    (fun '(b1, b2) => "The bounds " ++ show false b1 ++ " are looser than the expected bounds " ++ show false b2)
+                    bs)).
+
+    Global Instance show_lines_ErrorMessage : ShowLines ErrorMessage
+      := fun parens e
+         => maybe_wrap_parens_lines
+              parens
+              match e with
+              | Computed_bounds_are_not_tight_enough t computed_bounds expected_bounds syntax_tree arg_bounds
+                => ((["Computed bounds " ++ show true computed_bounds ++ " are not tight enough (expected bounds not looser than " ++ show true expected_bounds ++ ")."]%string)
+                      ++ [explain_too_loose_bounds (t:=type.base _) computed_bounds expected_bounds]
+                      ++ match ToString.C.ToFunctionLines
+                                 false (* do extra bounds check *) false (* static *) "" "f" nil syntax_tree None arg_bounds ZRange.type.base.option.None with
+                         | inl (E_lines, types_used)
+                           => ["When doing bounds analysis on the syntax tree:"]
+                                ++ E_lines ++ [""]
+                                ++ ["with input bounds " ++ show true arg_bounds ++ "." ++ String.NewLine]%string
+                         | inr errs
+                           => (["(Unprintible syntax tree used in bounds analysis)" ++ String.NewLine]%string)
+                               ++ ["Stringification failed on the syntax tree:"] ++ show_lines false syntax_tree ++ [errs]
+                         end)%list
+              | No_modular_inverse descr v m
+                => ["Could not compute a modular inverse (" ++ descr ++ ") for " ++ show false v ++ " mod " ++ show false m]
+              | Value_not_leZ descr lhs rhs
+                => ["Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs]
+              | Value_not_leQ descr lhs rhs
+                => ["Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs]
+              | Value_not_ltZ descr lhs rhs
+                => ["Value not < (" ++ descr ++ ") : expected " ++ show false lhs ++ " < " ++ show false rhs]
+              | Value_not_lt_listZ descr lhs rhs
+                => ["Value not < (" ++ descr ++ ") : expected " ++ show false lhs ++ " < " ++ show false rhs]
+              | Value_not_le_listZ descr lhs rhs
+                => ["Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs]
+              | Values_not_provably_distinctZ descr lhs rhs
+                => ["Values not provably distinct (" ++ descr ++ ") : expected " ++ show true lhs ++ " ≠ " ++ show true rhs]
+              | Values_not_provably_equalZ descr lhs rhs
+              | Values_not_provably_equal_listZ descr lhs rhs
+                => ["Values not provably equal (" ++ descr ++ ") : expected " ++ show true lhs ++ " = " ++ show true rhs]
+              | Unsupported_casts_in_input t e ls
+                => ["Unsupported casts in input syntax tree:"]
+                     ++ show_lines false e
+                     ++ ["Unsupported casts: " ++ @show_list _ (fun p v => show p (projT2 v)) false ls]
+              | Stringification_failed t e err => ["Stringification failed on the syntax tree:"] ++ show_lines false e ++ [err]
+              | Invalid_argument msg
+                => ["Invalid argument:" ++ msg]%string
+              end.
+    Local Instance show_ErrorMessage : Show ErrorMessage
+      := fun parens err => String.concat String.NewLine (show_lines parens err).
+  End show.
+
+  Definition invert_result {T} (v : ErrorT T)
+    := match v return match v with Success _ => T | _ => ErrorMessage end with
+       | Success v => v
+       | Error msg => msg
+       end.
+
+  Record to_fancy_args := { invert_low : Z (*log2wordmax*) -> Z -> option Z ; invert_high : Z (*log2wordmax*) -> Z -> option Z ; value_range : zrange ; flag_range : zrange }.
+
+  Definition RewriteAndEliminateDeadAndInline {t}
+             (DoRewrite : Expr t -> Expr t)
+             (with_dead_code_elimination : bool)
+             (with_subst01 : bool)
+             (E : Expr t)
+    : Expr t
+    := let E := DoRewrite E in
+       (* Note that DCE evaluates the expr with two different [var]
+          arguments, and so results in a pipeline that is 2x slower
+          unless we pass through a uniformly concrete [var] type
+          first *)
+       dlet_nd e := ToFlat E in
+       let E := FromFlat e in
+       let E := if with_subst01 then Subst01.Subst01 E
+                else if with_dead_code_elimination then DeadCodeElimination.EliminateDead E
+                     else E in
+       let E := UnderLets.LetBindReturn E in
+       let E := DoRewrite E in (* after inlining, see if any new rewrite redexes are available *)
+       dlet_nd e := ToFlat E in
+       let E := FromFlat e in
+       let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in
+       E.
+
+  Definition BoundsPipeline
+             (with_dead_code_elimination : bool := true)
+             (with_subst01 : bool)
+             (translate_to_fancy : option to_fancy_args)
+             (possible_values : list Z)
+             (relax_zrange := relax_zrange_gen possible_values)
+             {t}
+             (E : Expr t)
+             arg_bounds
+             out_bounds
+  : ErrorT (Expr t)
+    := (*let E := expr.Uncurry E in*)
+      let E := PartialEvaluateWithListInfoFromBounds E arg_bounds in
+      let E := PartialEvaluate E in
+      let E := RewriteAndEliminateDeadAndInline (RewriteRules.RewriteArith 0) with_dead_code_elimination with_subst01 E in
+      let E := RewriteRules.RewriteArith (2^8) E in (* reassociate small consts *)
+      let E := match translate_to_fancy with
+               | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancy invert_low invert_high E
+               | None => E
+               end in
+      dlet_nd e := ToFlat E in
+      let E := FromFlat e in
+      let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in
+      match E' with
+      | inl E
+        => let E := RewriteAndEliminateDeadAndInline RewriteRules.RewriteArithWithCasts with_dead_code_elimination with_subst01 E in
+           let E := match translate_to_fancy with
+                    | Some {| invert_low := invert_low ; invert_high := invert_high ; value_range := value_range ; flag_range := flag_range |}
+                      => RewriteRules.RewriteToFancyWithCasts invert_low invert_high value_range flag_range 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)
+        => Error (Unsupported_casts_in_input E unsupported_casts)
+      end.
+
+  Definition BoundsPipelineToStrings
+             (static : bool)
+             (type_prefix : string)
+             (name : string)
+             (comment : list string)
+             (with_dead_code_elimination : bool := true)
+             (with_subst01 : bool)
+             (translate_to_fancy : option to_fancy_args)
+             (possible_values : list Z)
+             {t}
+             (E : Expr t)
+             arg_bounds
+             out_bounds
+    : ErrorT (list string * ToString.C.ident_infos)
+    := let E := BoundsPipeline
+                  (*with_dead_code_elimination*)
+                  with_subst01
+                  translate_to_fancy
+                  possible_values
+                  E arg_bounds out_bounds in
+       match E with
+       | Success E' => let E := ToString.C.ToFunctionLines
+                                  true static type_prefix name comment E' None arg_bounds out_bounds in
+                      match E with
+                      | inl E => Success E
+                      | inr err => Error (Stringification_failed E' err)
+                      end
+       | Error err => Error err
+       end.
+
+  Definition BoundsPipelineToString
+             (static : bool)
+             (type_prefix : string)
+             (name : string)
+             (comment : list string)
+             (with_dead_code_elimination : bool := true)
+             (with_subst01 : bool)
+             (translate_to_fancy : option to_fancy_args)
+             relax_zrange
+             {t}
+             (E : Expr t)
+             arg_bounds
+             out_bounds
+    : ErrorT (string * ToString.C.ident_infos)
+    := let E := BoundsPipelineToStrings
+                  static type_prefix name comment
+                  (*with_dead_code_elimination*)
+                  with_subst01
+                  translate_to_fancy
+                  relax_zrange
+                  E arg_bounds out_bounds in
+       match E with
+       | Success (E, types_used) => Success (ToString.C.LinesToString E, types_used)
+       | Error err => Error err
+       end.
+
+  Local Notation arg_bounds_of_pipeline result
+    := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl)
+         (only parsing).
+  Local Notation out_bounds_of_pipeline result
+    := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl)
+         (only parsing).
+
+  Notation FromPipelineToString prefix name result
+    := (((prefix ++ name)%string,
+         match result with
+         | Success E'
+           => let E := ToString.C.ToFunctionLines
+                         true true (* static *) prefix (prefix ++ name)%string [] E' None
+                         (arg_bounds_of_pipeline result)
+                         (out_bounds_of_pipeline result) in
+              match E with
+              | inl E => Success E
+              | inr err => Error (Pipeline.Stringification_failed E' err)
+              end
+         | Error err => Error err
+         end)).
+
+
+  Local Ltac wf_interp_t :=
+    repeat first [ progress destruct_head'_and
+                 | progress autorewrite with interp
+                 | solve [ auto with interp wf ]
+                 | solve [ typeclasses eauto ]
+                 | break_innermost_match_step
+                 | solve [ auto 100 with wf ]
+                 | progress intros ].
+
+  Class bounds_goodT {t} bounds
+    := bounds_good :
+         Proper (type.and_for_each_lhs_of_arrow (t:=t) (@partial.abstract_domain_R base.type ZRange.type.base.option.interp (fun _ => eq)))
+                bounds.
+
+  Class type_goodT (t : type.type base.type)
+    := type_good : type.andb_each_lhs_of_arrow type.is_base t = true.
+
+  Hint Extern 1 (type_goodT _) => vm_compute; reflexivity : typeclass_instances.
+
+  Lemma Wf_RewriteAndEliminateDeadAndInline {t} DoRewrite with_dead_code_elimination with_subst01
+        (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E))
+        E
+        (Hwf : Wf E)
+    : Wf (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E).
+  Proof. cbv [RewriteAndEliminateDeadAndInline Let_In]; wf_interp_t. Qed.
+
+  Global Hint Resolve @Wf_RewriteAndEliminateDeadAndInline : wf.
+
+  Lemma Interp_RewriteAndEliminateDeadAndInline {cast_outside_of_range} {t} DoRewrite with_dead_code_elimination with_subst01
+        (Interp_DoRewrite : forall E, Wf E -> expr.Interp (@ident.gen_interp cast_outside_of_range) (DoRewrite E) == expr.Interp (@ident.gen_interp cast_outside_of_range) E)
+        (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E))
+        E
+        (Hwf : Wf E)
+    : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E)
+      == expr.Interp (@ident.gen_interp cast_outside_of_range) E.
+  Proof.
+    cbv [RewriteAndEliminateDeadAndInline Let_In];
+      repeat (wf_interp_t || rewrite !Interp_DoRewrite).
+  Qed.
+
+  Hint Rewrite @Interp_RewriteAndEliminateDeadAndInline : interp.
+
+  Local Opaque RewriteAndEliminateDeadAndInline.
+  Lemma BoundsPipeline_correct
+             (with_dead_code_elimination : bool := true)
+             (with_subst01 : bool)
+             (translate_to_fancy : option to_fancy_args)
+             (possible_values : list Z)
+             {t}
+             (e : Expr t)
+             arg_bounds
+             out_bounds
+             {type_good : type_goodT t}
+             rv
+             (Hrv : BoundsPipeline (*with_dead_code_elimination*) with_subst01 translate_to_fancy possible_values e arg_bounds out_bounds = Success rv)
+             (Hwf : Wf e)
+             (Hfancy : match translate_to_fancy with
+                       | Some {| invert_low := il ; invert_high := ih |}
+                         => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1))
+                           /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2))
+                       | None => True
+                       end)
+    : (forall arg1 arg2
+              (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+              (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true),
+          ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg1) = true
+          /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1
+                                           = type.app_curried (Interp e) arg2)
+      /\ Wf rv.
+  Proof.
+    assert (Hbounds_Proper : bounds_goodT arg_bounds) by (apply type.and_eqv_for_each_lhs_of_arrow_not_higher_order, type_good).
+    cbv [BoundsPipeline Let_In bounds_goodT] in *;
+      repeat match goal with
+             | [ H : match ?x with _ => _ end = Success _ |- _ ]
+               => destruct x eqn:?; cbv beta iota in H; [ | break_innermost_match_hyps; congruence ];
+                    let H' := fresh in
+                    inversion H as [H']; clear H; rename H' into H
+             end.
+    { intros;
+        match goal with
+        | [ H : _ = _ |- _ ]
+          => let H' := fresh in
+             pose proof H as H';
+               eapply CheckedPartialEvaluateWithBounds_Correct in H';
+               [ destruct H' as [H01 Hwf'] | .. ]
+        end;
+        [
+        | lazymatch goal with
+          | [ |- Wf _ ] => idtac
+          | _ => eassumption || reflexivity || apply relax_zrange_gen_good
+          end.. ].
+      { subst; split; [ | solve [ wf_interp_t ] ].
+        split_and; simpl in *.
+        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.
+  Local Transparent RewriteAndEliminateDeadAndInline.
+
+  Definition BoundsPipeline_correct_transT
+             {t}
+             arg_bounds
+             out_bounds
+             (InterpE : type.interp base.interp t)
+             (rv : Expr t)
+    := (forall arg1 arg2
+               (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+               (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true),
+           ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg1) = true
+           /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1
+                                            = type.app_curried InterpE arg2)
+       /\ Wf rv.
+
+  Lemma BoundsPipeline_correct_trans
+        (with_dead_code_elimination : bool := true)
+        (with_subst01 : bool)
+        (translate_to_fancy : option to_fancy_args)
+        (Hfancy : match translate_to_fancy with
+                  | Some {| invert_low := il ; invert_high := ih |}
+                    => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1))
+                      /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2))
+                  | None => True
+                  end)
+        (possible_values : list Z)
+        {t}
+        (e : Expr t)
+        arg_bounds out_bounds
+        {type_good : type_goodT t}
+        (InterpE : type.interp base.interp t)
+        (InterpE_correct_and_Wf
+         : (forall arg1 arg2
+                   (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+                   (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true),
+               type.app_curried (Interp e) arg1 = type.app_curried InterpE arg2)
+           /\ Wf e)
+        rv
+        (Hrv : BoundsPipeline (*with_dead_code_elimination*) with_subst01 translate_to_fancy possible_values e arg_bounds out_bounds = Success rv)
+    : BoundsPipeline_correct_transT arg_bounds out_bounds InterpE rv.
+  Proof.
+    destruct InterpE_correct_and_Wf as [InterpE_correct Hwf].
+    split; [ intros arg1 arg2 Harg12 Harg1; erewrite <- InterpE_correct | ]; try eapply @BoundsPipeline_correct;
+      lazymatch goal with
+      | [ |- type.andb_bool_for_each_lhs_of_arrow _ _ _ = true ] => eassumption
+      | _ => try assumption
+      end; try eassumption.
+    etransitivity; try eassumption; symmetry; assumption.
+  Qed.
+
+  Ltac solve_bounds_good :=
+    repeat first [ progress cbv [bounds_goodT Proper partial.abstract_domain_R type_base] in *
+                 | progress cbn [type.and_for_each_lhs_of_arrow type.for_each_lhs_of_arrow partial.abstract_domain type.interp ZRange.type.base.option.interp type.related] in *
+                 | exact I
+                 | apply conj
+                 | exact eq_refl ].
+
+  Global Instance bounds0_good {t : base.type} {bounds} : @bounds_goodT t bounds.
+  Proof. solve_bounds_good. Qed.
+
+  Global Instance bounds1_good {s d : base.type} {bounds} : @bounds_goodT (s -> d) bounds.
+  Proof. solve_bounds_good. Qed.
+
+  Global Instance bounds2_good {a b D : base.type} {bounds} : @bounds_goodT (a -> b -> D) bounds.
+  Proof. solve_bounds_good. Qed.
+
+  Global Instance bounds3_good {a b c D : base.type} {bounds} : @bounds_goodT (a -> b -> c -> D) bounds.
+  Proof. solve_bounds_good. Qed.
+End Pipeline.
+
+Module Export Hints.
+  Hint Extern 1 (@Pipeline.bounds_goodT _ _) => solve [ Pipeline.solve_bounds_good ] : typeclass_instances.
+  Global Strategy -100 [type.interp ZRange.type.option.interp ZRange.type.base.option.interp GallinaReify.Reify_as GallinaReify.reify type_base].
+  Global Strategy -10 [type.app_curried type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow type.related type.interp base.interp base.base_interp type.andb_bool_for_each_lhs_of_arrow fst snd ZRange.type.option.is_bounded_by].
+End Hints.
+
+Module PipelineTactics.
+  Export Hints.
+
+  Ltac solve_side_conditions_of_BoundsPipeline_correct :=
+    repeat first [ progress cbn [fst snd] in *
+                 | match goal with
+                   | [ |- ?x = ?x ] => reflexivity
+                   | [ |- unit ] => constructor
+                   | [ |- True ] => constructor
+                   | [ |- context[andb _ _ = true] ] => rewrite Bool.andb_true_iff
+                   | [ |- and _ _ ] => apply conj
+                   | [ |- ?x = ?y ] => is_evar y; reflexivity
+                   | [ |- ZRange.type.base.option.is_bounded_by _ _ = true ] => assumption
+                   end ].
+
+  Ltac do_unfolding :=
+    cbv [type.interp ZRange.type.option.interp ZRange.type.base.option.interp GallinaReify.Reify_as GallinaReify.reify type_base] in *;
+    cbn [type.app_curried type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow type.related type.interp base.interp base.base_interp type.andb_bool_for_each_lhs_of_arrow fst snd ZRange.type.option.is_bounded_by] in *.
+
+  Ltac curry_args lem :=
+    let T := type of lem in
+    lazymatch (eval cbn [fst snd] in T) with
+    | forall x : ?A * ?B, _
+      => let a := fresh in
+         let b := fresh in
+         curry_args (fun (a : A) (b : B) => lem (a, b))
+    | forall x : unit, _
+      => curry_args (lem tt)
+    | forall x : True, _
+      => curry_args (lem I)
+    | forall x : ?A /\ ?B, _
+      => let a := fresh in
+         let b := fresh in
+         curry_args (fun (a : A) (b : B) => lem (conj a b))
+    | forall x : ?A, _
+      => constr:(fun x : A => ltac:(let v := curry_args (lem x) in exact v))
+    | ?T
+      => let T' := (eval cbn [fst snd] in T) in
+         constr:(lem : T')
+    end.
+
+  Ltac use_compilers_correctness Hres :=
+    eapply Pipeline.BoundsPipeline_correct in Hres;
+    [ | eauto using relax_zrange_gen_good with typeclass_instances.. ];
+    [ do_unfolding;
+      let Hres' := fresh in
+      destruct Hres as [Hres' _] (* remove Wf conjunct *);
+      let lem' := curry_args Hres' in
+      pose proof lem' as Hres; clear Hres';
+      let H1 := fresh in
+      let H2 := fresh in
+      edestruct Hres as [H1 H2]; revgoals;
+      [ first [ ((* first try to be smart about which side of the lemma we use *)
+                  lazymatch goal with
+                  | [ |- _ = true ] => eapply H1
+                  | [ |- _ = _ ] => erewrite H2
+                  | [ |- ?list_Z_bounded_by _ _ ] => eapply H1
+                  end)
+                  (* but if that doesn't work, try both ways *)
+              | eapply H1
+              | erewrite H2 ];
+        clear H1 H2 Hres
+      | .. ];
+      solve_side_conditions_of_BoundsPipeline_correct
+    | match goal with
+      | [ |- Wf _ ]
+        => repeat apply expr.Wf_APP; auto with wf wf_gen_cache
+      end ].
+End PipelineTactics.