9 files changed, 785 insertions, 426 deletions

diff --git a/_CoqProject b/_CoqProject
index 31c52a268..fc49cbf15 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -253,15 +253,16 @@ src/Experiments/NewPipeline/Language.v
 src/Experiments/NewPipeline/LanguageInversion.v
 src/Experiments/NewPipeline/LanguageWf.v
 src/Experiments/NewPipeline/MiscCompilerPasses.v
-src/Experiments/NewPipeline/MiscCompilerPassesWf.v
+src/Experiments/NewPipeline/MiscCompilerPassesProofs.v
 src/Experiments/NewPipeline/Rewriter.v
+src/Experiments/NewPipeline/RewriterProofs.v
 src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
 src/Experiments/NewPipeline/StandaloneHaskellMain.v
 src/Experiments/NewPipeline/StandaloneOCamlMain.v
 src/Experiments/NewPipeline/Toplevel1.v
 src/Experiments/NewPipeline/Toplevel2.v
 src/Experiments/NewPipeline/UnderLets.v
-src/Experiments/NewPipeline/UnderLetsWf.v
+src/Experiments/NewPipeline/UnderLetsProofs.v
 src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.v
 src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v
 src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index 560f89199..60007288f 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -3,41 +3,88 @@ Require Import Crypto.Util.Sum.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Experiments.NewPipeline.Language.
+Require Import Crypto.Experiments.NewPipeline.LanguageInversion.
+Require Import Crypto.Experiments.NewPipeline.LanguageWf.
+Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs.
 Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation.
 Local Open Scope Z_scope.
 
 Module Compilers.
-  Export Language.Compilers.
-  Export UnderLets.Compilers.
-  Export AbstractInterpretation.Compilers.
+  Import Language.Compilers.
+  Import UnderLets.Compilers.
+  Import AbstractInterpretation.Compilers.
+  Import LanguageInversion.Compilers.
+  Import LanguageWf.Compilers.
+  Import UnderLetsProofs.Compilers.
   Import invert_expr.
   Import defaults.
 
+  Module Import partial.
+    Import AbstractInterpretation.Compilers.partial.
+    Section with_var2.
+      Context {var1 var2 : type -> Type}.
+
+      Lemma wf_eta_expand_with_bound G {t} e1 e2 b_in (Hwf : @expr.wf _ _ var1 var2 G t e1 e2)
+        : expr.wf G (eta_expand_with_bound e1 b_in) (eta_expand_with_bound e2 b_in).
+      Proof.
+        cbv [eta_expand_with_bound ident.eta_expand_with_bound eta_expand_with_bound'].
+      Admitted.
+    End with_var2.
+
+    Lemma Wf_EtaExpandWithBound {t} (E : Expr t) b_in (Hwf : Wf E)
+      : Wf (EtaExpandWithBound E b_in).
+    Proof. repeat intro; apply wf_eta_expand_with_bound, Hwf. Qed.
+  End partial.
+
   Axiom admit_pf : False.
   Local Notation admit := (match admit_pf with end).
 
+  Lemma Wf_PartialEvaluateWithListInfoFromBounds
+        {t} (E : Expr t)
+        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+        (Hwf : Wf E)
+    : Wf (PartialEvaluateWithListInfoFromBounds E b_in).
+  Proof. apply Wf_EtaExpandWithBound, Hwf. Qed.
+
+  Lemma Interp_PartialEvaluateWithListInfoFromBounds
+        {t} (E : Expr t)
+        (Hwf : Wf E)
+        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp 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) b_in arg1 = true),
+      type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds E b_in)) arg1 = type.app_curried (Interp E) arg2.
+  Proof.
+  Admitted.
+
+  Hint Resolve Wf_EtaExpandWithBound Wf_PartialEvaluateWithListInfoFromBounds : wf.
+
   Theorem CheckedPartialEvaluateWithBounds_Correct
           (relax_zrange : zrange -> option zrange)
           (Hrelax : forall r r' z, is_tighter_than_bool z r = true
                                    -> relax_zrange r = Some r'
                                    -> is_tighter_than_bool z r' = true)
           {t} (E : Expr t)
+          (Hwf : Wf E)
           (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
           (b_out : ZRange.type.base.option.interp (type.final_codomain t))
           rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange E b_in b_out = inl rv)
-    : forall arg
-             (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg = true),
-      ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg) = true
-      /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg
-                                 = type.app_curried (Interp E) arg.
+    : 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) b_in arg1 = true),
+      ZRange.type.base.option.is_bounded_by b_out (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.
   Proof.
     cbv [CheckedPartialEvaluateWithBounds CheckPartialEvaluateWithBounds Let_In] in *;
       break_innermost_match_hyps; inversion_sum; subst.
-    intros arg Harg.
+    intros arg1 arg2 Harg12 Harg1.
     split.
     { eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ].
-      revert Harg.
+      clear dependent arg2.
+      revert Harg1.
       exact admit. (* boundedness *) }
-    { exact admit. (* correctness of interp *) }
+    { intro cast_outside_of_range; revert cast_outside_of_range Harg12.
+      exact admit. (* correctness of interp *) }
   Qed.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index afd028ee8..6c31dd0d9 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -143,6 +143,15 @@ Module Compilers.
          | arrow s d => fun x_xs y_ys => R s (fst x_xs) (fst y_ys) && @andb_bool_for_each_lhs_of_arrow _ f g R d (snd x_xs) (snd y_ys)
          end%bool.
 
+    Fixpoint and_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type}
+             (R : forall t, f t -> g t -> Prop)
+             {t}
+      : for_each_lhs_of_arrow f t -> for_each_lhs_of_arrow g t -> Prop
+      := match t with
+         | base t => fun _ _ => True
+         | arrow s d => fun x_xs y_ys => R s (fst x_xs) (fst y_ys) /\ @and_for_each_lhs_of_arrow _ f g R d (snd x_xs) (snd y_ys)
+         end.
+
     Section interpM.
       Context {base_type} (M : Type -> Type) (base_interp : base_type -> Type).
       (** half-monadic denotation function; denote [type]s into their
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index c8b19a5f4..4f4a2f473 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -26,6 +26,10 @@ Module Compilers.
   Import Language.Compilers.
   Import LanguageInversion.Compilers.
   Import expr.Notations.
+
+  Create HintDb wf discriminated.
+  Create HintDb interp discriminated.
+
   Module type.
     Section eqv.
       Context {base_type} {interp_base_type : base_type -> Type}.
@@ -43,6 +47,37 @@ Module Compilers.
         etransitivity; first [ eassumption | symmetry; eassumption ].
       Qed.
     End eqv.
+
+    Section app_curried_instances.
+      Context {base_type} {base_interp : base_type -> Type}.
+      (* Might want to add the following to make [app_curried_Proper] usable by [setoid_rewrite]? *)
+      (* See https://github.com/coq/coq/issues/8179
+<<
+Lemma PER_valid_l {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R x.
+Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
+Lemma PER_valid_r {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R y.
+Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
+Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_l _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances.
+Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances.
+>>
+*)
+      Lemma app_curried_Proper {t}
+        : Proper (@type.eqv base_type base_interp t ==> type.and_for_each_lhs_of_arrow (@type.eqv _ _) ==> eq)
+                 (@type.app_curried base_type base_interp t).
+      Proof.
+        cbv [Proper respectful]; induction t; cbn [type.eqv type.app_curried]; cbv [Proper respectful]; [ intros; subst; reflexivity | ].
+        intros f g Hfg x y [Hxy ?]; eauto.
+      Qed.
+      Global Instance and_for_each_lhs_of_arrow_Reflexive {f} {R} {_ : forall t, Reflexive (R t)} {t}
+        : Reflexive (@type.and_for_each_lhs_of_arrow base_type f f R t).
+      Proof. cbv [Reflexive] in *; induction t; cbn; repeat split; eauto. Qed.
+      Global Instance and_for_each_lhs_of_arrow_Symmetric {f} {R} {_ : forall t, Symmetric (R t)} {t}
+        : Symmetric (@type.and_for_each_lhs_of_arrow base_type f f R t).
+      Proof. cbv [Symmetric] in *; induction t; cbn; repeat split; intuition eauto. Qed.
+      Global Instance and_for_each_lhs_of_arrow_Transitive {f} {R} {_ : forall t, Transitive (R t)} {t}
+        : Transitive (@type.and_for_each_lhs_of_arrow base_type f f R t).
+      Proof. cbv [Transitive] in *; induction t; cbn; repeat split; intuition eauto. Qed.
+    End app_curried_instances.
   End type.
 
   Module ident.
@@ -444,6 +479,11 @@ Module Compilers.
     Notation Interp_Reify := Interp_Reify_as.
   End expr.
 
+  Hint Resolve expr.Wf_Reify : wf.
+  Hint Rewrite @expr.Interp_Reify @expr.interp_reify @expr.interp_reify_list : interp.
+
+  Notation Wf := expr.Wf.
+
   Local Ltac destructure_step :=
     first [ progress subst
           | progress inversion_option
@@ -798,6 +838,10 @@ Module Compilers.
 
   Ltac prove_Wf _ :=
     lazymatch goal with
-    | [ |- expr.Wf ?e ] => apply (@GeneralizeVar.Wf_via_flat _ e); vm_compute; split; reflexivity
+    | [ |- expr.Wf ?e ] => apply (@GeneralizeVar.Wf_via_flat _ e); vm_cast_no_check (conj (eq_refl e) (eq_refl true))
     end.
+
+  Global Hint Extern 0 (?x == ?x) => apply expr.Wf_Interp_Proper : wf interp.
+  Hint Resolve GeneralizeVar.Wf_FromFlat_ToFlat GeneralizeVar.Wf_GeneralizeVar : wf.
+  Hint Rewrite @GeneralizeVar.Interp_GeneralizeVar @GeneralizeVar.Interp_FromFlat_ToFlat : interp.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/MiscCompilerPassesWf.v b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v
index 50211feb3..52101023a 100644
--- a/src/Experiments/NewPipeline/MiscCompilerPassesWf.v
+++ b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v
@@ -15,14 +15,6 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.ListUtil.
 Import ListNotations. Local Open Scope list_scope.
 
-(*
-
-
-Require Import Crypto.Util.ListUtil Coq.Lists.List.
-Require Import Crypto.Experiments.NewPipeline.Language.
-Require Import Crypto.Util.Notations.
-Import ListNotations. Local Open Scope Z_scope.
-*)
 Module Compilers.
   Import Language.Compilers.
   Import LanguageInversion.Compilers.
@@ -122,6 +114,9 @@ Module Compilers.
     End with_ident.
   End DeadCodeElimination.
 
+  Hint Resolve DeadCodeElimination.Wf_EliminateDead : wf.
+  Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp.
+
   Module Subst01.
     Import MiscCompilerPasses.Compilers.Subst01.
 
@@ -201,4 +196,7 @@ Module Compilers.
       End interp.
     End with_ident.
   End Subst01.
+
+  Hint Resolve Subst01.Wf_Subst01 : wf.
+  Hint Rewrite @Subst01.Interp_Subst01 : interp.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v
new file mode 100644
index 000000000..a1e31b319
--- /dev/null
+++ b/src/Experiments/NewPipeline/RewriterProofs.v
@@ -0,0 +1,59 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.MSets.MSetPositive.
+Require Import Coq.FSets.FMapPositive.
+Require Import Crypto.Experiments.NewPipeline.Language.
+Require Import Crypto.Experiments.NewPipeline.LanguageInversion.
+Require Import Crypto.Experiments.NewPipeline.LanguageWf.
+Require Import Crypto.Experiments.NewPipeline.Rewriter.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.SpecializeAllWays.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.ListUtil.
+Import ListNotations. Local Open Scope list_scope.
+Local Open Scope Z_scope.
+
+Module Compilers.
+  Import Language.Compilers.
+  Import LanguageInversion.Compilers.
+  Import LanguageWf.Compilers.
+  Import Rewriter.Compilers.
+  Import expr.Notations.
+  Import defaults.
+
+  Module Import RewriteRules.
+    Import Rewriter.Compilers.RewriteRules.
+
+    Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e).
+    Admitted.
+    Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e).
+    Admitted.
+    Lemma Wf_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z) {t} e (Hwf : Wf e) : Wf (@RewriteToFancy invert_low invert_high t e).
+    Admitted.
+
+    Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e.
+    Admitted.
+    Lemma Interp_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Interp (@RewriteArith max_const_val t e) == Interp e.
+    Admitted.
+
+    Lemma Interp_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z)
+          (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
+          (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
+          {t} e (Hwf : Wf e)
+      : Interp (@RewriteToFancy invert_low invert_high t e) == Interp e.
+    Admitted.
+  End RewriteRules.
+
+  Lemma Wf_PartialEvaluate {t} e (Hwf : Wf e) : Wf (@PartialEvaluate t e).
+  Proof. apply Wf_RewriteNBE, Hwf. Qed.
+
+  Lemma Interp_PartialEvaluate {t} e (Hwf : Wf e) : Interp (@PartialEvaluate t e) == Interp e.
+  Proof. apply Interp_RewriteNBE, Hwf. Qed.
+
+
+  Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy : wf.
+  Hint Rewrite @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy : interp.
+End Compilers.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 9464e270a..bec153f53 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -45,10 +45,14 @@ Require Import Crypto.Experiments.NewPipeline.Arithmetic.
 Require Crypto.Experiments.NewPipeline.Language.
 Require Crypto.Experiments.NewPipeline.UnderLets.
 Require Crypto.Experiments.NewPipeline.AbstractInterpretation.
-Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs.
 Require Crypto.Experiments.NewPipeline.Rewriter.
 Require Crypto.Experiments.NewPipeline.MiscCompilerPasses.
 Require Crypto.Experiments.NewPipeline.CStringification.
+Require Crypto.Experiments.NewPipeline.LanguageWf.
+Require Crypto.Experiments.NewPipeline.UnderLetsProofs.
+Require Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs.
+Require Crypto.Experiments.NewPipeline.RewriterProofs.
+Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs.
 Require Import Crypto.Util.Notations.
 Import ListNotations. Local Open Scope Z_scope.
 
@@ -274,6 +278,10 @@ Module MontgomeryStyleRing.
     := (andb (is_bounded_by bounds (@fst _ unit ls)) true).
   Local Notation is_bounded_by2 bounds ls
     := (andb (is_bounded_by bounds (fst ls)) (is_bounded_by1 bounds (snd ls))).
+  Local Notation is_eq1 arg1 arg2
+    := (and ((@fst _ unit arg1) = (@fst _ unit arg2)) True).
+  Local Notation is_eq2 arg1 arg2
+    := (and (fst arg1 = fst arg2) (is_eq1 (snd arg1) (snd arg2))).
 
   Lemma length_is_bounded_by bounds ls
     : is_bounded_by bounds ls = true -> length ls = length bounds.
@@ -301,50 +309,55 @@ Module MontgomeryStyleRing.
             (Hfrom_montgomery_mod
              : forall v, valid v -> valid (from_montgomery_mod v))
             (Interp_rfrom_montgomeryv : list Z -> list Z)
-            (HInterp_rfrom_montgomeryv : forall arg,
-                is_bounded_by1 bounds arg = true
-                -> is_bounded_by bounds (Interp_rfrom_montgomeryv (fst arg)) = true
-                   /\ Interp_rfrom_montgomeryv (fst arg) = from_montgomery_mod (fst arg))
+            (HInterp_rfrom_montgomeryv : forall arg1 arg2,
+                is_eq1 arg1 arg2
+                -> is_bounded_by1 bounds arg1 = true
+                -> is_bounded_by bounds (Interp_rfrom_montgomeryv (fst arg1)) = true
+                   /\ Interp_rfrom_montgomeryv (fst arg1) = from_montgomery_mod (fst arg2))
             (mulmod : list Z -> list Z -> list Z)
             (Hmulmod
              : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (mulmod a b)) mod (s - Associational.eval c)
-                                            = (eval (from_montgomery_mod a) * eval (from_montgomery_mod b)) mod (s - Associational.eval c))
+                                                        = (eval (from_montgomery_mod a) * eval (from_montgomery_mod b)) mod (s - Associational.eval c))
                /\ (forall a (_ : valid a) b (_ : valid b), valid (mulmod a b)))
             (Interp_rmulv : list Z -> list Z -> list Z)
-            (HInterp_rmulv : forall arg,
-                is_bounded_by2 bounds arg = true
-                -> is_bounded_by bounds (Interp_rmulv (fst arg) (fst (snd arg))) = true
-                   /\ Interp_rmulv (fst arg) (fst (snd arg)) = mulmod (fst arg) (fst (snd arg)))
+            (HInterp_rmulv : forall arg1 arg2,
+                is_eq2 arg1 arg2
+                -> is_bounded_by2 bounds arg1 = true
+                -> is_bounded_by bounds (Interp_rmulv (fst arg1) (fst (snd arg1))) = true
+                   /\ Interp_rmulv (fst arg1) (fst (snd arg1)) = mulmod (fst arg2) (fst (snd arg2)))
             (addmod : list Z -> list Z -> list Z)
             (Haddmod
              : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (addmod a b)) mod (s - Associational.eval c)
-                                                   = (eval (from_montgomery_mod a) + eval (from_montgomery_mod b)) mod (s - Associational.eval c))
+                                                        = (eval (from_montgomery_mod a) + eval (from_montgomery_mod b)) mod (s - Associational.eval c))
                /\ (forall a (_ : valid a) b (_ : valid b), valid (addmod a b)))
             (Interp_raddv : list Z -> list Z -> list Z)
-            (HInterp_raddv : forall arg,
-                is_bounded_by2 bounds arg = true
-                -> is_bounded_by bounds (Interp_raddv (fst arg) (fst (snd arg))) = true
-                   /\ Interp_raddv (fst arg) (fst (snd arg)) = addmod (fst arg) (fst (snd arg)))
+            (HInterp_raddv : forall arg1 arg2,
+                is_eq2 arg1 arg2
+                -> is_bounded_by2 bounds arg1 = true
+                -> is_bounded_by bounds (Interp_raddv (fst arg1) (fst (snd arg1))) = true
+                   /\ Interp_raddv (fst arg1) (fst (snd arg1)) = addmod (fst arg2) (fst (snd arg2)))
             (submod : list Z -> list Z -> list Z)
             (Hsubmod
              : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (submod a b)) mod (s - Associational.eval c)
-                                                   = (eval (from_montgomery_mod a) - eval (from_montgomery_mod b)) mod (s - Associational.eval c))
+                                                        = (eval (from_montgomery_mod a) - eval (from_montgomery_mod b)) mod (s - Associational.eval c))
                /\ (forall a (_ : valid a) b (_ : valid b), valid (submod a b)))
             (Interp_rsubv : list Z -> list Z -> list Z)
-            (HInterp_rsubv : forall arg,
-                is_bounded_by2 bounds arg = true
-                -> is_bounded_by bounds (Interp_rsubv (fst arg) (fst (snd arg))) = true
-                   /\ Interp_rsubv (fst arg) (fst (snd arg)) = submod (fst arg) (fst (snd arg)))
+            (HInterp_rsubv : forall arg1 arg2,
+                is_eq2 arg1 arg2
+                -> is_bounded_by2 bounds arg1 = true
+                -> is_bounded_by bounds (Interp_rsubv (fst arg1) (fst (snd arg1))) = true
+                   /\ Interp_rsubv (fst arg1) (fst (snd arg1)) = submod (fst arg2) (fst (snd arg2)))
             (oppmod : list Z -> list Z)
             (Hoppmod
              : (forall a (_ : valid a), eval (from_montgomery_mod (oppmod a)) mod (s - Associational.eval c)
-                                   = (-eval (from_montgomery_mod a)) mod (s - Associational.eval c))
+                                        = (-eval (from_montgomery_mod a)) mod (s - Associational.eval c))
                /\ (forall a (_ : valid a), valid (oppmod a)))
             (Interp_roppv : list Z -> list Z)
-            (HInterp_roppv : forall arg,
-                is_bounded_by1 bounds arg = true
-                -> is_bounded_by bounds (Interp_roppv (fst arg)) = true
-                   /\ Interp_roppv (fst arg) = oppmod (fst arg))
+            (HInterp_roppv : forall arg1 arg2,
+                is_eq1 arg1 arg2
+                -> is_bounded_by1 bounds arg1 = true
+                -> is_bounded_by bounds (Interp_roppv (fst arg1)) = true
+                   /\ Interp_roppv (fst arg1) = oppmod (fst arg2))
             (zeromod : list Z)
             (Hzeromod
              : (eval (from_montgomery_mod zeromod)) mod (s - Associational.eval c)
@@ -356,40 +369,37 @@ Module MontgomeryStyleRing.
             (onemod : list Z)
             (Honemod
              : (eval (from_montgomery_mod onemod)) mod (s - Associational.eval c)
-                = 1 mod (s - Associational.eval c)
+               = 1 mod (s - Associational.eval c)
                /\ valid onemod)
             (Interp_ronev : list Z)
             (HInterp_ronev : is_bounded_by bounds Interp_ronev = true
-                              /\ Interp_ronev = onemod)
+                             /\ Interp_ronev = onemod)
             (encodemod : Z -> list Z)
             (Hencodemod
              : (forall v, 0 <= v < s - Associational.eval c -> eval (from_montgomery_mod (encodemod v)) mod (s - Associational.eval c) = v mod (s - Associational.eval c))
                /\ (forall v, 0 <= v < s - Associational.eval c -> valid (encodemod v)))
             (Interp_rencodev : Z -> list Z)
-            (HInterp_rencodev : forall arg,
-                is_bounded_by0 prime_bound (@fst _ unit arg) && true = true
-                -> is_bounded_by bounds (Interp_rencodev (fst arg)) = true
-                   /\ Interp_rencodev (fst arg) = encodemod (fst arg)).
+            (HInterp_rencodev : forall arg1 arg2,
+                is_eq1 arg1 arg2
+                -> is_bounded_by0 prime_bound (@fst _ unit arg1) && true = true
+                -> is_bounded_by bounds (Interp_rencodev (fst arg1)) = true
+                   /\ Interp_rencodev (fst arg1) = encodemod (fst arg2)).
 
     Local Notation T := (list Z) (only parsing).
     Local Notation encoded_ok ls
       := (is_bounded_by bounds ls = true /\ valid ls) (only parsing).
     Local Notation encoded_okf := (fun ls => encoded_ok ls) (only parsing).
-
     Definition Fdecode (v : T) : F m
       := F.of_Z m (Positional.eval weight n (Interp_rfrom_montgomeryv v)).
     Definition T_eq (x y : T)
       := Fdecode x = Fdecode y.
-
     Definition encodedT := sig encoded_okf.
-
     Definition ring_mul (x y : T) : T
       := Interp_rmulv x y.
     Definition ring_add (x y : T) : T := Interp_raddv x y.
     Definition ring_sub (x y : T) : T := Interp_rsubv x y.
     Definition ring_opp (x : T) : T := Interp_roppv x.
     Definition ring_encode (x : F m) : T := Interp_rencodev (F.to_Z x).
-
     Definition GoodT : Prop
       := @subsetoid_ring
            (list Z) encoded_okf T_eq
@@ -401,12 +411,10 @@ Module MontgomeryStyleRing.
               (list Z) encoded_okf T_eq Interp_ronev ring_add ring_mul
               (F m) (fun _ => True) eq 1%F F.add F.mul
               Fdecode.
-
     Hint Rewrite ->@F.to_Z_add : push_FtoZ.
     Hint Rewrite ->@F.to_Z_mul : push_FtoZ.
     Hint Rewrite ->@F.to_Z_opp : push_FtoZ.
     Hint Rewrite ->@F.to_Z_of_Z : push_FtoZ.
-
     Lemma Fm_bounded_alt (x : F m)
       : (0 <=? F.to_Z x) && (F.to_Z x <=? Z.pos m - 1) = true.
     Proof using m_eq.
@@ -415,7 +423,6 @@ Module MontgomeryStyleRing.
       pose proof (Z.mod_pos_bound x (Z.pos m)).
       rewrite andb_true_iff; split; Z.ltb_to_lt; lia.
     Qed.
-
     Lemma Fm_bounded_alt' (x : F m)
       : 0 <= F.to_Z x < Z.pos m.
     Proof using m_eq.
@@ -424,7 +431,6 @@ Module MontgomeryStyleRing.
       pose proof (Z.mod_pos_bound x (Z.pos m)).
       split; Z.ltb_to_lt; lia.
     Qed.
-
     Lemma Good : GoodT.
     Proof.
       split_and.
@@ -434,8 +440,8 @@ Module MontgomeryStyleRing.
       eapply subsetoid_ring_by_ring_isomorphism;
         cbv [ring_opp ring_add ring_sub ring_mul ring_encode F.sub] in *;
         repeat match goal with
-               | [ H : forall arg : _ * unit, _ |- _ ] => specialize (fun arg => H (arg, tt))
-               | [ H : forall arg : _ * (_ * unit), _ |- _ ] => specialize (fun a b => H (a, (b, tt)))
+               | [ H : forall arg1 arg2 : _ * unit, _ |- _ ] => specialize (fun arg => H (arg, tt) (arg, tt) ltac:(tauto))
+               | [ H : forall arg arg2 : _ * (_ * unit), _ |- _ ] => specialize (fun a b => H (a, (b, tt)) (a, (b, tt)) ltac:(tauto))
                | _ => progress cbn [fst snd] in *
                | _ => solve [ auto using andb_true_intro, conj with nocore ]
                | _ => progress intros
@@ -489,19 +495,27 @@ End MontgomeryStyleRing.
 Import Associational Positional.
 
 Import
+  Crypto.Experiments.NewPipeline.LanguageWf
+  Crypto.Experiments.NewPipeline.UnderLetsProofs
+  Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs
+  Crypto.Experiments.NewPipeline.RewriterProofs
+  Crypto.Experiments.NewPipeline.AbstractInterpretationProofs
   Crypto.Experiments.NewPipeline.Language
   Crypto.Experiments.NewPipeline.UnderLets
   Crypto.Experiments.NewPipeline.AbstractInterpretation
-  Crypto.Experiments.NewPipeline.AbstractInterpretationProofs
   Crypto.Experiments.NewPipeline.Rewriter
   Crypto.Experiments.NewPipeline.MiscCompilerPasses
   Crypto.Experiments.NewPipeline.CStringification.
 
 Import
+  LanguageWf.Compilers
+  UnderLetsProofs.Compilers
+  MiscCompilerPassesProofs.Compilers
+  RewriterProofs.Compilers
+  AbstractInterpretationProofs.Compilers
   Language.Compilers
   UnderLets.Compilers
   AbstractInterpretation.Compilers
-  AbstractInterpretationProofs.Compilers
   Rewriter.Compilers
   MiscCompilerPasses.Compilers
   CStringification.Compilers.
@@ -511,10 +525,6 @@ Local Coercion Z.of_nat : nat >-> Z.
 Local Coercion QArith_base.inject_Z : Z >-> Q.
 Notation "x" := (expr.Var x) (only printing, at level 9) : expr_scope.
 
-Axiom admit_pf : False.
-Notation admit := (match admit_pf with end).
-
-
 Module Pipeline.
   Import GeneralizeVar.
   Inductive ErrorMessage :=
@@ -749,6 +759,14 @@ Module Pipeline.
        | 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 ] ].
+
   Lemma BoundsPipeline_correct
              (with_dead_code_elimination : bool := true)
              (with_subst01 : bool)
@@ -762,11 +780,19 @@ Module Pipeline.
              out_bounds
              rv
              (Hrv : BoundsPipeline (*with_dead_code_elimination*) with_subst01 translate_to_fancy relax_zrange e arg_bounds out_bounds = Success rv)
-    : forall arg
-             (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg = true),
-      ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg) = true
-      /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg
-                                 = type.app_curried (Interp e) arg.
+             (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.
   Proof.
     cbv [BoundsPipeline Let_In] in *;
       repeat match goal with
@@ -778,15 +804,25 @@ Module Pipeline.
     { intros;
         match goal with
         | [ H : _ = _ |- _ ]
-          => eapply CheckedPartialEvaluateWithBounds_Correct in H;
-              [ destruct H as [H0 H1] | .. ]
+          => let H' := fresh in
+             pose proof H as H';
+               eapply CheckedPartialEvaluateWithBounds_Correct in H';
+               [ destruct H' as [H0 H1] | .. ]
         end;
         [
-        | eassumption || (try reflexivity).. ].
-      subst.
-      split; [ assumption | ].
-      { intros; rewrite H1.
-        exact admit. (* interp correctness *) } }
+        | match goal with
+          | [ |- Wf _ ] => idtac
+          | _ => eassumption || reflexivity
+          end.. ].
+      { subst.
+        split; [ solve [ eauto with nocore ] | ].
+        { intros; rewrite H1; clear H1.
+          transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1).
+          { apply type.app_curried_Proper; [ | symmetry; assumption ].
+            clear dependent arg1; clear dependent arg2; clear dependent out_bounds.
+            wf_interp_t. }
+          { apply Interp_PartialEvaluateWithListInfoFromBounds; auto. } } }
+      { wf_interp_t. } }
   Qed.
 
   Definition BoundsPipeline_correct_transT
@@ -795,16 +831,23 @@ Module Pipeline.
              out_bounds
              (InterpE : type.interp base.interp t)
              (rv : Expr t)
-    := forall arg
-              (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg = true),
-      ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg) = true
-      /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg
-                                 = type.app_curried InterpE arg.
+    := 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.
 
   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)
         relax_zrange
         (Hrelax
          : forall r r' z : zrange,
@@ -813,16 +856,23 @@ Module Pipeline.
         (e : Expr t)
         arg_bounds out_bounds
         (InterpE : type.interp base.interp t)
-        (InterpE_correct
-         : forall arg
-                  (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg = true),
-            type.app_curried (Interp e) arg = type.app_curried InterpE arg)
+        (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 relax_zrange e arg_bounds out_bounds = Success rv)
     : BoundsPipeline_correct_transT arg_bounds out_bounds InterpE rv.
   Proof.
-    intros arg Harg; rewrite <- InterpE_correct by assumption.
-    eapply @BoundsPipeline_correct; eassumption.
+    destruct InterpE_correct_and_Wf as [InterpE_correct Hwf].
+    intros arg1 arg2 Harg12 Harg1; erewrite <- InterpE_correct; [ 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.
 End Pipeline.
 
@@ -873,239 +923,289 @@ Proof.
 Qed.
 
 Ltac cache_reify _ :=
-  intros;
-  etransitivity;
-  [
-  | repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end;
-    Reify_rhs ();
-    reflexivity ];
-  subst_evars;
-  reflexivity.
-
-Create HintDb reify_gen_cache.
+  split;
+  [ intros;
+    etransitivity;
+    [
+    | repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end;
+      Reify_rhs ();
+      reflexivity ];
+    subst_evars;
+    reflexivity
+  | prove_Wf () ].
+
+Create HintDb reify_gen_cache discriminated.
+Create HintDb wf_gen_cache discriminated.
+Hint Resolve conj : reify_gen_cache wf_gen_cache.
+Hint Unfold Wf : wf_gen_cache.
 
 Derive carry_mul_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (f g : list Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z))
-                        (idxs : list nat),
-                    Interp (t:=reify_type_of carry_mulmod)
-                           carry_mul_gen limbwidth_num limbwidth_den s c n idxs f g
-                    = carry_mulmod limbwidth_num limbwidth_den s c n idxs f g)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (f g : list Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z))
+                         (idxs : list nat),
+                     Interp (t:=reify_type_of carry_mulmod)
+                            carry_mul_gen limbwidth_num limbwidth_den s c n idxs f g
+                     = carry_mulmod limbwidth_num limbwidth_den s c n idxs f g)
+                 /\ Wf carry_mul_gen)
        As carry_mul_gen_correct.
 Proof. Time cache_reify (). Time Qed.
-Hint Extern 1 (_ = carry_mulmod _ _ _ _ _ _ _ _) => simple apply carry_mul_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = carry_mulmod _ _ _ _ _ _ _ _) => simple apply (proj1 carry_mul_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 carry_mul_gen_correct) : wf_gen_cache.
 
 Derive carry_square_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (f : list Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z))
-                        (idxs : list nat),
-                    Interp (t:=reify_type_of carry_squaremod)
-                           carry_square_gen limbwidth_num limbwidth_den s c n idxs f
-                    = carry_squaremod limbwidth_num limbwidth_den s c n idxs f)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (f : list Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z))
+                         (idxs : list nat),
+                     Interp (t:=reify_type_of carry_squaremod)
+                            carry_square_gen limbwidth_num limbwidth_den s c n idxs f
+                     = carry_squaremod limbwidth_num limbwidth_den s c n idxs f)
+                 /\ Wf carry_square_gen)
        As carry_square_gen_correct.
 Proof. Time cache_reify (). Time Qed.
-Hint Extern 1 (_ = carry_squaremod _ _ _ _ _ _ _) => simple apply carry_square_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = carry_squaremod _ _ _ _ _ _ _) => simple apply (proj1 carry_square_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 carry_square_gen_correct) : wf_gen_cache.
 
 Derive carry_scmul_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (x : Z) (f : list Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z))
-                        (idxs : list nat),
-                    Interp (t:=reify_type_of carry_scmulmod)
-                           carry_scmul_gen limbwidth_num limbwidth_den s c n idxs x f
-                    = carry_scmulmod limbwidth_num limbwidth_den s c n idxs x f)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (x : Z) (f : list Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z))
+                         (idxs : list nat),
+                     Interp (t:=reify_type_of carry_scmulmod)
+                            carry_scmul_gen limbwidth_num limbwidth_den s c n idxs x f
+                     = carry_scmulmod limbwidth_num limbwidth_den s c n idxs x f)
+                 /\ Wf carry_scmul_gen)
        As carry_scmul_gen_correct.
 Proof. Time cache_reify (). Time Qed.
-Hint Extern 1 (_ = carry_scmulmod _ _ _ _ _ _ _ _) => simple apply carry_scmul_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = carry_scmulmod _ _ _ _ _ _ _ _) => simple apply (proj1 carry_scmul_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 carry_scmul_gen_correct) : wf_gen_cache.
 
 Derive carry_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (f : list Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z))
-                        (idxs : list nat),
-                    Interp (t:=reify_type_of carrymod)
-                           carry_gen limbwidth_num limbwidth_den s c n idxs f
-                    = carrymod limbwidth_num limbwidth_den s c n idxs f)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (f : list Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z))
+                         (idxs : list nat),
+                     Interp (t:=reify_type_of carrymod)
+                            carry_gen limbwidth_num limbwidth_den s c n idxs f
+                     = carrymod limbwidth_num limbwidth_den s c n idxs f)
+                 /\ Wf carry_gen)
        As carry_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = carrymod _ _ _ _ _ _ _) => simple apply carry_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = carrymod _ _ _ _ _ _ _) => simple apply (proj1 carry_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 carry_gen_correct) : wf_gen_cache.
 
 Derive encode_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (v : Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z)),
-                    Interp (t:=reify_type_of encodemod)
-                           encode_gen limbwidth_num limbwidth_den s c n v
-                    = encodemod limbwidth_num limbwidth_den s c n v)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (v : Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z)),
+                     Interp (t:=reify_type_of encodemod)
+                            encode_gen limbwidth_num limbwidth_den s c n v
+                     = encodemod limbwidth_num limbwidth_den s c n v)
+                 /\ Wf encode_gen)
        As encode_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = encodemod _ _ _ _ _ _) => simple apply encode_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = encodemod _ _ _ _ _ _) => simple apply (proj1 encode_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 encode_gen_correct) : wf_gen_cache.
 
 Derive add_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (f g : list Z)
-                        (n : nat),
-                    Interp (t:=reify_type_of addmod)
-                           add_gen limbwidth_num limbwidth_den n f g
-                    = addmod limbwidth_num limbwidth_den n f g)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (f g : list Z)
+                         (n : nat),
+                     Interp (t:=reify_type_of addmod)
+                            add_gen limbwidth_num limbwidth_den n f g
+                     = addmod limbwidth_num limbwidth_den n f g)
+                 /\ Wf add_gen)
        As add_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply add_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply (proj1 add_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 add_gen_correct) : wf_gen_cache.
 
 Derive sub_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z))
-                        (coef : Z)
-                        (f g : list Z),
-                    Interp (t:=reify_type_of submod)
-                           sub_gen limbwidth_num limbwidth_den s c n coef f g
-                    = submod limbwidth_num limbwidth_den s c n coef f g)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z))
+                         (coef : Z)
+                         (f g : list Z),
+                     Interp (t:=reify_type_of submod)
+                            sub_gen limbwidth_num limbwidth_den s c n coef f g
+                     = submod limbwidth_num limbwidth_den s c n coef f g)
+                 /\ Wf sub_gen)
        As sub_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = submod _ _ _ _ _ _ _ _) => simple apply sub_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = submod _ _ _ _ _ _ _ _) => simple apply (proj1 sub_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 sub_gen_correct) : wf_gen_cache.
+
 Derive opp_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z))
-                        (coef : Z)
-                        (f : list Z),
-                    Interp (t:=reify_type_of oppmod)
-                           opp_gen limbwidth_num limbwidth_den s c n coef f
-                    = oppmod limbwidth_num limbwidth_den s c n coef f)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z))
+                         (coef : Z)
+                         (f : list Z),
+                     Interp (t:=reify_type_of oppmod)
+                            opp_gen limbwidth_num limbwidth_den s c n coef f
+                     = oppmod limbwidth_num limbwidth_den s c n coef f)
+                 /\ Wf opp_gen)
        As opp_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = oppmod _ _ _ _ _ _ _) => simple apply opp_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = oppmod _ _ _ _ _ _ _) => simple apply (proj1 opp_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 opp_gen_correct) : wf_gen_cache.
+
 Definition zeromod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 0.
 Definition onemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 1.
 Definition primemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n (s - Associational.eval c).
+
 Derive zero_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z)),
-                    Interp (t:=reify_type_of zeromod)
-                           zero_gen limbwidth_num limbwidth_den s c n
-                    = zeromod limbwidth_num limbwidth_den s c n)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z)),
+                     Interp (t:=reify_type_of zeromod)
+                            zero_gen limbwidth_num limbwidth_den s c n
+                     = zeromod limbwidth_num limbwidth_den s c n)
+                 /\ Wf zero_gen)
        As zero_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = zeromod _ _ _ _ _) => simple apply zero_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = zeromod _ _ _ _ _) => simple apply (proj1 zero_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 zero_gen_correct) : wf_gen_cache.
 
 Derive one_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z)),
-                    Interp (t:=reify_type_of onemod)
-                           one_gen limbwidth_num limbwidth_den s c n
-                    = onemod limbwidth_num limbwidth_den s c n)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z)),
+                     Interp (t:=reify_type_of onemod)
+                            one_gen limbwidth_num limbwidth_den s c n
+                     = onemod limbwidth_num limbwidth_den s c n)
+                 /\ Wf one_gen)
        As one_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = onemod _ _ _ _ _) => simple apply one_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = onemod _ _ _ _ _) => simple apply (proj1 one_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 one_gen_correct) : wf_gen_cache.
 
 Derive prime_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (n : nat)
-                        (s : Z)
-                        (c : list (Z * Z)),
-                    Interp (t:=reify_type_of primemod)
-                           prime_gen limbwidth_num limbwidth_den s c n
-                    = primemod limbwidth_num limbwidth_den s c n)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (n : nat)
+                         (s : Z)
+                         (c : list (Z * Z)),
+                     Interp (t:=reify_type_of primemod)
+                            prime_gen limbwidth_num limbwidth_den s c n
+                     = primemod limbwidth_num limbwidth_den s c n)
+                 /\ Wf prime_gen)
        As prime_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = primemod _ _ _ _ _) => simple apply prime_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = primemod _ _ _ _ _) => simple apply (proj1 prime_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 prime_gen_correct) : wf_gen_cache.
 
 Derive id_gen
-       SuchThat (forall (ls : list Z),
-                    Interp (t:=reify_type_of (@id (list Z)))
-                           id_gen ls
-                    = id ls)
+       SuchThat ((forall (ls : list Z),
+                     Interp (t:=reify_type_of (@id (list Z)))
+                            id_gen ls
+                     = id ls)
+                 /\ Wf id_gen)
        As id_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = id _) => simple apply id_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = id _) => simple apply (proj1 id_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 id_gen_correct) : wf_gen_cache.
 
 Derive selectznz_gen
-       SuchThat (forall (cond : Z) (f g : list Z),
-                    Interp (t:=reify_type_of Positional.select)
-                           selectznz_gen cond f g
-                    = Positional.select cond f g)
+       SuchThat ((forall (cond : Z) (f g : list Z),
+                     Interp (t:=reify_type_of Positional.select)
+                            selectznz_gen cond f g
+                     = Positional.select cond f g)
+                 /\ Wf selectznz_gen)
        As selectznz_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = Positional.select _ _ _) => simple apply selectznz_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = Positional.select _ _ _) => simple apply (proj1 selectznz_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 selectznz_gen_correct) : wf_gen_cache.
 
 Derive to_bytes_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (n : nat)
-                        (bitwidth : Z)
-                        (m_enc : list Z)
-                        (f : list Z),
-                    Interp (t:=reify_type_of freeze_to_bytesmod)
-                           to_bytes_gen limbwidth_num limbwidth_den n bitwidth m_enc f
-                    = freeze_to_bytesmod limbwidth_num limbwidth_den n bitwidth m_enc f)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (n : nat)
+                         (bitwidth : Z)
+                         (m_enc : list Z)
+                         (f : list Z),
+                     Interp (t:=reify_type_of freeze_to_bytesmod)
+                            to_bytes_gen limbwidth_num limbwidth_den n bitwidth m_enc f
+                     = freeze_to_bytesmod limbwidth_num limbwidth_den n bitwidth m_enc f)
+                 /\ Wf to_bytes_gen)
        As to_bytes_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = freeze_to_bytesmod _ _ _ _ _ _) => simple apply to_bytes_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = freeze_to_bytesmod _ _ _ _ _ _) => simple apply (proj1 to_bytes_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 to_bytes_gen_correct) : wf_gen_cache.
 
 Derive from_bytes_gen
-       SuchThat (forall (limbwidth_num limbwidth_den : Z)
-                        (n : nat)
-                        (f : list Z),
-                    Interp (t:=reify_type_of from_bytesmod)
-                           from_bytes_gen limbwidth_num limbwidth_den n f
-                    = from_bytesmod limbwidth_num limbwidth_den n f)
+       SuchThat ((forall (limbwidth_num limbwidth_den : Z)
+                         (n : nat)
+                         (f : list Z),
+                     Interp (t:=reify_type_of from_bytesmod)
+                            from_bytes_gen limbwidth_num limbwidth_den n f
+                     = from_bytesmod limbwidth_num limbwidth_den n f)
+                 /\ Wf from_bytes_gen)
        As from_bytes_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = from_bytesmod _ _ _ _) => simple apply from_bytes_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = from_bytesmod _ _ _ _) => simple apply (proj1 from_bytes_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 from_bytes_gen_correct) : wf_gen_cache.
 
 Derive mulx_gen
-       SuchThat (forall (s x y : Z),
-                    Interp (t:=reify_type_of mulx)
-                           mulx_gen s x y
-                    = mulx s x y)
+       SuchThat ((forall (s x y : Z),
+                     Interp (t:=reify_type_of mulx)
+                            mulx_gen s x y
+                     = mulx s x y)
+                 /\ Wf mulx_gen)
        As mulx_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = mulx _ _ _) => simple apply mulx_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = mulx _ _ _) => simple apply (proj1 mulx_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 mulx_gen_correct) : wf_gen_cache.
 
 Derive addcarryx_gen
-       SuchThat (forall (s c x y : Z),
-                    Interp (t:=reify_type_of addcarryx)
-                           addcarryx_gen s c x y
-                    = addcarryx s c x y)
+       SuchThat ((forall (s c x y : Z),
+                     Interp (t:=reify_type_of addcarryx)
+                            addcarryx_gen s c x y
+                     = addcarryx s c x y)
+                 /\ Wf addcarryx_gen)
        As addcarryx_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = addcarryx _ _ _ _) => simple apply addcarryx_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = addcarryx _ _ _ _) => simple apply (proj1 addcarryx_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 addcarryx_gen_correct) : wf_gen_cache.
 
 Derive subborrowx_gen
-       SuchThat (forall (s c x y : Z),
-                    Interp (t:=reify_type_of subborrowx)
-                           subborrowx_gen s c x y
-                    = subborrowx s c x y)
+       SuchThat ((forall (s c x y : Z),
+                     Interp (t:=reify_type_of subborrowx)
+                            subborrowx_gen s c x y
+                     = subborrowx s c x y)
+                 /\ Wf subborrowx_gen)
        As subborrowx_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = subborrowx _ _ _ _) => simple apply subborrowx_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = subborrowx _ _ _ _) => simple apply (proj1 subborrowx_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 subborrowx_gen_correct) : wf_gen_cache.
 
 Derive cmovznz_gen
-       SuchThat (forall (bitwidth cond z nz : Z),
-                    Interp (t:=reify_type_of cmovznz)
-                           cmovznz_gen bitwidth cond z nz
-                    = cmovznz bitwidth cond z nz)
+       SuchThat ((forall (bitwidth cond z nz : Z),
+                     Interp (t:=reify_type_of cmovznz)
+                            cmovznz_gen bitwidth cond z nz
+                     = cmovznz bitwidth cond z nz)
+                 /\ Wf cmovznz_gen)
        As cmovznz_gen_correct.
 Proof. cache_reify (). Qed.
-Hint Extern 1 (_ = cmovznz _ _ _ _) => simple apply cmovznz_gen_correct : reify_gen_cache.
+Hint Extern 1 (_ = cmovznz _ _ _ _) => simple apply (proj1 cmovznz_gen_correct) : reify_gen_cache.
+Hint Immediate (proj2 cmovznz_gen_correct) : wf_gen_cache.
+
+
+Axiom admit_pf : False.
+Notation admit := (match admit_pf with end).
 
 
 (** XXX TODO: Translate Jade's python script *)
@@ -1190,7 +1290,7 @@ Module Import UnsaturatedSolinas.
     Notation BoundsPipeline_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               (*false*) true None
+               (*false*) true None I
                relax_zrange
                (relax_zrange_gen_good _)
                _
@@ -1212,7 +1312,7 @@ Module Import UnsaturatedSolinas.
     Notation BoundsPipeline_no_subst01_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               (*false*) false None
+               (*false*) false None I
                relax_zrange
                (relax_zrange_gen_good _)
                _
@@ -1234,7 +1334,7 @@ Module Import UnsaturatedSolinas.
     Notation BoundsPipeline_with_bytes_no_subst01_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               (*false*) false None
+               (*false*) false None I
                relax_zrange_with_bytes
                (relax_zrange_gen_good _)
                _
@@ -1660,10 +1760,10 @@ Module Import UnsaturatedSolinas.
             lazymatch goal with
             | [ H : ?P ?rop |- context[expr.Interp _ ?rop] ]
               => intros;
-                  let H1 := fresh in
-                  let H2 := fresh in
-                  unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | eapply H2 ] ] ];
-                    solve [ exact tt | eassumption | reflexivity ]
+                  let H1 := fresh "HH1" in
+                  let H2 := fresh "HH2" in
+                  unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | refine (H2 _) ] ] ];
+                    solve [ exact tt | eassumption | reflexivity | repeat split ]
             | _ => idtac
             end;
             repeat first [ assumption
@@ -1675,7 +1775,7 @@ Module Import UnsaturatedSolinas.
                          | intros; apply eval_encodemod
                          | apply conj ]. }
         { cbv zeta; intros f Hf; split.
-          { apply Hto_bytesv; assumption. }
+          { apply Hto_bytesv; solve [ assumption | repeat split ]. }
           { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *.
             rewrite Bool.andb_true_iff in *; split_and'.
             etransitivity; [ apply eval_freeze_to_bytesmod | f_equal; (eassumption || (symmetry; eassumption)) ];
@@ -1693,7 +1793,7 @@ Module Import UnsaturatedSolinas.
               split.
               { etransitivity; [ erewrite <- eval_zeros; [ | apply weight_0, wprops ] | apply H15 ].
                 apply Z.eq_le_incl; f_equal.
-                admit.
+                repeat match goal with H : _ |- _ => revert H end; exact admit.
                 omega. }
               { eapply Z.le_lt_trans; [ apply H15 | ].
                 assert (Hlen : length (encode (weight (Qnum limbwidth) (QDen limbwidth)) n s c (s - 1)) = n) by distr_length.
@@ -1704,11 +1804,11 @@ Module Import UnsaturatedSolinas.
                 revert ls.
                 clearbody limbwidth.
                 induction n as [|n' IHn'], ls as [|l ls]; cbn [length]; intros; try omega.
-                admit.
+                repeat match goal with H : _ |- _ => revert H end; exact admit.
                 cbn [map].
-                admit. }
-              admit. }
-      Admitted.
+                repeat match goal with H : _ |- _ => revert H end; exact admit. }
+              repeat match goal with H : _ |- _ => revert H end; exact admit. } } }
+      Qed.
     End make_ring.
 
     Section for_stringification.
@@ -1817,23 +1917,50 @@ Ltac peel_interp_app _ :=
                end ] ]
   end.
 Ltac pre_cache_reify _ :=
-  cbv [type.app_curried];
-  let arg := fresh "arg" in
-  intros arg _;
-  peel_interp_app ();
-  [ lazymatch goal with
-    | [ |- ?R (Interp ?ev) _ ]
-      => (tryif is_evar ev
-           then let ev' := fresh "ev" in set (ev' := ev)
-           else idtac)
-    end;
-    cbv [pointwise_relation]; intros; clear
-  | .. ].
+  let H' := fresh in
+  lazymatch goal with
+  | [ |- ?P /\ Wf ?e ]
+    => let P' := fresh in
+       evar (P' : Prop);
+       assert (H' : P' /\ Wf e); subst P'
+  end;
+  [
+      | split; [ destruct H' as [H' _] | destruct H' as [_ H']; exact H' ];
+        cbv [type.app_curried];
+        let arg := fresh "arg" in
+        let arg2 := fresh in
+        intros arg arg2;
+        cbn [type.and_for_each_lhs_of_arrow type.eqv];
+        let H := fresh in
+        intro H;
+        repeat match type of H with
+               | and _ _ => let H' := fresh in
+                            destruct H as [H' H];
+                            rewrite <- H'
+               end;
+        clear dependent arg2; clear H;
+        intros _;
+        peel_interp_app ();
+        [ lazymatch goal with
+          | [ |- ?R (Interp ?ev) _ ]
+            => (tryif is_evar ev
+                 then let ev' := fresh "ev" in set (ev' := ev)
+                 else idtac)
+          end;
+          cbv [pointwise_relation];
+          repeat lazymatch goal with
+                 | [ H : _ |- _ ] => first [ constr_eq H H'; fail 1
+                                           | revert H ]
+                 end;
+          eexact H'
+        | .. ] ];
+  [ intros; clear | .. ].
 Ltac do_inline_cache_reify do_if_not_cached :=
   pre_cache_reify ();
   [ try solve [
+          cbv beta zeta;
           repeat match goal with H := ?e |- _ => is_evar e; subst H end;
-          eauto with nocore reify_gen_cache;
+          try solve [ split; [ solve [ eauto with nocore reify_gen_cache ] | solve [ eauto with wf_gen_cache; prove_Wf () ] ] ];
           do_if_not_cached ()
         ];
     cache_reify ()
@@ -2067,185 +2194,217 @@ Abort.
 Module WordByWordMontgomery.
   Import Arithmetic.WordByWordMontgomery.
   Derive mul_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (m' : Z)
-                          (f g : list Z),
-                      Interp (t:=reify_type_of mulmod)
-                             mul_gen bitwidth n m m' f g
-                      = mulmod bitwidth n m m' f g)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (m' : Z)
+                           (f g : list Z),
+                       Interp (t:=reify_type_of mulmod)
+                              mul_gen bitwidth n m m' f g
+                       = mulmod bitwidth n m m' f g)
+                   /\ Wf mul_gen)
          As mul_gen_correct.
   Proof. Time cache_reify (). Time Qed.
-  Hint Extern 1 (_ = mulmod _ _ _ _ _ _) => simple apply mul_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = mulmod _ _ _ _ _ _) => simple apply (proj1 mul_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 mul_gen_correct) : wf_gen_cache.
 
   Derive square_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (m' : Z)
-                          (f : list Z),
-                      Interp (t:=reify_type_of squaremod)
-                             square_gen bitwidth n m m' f
-                      = squaremod bitwidth n m m' f)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (m' : Z)
+                           (f : list Z),
+                       Interp (t:=reify_type_of squaremod)
+                              square_gen bitwidth n m m' f
+                       = squaremod bitwidth n m m' f)
+                   /\ Wf square_gen)
          As square_gen_correct.
   Proof.
     Time cache_reify ().
     (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *)
     (*
-    intros; etransitivity; [ | cbv [squaremod]; apply mul_gen_correct ].
-    subst square_gen.
-    instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f f):list Z) in refine (r @ mul_gen)%Expr)).
-    reflexivity.
+    split.
+    { intros; etransitivity; [ | cbv [squaremod]; apply mul_gen_correct ].
+      subst square_gen.
+      instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f f):list Z) in refine (r @ mul_gen)%Expr)).
+      reflexivity. }
+    { prove_Wf (). }
      *)
   Time Qed.
-  Hint Extern 1 (_ = squaremod _ _ _ _ _) => simple apply square_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = squaremod _ _ _ _ _) => simple apply (proj1 square_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 square_gen_correct) : wf_gen_cache.
 
   Derive encode_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (m' : Z)
-                          (v : Z),
-                      Interp (t:=reify_type_of encodemod)
-                             encode_gen bitwidth n m m' v
-                      = encodemod bitwidth n m m' v)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (m' : Z)
+                           (v : Z),
+                       Interp (t:=reify_type_of encodemod)
+                              encode_gen bitwidth n m m' v
+                       = encodemod bitwidth n m m' v)
+                   /\ Wf encode_gen)
          As encode_gen_correct.
   Proof.
     Time cache_reify ().
     (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *)
     (*
-    intros; etransitivity; [ | cbv [encodemod]; apply mul_gen_correct ].
-    subst encode_gen; revert bitwidth n m m' v.
-    lazymatch goal with
-    | [ |- forall bw n m m' v, ?interp ?ev bw n m m' v = ?interp' mul_gen bw n m m' (@?A bw n m m' v) (@?B bw n m m' v) ]
-      => let rv := constr:(fun F bw n m m' v => (F bw n m m' (A bw n m m' v) (B bw n m m' v)):list Z) in
-         intros;
-           instantiate (1:=ltac:(let r := Reify rv in
-                                 refine (r @ mul_gen)%Expr))
-    end.
-    reflexivity.
+    split.
+    { intros; etransitivity; [ | cbv [encodemod]; apply mul_gen_correct ].
+      subst encode_gen; revert bitwidth n m m' v.
+      lazymatch goal with
+      | [ |- forall bw n m m' v, ?interp ?ev bw n m m' v = ?interp' mul_gen bw n m m' (@?A bw n m m' v) (@?B bw n m m' v) ]
+        => let rv := constr:(fun F bw n m m' v => (F bw n m m' (A bw n m m' v) (B bw n m m' v)):list Z) in
+           intros;
+             instantiate (1:=ltac:(let r := Reify rv in
+                                   refine (r @ mul_gen)%Expr))
+      end.
+      reflexivity. }
+    { prove_Wf (). }
      *)
   Time Qed.
-  Hint Extern 1 (_ = encodemod _ _ _ _ _) => simple apply encode_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = encodemod _ _ _ _ _) => simple apply (proj1 encode_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 encode_gen_correct) : wf_gen_cache.
 
   Derive add_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (f g : list Z),
-                      Interp (t:=reify_type_of addmod)
-                             add_gen bitwidth n m f g
-                      = addmod bitwidth n m f g)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (f g : list Z),
+                       Interp (t:=reify_type_of addmod)
+                              add_gen bitwidth n m f g
+                       = addmod bitwidth n m f g)
+                   /\ Wf add_gen)
          As add_gen_correct.
   Proof. Time cache_reify (). Time Qed.
-  Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply add_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply (proj1 add_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 add_gen_correct) : wf_gen_cache.
 
   Derive sub_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (f g : list Z),
-                      Interp (t:=reify_type_of submod)
-                             sub_gen bitwidth n m f g
-                      = submod bitwidth n m f g)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (f g : list Z),
+                       Interp (t:=reify_type_of submod)
+                              sub_gen bitwidth n m f g
+                       = submod bitwidth n m f g)
+                   /\ Wf sub_gen)
          As sub_gen_correct.
   Proof. Time cache_reify (). Time Qed.
-  Hint Extern 1 (_ = submod _ _ _ _ _) => simple apply sub_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = submod _ _ _ _ _) => simple apply (proj1 sub_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 sub_gen_correct) : wf_gen_cache.
 
   Derive opp_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (f : list Z),
-                      Interp (t:=reify_type_of oppmod)
-                             opp_gen bitwidth n m f
-                      = oppmod bitwidth n m f)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (f : list Z),
+                       Interp (t:=reify_type_of oppmod)
+                              opp_gen bitwidth n m f
+                       = oppmod bitwidth n m f)
+                   /\ Wf opp_gen)
          As opp_gen_correct.
   Proof. Time cache_reify (). Time Qed.
-  Hint Extern 1 (_ = oppmod _ _ _ _) => simple apply opp_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = oppmod _ _ _ _) => simple apply (proj1 opp_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 opp_gen_correct) : wf_gen_cache.
 
   Derive from_montgomery_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (m' : Z)
-                          (f : list Z),
-                      Interp (t:=reify_type_of from_montgomery_mod)
-                             from_montgomery_gen bitwidth n m m' f
-                      = from_montgomery_mod bitwidth n m m' f)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (m' : Z)
+                           (f : list Z),
+                       Interp (t:=reify_type_of from_montgomery_mod)
+                              from_montgomery_gen bitwidth n m m' f
+                       = from_montgomery_mod bitwidth n m m' f)
+                   /\ Wf from_montgomery_gen)
          As from_montgomery_gen_correct.
   Proof.
     Time cache_reify ().
     (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *)
     (*
-    intros; etransitivity; [ | cbv [from_montgomery_mod]; apply mul_gen_correct ].
-    subst from_montgomery_gen.
-    instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f (onemod bitwidth n)):list Z) in refine (r @ mul_gen)%Expr)).
-    reflexivity.
+    split.
+    { intros; etransitivity; [ | cbv [from_montgomery_mod]; apply mul_gen_correct ].
+      subst from_montgomery_gen.
+      instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f (onemod bitwidth n)):list Z) in refine (r @ mul_gen)%Expr)).
+      reflexivity. }
+    { prove_Wf (). }
      *)
   Qed.
-  Hint Extern 1 (_ = from_montgomery_mod _ _ _ _ _) => simple apply from_montgomery_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = from_montgomery_mod _ _ _ _ _) => simple apply (proj1 from_montgomery_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 from_montgomery_gen_correct) : wf_gen_cache.
 
   Definition zeromod bitwidth n m m' := encodemod bitwidth n m m' 0.
   Definition onemod bitwidth n m m' := encodemod bitwidth n m m' 1.
   Derive zero_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (m' : Z),
-                      Interp (t:=reify_type_of zeromod)
-                             zero_gen bitwidth n m m'
-                      = zeromod bitwidth n m m')
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (m' : Z),
+                       Interp (t:=reify_type_of zeromod)
+                              zero_gen bitwidth n m m'
+                       = zeromod bitwidth n m m')
+                   /\ Wf zero_gen)
          As zero_gen_correct.
   Proof.
     (* Time cache_reify (). *)
     (* we do something faster *)
-    intros; etransitivity; [ | cbv [zeromod]; apply encode_gen_correct ].
-    subst zero_gen.
-    instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 0):list Z) in refine (r @ encode_gen)%Expr)).
-    reflexivity.
+    split.
+    { intros; etransitivity; [ | cbv [zeromod]; apply encode_gen_correct ].
+      subst zero_gen.
+      instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 0):list Z) in refine (r @ encode_gen)%Expr)).
+      reflexivity. }
+    { prove_Wf (). }
   Qed.
-  Hint Extern 1 (_ = zeromod _ _ _ _) => simple apply zero_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = zeromod _ _ _ _) => simple apply (proj1 zero_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 zero_gen_correct) : wf_gen_cache.
 
   Derive one_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (m : Z)
-                          (m' : Z),
-                      Interp (t:=reify_type_of onemod)
-                             one_gen bitwidth n m m'
-                      = onemod bitwidth n m m')
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (m : Z)
+                           (m' : Z),
+                       Interp (t:=reify_type_of onemod)
+                              one_gen bitwidth n m m'
+                       = onemod bitwidth n m m')
+                   /\ Wf one_gen)
          As one_gen_correct.
   Proof.
     (* Time cache_reify (). *)
     (* we do something faster *)
-    intros; etransitivity; [ | cbv [onemod]; apply encode_gen_correct ].
-    subst one_gen.
-    instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 1):list Z) in refine (r @ encode_gen)%Expr)).
-    reflexivity.
+    split.
+    { intros; etransitivity; [ | cbv [onemod]; apply encode_gen_correct ].
+      subst one_gen.
+      instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 1):list Z) in refine (r @ encode_gen)%Expr)).
+      reflexivity. }
+    { prove_Wf (). }
   Qed.
-  Hint Extern 1 (_ = onemod _ _ _ _) => simple apply one_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = onemod _ _ _ _) => simple apply (proj1 one_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 one_gen_correct) : wf_gen_cache.
 
   Derive nonzero_gen
-         SuchThat (forall (f : list Z),
-                      Interp (t:=reify_type_of nonzeromod)
-                             nonzero_gen f
-                      = nonzeromod f)
+         SuchThat ((forall (f : list Z),
+                       Interp (t:=reify_type_of nonzeromod)
+                              nonzero_gen f
+                       = nonzeromod f)
+                   /\ Wf nonzero_gen)
          As nonzero_gen_correct.
   Proof. Time cache_reify (). Time Qed.
-  Hint Extern 1 (_ = nonzeromod _) => simple apply nonzero_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = nonzeromod _) => simple apply (proj1 nonzero_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 nonzero_gen_correct) : wf_gen_cache.
 
   Derive to_bytes_gen
-         SuchThat (forall (bitwidth : Z)
-                          (n : nat)
-                          (f : list Z),
-                      Interp (t:=reify_type_of to_bytesmod)
-                             to_bytes_gen bitwidth n f
-                      = to_bytesmod bitwidth n f)
+         SuchThat ((forall (bitwidth : Z)
+                           (n : nat)
+                           (f : list Z),
+                       Interp (t:=reify_type_of to_bytesmod)
+                              to_bytes_gen bitwidth n f
+                       = to_bytesmod bitwidth n f)
+                   /\ Wf to_bytes_gen)
          As to_bytes_gen_correct.
   Proof. cache_reify (). Qed.
-  Hint Extern 1 (_ = to_bytesmod _ _ _) => simple apply to_bytes_gen_correct : reify_gen_cache.
+  Hint Extern 1 (_ = to_bytesmod _ _ _) => simple apply (proj1 to_bytes_gen_correct) : reify_gen_cache.
+  Hint Immediate (proj2 to_bytes_gen_correct) : wf_gen_cache.
 
   Section rcarry_mul.
     Context (s : Z)
@@ -2323,7 +2482,7 @@ Module WordByWordMontgomery.
     Notation BoundsPipeline_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               (*false*) true None
+               (*false*) true None I
                relax_zrange
                (relax_zrange_gen_good _)
                _
@@ -2345,7 +2504,7 @@ Module WordByWordMontgomery.
     Notation BoundsPipeline_no_subst01_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               (*false*) false None
+               (*false*) false None I
                relax_zrange
                (relax_zrange_gen_good _)
                _
@@ -2367,7 +2526,7 @@ Module WordByWordMontgomery.
     Notation BoundsPipeline_with_bytes_no_subst01_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               (*false*) false None
+               (*false*) false None I
                relax_zrange_with_bytes
                (relax_zrange_gen_good _)
                _
@@ -2690,8 +2849,8 @@ Module WordByWordMontgomery.
               => intros;
                   let H1 := fresh in
                   let H2 := fresh in
-                  unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | eapply H2 ] ] ];
-                    solve [ exact tt | eassumption | reflexivity ]
+                  unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | refine (H2 _) ] ] ];
+                    solve [ exact tt | eassumption | reflexivity | repeat split ]
             | _ => idtac
             end;
             repeat first [ eassumption
@@ -2705,21 +2864,21 @@ Module WordByWordMontgomery.
                          | intros; apply conj
                          | omega ]. }
         { cbv zeta; intros f Hf; split.
-          { apply Hto_bytesv; assumption. }
+          { apply Hto_bytesv; solve [ assumption | repeat split ]. }
           { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *.
             rewrite Bool.andb_true_iff in *; split_and'.
             apply to_bytesmod_correct; eauto; [].
             split; cbv [small].
-            admit.
-            admit. } }
+            repeat match goal with H : _ |- _ => revert H end; exact admit.
+            repeat match goal with H : _ |- _ => revert H end; exact admit. } }
         { intros.
           split; [ intro H'; eapply nonzeromod_correct;
                    [ .. | rewrite <- H'; symmetry; eapply Hrnonzerov ]
                  | etransitivity; [ apply Hrnonzerov | eapply nonzeromod_correct; [ .. | eassumption ] ] ];
-          try eassumption.
-          admit.
-          admit. }
-      Admitted.
+          try solve [ eassumption | repeat split ].
+          repeat match goal with H : _ |- _ => revert H end; exact admit.
+          repeat match goal with H : _ |- _ => revert H end; exact admit. }
+      Qed.
     End make_ring.
 
     Section for_stringification.
@@ -2826,15 +2985,17 @@ Module SaturatedSolinas.
   End MulMod.
 
   Derive mulmod_gen
-         SuchThat (forall (log2base s : Z) (c : list (Z * Z)) (n nreductions : nat)
-                          (f g : list Z),
-                      Interp (t:=reify_type_of mulmod')
-                             mulmod_gen s c log2base n nreductions f g
-                      = mulmod' s c log2base n nreductions f g)
+         SuchThat ((forall (log2base s : Z) (c : list (Z * Z)) (n nreductions : nat)
+                           (f g : list Z),
+                       Interp (t:=reify_type_of mulmod')
+                              mulmod_gen s c log2base n nreductions f g
+                       = mulmod' s c log2base n nreductions f g)
+                   /\ Wf mulmod_gen)
          As mulmod_gen_correct.
   Proof. Time cache_reify (). Time Qed.
   Module Export ReifyHints.
-    Global Hint Extern 1 (_ = mulmod' _ _ _ _ _ _ _) => simple apply mulmod_gen_correct : reify_gen_cache.
+    Global Hint Extern 1 (_ = mulmod' _ _ _ _ _ _ _) => simple apply (proj1 mulmod_gen_correct) : reify_gen_cache.
+    Hint Immediate (proj2 mulmod_gen_correct) : wf_gen_cache.
   End ReifyHints.
 
   Section rmulmod.
@@ -2884,7 +3045,7 @@ Module SaturatedSolinas.
   Notation BoundsPipeline_correct in_bounds out_bounds op
     := (fun rv (rop : Expr (reify_type_of op)) Hrop
         => @Pipeline.BoundsPipeline_correct_trans
-             (*false*) false None
+             (*false*) false None I
              relax_zrange
              (relax_zrange_gen_good _)
              _
@@ -3513,16 +3674,18 @@ Module BarrettReduction.
   Strategy -10 [barrett_reduce reduce].
 
   Derive barrett_red_gen
-         SuchThat (forall (k M muLow : Z)
-                          (n nout: nat)
-                          (xLow xHigh : Z),
-                      Interp (t:=reify_type_of barrett_reduce)
-                             barrett_red_gen k M muLow n nout xLow xHigh
-                      = barrett_reduce k M muLow n nout xLow xHigh)
+         SuchThat ((forall (k M muLow : Z)
+                           (n nout: nat)
+                           (xLow xHigh : Z),
+                       Interp (t:=reify_type_of barrett_reduce)
+                              barrett_red_gen k M muLow n nout xLow xHigh
+                       = barrett_reduce k M muLow n nout xLow xHigh)
+                   /\ Wf barrett_red_gen)
          As barrett_red_gen_correct.
   Proof. Time cache_reify (). Time Qed. (* Now only takes ~5-10 s, because we set up [Strategy] commands correctly *)
   Module Export ReifyHints.
-    Global Hint Extern 1 (_ = barrett_reduce _ _ _ _ _ _ _) => simple apply barrett_red_gen_correct : reify_gen_cache.
+    Global Hint Extern 1 (_ = barrett_reduce _ _ _ _ _ _ _) => simple apply (proj1 barrett_red_gen_correct) : reify_gen_cache.
+    Hint Immediate (proj2 barrett_red_gen_correct) : wf_gen_cache.
   End ReifyHints.
 
   Section rbarrett_red.
@@ -3574,10 +3737,24 @@ Module BarrettReduction.
       := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list;
                   Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list |}).
 
+    Lemma fancy_args_good
+      : match fancy_args with
+        | Some {| Pipeline.invert_low := il ; Pipeline.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.
+    Proof.
+      cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right];
+        split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence.
+    Qed.
+
     Notation BoundsPipeline_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               false (* subst01 *) fancy_args
+               false (* subst01 *)
+               fancy_args
+               fancy_args_good
                relax_zrange
                relax_zrange_good
                _
@@ -3695,17 +3872,19 @@ Module MontgomeryReduction.
   End MontRed'.
 
   Derive montred_gen
-         SuchThat (forall (N R N' : Z)
-                          (Zlog2R : Z)
-                          (n nout: nat)
-                          (lo_hi : Z * Z),
-                      Interp (t:=reify_type_of montred')
-                             montred_gen N R N' Zlog2R n nout lo_hi
-                      = montred' N R N' Zlog2R n nout lo_hi)
+         SuchThat ((forall (N R N' : Z)
+                           (Zlog2R : Z)
+                           (n nout: nat)
+                           (lo_hi : Z * Z),
+                       Interp (t:=reify_type_of montred')
+                              montred_gen N R N' Zlog2R n nout lo_hi
+                       = montred' N R N' Zlog2R n nout lo_hi)
+                   /\ Wf montred_gen)
          As montred_gen_correct.
   Proof. Time cache_reify (). Time Qed.
   Module Export ReifyHints.
-    Global Hint Extern 1 (_ = montred' _ _ _ _ _ _ _) => simple apply montred_gen_correct : reify_gen_cache.
+    Global Hint Extern 1 (_ = montred' _ _ _ _ _ _ _) => simple apply (proj1 montred_gen_correct) : reify_gen_cache.
+    Hint Immediate (proj2 montred_gen_correct) : wf_gen_cache.
   End ReifyHints.
 
   Section rmontred.
@@ -3729,10 +3908,24 @@ Module MontgomeryReduction.
       := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list;
                   Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list |}).
 
+    Lemma fancy_args_good
+      : match fancy_args with
+        | Some {| Pipeline.invert_low := il ; Pipeline.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.
+    Proof.
+      cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right];
+        split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence.
+    Qed.
+
     Notation BoundsPipeline_correct in_bounds out_bounds op
       := (fun rv (rop : Expr (reify_type_of op)) Hrop
           => @Pipeline.BoundsPipeline_correct_trans
-               false (* subst01 *) fancy_args
+               false (* subst01 *)
+               fancy_args
+               fancy_args_good
                relax_zrange
                (relax_zrange_gen_good _)
                _
diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v
index ab8f6d3e9..83afb62fb 100644
--- a/src/Experiments/NewPipeline/Toplevel2.v
+++ b/src/Experiments/NewPipeline/Toplevel2.v
@@ -2464,7 +2464,8 @@ Module Barrett256.
   Proof.
     intros.
     rewrite <-barrett_reduce_correct_specialized by assumption.
-    destruct (barrett_red256_correct (xLow, (xHigh, tt))) as [H1 H2].
+    destruct (barrett_red256_correct (xLow, (xHigh, tt)) (xLow, (xHigh, tt))) as [H1 H2].
+    { repeat split. }
     { cbn -[Z.pow].
       rewrite !andb_true_iff.
       assert (M < 2^machine_wordsize) by (vm_compute; reflexivity).
@@ -2930,7 +2931,8 @@ Module Montgomery256.
   Proof.
     intros.
     rewrite <-montred'_correct_specialized by assumption.
-    destruct (montred256_correct ((lo, hi), tt)) as [H2 H3].
+    destruct (montred256_correct ((lo, hi), tt) ((lo, hi), tt)) as [H2 H3].
+    { repeat split. }
     { cbn -[Z.pow].
       rewrite !andb_true_iff.
       repeat apply conj; Z.ltb_to_lt; trivial; cbv [R N machine_wordsize] in *; lia. }
diff --git a/src/Experiments/NewPipeline/UnderLetsWf.v b/src/Experiments/NewPipeline/UnderLetsProofs.v
index 7d0e1aa6b..5a806ef9f 100644
--- a/src/Experiments/NewPipeline/UnderLetsWf.v
+++ b/src/Experiments/NewPipeline/UnderLetsProofs.v
@@ -146,6 +146,9 @@ Module Compilers.
     Proof. apply Interp_SubstVarOrIdent, Hwf. Qed.
   End SubstVarLike.
 
+  Hint Resolve SubstVarLike.Wf_SubstVar SubstVarLike.Wf_SubstVarFstSndPairOpp SubstVarLike.Wf_SubstVarLike SubstVarLike.Wf_SubstVarOrIdent : wf.
+  Hint Rewrite @SubstVarLike.Interp_SubstVar @SubstVarLike.Interp_SubstVarFstSndPairOpp @SubstVarLike.Interp_SubstVarLike @SubstVarLike.Interp_SubstVarOrIdent : interp.
+
   Module UnderLets.
     Import UnderLets.Compilers.UnderLets.
     Section with_ident.
@@ -456,4 +459,7 @@ Module Compilers.
       Qed.
     End reify.
   End UnderLets.
+
+  Hint Resolve UnderLets.Wf_LetBindReturn : wf.
+  Hint Rewrite @UnderLets.Interp_LetBindReturn : interp.
 End Compilers.