Push bounds side conditions through the pipeline

This will (hopefully) be useful for karatsuba.

10 files changed, 163 insertions, 48 deletions

diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v
index 7674e5f0e..ca7330796 100644
--- a/src/Compilers/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/MapCastByDeBruijnInterp.v
@@ -8,15 +8,18 @@ Require Import Crypto.Compilers.Named.MapCastInterp.
 Require Import Crypto.Compilers.Named.MapCastWf.
 Require Import Crypto.Compilers.Named.InterpretToPHOASInterp.
 Require Import Crypto.Compilers.Named.CompileInterp.
+Require Import Crypto.Compilers.Named.CompileInterpSideConditions.
 Require Import Crypto.Compilers.Named.CompileWf.
 Require Import Crypto.Compilers.Named.PositiveContext.
 Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
 Require Import Crypto.Compilers.Named.PositiveContext.DefaultsProperties.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.MapCastByDeBruijn.
+Require Import Crypto.Compilers.InterpSideConditions.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
+Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
 Section language.
@@ -30,6 +33,7 @@ Section language.
           (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst)
           {interp_base_type_bounds : base_type_code -> Type}
           (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst)
+          (interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop)
           (pick_typeb : forall t, interp_base_type_bounds t -> base_type_code).
   Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
   Context (cast_op : forall t tR (opc : op t tR) args_bs,
@@ -43,12 +47,14 @@ Section language.
   Context (interp_op_bounds_correct
            : forall t tR opc bs
                     (v : interp_flat_type interp_base_type t)
-                    (H : inbounds t bs v),
+                    (H : inbounds t bs v)
+                    (Hside : to_prop (interped_op_side_conditions _ _ opc v)),
               inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v))
           (pull_cast_back
            : forall t tR opc bs
                     (v : interp_flat_type interp_base_type (pick_type bs))
-                    (H : inbounds t bs (cast_back t bs v)),
+                    (H : inbounds t bs (cast_back t bs v))
+                    (Hside : to_prop (interped_op_side_conditions _ _ opc (cast_back t bs v))),
               interp_op t tR opc (cast_back t bs v)
               =
               cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v)).
@@ -76,7 +82,8 @@ Section language.
         (Hwf : Wf e)
         (input_bounds : interp_flat_type interp_base_type_bounds (domain t))
     : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e'))
-             v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v),
+             v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v)
+             (Hside : to_prop (InterpSideConditions interp_op interped_op_side_conditions e v)),
       Interp interp_op_bounds e input_bounds = b
       /\ @inbounds _ b (Interp interp_op e v)
       /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v).
@@ -102,7 +109,8 @@ Section language.
       |
       | change (interp interp_op (?e ?var) ?v') with (Interp interp_op e v');
         unfold Interp, InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen;
-        rewrite <- interp_interp_to_phoas; [ reflexivity | ] ].
+        rewrite <- interp_interp_to_phoas; [ reflexivity | ]
+      | ].
     { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=e _);
         [ reflexivity | auto | .. | eassumption ];
         auto using name_list_unique_DefaultNamesFor. }
@@ -114,5 +122,8 @@ Section language.
           [ auto | .. | eassumption ];
           auto using name_list_unique_DefaultNamesFor. }
       { intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence. } }
+    { erewrite (interp_side_conditions_compile (ContextOk:=PositiveContextOk)) with (e':=e _);
+        [ assumption | auto | .. | eassumption ];
+        auto using name_list_unique_DefaultNamesFor. }
   Qed.
 End language.
diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v
index ad067af64..e6dbb01ed 100644
--- a/src/Compilers/Named/MapCastInterp.v
+++ b/src/Compilers/Named/MapCastInterp.v
@@ -8,12 +8,15 @@ Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.ContextProperties.
 Require Import Crypto.Compilers.Named.ContextProperties.SmartMap.
+Require Import Crypto.Compilers.Named.InterpSideConditions.
+Require Import Crypto.Compilers.Named.InterpSideConditionsInterp.
 Require Import Crypto.Compilers.Named.MapCast.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.DestructHead.
@@ -35,6 +38,7 @@ Section language.
           {interp_base_type : base_type_code -> Type}
           (interp_op : forall src dst,
               op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst)
+          (interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop)
           (cast_backb: forall t b, interp_base_type (pick_typeb t b) -> interp_base_type t).
   Let cast_back : forall t b, interp_flat_type interp_base_type (@pick_type t b) -> interp_flat_type interp_base_type t
     := fun t b => SmartFlatTypeMapUnInterp cast_backb.
@@ -46,12 +50,14 @@ Section language.
   Context (interp_op_bounds_correct:
              forall t tR opc bs
                     (v : interp_flat_type interp_base_type t)
-                    (H : inbounds t bs v),
+                    (H : inbounds t bs v)
+                    (Hside : to_prop (interped_op_side_conditions _ _ opc v)),
                inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v))
           (pull_cast_back:
              forall t tR opc bs
                     (v : interp_flat_type interp_base_type (pick_type t bs))
-                    (H : inbounds t bs (cast_back t bs v)),
+                    (H : inbounds t bs (cast_back t bs v))
+                    (Hside : to_prop (interped_op_side_conditions _ _ opc (cast_back t bs v))),
                interp_op t tR opc (cast_back t bs v)
                =
                cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v))
@@ -139,6 +145,14 @@ Section language.
     | [ |- ?A /\ (exists v, None = Some v /\ @?B v) ]
       => exfalso
     end.
+  Local Ltac handle_bounds_side_conditions_step :=
+    match goal with
+    | [ H : interpf ?e = Some ?v, H' : interpf_side_conditions_gen _ _ _ ?e = Some (_, ?v')%core |- _ ]
+      => first [ constr_eq v v'; fail 1
+               | assert (Some v = Some v')
+                 by (erewrite <- H, snd_interpf_side_conditions_gen_eq, H'; reflexivity);
+                 inversion_option; (subst v || subst v') ]
+    end.
   Local Ltac fin_inbounds_cast_back_t_step :=
     match goal with
     | [ |- inboundsb _ _ _ /\ _ ]
@@ -170,7 +184,9 @@ Section language.
           | handle_exists_in_goal
           | solve [ auto ]
           | specializer_t_step
-          | fin_inbounds_cast_back_t_step ].
+          | fin_inbounds_cast_back_t_step
+          | handle_options_step
+          | handle_bounds_side_conditions_step ].
   Local Ltac t := repeat t_step.
 
   Local Ltac do_specialize_IHe :=
@@ -209,11 +225,13 @@ Section language.
                                      /\ cast_backb t b v' = v)
       r (Hr:interpf (interp_op:=interp_op) (ctx:=oldValues) e = Some r)
       r' (Hr':interpf (interp_op:=interp_op) (ctx:=newValues) e' = Some r')
+      (Hside : prop_of_option (interpf_side_conditions interp_op interped_op_side_conditions oldValues e))
     , interpf (interp_op:=interp_op_bounds) (ctx:=varBounds) e = Some b
       /\ @inbounds _ b r /\ cast_back _ _ r' = r.
   Proof using Type*.
     induction e; simpl interpf; simpl mapf_cast; unfold option_map, cast_back in *; intros;
-      repeat (break_match_hyps; inversion_option; inversion_sigma; simpl in *; unfold option_map in *; subst; try tauto).
+      unfold interpf_side_conditions in *; simpl in Hside;
+      repeat (repeat handle_options_step; break_match_hyps; inversion_option; inversion_sigma; autorewrite with push_to_prop in *; simpl in *; unfold option_map in *; subst; try tauto).
     { destruct (Hctx _ _ _ Hr) as [b' [Hb'[Hb'v[v'[Hv' Hv'v]]]]]; clear Hctx Hr; subst.
       repeat match goal with
                [H: ?e = Some ?x, G:?e = Some ?x' |- _] =>
@@ -221,17 +239,20 @@ Section language.
              end.
       auto. }
     { do_specialize_IHe.
-      destruct_head and; subst; intuition eauto; symmetry; rewrite_hyp ?*; eauto. }
+      repeat (handle_options_step || destruct_head_and || specialize_by_assumption).
+      subst; intuition eauto; try (symmetry; rewrite_hyp ?*; eauto);
+        repeat handle_bounds_side_conditions_step; auto. }
     { cbv [LetIn.Let_In] in *.
       do_specialize_IHe.
-      destruct IHe1 as [IHe1_eq IHe1]; rewrite_hyp *.
-      { apply IHe2; clear IHe2; try reflexivity.
-        intros ??? H.
+      destruct_head'_and.
+      destruct IHe1 as [IHe1_eq IHe1]; rewrite_hyp *; try assumption.
+      { apply IHe2; clear IHe2; try reflexivity; [ | t ].
+        intros ??? Hlookup.
         let b := fresh "b" in
         let H' := fresh "H'" in
         match goal with |- exists b0, ?v = Some b0 /\ _ => destruct v as [b|] eqn:H' end;
           [ exists b; split; [ reflexivity | ] | exfalso ];
-          revert H H'; t. } }
+          revert Hlookup H'; t. } }
     { do_specialize_IHe.
       t. }
   Qed.
@@ -253,6 +274,7 @@ Section language.
         v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v)
         r (Hr:interp (interp_op:=interp_op) (ctx:=oldValues) e v = Some r)
         r' (Hr':interp (interp_op:=interp_op) (ctx:=newValues) e' v' = Some r')
+        (Hside : prop_of_option (interp_side_conditions interp_op interped_op_side_conditions oldValues e v))
         , interp (interp_op:=interp_op_bounds) (ctx:=varBounds) e input_bounds = Some b
           /\ @inbounds _ b r /\ cast_back _ _ r' = r.
   Proof using Type*.
diff --git a/src/Compilers/Wf.v b/src/Compilers/Wf.v
index f0f5b505f..a56d3bbdd 100644
--- a/src/Compilers/Wf.v
+++ b/src/Compilers/Wf.v
@@ -4,7 +4,7 @@ Require Import Crypto.Util.Notations.
 
 Create HintDb wf discriminated.
 
-Ltac solve_wf_side_condition := solve [ eassumption | eauto 30 with wf ].
+Ltac solve_wf_side_condition := solve [ eassumption | eauto 250 with wf ].
 
 Section language.
   Context {base_type_code : Type}
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index 7b1254138..66145080c 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -156,7 +156,7 @@ Module Import Bounds.
     Definition id_with_alt {T1 T2 Tout} (x : interp_base_type T1) (y : interp_base_type T2)
       : interp_base_type Tout
       := truncation_bounds match T1, T2, Tout with
-                           | TZ, TZ, TZ => (*y*)x
+                           | TZ, TZ, TZ => y
                            | _, _, _ => x
                            end.
   End with_bitwidth.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index c0172c67a..e7ec688d3 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -9,6 +9,7 @@ Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Stabilization.
+Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
 Require Import Crypto.Util.Tactics.DestructHead.
@@ -332,7 +333,7 @@ Lemma is_bounded_by_interp_op t tR (opc : op t tR)
       (bs : interp_flat_type Bounds.interp_base_type _)
       (v : interp_flat_type interp_base_type _)
       (H : Bounds.is_bounded_by bs v)
-      (*H_side : interped_op_side_conditions opc v = true*)
+      (H_side : to_prop (interped_op_side_conditions opc v))
   : Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v).
 Proof.
   destruct opc;
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
index 38ed60038..1701b4688 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
 Require Import Crypto.Util.Option.
+Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SpecializeBy.
@@ -31,7 +32,8 @@ Section with_round_up.
            : forall t tR (opc : op t tR)
                     (bs : interp_flat_type Bounds.interp_base_type _)
                     (v : interp_flat_type interp_base_type _)
-                    (H : Bounds.is_bounded_by bs v),
+                    (H : Bounds.is_bounded_by bs v)
+                    (Hside : to_prop (interped_op_side_conditions opc v)),
               Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v)).
   Context {round_up : nat -> option nat}.
 
@@ -132,6 +134,7 @@ Section with_round_up.
         (H : Bounds.is_bounded_by bs
                                   (SmartFlatTypeMapUnInterp
                                      (fun (t1 : base_type) (b0 : Bounds.interp_base_type t1) => cast_const) v))
+        (Hside : to_prop (interped_op_side_conditions opc (cast_back_flat_const v)))
     : interp_op t tR opc (cast_back_flat_const v)
       = cast_back_flat_const (interp_op (pick_type bs) (pick_type (Bounds.interp_op opc bs)) (genericize_op opc) v).
   Proof.
@@ -151,7 +154,9 @@ Section with_round_up.
                    | match goal with
                      | [ H : forall v, _ <= ?f v <= _ /\ _ -> _ |- context[?f ?v'] ]
                        => specialize (H v')
+                     | _ => progress specialize_by_assumption
                      | _ => progress specialize_by auto
+                     | [ H : forall v : unit, _ |- _ ] => specialize (H tt)
                      | [ H : forall v : _ * _, _ /\ _ -> _ |- _ ]
                        => specialize (fun v1 v2 p1 p2 => H (v1, v2) (conj p1 p2));
                           cbn [fst snd] in H;
diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
index 330075ee5..28e305a8f 100644
--- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
@@ -5,10 +5,12 @@ Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Compilers.Z.MapCastByDeBruijnInterp.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.InterpSideConditions.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.IsBoundedBy.
 Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.PullCast.
 Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
+Require Import Crypto.Util.PointedProp.
 
 Lemma MapCastCorrect
       {round_up}
@@ -16,7 +18,8 @@ Lemma MapCastCorrect
       (Hwf : Wf e)
       (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
   : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
-           v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v),
+           v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
+           (Hside : to_prop (InterpSideConditions e v)),
     Interp (@Bounds.interp_op) e input_bounds = b
     /\ Bounds.is_bounded_by b (Interp interp_op e v)
     /\ cast_back_flat_const (Interp interp_op e' v') = (Interp interp_op e v).
@@ -34,6 +37,7 @@ Lemma MapCastCorrect_eq
       (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
   : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
            v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
+           (Hside : to_prop (InterpSideConditions e v))
            (Hevb : evb = Interp (@Bounds.interp_op) e input_bounds)
            (Hev : ev = Interp interp_op e v),
     evb = b
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index 5408c944c..88492074b 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -79,26 +79,37 @@ Require Import Crypto.Util.Sigma.MapProjections.
 Record PipelineOptions := { anf : bool }.
 Definition default_PipelineOptions :=
   {| anf := false |}.
-(** Do not change the name or the type of this definition *)
-Definition PostWfPipeline
-           round_up
+(** Do not change the name or the type of these two definitions *)
+(** The definition [PostWfPreBoundsPipeline] is for the part of the
+    pipeline that comes before [MapCast]; it must preserve the type of
+    the expression. *)
+Definition PostWfPreBoundsPipeline
            (opts : PipelineOptions)
            {t} (e : Expr base_type op t)
+  : Expr base_type op t
+  := let e := InlineConst e in
+     let e := InlineConst (SimplifyArith false e) in
+     let e := InlineConst (SimplifyArith false e) in
+     let e := InlineConst (SimplifyArith false e) in
+     let e := if opts.(anf) then InlineConst (ANormal e) else e in
+     let e := RewriteAdc e in
+     let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
+     let e := if opts.(anf) then InlineConstAndOpp (ANormal e) else e in
+     let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
+     (*let e := CSE false e in*)
+     e.
+(** The definition [PostWfBoundsPipeline] is for the part of the
+    pipeline that begins with [MapCast]. *)
+Definition PostWfBoundsPipeline
+           round_up
+           (opts : PipelineOptions)
+           {t} (e0 : Expr base_type op t)
+           (e : Expr base_type op t)
            (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
   : option (@ProcessedReflectivePackage round_up)
   := Build_ProcessedReflectivePackage_from_option_sigma
-       e input_bounds
-       (let e := InlineConst e in
-        let e := InlineConst (SimplifyArith false e) in
-        let e := InlineConst (SimplifyArith false e) in
-        let e := InlineConst (SimplifyArith false e) in
-        let e := if opts.(anf) then InlineConst (ANormal e) else e in
-        let e := RewriteAdc e in
-        let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
-        let e := if opts.(anf) then InlineConstAndOpp (ANormal e) else e in
-        let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
-        (*let e := CSE false e in*)
-        let e := MapCast _ e input_bounds in
+       e0 input_bounds
+       (let e := MapCast _ e input_bounds in
         option_map
           (projT2_map
              (fun b e'
@@ -107,24 +118,27 @@ Definition PostWfPipeline
                  e'))
           e).
 
-(** *** Correctness proof of the Pre-Wf Pipeline *)
+(** *** Correctness proof of the Post-Wf Pipeline *)
 (** Do not change the statement of this lemma. *)
 Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Compilers.Equality.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.InterpSideConditions.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.PointedProp.
 
 Section with_round_up_list.
   Context {allowable_lgsz : list nat}.
 
   Local Notation pick_typeb := (@Bounds.bounds_to_base_type (Bounds.round_up_to_in_list allowable_lgsz)) (only parsing).
   Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
+  Local Opaque to_prop InterpSideConditions.
 
   Definition PostWfPipelineCorrect
              opts
@@ -132,23 +146,25 @@ Section with_round_up_list.
              (e : Expr base_type op t)
              (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
              (Hwf : Wf e)
-             {b e'} (He : PostWfPipeline _ opts e input_bounds
-                          = Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |})
+             (e' := PostWfPreBoundsPipeline opts e)
+             {b e''} (He' : PostWfBoundsPipeline _ opts e e' input_bounds
+                            = Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e'' |})
              (v : interp_flat_type Syntax.interp_base_type (domain t))
              (v' : interp_flat_type Syntax.interp_base_type (pick_type input_bounds))
              (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
+             (Hside : to_prop (InterpSideConditions e' v))
     : Bounds.is_bounded_by b (Interp interp_op e v)
-      /\ cast_back_flat_const (Interp interp_op e' v') = Interp interp_op e v.
+      /\ cast_back_flat_const (Interp interp_op e'' v') = Interp interp_op e v.
   Proof.
     (** These first two lines probably shouldn't change much *)
-    unfold PostWfPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *.
+    unfold PostWfBoundsPipeline, PostWfPreBoundsPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *; subst e'.
     repeat (break_match_hyps || inversion_option || inversion_ProcessedReflectivePackage
             || inversion_sigma || eliminate_hprop_eq || inversion_prod
             || simpl in * || subst).
     (** Now handle all the transformations that come after the word-size selection *)
     all:autorewrite with reflective_interp.
     (** Now handle word-size selection *)
-    all:(eapply MapCastCorrect_eq; [ | eassumption | eassumption | .. ];
+    all:(eapply MapCastCorrect_eq; [ | eassumption | eassumption | assumption | .. ];
          [ solve [ auto 60 with wf ] | reflexivity | ]).
     (** Now handle all the transformations that come before the word-size selection *)
     all:repeat autorewrite with reflective_interp; reflexivity.
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 1f82cb9f8..f132eb92a 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -22,6 +22,8 @@ Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Compilers.Z.Bounds.Relax.
 Require Import Crypto.Compilers.Reify.
 Require Import Crypto.Compilers.Z.Reify.
+Require Import Crypto.Compilers.InterpSideConditions.
+Require Import Crypto.Compilers.Z.InterpSideConditions.
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.SubstLet.
@@ -123,6 +125,45 @@ Ltac unify_abstract_cbv_interp_rhs_reflexivity :=
        unify LHS RHS'; abstract exact_no_check (eq_refl RHS')
   end.
 
+(** *** Boundedness Lemma Side Conditions *)
+(** The tactic [handle_boundedness_side_condition] unfolds relevant
+    identifiers in the side-condition of the boundedness lemma.  It
+    then calls [boundedness_side_condition_solver], which can be
+    overridden. *)
+(** The tactic [boundedness_side_condition_solver] attempts to solve
+    the algebraic side conditions of the boundedness lemma; it leaves
+    them over if it cannot solve them. *)
+Ltac boundedness_side_condition_solver :=
+  repeat match goal with
+         | [ |- _ /\ _ ] => apply conj
+         | [ |- ?x = ?x ] => reflexivity
+         end;
+  try abstract ring.
+Ltac handle_boundedness_side_condition :=
+  (** TODO: This next bit, with repeat intros [? ?], could be done
+        with a single [apply], if we make the right lemma.  We should
+        write that lemma. *)
+  cbv [PointedProp.to_prop Syntax.interp_flat_type Syntax.interp_base_type Syntax.domain Syntax.codomain];
+  repeat match goal with
+         | [ |- forall x : _ * _, _ ]
+           => let a := fresh in let b := fresh in intros [a b]; revert a b
+         | [ |- forall x, _ ]
+           => let x := fresh "x" in intro x
+         end;
+  cbv [id
+         fst snd
+         InterpSideConditions Compilers.InterpSideConditions.InterpSideConditions interp_side_conditions interpf_side_conditions interpf_side_conditions_gen
+         Z.Syntax.Util.interped_op_side_conditions
+         ExprInversion.invert_Abs
+         Syntax.interp_op Syntax.lift_op
+         Syntax.Zinterp_op
+         SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartValf SmartMap.SmartFlatTypeMapInterp2
+         Syntax.cast_const Syntax.ZToInterp Syntax.interpToZ];
+  cbv [PointedProp.and_pointed_Prop];
+  try match goal with
+      | [ |- True ] => exact I
+      end;
+  boundedness_side_condition_solver.
 
 (** ** Assemble the parts of Pipeline.Definition, in Gallina *)
 (** In this section, we assemble [PreWfPipeline] and [PostWfPipeline],
@@ -144,6 +185,7 @@ Require Import Crypto.Compilers.Z.Syntax.Equality.
 Require Import Crypto.Compilers.Z.Syntax.Util.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Compilers.Z.Bounds.Relax.
+Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.PartiallyReifiedProp.
 Require Import Crypto.Util.Equality.
 
@@ -164,6 +206,7 @@ Section with_round_up_list.
              {fZ}
              {final_e_evar : interp_flat_type Syntax.interp_base_type (pick_type given_output_bounds)}
              {e}
+             {e_pre_pkg}
              {e_pkg}
              (** ** reification *)
              (rexpr_sig : { rexpr : Expr base_type op t | forall x, Interp Syntax.interp_op rexpr x = fZ x })
@@ -174,8 +217,10 @@ Section with_round_up_list.
              (Hwf : forall var1 var2,
                  let P := (@reflect_wfT base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil _ _ (ExprEta' e _) (ExprEta' e _)) in
                  trueify P = P)
+             (** ** post-wf-pre-bounds-pipeline *)
+             (Hpost_wf_pre_bounds : e_pre_pkg = PostWfPreBoundsPipeline opts e)
              (** ** post-wf-pipeline *)
-             (Hpost : e_pkg = PostWfPipeline _ opts e input_bounds)
+             (Hpost : e_pkg = PostWfBoundsPipeline _ opts e e_pre_pkg input_bounds)
              (Hpost_correct : Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg)
              (** ** renaming *)
              (Hrenaming : e_final = e')
@@ -187,8 +232,9 @@ Section with_round_up_list.
                 = eq_rect _ (fun t => Expr base_type op (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane))
              (** ** instantiation of original evar *)
              (Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v')
-             (** ** side condition *)
-             (Hv : Bounds.is_bounded_by input_bounds (cast_back_flat_const v'))
+             (** ** side conditions (boundedness) *)
+             (Hv1 : Bounds.is_bounded_by input_bounds (cast_back_flat_const v'))
+             (Hv2 : forall v, PointedProp.to_prop (InterpSideConditions e_pre_pkg v))
     : Bounds.is_bounded_by given_output_bounds (fZ (cast_back_flat_const v'))
       /\ cast_back_flat_const final_e_evar = fZ (cast_back_flat_const v').
   Proof.
@@ -223,8 +269,8 @@ End with_round_up_list.
 Ltac refine_with_pipeline_correct opts :=
   lazymatch goal with
   | [ |- _ /\ ?castback ?fW = ?fZ ?arg ]
-    => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ _ _ _ _ _ _) in
-       simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _);
+    => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ _ _ _ _ _ _ _) in
+       simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _ _ _);
        subst fW fZ
   end;
   [ eexists
@@ -264,6 +310,8 @@ Ltac solve_side_conditions :=
    unify_abstract_vm_compute_rhs_reflexivity |
    (** ** reflective wf side-condition 2 *)
    unify_abstract_vm_compute_rhs_reflexivity |
+   (** ** post-wf-pre-bounds-pipeline *)
+   unify_abstract_vm_compute_rhs_reflexivity |
    (** ** post-wf pipeline *)
    unify_abstract_vm_compute_rhs_reflexivity |
    (** ** post-wf pipeline gives [Some _] *)
@@ -283,7 +331,9 @@ Ltac solve_side_conditions :=
    (** ** unfolding of [interp] constants *)
    unify_abstract_cbv_interp_rhs_reflexivity |
    (** ** boundedness of inputs *)
-   abstract handle_bounds_from_hyps ].
+   abstract handle_bounds_from_hyps |
+   (** ** boundedness side-condition *)
+   handle_boundedness_side_condition ].
 
 
 (** ** The Entire Pipeline *)
diff --git a/src/Compilers/Z/MapCastByDeBruijnInterp.v b/src/Compilers/Z/MapCastByDeBruijnInterp.v
index cd145c6fa..068c74ef2 100644
--- a/src/Compilers/Z/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/Z/MapCastByDeBruijnInterp.v
@@ -4,7 +4,10 @@ Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Compilers.MapCastByDeBruijnInterp.
 Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
 Require Import Crypto.Compilers.Z.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Z.InterpSideConditions.
+Require Import Crypto.Util.PointedProp.
 
 Section language.
   Context {interp_base_type_bounds : base_type -> Type}
@@ -22,12 +25,14 @@ Section language.
   Context (interp_op_bounds_correct
            : forall t tR opc bs
                     (v : interp_flat_type interp_base_type t)
-                    (H : inbounds t bs v),
+                    (H : inbounds t bs v)
+                    (Hside : to_prop (interped_op_side_conditions opc v)),
               inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v))
           (pull_cast_back
            : forall t tR opc bs
                     (v : interp_flat_type interp_base_type (pick_type bs))
-                    (H : inbounds t bs (cast_back t bs v)),
+                    (H : inbounds t bs (cast_back t bs v))
+                    (Hside : to_prop (interped_op_side_conditions opc (cast_back t bs v))),
               interp_op t tR opc (cast_back t bs v)
               =
               cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v)).
@@ -40,7 +45,8 @@ Section language.
         (Hwf : Wf e)
         (input_bounds : interp_flat_type interp_base_type_bounds (domain t))
     : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e'))
-             v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v),
+             v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v)
+             (Hside : to_prop (InterpSideConditions e v)),
       Interp interp_op_bounds e input_bounds = b
       /\ @inbounds _ b (Interp interp_op e v)
       /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v).