path: root/src/BoundsPipeline.v

(** * 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.RewriterAll.
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.RewriterAll
  Crypto.AbstractInterpretationWf
  Crypto.AbstractInterpretationProofs
  Crypto.Language
  Crypto.UnderLets
  Crypto.AbstractInterpretation
  Crypto.Rewriter
  Crypto.MiscCompilerPasses
  Crypto.CStringification.

Import
  LanguageWf.Compilers
  UnderLetsProofs.Compilers
  MiscCompilerPassesProofs.Compilers
  RewriterAll.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
         | base.type.zrange
           => 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.option A
           => fun a b
              => match a, b with
                 | None, None => (false, nil, nil)
                 | Some _, None => (false, nil, nil)
                 | None, Some _ => (true, nil, nil)
                 | Some None, Some None
                 | Some (Some _), Some None
                 | Some None, Some (Some _)
                   => (false, nil, nil)
                 | Some (Some a), Some (Some b)
                   => @find_too_loose_base_bounds A a b
                 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" syntax_tree (fun _ _ => nil) 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
           let E := RewriteRules.RewriteStripLiteralCasts E 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)
             (with_dead_code_elimination : bool := true)
             (with_subst01 : bool)
             (translate_to_fancy : option to_fancy_args)
             (possible_values : list Z)
             {t}
             (E : Expr t)
             (comment : type.for_each_lhs_of_arrow ToString.C.OfPHOAS.var_data t -> ToString.C.OfPHOAS.var_data (type.final_codomain t) -> list string)
             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 E' comment 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)
             (with_dead_code_elimination : bool := true)
             (with_subst01 : bool)
             (translate_to_fancy : option to_fancy_args)
             relax_zrange
             {t}
             (E : Expr t)
             (comment : type.for_each_lhs_of_arrow ToString.C.OfPHOAS.var_data t -> ToString.C.OfPHOAS.var_data (type.final_codomain t) -> list string)
             arg_bounds
             out_bounds
    : ErrorT (string * ToString.C.ident_infos)
    := let E := BoundsPipelineToStrings
                  static type_prefix name
                  (*with_dead_code_elimination*)
                  with_subst01
                  translate_to_fancy
                  relax_zrange
                  E comment 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 t E arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c t E arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl)
         (only parsing).
  Local Notation out_bounds_of_pipeline result
    := ((fun a b c t E arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c t E arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl)
         (only parsing).

  Notation FromPipelineToString prefix name result
    := (fun comment
        => ((prefix ++ name)%string,
            match result with
            | Success E'
              => let E := ToString.C.ToFunctionLines
                            true true (* static *) prefix (prefix ++ name)%string
                            E'
                            (comment (prefix ++ name)%string)
                            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.