Rebase + remove WordizeUtil dependency from Z/Interpretations

28 files changed, 622 insertions, 307 deletions

diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v
index 20a76f17f..eaa00bea4 100644
--- a/src/Experiments/Ed25519Extraction.v
+++ b/src/Experiments/Ed25519Extraction.v
@@ -233,7 +233,7 @@ Extraction Implicit Word.split1 [ 2 ].
 Extraction Implicit Word.split2 [ 2 ].
 Extraction Implicit WordUtil.cast_word [1 2 3].
 Extraction Implicit WordUtil.wfirstn [ 2 4 ].
-Extract Inlined Constant WordUtil.cast_word => "".
+Extraction Inline WordUtil.cast_word.
 Extract Inductive Word.word => "[Prelude.Bool]" [ "[]" "(:)" ]
   "(\fWO fWS w -> {- match_on_word -} case w of {[] -> fWO (); (b:w') -> fWS b w' } )".
 
@@ -296,4 +296,4 @@ True
 
 Import Crypto.Spec.MxDH.
 Extraction Inline MxDH.ladderstep MxDH.montladder.
-Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
\ No newline at end of file
+Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
index bb833507f..5d9e64901 100644
--- a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
@@ -5,9 +5,14 @@ Require Import Crypto.Util.ZUtil.
 
 Local Open Scope Z_scope.
 
-Lemma neg_nonneg : forall x y, 0 <= ModularBaseSystemListZOperations.neg x y.
-Proof. Admitted.
+Lemma neg_nonneg : forall x y, 0 <= x -> 0 <= ModularBaseSystemListZOperations.neg x y.
+Proof.
+  unfold neg; intros; break_match; auto with zarith.
+Qed.
 Hint Resolve neg_nonneg : zarith.
-Lemma neg_upperbound : forall x y, ModularBaseSystemListZOperations.neg x y <= Z.ones x.
-Proof. Admitted.
+
+Lemma neg_upperbound : forall x y, 0 <= x -> ModularBaseSystemListZOperations.neg x y <= Z.ones x.
+Proof.
+  unfold neg; intros; break_match; auto with zarith.
+Qed.
 Hint Resolve neg_upperbound : zarith.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 155698e56..7480db3b0 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -1071,7 +1071,7 @@ Section SquareRoots.
         by (rewrite carry_mul_opt_correct by auto;
            cbv [eq]; rewrite carry_mul_rep, mul_rep; reflexivity)
     end.
-    let RHS := match goal with |- {vs | eq ?vs ?RHS} => RHS end in
+    let RHS := match goal with |- {vs | eq vs ?RHS} => RHS end in
     let RHSf := match (eval pattern powx in RHS) with ?RHSf _ => RHSf end in
     change ({vs | eq vs (Let_In powx RHSf)}).
     match goal with
diff --git a/src/MxDHRepChange.v b/src/MxDHRepChange.v
index c99635baf..4596ad188 100644
--- a/src/MxDHRepChange.v
+++ b/src/MxDHRepChange.v
@@ -23,13 +23,15 @@ Section MxDHRepChange.
   Qed.
 
   Ltac t :=
+    let hom := match goal with H : is_homomorphism |- _ => H end in
+    let mhom := constr:(@homomorphism_is_homomorphism _ _ _ _ _ _ _ _ _ _ _ hom) in
     repeat (
-        rewrite homomorphism_id ||
-        rewrite homomorphism_one ||
+        rewrite (@homomorphism_id _ _ _ _ _ _ _ _ _ _ _ _ _ mhom) ||
+        rewrite (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ hom) ||
+        rewrite (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ hom) ||
+        rewrite (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ hom) ||
+        rewrite (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ hom) ||
         rewrite homomorphism_a24 ||
-        rewrite homomorphism_sub ||
-        rewrite homomorphism_add ||
-        rewrite homomorphism_mul ||
         rewrite homomorphism_multiplicative_inverse_complete' ||
         reflexivity
       ).
@@ -75,7 +77,7 @@ Section MxDHRepChange.
 
   Lemma MxLoopIterRepChange b Fu s i Ku (HKu:Keq (FtoK Fu) Ku) : loopiter_eq
     (loopiter_phi (loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 Fu s i))
-    (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 Ku (loopiter_phi s) i).  
+    (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 Ku (loopiter_phi s) i).
   Proof.
     destruct_head' prod; break_match.
     simpl.
@@ -98,7 +100,9 @@ Section MxDHRepChange.
     generalize dependent init; generalize dependent init'.
     induction xs; [solve [eauto]|].
     repeat intro; simpl; rewrite IHxs by eauto.
-    f_equiv; eapply Proper_step'; eauto.
+    apply (_ : Proper ((R ==> eq ==> R) ==> SetoidList.eqlistA eq ==> R ==> R) (@fold_left _ _));
+      try reflexivity;
+      eapply Proper_step'; eauto.
   Qed.
 
   Global Instance Proper_downto {T R} {Equivalence_R:@Equivalence T R} :
@@ -154,4 +158,4 @@ Section MxDHRepChange.
     exact 0.
     exact 0.
   Qed.
-End MxDHRepChange.
\ No newline at end of file
+End MxDHRepChange.
diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v
index 9b58b5f5c..a3b51f28f 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -1,7 +1,5 @@
 (** * Interpretation of PHOAS syntax for expression trees on ℤ *)
-Require Import Bedrock.Nomega.
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.NArith.NArith.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
@@ -16,9 +14,6 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.WordUtil.
 Require Import Bedrock.Word.
-Require Import Crypto.Assembly.WordizeUtil.
-Require Import Crypto.Assembly.Evaluables.
-Require Import Crypto.Assembly.QhasmUtil.
 Export Reflection.Syntax.Notations.
 
 Local Notation eta x := (fst x, snd x).
@@ -215,16 +210,13 @@ Module Word64.
     := (forall x y z w,
            bounds_statement (wop x y z w) (Zop (word64ToZ x) (word64ToZ y) (word64ToZ z) (word64ToZ w))).
 
-  Require Import Crypto.Assembly.WordizeUtil.
-
   Lemma word64ToZ_add : bounds_2statement add Z.add. Proof. w64ToZ_t. Qed.
   Lemma word64ToZ_sub : bounds_2statement sub Z.sub. Proof. w64ToZ_t. Qed.
   Lemma word64ToZ_mul : bounds_2statement mul Z.mul. Proof. w64ToZ_t. Qed.
-
   Lemma word64ToZ_shl : bounds_2statement shl Z.shiftl.
   Proof.
     w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin.
-    rewrite wordToN_NToWord; [rewrite <- Z_inj_shiftl; reflexivity|].
+    rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftl; reflexivity|].
     apply N2Z.inj_lt.
     rewrite Z_inj_shiftl. 
     destruct (Z.lt_ge_cases 0 ((word64ToZ x) << (word64ToZ y)))%Z;
@@ -236,7 +228,7 @@ Module Word64.
   Lemma word64ToZ_shr : bounds_2statement shr Z.shiftr.
   Proof.
     w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin.
-    rewrite wordToN_NToWord; [rewrite <- Z_inj_shiftr; reflexivity|].
+    rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftr; reflexivity|].
     apply N2Z.inj_lt.
     rewrite Z_inj_shiftr.
     destruct (Z.lt_ge_cases 0 ((word64ToZ x) >> (word64ToZ y)))%Z;
@@ -434,9 +426,9 @@ Module ZBounds.
     : Tuple.tuple t (S pred_n)
     := Tuple.push_option
          match int_width, Tuple.lift_option modulus, Tuple.lift_option value with
-         | Some int_width, Some modulus, Some value
-           => if check_conditional_subtract_bounds pred_n int_width modulus value
-              then Some (conditional_subtract' pred_n int_width modulus value)
+         | Some int_width, Some modulus, Some value'
+           => if check_conditional_subtract_bounds pred_n int_width modulus value'
+              then Some (conditional_subtract' pred_n int_width modulus value')
               else None
          | _, _, _ => None
          end.
@@ -684,6 +676,10 @@ Module BoundedWord64.
   Ltac ktrans k := do k (etransitivity; [|eassumption]); assumption.
   Ltac trans' := first [ assumption | ktrans ltac:1 | ktrans ltac:2 ].
 
+  Local Hint Resolve Word64.bit_width_pos : zarith.
+  Local Hint Extern 1 (Z.log2 _ < _)%Z => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eassumption | eassumption ] : zarith.
+  (* Local *) Hint Resolve <- Z.log2_lt_pow2_alt : zarith.
+
 
   (** TODO(jadep): Use the bounds lemma here to prove that if each
       component of [ret_val] is [Some (l, v, u)], then we can fill in
@@ -696,6 +692,28 @@ Module BoundedWord64.
                pred_n (BoundedWordToBounds x)
                (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true)
     : HList.hlist
+        (fun vlu : Z * ZBounds.bounds =>
+           (0 <= ZBounds.lower (snd vlu))%Z /\
+           (ZBounds.lower (snd vlu) <= fst vlu <= ZBounds.upper (snd vlu))%Z /\
+           (Z.log2 (ZBounds.upper (snd vlu)) < Word64.bit_width)%Z)
+        (Tuple.map2 (fun v lu => (v, lu))
+                    (ModularBaseSystemListZOperations.conditional_subtract_modulus
+                       (S pred_n)
+                       (Word64.word64ToZ (value x))
+                       (Tuple.map Word64.word64ToZ (Tuple.map value y))
+                       (Tuple.map Word64.word64ToZ (Tuple.map value z)))
+                    (ZBounds.conditional_subtract'
+                       pred_n (BoundedWordToBounds x)
+                       (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))).
+  Proof. Admitted.
+
+  Lemma conditional_subtract_bounded_word
+        (pred_n : nat) (x : BoundedWord)
+        (y z : Tuple.tuple BoundedWord (S pred_n))
+        (H : ZBounds.check_conditional_subtract_bounds
+               pred_n (BoundedWordToBounds x)
+               (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true)
+    : HList.hlist
         (fun vlu : Word64.word64 * ZBounds.bounds =>
            (0 <= ZBounds.lower (snd vlu))%Z /\
            (ZBounds.lower (snd vlu) <= Word64.word64ToZ (fst vlu) <= ZBounds.upper (snd vlu))%Z /\
@@ -706,12 +724,73 @@ Module BoundedWord64.
                     (ZBounds.conditional_subtract'
                        pred_n (BoundedWordToBounds x)
                        (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))).
-  Proof. Admitted.
+  Proof.
+    generalize (conditional_subtract_bounded pred_n x y z H).
+    unfold Word64.conditional_subtract; rewrite Tuple.map2_map_fst.
+    rewrite <- (Tuple.map_map2 (fun a b => (a, b)) (fun ab => (Word64.ZToWord64 (fst ab), snd ab))).
+    rewrite HList.hlist_map; simpl @fst; simpl @snd.
+    apply HList.hlist_impl, HList.const.
+    intros; destruct_head' and; repeat split;
+      autorewrite with push_word64ToZ; omega.
+  Qed.
 
+  Lemma conditional_subtract_bounded_lite_helper
+        (pred_n : nat) (x : BoundedWord)
+        (y z : Tuple.tuple BoundedWord (S pred_n))
+        (H : ZBounds.check_conditional_subtract_bounds
+               pred_n (BoundedWordToBounds x)
+               (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true)
+    : HList.hlist
+        (fun v : Z =>
+           (0 <= v)%Z /\
+           (Z.log2 v < Word64.bit_width)%Z)
+        (Tuple.map
+           (@fst _ _)
+           (Tuple.map2 (fun v lu => (v, lu))
+                       (ModularBaseSystemListZOperations.conditional_subtract_modulus
+                          (S pred_n)
+                          (Word64.word64ToZ (value x))
+                          (Tuple.map Word64.word64ToZ (Tuple.map value y))
+                          (Tuple.map Word64.word64ToZ (Tuple.map value z)))
+                       (ZBounds.conditional_subtract'
+                          pred_n (BoundedWordToBounds x)
+                          (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z)))).
+  Proof.
+    generalize (conditional_subtract_bounded pred_n x y z H).
+    rewrite HList.hlist_map.
+    apply HList.hlist_impl, HList.const; intros.
+    destruct_head' and.
+    split; try omega; [].
+    eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ]; omega.
+  Qed.
+
+  Lemma conditional_subtract_bounded_lite
+        (pred_n : nat)
+        (xbw : BoundedWord) (ybw zbw : Tuple.tuple BoundedWord (S pred_n))
+        (x : Word64.word64) (y z : Tuple.tuple Word64.word64 (S pred_n))
+        (xb : ZBounds.bounds)  (yb zb : Tuple.tuple ZBounds.bounds (S pred_n))
+        (Hx : value xbw = x) (Hy : Tuple.map value ybw = y) (Hz : Tuple.map value zbw = z)
+        (Hxb : BoundedWordToBounds xbw = xb)
+        (Hyb : Tuple.map BoundedWordToBounds ybw = yb) (Hzb : Tuple.map BoundedWordToBounds zbw = zb)
+        (Hc : ZBounds.check_conditional_subtract_bounds pred_n xb yb zb = true)
+    : HList.hlist (fun v : Z => (0 <= v)%Z /\ (Z.log2 v < Z.of_nat Word64.bit_width)%Z)
+                  (ModularBaseSystemListZOperations.conditional_subtract_modulus
+                     (S pred_n)
+                     (Word64.word64ToZ x)
+                     (Tuple.map Word64.word64ToZ y)
+                     (Tuple.map Word64.word64ToZ z)).
+  Proof.
+    subst.
+    generalize (conditional_subtract_bounded_lite_helper pred_n xbw ybw zbw Hc).
+    rewrite Tuple.map_map2; simpl @fst.
+    rewrite Tuple.map2_fst, Tuple.map_id.
+    trivial.
+  Qed.
+
+  (* TODO (rsloan): not entirely sure what's the best way to match on these... *)
   Local Ltac kill_assumptions :=
     repeat split; abstract (cbn; assumption).
 
-  (* TODO (rsloan): not entirely sure what's the best way to match on these... *)
   Local Ltac apply_update lem lower0 value0 upper0 lower1 value1 upper1 := first
     [ apply (lem 64 lower1 value1 upper1 lower0 value0 upper0); kill_assumptions
     | apply (lem 64 lower0 value0 upper0 lower1 value1 upper1); kill_assumptions].
@@ -780,7 +859,7 @@ Module BoundedWord64.
                      | progress subst
                      | progress inversion_option
                      | intro
-                     | solve [ auto using conditional_subtract_bounded ] ]
+                     | solve [ auto using conditional_subtract_bounded_word ] ]
       ).
   Defined.
 
@@ -851,18 +930,18 @@ Module BoundedWord64.
     eauto.
   Qed.
 
-  Local Notation binop_correct_None op opW opB :=
+  Local Notation binop_correct_None op opB :=
     (forall x y, op (Some x) (Some y) = None -> opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y)) = None)
       (only parsing).
 
-  Local Notation op4_correct_None op opW opB :=
+  Local Notation op4_correct_None op opB :=
     (forall x y z w, op (Some x) (Some y) (Some z) (Some w) = None
                      -> opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y))
                             (Some (BoundedWordToBounds z)) (Some (BoundedWordToBounds w))
                         = None)
       (only parsing).
 
-  Local Notation op1_tuple2_correct_None op opW opB :=
+  Local Notation op1_tuple2_correct_None op opB :=
     (forall x y z,
         Tuple.lift_option (op (Some x) (Tuple.push_option (Some y)) (Tuple.push_option (Some z))) = None
         -> Tuple.lift_option
@@ -873,7 +952,7 @@ Module BoundedWord64.
       (only parsing).
 
   Lemma t_map2_correct_None opW opB pf
-    : binop_correct_None (t_map2 opW opB pf) opW opB.
+    : binop_correct_None (t_map2 opW opB pf) opB.
   Proof.
     intros ?? H.
     unfold t_map2 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds;
@@ -883,7 +962,7 @@ Module BoundedWord64.
   Qed.
 
   Lemma t_map4_correct_None opW opB pf
-    : op4_correct_None (t_map4 opW opB pf) opW opB.
+    : op4_correct_None (t_map4 opW opB pf) opB.
   Proof.
     intros ???? H.
     unfold t_map4 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds;
@@ -893,7 +972,7 @@ Module BoundedWord64.
   Qed.
 
   Lemma t_map1_tuple2_correct_None {n} opW opB pf
-    : op1_tuple2_correct_None (t_map1_tuple2 (n:=n) opW opB pf) opW opB.
+    : op1_tuple2_correct_None (t_map1_tuple2 (n:=n) opW opB pf) opB.
   Proof.
     intros ??? H.
     unfold t_map1_tuple2 in H; unfold BoundedWordToBounds in *.
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v
index 457d0d5ad..71d25fa3f 100644
--- a/src/Reflection/Z/Interpretations/Relations.v
+++ b/src/Reflection/Z/Interpretations/Relations.v
@@ -231,8 +231,8 @@ Lemma related_tuples_lift_relation2_untuple'
     <-> LiftOption.lift_relation2
           (interp_flat_type_rel_pointwise2 (fun _ => R))
           TZ
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) t)
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) u).
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
 Proof.
   induction n.
   { destruct_head' option; reflexivity. }
@@ -257,8 +257,8 @@ Lemma related_tuples_lift_relation2_untuple'_ext
     <-> LiftOption.lift_relation2
           (interp_flat_type_rel_pointwise2 (fun _ => R))
           TZ
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
 Proof.
   induction n.
   { destruct_head_hnf' option; reflexivity. }
@@ -270,7 +270,7 @@ Proof.
         (etransitivity;
          [ | first [ refine (f_equal (option_map (@fst _ _)) (_ : _ = Some (_, _))); eassumption
                    | refine (f_equal (option_map (@snd _ _)) (_ : _ = Some (_, _))); eassumption ] ]);
-        simpl in *; break_match; simpl in *; congruence. }
+        instantiate; simpl in *; break_match; simpl in *; congruence. }
     destruct_head_hnf' prod;
       destruct_head_hnf' option;
       simpl @fst in *; simpl @snd in *;
@@ -319,6 +319,7 @@ Local Arguments LiftOption.of' _ _ !_ / .
 Local Arguments BoundedWord64.BoundedWordToBounds !_ / .
 
 Local Ltac t_map1_tuple2_t_step :=
+  instantiate;
   first [ exact I
         | reflexivity
         | progress destruct_head_hnf' False
@@ -330,7 +331,7 @@ Local Ltac t_map1_tuple2_t_step :=
         | intro
         | apply @related_tuples_None_left; constructor
         | apply -> @related_tuples_Some_left
-        | apply <- @related_tuples_proj_eq_rel_untuple
+        | refine (proj2 (@related_tuples_proj_eq_rel_untuple _ _ _ _ _ _) _)
         | apply <- @related_tuples_lift_relation2_untuple'
         | match goal with
           | [ H : appcontext[LiftOption.lift_relation] |- _ ]
@@ -491,7 +492,7 @@ Local Ltac Word64.Rewrites.word64_util_arith ::=
                       auto with zarith ]
             | apply Z.land_nonneg; Word64.Rewrites.word64_util_arith
             | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ];
-              apply Z.min_case_strong; intros;
+              instantiate; apply Z.min_case_strong; intros;
               first [ etransitivity; [ apply Z.land_upper_bound_l | ]; omega
                     | etransitivity; [ apply Z.land_upper_bound_r | ]; omega ]
             | rewrite Z.log2_lor by omega;
@@ -556,10 +557,15 @@ Tactic Notation "admit" := abstract case proof_admitted.
 Local Arguments related'_Z _ _ _ / .
 Lemma related_Z_t_map1_tuple2 n opZ opW opB pf
       (H : forall x y z bxs bys bzs brs,
-          Tuple.push_option (Some brs) = opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs))
+          Some brs = Tuple.lift_option (opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs)))
           -> is_in_bounds x bxs
-          (*-> is_in_bounds y bys
-          -> is_in_bounds z bzs
+          -> { ybw : Tuple.tuple BoundedWord64.BoundedWord _
+             | Tuple.map BoundedWord64.value ybw = y
+               /\ Tuple.map BoundedWord64.BoundedWordToBounds ybw = bys }
+          -> { zbw : Tuple.tuple BoundedWord64.BoundedWord _
+             | Tuple.map BoundedWord64.value zbw = z
+               /\ Tuple.map BoundedWord64.BoundedWordToBounds zbw = bzs }
+          (*
           -> is_in_bounds (opW x y z) brs*)
           -> Tuple.map Word64.word64ToZ (opW x y z) = (opZ (Word64.word64ToZ x) (Tuple.map Word64.word64ToZ y) (Tuple.map Word64.word64ToZ z)))
       sv1 sv2
@@ -594,8 +600,13 @@ Local Ltac related_Z_op_fin_t_step :=
         | progress inversion_option
         | intro
         | progress autorewrite with push_word64ToZ
-        | match goal with H : andb _ _ = true |- _ => rewrite Bool.andb_true_iff in H end
-        | progress Z.ltb_to_lt ].
+        | match goal with
+          | [ H : andb _ _ = true |- _ ] => rewrite Bool.andb_true_iff in H
+          | [ H : context[Tuple.lift_option (Tuple.push_option _)] |- _ ]
+            => rewrite Tuple.lift_push_option in H
+          end
+        | progress Z.ltb_to_lt
+        | (progress unfold ZBounds.conditional_subtract in * ); break_match_hyps ].
 Local Ltac related_Z_op_fin_t := repeat related_Z_op_fin_t_step.
 
 Local Opaque Word64.bit_width.
@@ -614,9 +625,13 @@ Proof.
   { apply related_Z_t_map4; related_Z_op_fin_t. }
   { apply related_Z_t_map4; related_Z_op_fin_t. }
   { apply related_Z_t_map1_tuple2; related_Z_op_fin_t;
-      rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith.
-    pose proof BoundedWord64.conditional_subtract_bounded.
-    admit. (** TODO(jadep or jgross): Fill me in *) }
+      rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith; [].
+    destruct_head' sig; destruct_head' and; subst.
+    eapply BoundedWord64.conditional_subtract_bounded_lite
+    with (xbw := {| BoundedWord64.value := _ |});
+      [ .. | eassumption ]; reflexivity.
+    Grab Existential Variables.
+    omega. }
 Qed.
 
 Create HintDb interp_related discriminated.
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 80932d4df..3d448f97c 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -126,48 +126,7 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv
       /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
        (only parsing).
 
-Local Ltac args_to_bounded_helper v :=
-  lazymatch v with
-  | (?x, ?xs)
-    => args_to_bounded_helper x; [ .. | args_to_bounded_helper xs ]
-  | ?w
-    => try refine (_, _); [ refine {| BoundedWord64.value := w |} | .. ]
-  end.
-
-Local Ltac make_args x :=
-  let x' := fresh "x'" in
-  pose (x : id _) as x';
-  cbv [fe25519W wire_digitsW] in x; destruct_head' prod;
-  cbv [fst snd] in *;
-  simpl @fe25519WToZ in *;
-  simpl @wire_digitsWToZ in *;
-  let T := fresh in
-  evar (T : Type);
-  cut T; subst T;
-  [ let H := fresh in
-    intro H;
-    let xv := (eval hnf in x') in
-    args_to_bounded_helper xv;
-    [ instantiate;
-      destruct_head' and;
-      match goal with
-      | [ H : ?T |- _ ]
-        => is_evar T;
-           refine (let c := proj1 H in _); (* work around broken evars in Coq 8.4 *)
-           lazymatch goal with H := proj1 _ |- _ => refine H end
-      end.. ]
-  | instantiate;
-    repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end;
-    repeat match goal with H : wire_digits_is_bounded _ = true |- _ => unfold_is_bounded_in H end;
-    destruct_head' and;
-    Z.ltb_to_lt;
-    repeat first [ eexact I
-                 | apply conj;
-                   [ repeat apply conj; [ | eassumption | eassumption | ];
-                     instantiate; vm_compute; [ refine (fun x => match x with eq_refl => I end) | reflexivity ]
-                   | ] ] ].
-
-Local Ltac app_tuples x y :=
+Ltac app_tuples x y :=
   let tx := type of x in
   lazymatch (eval hnf in tx) with
   | prod _ _ => let xs := app_tuples (snd x) y in
@@ -175,15 +134,120 @@ Local Ltac app_tuples x y :=
   | _ => constr:((x, y))
   end.
 
-Class is_evar {T} (x : T) := make_is_evar : True.
-Hint Extern 0 (is_evar ?e) => is_evar e; exact I : typeclass_instances.
+Local Arguments Tuple.map2 : simpl never.
+Local Arguments Tuple.map : simpl never.
+
+Fixpoint args_to_bounded_helperT {n}
+         (v : Tuple.tuple' Word64.word64 n)
+         (bounds : Tuple.tuple' (Z * Z) n)
+         (pf : List.fold_right
+                 andb true
+                 (Tuple.to_list
+                    _
+                    (Tuple.map2
+                       (n:=S n)
+                       (fun bounds v =>
+                          let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool)
+                       bounds
+                       (Tuple.map (n:=S n) Word64.word64ToZ v))) = true)
+         (res : Type)
+         {struct n}
+  : Type.
+Proof.
+  refine (match n return (forall (v : Tuple.tuple' _ n) (bounds : Tuple.tuple' _ n),
+                             List.fold_right
+                               _ _ (Tuple.to_list
+                                      _
+                                      (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true
+                             -> Type)
+          with
+          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res
+          | S n' => fun v' bounds' pf0 => let t := _ in
+                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
+          end v bounds pf).
+  { clear -pf0.
+    abstract (
+        destruct v', bounds'; simpl @fst;
+        rewrite Tuple.map_S in pf0;
+        simpl in pf0;
+        rewrite Tuple.map2_S in pf0;
+        simpl @List.fold_right in *;
+        rewrite Bool.andb_true_iff in pf0; tauto
+      ). }
+Defined.
+
+Fixpoint args_to_bounded_helper {n} res
+         {struct n}
+  : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
+Proof.
+  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
+         | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |}
+         | S n'
+           => fun v bounds pf f pf'
+              => @args_to_bounded_helper
+                   n' res (fst v) (fst bounds) _
+                   (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |}))
+         end.
+  { clear -pf pf'.
+    unfold Tuple.map2, Tuple.map in pf; simpl in *.
+    abstract (
+        destruct bounds;
+        simpl in *;
+        rewrite !Bool.andb_true_iff in pf;
+        destruct_head' and;
+        Z.ltb_to_lt; auto
+      ). }
+  { simpl in *.
+    clear -pf pf'.
+    abstract (
+        destruct bounds as [? [? ?] ], v; simpl in *;
+        rewrite Tuple.map_S in pf; simpl in pf; rewrite Tuple.map2_S in pf;
+        simpl in pf;
+        rewrite !Bool.andb_true_iff in pf;
+        destruct_head' and;
+        Z.ltb_to_lt; auto
+      ). }
+Defined.
+
+Definition assoc_right''
+  := Eval cbv [Tuple.assoc_right' Tuple.rsnoc' fst snd] in @Tuple.assoc_right'.
+
+Definition args_to_bounded {n} v bounds pf
+  := Eval cbv [args_to_bounded_helper assoc_right''] in
+      @args_to_bounded_helper n _ v bounds pf (@assoc_right'' _ _).
+
+Local Ltac get_len T :=
+  match (eval hnf in T) with
+  | prod ?A ?B
+    => let a := get_len A in
+       let b := get_len B in
+       (eval compute in (a + b)%nat)
+  | _ => constr:(1%nat)
+  end.
+
+Local Ltac args_to_bounded x H :=
+  let x' := fresh in
+  set (x' := x);
+  compute in x;
+  let len := (let T := type of x in get_len T) in
+  destruct_head' prod;
+  let c := constr:(args_to_bounded (n:=pred len) x' _ H) in
+  let bounds := lazymatch c with args_to_bounded _ ?bounds _ => bounds end in
+  let c := (eval cbv [all_binders_for ExprUnOpT interp_flat_type args_to_bounded bounds pred fst snd] in c) in
+  apply c; compute; clear;
+  try abstract (
+        repeat split;
+        solve [ reflexivity
+              | refine (fun v => match v with eq_refl => I end) ]
+      ).
 
 Definition unop_args_to_bounded (x : fe25519W) (H : is_bounded (fe25519WToZ x) = true)
   : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT).
-Proof. make_args x. Defined.
+Proof. args_to_bounded x H. Defined.
+
 Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true)
   : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET).
-Proof. make_args x. Defined.
+Proof. args_to_bounded x H. Defined.
 Definition binop_args_to_bounded (x : fe25519W * fe25519W)
            (H : is_bounded (fe25519WToZ (fst x)) = true)
            (H' : is_bounded (fe25519WToZ (snd x)) = true)
@@ -225,7 +289,6 @@ Local Ltac make_bounds_prop bounds orig_bounds :=
              | None => false
              end).
 
-
 Definition unop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprUnOpT)) : bool.
 Proof. make_bounds_prop bounds ExprUnOp_bounds. Defined.
 Definition binop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprBinOpT)) : bool.
@@ -244,7 +307,7 @@ Defined.
     various kinds of correct and boundedness, and abstract in Gallina
     rather than Ltac *)
 
-Local Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
+Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Heq := fresh "Heq" in
   let Hbounds0 := fresh "Hbounds0" in
   let Hbounds1 := fresh "Hbounds1" in
@@ -311,192 +374,6 @@ Local Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   change Word64.word64ToZ with word64ToZ in *;
   repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
 
-Local Opaque Interp.
-Lemma ExprBinOp_correct_and_bounded
-      ropW op (ropZ_sig : rexpr_binop_sig op)
-      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
-      (H0 : forall xy
-                   (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy)))
-                   (Hxy : is_bounded (fe25519WToZ (fst xy)) = true
-                          /\ is_bounded (fe25519WToZ (snd xy)) = true),
-          let Hx := let (Hx, Hy) := Hxy in Hx in
-          let Hy := let (Hx, Hy) := Hxy in Hy in
-          let args := binop_args_to_bounded xy Hx Hy in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
-                                    (LiftOption.to' (Some args)))
-          with
-          | Some _ => True
-          | None => False
-          end)
-      (H1 : forall xy
-                   (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy)))
-                   (Hxy : is_bounded (fe25519WToZ (fst xy)) = true
-                          /\ is_bounded (fe25519WToZ (snd xy)) = true),
-          let Hx := let (Hx, Hy) := Hxy in Hx in
-          let Hy := let (Hx, Hy) := Hxy in Hy in
-          let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
-          with
-          | Some bounds => binop_bounds_good bounds = true
-          | None => False
-          end)
-  : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
-Proof.
-  intros x y Hx Hy.
-  pose x as x'; pose y as y'.
-  hnf in x, y; destruct_head' prod.
-  specialize (H0 (x', y') (conj Hx Hy)).
-  specialize (H1 (x', y') (conj Hx Hy)).
-  let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
-
-Lemma ExprUnOp_correct_and_bounded
-      ropW op (ropZ_sig : rexpr_unop_sig op)
-      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
-      (H0 : forall x
-                   (x := eta_fe25519W x)
-                   (Hx : is_bounded (fe25519WToZ x) = true),
-          let args := unop_args_to_bounded x Hx in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
-                                    (LiftOption.to' (Some args)))
-          with
-          | Some _ => True
-          | None => False
-          end)
-      (H1 : forall x
-                   (x := eta_fe25519W x)
-                   (Hx : is_bounded (fe25519WToZ x) = true),
-          let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
-          with
-          | Some bounds => unop_bounds_good bounds = true
-          | None => False
-          end)
-  : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
-Proof.
-  intros x Hx.
-  pose x as x'.
-  hnf in x; destruct_head' prod.
-  specialize (H0 x' Hx).
-  specialize (H1 x' Hx).
-  let args := constr:(unop_args_to_bounded x' Hx) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
-
-Lemma ExprUnOpFEToWire_correct_and_bounded
-      ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op)
-      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
-      (H0 : forall x
-                   (x := eta_fe25519W x)
-                   (Hx : is_bounded (fe25519WToZ x) = true),
-          let args := unop_args_to_bounded x Hx in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
-                                    (LiftOption.to' (Some args)))
-          with
-          | Some _ => True
-          | None => False
-          end)
-      (H1 : forall x
-                   (x := eta_fe25519W x)
-                   (Hx : is_bounded (fe25519WToZ x) = true),
-          let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
-          with
-          | Some bounds => unopFEToWire_bounds_good bounds = true
-          | None => False
-          end)
-  : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
-Proof.
-  intros x Hx.
-  pose x as x'.
-  hnf in x; destruct_head' prod.
-  specialize (H0 x' Hx).
-  specialize (H1 x' Hx).
-  let args := constr:(unop_args_to_bounded x' Hx) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
-
-Lemma ExprUnOpWireToFE_correct_and_bounded
-      ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op)
-      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
-      (H0 : forall x
-                   (x := eta_wire_digitsW x)
-                   (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
-          let args := unopWireToFE_args_to_bounded x Hx in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
-                                    (LiftOption.to' (Some args)))
-          with
-          | Some _ => True
-          | None => False
-          end)
-      (H1 : forall x
-                   (x := eta_wire_digitsW x)
-                   (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
-          let args := unopWireToFE_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
-          with
-          | Some bounds => unopWireToFE_bounds_good bounds = true
-          | None => False
-          end)
-  : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
-Proof.
-  intros x Hx.
-  pose x as x'.
-  hnf in x; destruct_head' prod.
-  specialize (H0 x' Hx).
-  specialize (H1 x' Hx).
-  let args := constr:(unopWireToFE_args_to_bounded x' Hx) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
-
-Lemma ExprUnOpFEToZ_correct_and_bounded
-      ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op)
-      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
-      (H0 : forall x
-                   (x := eta_fe25519W x)
-                   (Hx : is_bounded (fe25519WToZ x) = true),
-          let args := unop_args_to_bounded x Hx in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
-                                    (LiftOption.to' (Some args)))
-          with
-          | Some _ => True
-          | None => False
-          end)
-      (H1 : forall x
-                   (x := eta_fe25519W x)
-                   (Hx : is_bounded (fe25519WToZ x) = true),
-          let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
-          match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
-          with
-          | Some bounds => unopFEToZ_bounds_good bounds = true
-          | None => False
-          end)
-  : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op.
-Proof.
-  intros x Hx.
-  pose x as x'.
-  hnf in x; destruct_head' prod.
-  specialize (H0 x' Hx).
-  specialize (H1 x' Hx).
-  let args := constr:(unop_args_to_bounded x' Hx) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
 
 Ltac rexpr_correct :=
   let ropW' := fresh in
diff --git a/src/Specific/GF25519Reflective/CommonBinOp.v b/src/Specific/GF25519Reflective/CommonBinOp.v
new file mode 100644
index 000000000..32dae16e6
--- /dev/null
+++ b/src/Specific/GF25519Reflective/CommonBinOp.v
@@ -0,0 +1,50 @@
+Require Export Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Lemma ExprBinOp_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_binop_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall xy
+                   (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy)))
+                   (Hxy : is_bounded (fe25519WToZ (fst xy)) = true
+                          /\ is_bounded (fe25519WToZ (snd xy)) = true),
+          let Hx := let (Hx, Hy) := Hxy in Hx in
+          let Hy := let (Hx, Hy) := Hxy in Hy in
+          let args := binop_args_to_bounded xy Hx Hy in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall xy
+                   (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy)))
+                   (Hxy : is_bounded (fe25519WToZ (fst xy)) = true
+                          /\ is_bounded (fe25519WToZ (snd xy)) = true),
+          let Hx := let (Hx, Hy) := Hxy in Hx in
+          let Hy := let (Hx, Hy) := Hxy in Hy in
+          let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => binop_bounds_good bounds = true
+          | None => False
+          end)
+  : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x y Hx Hy.
+  pose x as x'; pose y as y'.
+  hnf in x, y; destruct_head' prod.
+  specialize (H0 (x', y') (conj Hx Hy)).
+  specialize (H1 (x', y') (conj Hx Hy)).
+  let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in
+  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
+Qed.
diff --git a/src/Specific/GF25519Reflective/CommonUnOp.v b/src/Specific/GF25519Reflective/CommonUnOp.v
new file mode 100644
index 000000000..eac381b50
--- /dev/null
+++ b/src/Specific/GF25519Reflective/CommonUnOp.v
@@ -0,0 +1,44 @@
+Require Export Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Lemma ExprUnOp_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_unop_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x
+                   (x := eta_fe25519W x)
+                   (Hx : is_bounded (fe25519WToZ x) = true),
+          let args := unop_args_to_bounded x Hx in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x
+                   (x := eta_fe25519W x)
+                   (Hx : is_bounded (fe25519WToZ x) = true),
+          let args := unop_args_to_bounded x Hx in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => unop_bounds_good bounds = true
+          | None => False
+          end)
+  : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x Hx.
+  pose x as x'.
+  hnf in x; destruct_head' prod.
+  specialize (H0 x' Hx).
+  specialize (H1 x' Hx).
+  let args := constr:(unop_args_to_bounded x' Hx) in
+  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
+Qed.
diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
new file mode 100644
index 000000000..2fa1d2ee3
--- /dev/null
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
@@ -0,0 +1,44 @@
+Require Export Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Lemma ExprUnOpFEToWire_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x
+                   (x := eta_fe25519W x)
+                   (Hx : is_bounded (fe25519WToZ x) = true),
+          let args := unop_args_to_bounded x Hx in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x
+                   (x := eta_fe25519W x)
+                   (Hx : is_bounded (fe25519WToZ x) = true),
+          let args := unop_args_to_bounded x Hx in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => unopFEToWire_bounds_good bounds = true
+          | None => False
+          end)
+  : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x Hx.
+  pose x as x'.
+  hnf in x; destruct_head' prod.
+  specialize (H0 x' Hx).
+  specialize (H1 x' Hx).
+  let args := constr:(unop_args_to_bounded x' Hx) in
+  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
+Qed.
diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
new file mode 100644
index 000000000..7528cfc2d
--- /dev/null
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
@@ -0,0 +1,44 @@
+Require Export Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Lemma ExprUnOpFEToZ_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x
+                   (x := eta_fe25519W x)
+                   (Hx : is_bounded (fe25519WToZ x) = true),
+          let args := unop_args_to_bounded x Hx in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x
+                   (x := eta_fe25519W x)
+                   (Hx : is_bounded (fe25519WToZ x) = true),
+          let args := unop_args_to_bounded x Hx in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => unopFEToZ_bounds_good bounds = true
+          | None => False
+          end)
+  : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x Hx.
+  pose x as x'.
+  hnf in x; destruct_head' prod.
+  specialize (H0 x' Hx).
+  specialize (H1 x' Hx).
+  let args := constr:(unop_args_to_bounded x' Hx) in
+  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
+Qed.
diff --git a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
new file mode 100644
index 000000000..d61807413
--- /dev/null
+++ b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
@@ -0,0 +1,44 @@
+Require Export Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Lemma ExprUnOpWireToFE_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x
+                   (x := eta_wire_digitsW x)
+                   (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
+          let args := unopWireToFE_args_to_bounded x Hx in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x
+                   (x := eta_wire_digitsW x)
+                   (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
+          let args := unopWireToFE_args_to_bounded x Hx in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => unopWireToFE_bounds_good bounds = true
+          | None => False
+          end)
+  : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x Hx.
+  pose x as x'.
+  hnf in x; destruct_head' prod.
+  specialize (H0 x' Hx).
+  specialize (H1 x' Hx).
+  let args := constr:(unopWireToFE_args_to_bounded x' Hx) in
+  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
+Qed.
diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v
index 36357fcb7..ae3a6a4c6 100644
--- a/src/Specific/GF25519Reflective/Reified/Add.v
+++ b/src/Specific/GF25519Reflective/Reified/Add.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonBinOp.
 
 Definition raddZ_sig : rexpr_binop_sig add. Proof. reify_sig. Defined.
 Definition raddW := Eval vm_compute in rword_of_Z raddZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
index 0ff563a8c..3051121c0 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonBinOp.
 
 Definition rcarry_addZ_sig : rexpr_binop_sig carry_add. Proof. reify_sig. Defined.
 Definition rcarry_addW := Eval vm_compute in rword_of_Z rcarry_addZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
index 4c21fbeb8..571b9db97 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonUnOp.
 
 Definition rcarry_oppZ_sig : rexpr_unop_sig carry_opp. Proof. reify_sig. Defined.
 Definition rcarry_oppW := Eval vm_compute in rword_of_Z rcarry_oppZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v
index 3acfb1f45..fda466861 100644
--- a/src/Specific/GF25519Reflective/Reified/CarrySub.v
+++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonBinOp.
 
 Definition rcarry_subZ_sig : rexpr_binop_sig carry_sub. Proof. reify_sig. Defined.
 Definition rcarry_subW := Eval vm_compute in rword_of_Z rcarry_subZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v
index e3ecc62c8..0dcea29e4 100644
--- a/src/Specific/GF25519Reflective/Reified/Freeze.v
+++ b/src/Specific/GF25519Reflective/Reified/Freeze.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonUnOp.
 
 Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined.
 Definition rfreezeW := Eval vm_compute in rword_of_Z rfreezeZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v
index 73ee6904a..69eb3ba41 100644
--- a/src/Specific/GF25519Reflective/Reified/GeModulus.v
+++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonUnOpFEToZ.
 
 Definition rge_modulusZ_sig : rexpr_unop_FEToZ_sig ge_modulus. Proof. reify_sig. Defined.
 Definition rge_modulusW := Eval vm_compute in rword_of_Z rge_modulusZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v
index a206f02a1..0c298134d 100644
--- a/src/Specific/GF25519Reflective/Reified/Mul.v
+++ b/src/Specific/GF25519Reflective/Reified/Mul.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonBinOp.
 
 Definition rmulZ_sig : rexpr_binop_sig mul. Proof. reify_sig. Defined.
 Definition rmulW := Eval vm_compute in rword_of_Z rmulZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v
index 907771b14..58f2a6fbb 100644
--- a/src/Specific/GF25519Reflective/Reified/Opp.v
+++ b/src/Specific/GF25519Reflective/Reified/Opp.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonUnOp.
 
 Definition roppZ_sig : rexpr_unop_sig opp. Proof. reify_sig. Defined.
 Definition roppW := Eval vm_compute in rword_of_Z roppZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v
index a7cf4fc13..cd85d0cd7 100644
--- a/src/Specific/GF25519Reflective/Reified/Pack.v
+++ b/src/Specific/GF25519Reflective/Reified/Pack.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonUnOpFEToWire.
 
 Definition rpackZ_sig : rexpr_unop_FEToWire_sig pack. Proof. reify_sig. Defined.
 Definition rpackW := Eval vm_compute in rword_of_Z rpackZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v
index 9b684248d..03356cd50 100644
--- a/src/Specific/GF25519Reflective/Reified/Sub.v
+++ b/src/Specific/GF25519Reflective/Reified/Sub.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonBinOp.
 
 Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined.
 Definition rsubW := Eval vm_compute in rword_of_Z rsubZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v
index 027eedf39..a96f87d96 100644
--- a/src/Specific/GF25519Reflective/Reified/Unpack.v
+++ b/src/Specific/GF25519Reflective/Reified/Unpack.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519Reflective.CommonUnOpWireToFE.
 
 Definition runpackZ_sig : rexpr_unop_WireToFE_sig unpack. Proof. reify_sig. Defined.
 Definition runpackW := Eval vm_compute in rword_of_Z runpackZ_sig.
diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
index 76ac2c91b..404afc1ea 100755
--- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
+++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
@@ -25,7 +25,7 @@ Definition r%(lname)sW_correct_and_bounded
        match proof_admitted with end match proof_admitted with end.
 """ % locals()
     with open(name.replace('_', '') + '.v', 'w') as f:
-        f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common.
+        f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common%(uopkind)s.
 
 Definition r%(lname)sZ_sig : rexpr_%(lopkind)s_sig %(lname)s. Proof. reify_sig. Defined.
 Definition r%(lname)sW := Eval vm_compute in rword_of_Z r%(lname)sZ_sig.
diff --git a/src/Util/HList.v b/src/Util/HList.v
index aacefe8f3..ec9dcdd7b 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -88,6 +88,18 @@ Proof.
   destruct n; [ constructor | apply hlist'_impl ].
 Defined.
 
+Local Arguments Tuple.map : simpl never.
+Lemma hlist_map {n A B F} {f:A -> B} (xs:tuple A n)
+  : hlist F (Tuple.map f xs) = hlist (fun x => F (f x)) xs.
+Proof.
+  destruct n as [|n]; [ reflexivity | ].
+  induction n; [ reflexivity | ].
+  specialize (IHn (fst xs)).
+  destruct xs; rewrite Tuple.map_S.
+  simpl @hlist in *; rewrite <- IHn.
+  reflexivity.
+Qed.
+
 Module Tuple.
   Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
   : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 4d97c7857..79747ec2d 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -20,6 +20,42 @@ Definition tuple T n : Type :=
   | S n' => tuple' T n'
   end.
 
+(** right-associated tuples *)
+Fixpoint rtuple' T n : Type :=
+  match n with
+  | O => T
+  | S n' => (T * rtuple' T n')%type
+  end.
+
+Definition rtuple T n : Type :=
+  match n with
+  | O => unit
+  | S n' => rtuple' T n'
+  end.
+
+Fixpoint rsnoc' T n {struct n} : forall (x : rtuple' T n) (y : T), rtuple' T (S n)
+  := match n return forall (x : rtuple' T n) (y : T), rtuple' T (S n) with
+     | O => fun x y => (x, y)
+     | S n' => fun x y => (fst x, @rsnoc' T n' (snd x) y)
+     end.
+Global Arguments rsnoc' {T n} _ _.
+
+Fixpoint assoc_right' {n T} {struct n}
+  : tuple' T n -> rtuple' T n
+  := match n return tuple' T n -> rtuple' T n with
+     | 0 => fun x => x
+     | S n' => fun ts => let xs := @assoc_right' n' T (fst ts) in
+                         let x := snd ts in
+                         rsnoc' xs x
+     end.
+
+Definition assoc_right {n T}
+  : tuple T n -> rtuple T n
+  := match n with
+     | 0 => fun x => x
+     | S n' => @assoc_right' n' T
+     end.
+
 Definition tl' {T n} : tuple' T (S n) -> tuple' T n := @fst _ _.
 Definition tl {T n} : tuple T (S n) -> tuple T n :=
   match n with
@@ -168,6 +204,11 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
 Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n
   := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys.
 
+Lemma map2_S {n A B C} (f:A -> B -> C) (xs:tuple' A n) (ys:tuple' B n) (x:A) (y:B)
+  : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y).
+Proof.
+Admitted.
+
 Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n)
   : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys.
 Proof.
@@ -193,6 +234,23 @@ Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
 Proof.
 Admitted.
 
+Lemma map2_map {n A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:tuple A' n) (ys:tuple B' n)
+  : map2 f (map g xs) (map h ys) = map2 (fun a b => f (g a) (h b)) xs ys.
+Proof.
+Admitted.
+
+Lemma map2_map_fst {n A B C A'} (f:A -> B -> C) (g:A' -> A) (xs:tuple A' n) (ys:tuple B n)
+  : map2 f (map g xs) ys = map2 (fun a b => f (g a) b) xs ys.
+Proof.
+  rewrite <- (map2_map f g (fun x => x)), map_id; reflexivity.
+Qed.
+
+Lemma map2_map_snd {n A B C B'} (f:A -> B -> C) (g:B' -> B) (xs:tuple A n) (ys:tuple B' n)
+  : map2 f xs (map g ys) = map2 (fun a b => f a (g b)) xs ys.
+Proof.
+  rewrite <- (map2_map f (fun x => x) g), map_id; reflexivity.
+Qed.
+
 Lemma map_map {n A B C} (g : B -> C) (f : A -> B) (xs:tuple A n)
   : map g (map f xs) = map (fun x => g (f x)) xs.
 Proof.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 4c74fe9b4..f0e6ef335 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,6 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.NArith.NArith.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Bedrock.Word.
@@ -51,6 +52,32 @@ Proof.
   auto.
 Qed.
 
+Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N.
+Proof.
+  intros; induction x.
+
+  - simpl; apply N.lt_1_r; intuition.
+
+  - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition.
+      apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0.
+
+    + intuition; inversion H.
+
+    + apply N.neq_0_lt_0 in IHx; intuition.
+Qed.
+
+Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N.
+Proof.
+  induction n.
+
+  - simpl; intuition.
+
+  - rewrite Nat2N.inj_succ.
+    rewrite N.pow_succ_r; try apply N_ge_0.
+    rewrite <- IHn.
+    simpl; intuition.
+Qed.
+
 Lemma Npow2_Zlog2 : forall x n,
     (Z.log2 (Z.of_N x) < Z.of_nat n)%Z
  -> (x < Npow2 n)%N.
@@ -243,16 +270,26 @@ Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
 Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
 Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
 
-Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m :=
-  match n, m return wordsize_eq n m -> word n -> word m with
-  | O, O => fun _ _ => WO
-  | S n', S m' => fun _ w => WS (whd w) (@cast_word _ _ _ (wtl w))
-  | _, _ => fun _ _ => !
+Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y
+  := match x, y with
+     | O, O => fun _ => eq_refl
+     | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf))
+     | _, _ => fun x => x
+     end.
+
+Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl.
+Proof.
+  induction n; [ reflexivity | simpl ].
+  rewrite IHn; reflexivity.
+Qed.
+
+Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m :=
+  match correct_wordsize_eq n m pf in _ = y return word n -> word y with
+  | eq_refl => fun w => w
   end.
-Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *)
 
 Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
-Proof. induction w; simpl; auto using f_equal. Qed.
+Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed.
 
 Lemma wordToNat_cast_word {n} (w:word n) m pf :
   wordToNat (@cast_word n m pf w) = wordToNat w.
@@ -721,4 +758,4 @@ Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _.
 Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
     @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
 Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a.
-Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
\ No newline at end of file
+Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 17e8d62bf..42e88e8c4 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -944,6 +944,7 @@ Module Z.
       rewrite Z.ones_succ by assumption.
       zero_bounds.
   Qed.
+  Hint Resolve ones_nonneg : zarith.
 
   Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
   Proof.
@@ -953,6 +954,7 @@ Module Z.
     apply Z.lt_succ_lt_pred.
     apply Z.pow_gt_1; omega.
   Qed.
+  Hint Resolve ones_pos_pos : zarith.
 
   Lemma pow2_mod_id_iff : forall a n, 0 <= n ->
                                       (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n).
@@ -2128,7 +2130,7 @@ Module Z.
   Qed.
   Hint Resolve log2_ones_lt_nonneg : zarith.
 
-  Lemma log2_lt_pow2_alt a b : 0 < b -> a < 2^b <-> Z.log2 a < b.
+  Lemma log2_lt_pow2_alt a b : 0 < b -> (a < 2^b <-> Z.log2 a < b).
   Proof.
     destruct (Z_lt_le_dec 0 a); auto using Z.log2_lt_pow2; [].
     rewrite Z.log2_nonpos by omega.