Split up GF25519Reflective.Common: faster+parallel

After    | File Name                                     | Before   || Change
--------------------------------------------------------------------------------
2m53.12s | Total                                         | 2m52.26s || +0m00.85s
--------------------------------------------------------------------------------
0m01.38s | Specific/GF25519Reflective/Common             | 0m43.51s || -0m42.12s
0m14.82s | Specific/GF25519Reflective/CommonBinOp        |   N/A    || +0m14.82s
0m10.91s | Specific/GF25519Reflective/CommonUnOp         |   N/A    || +0m10.91s
0m10.44s | Specific/GF25519Reflective/CommonUnOpWireToFE |   N/A    || +0m10.43s
0m06.42s | Specific/GF25519Reflective/CommonUnOpFEToWire |   N/A    || +0m06.41s
1m18.24s | Experiments/Ed25519                           | 1m18.57s || -0m00.32s
0m07.97s | Specific/GF25519Reflective/Reified/Mul        | 0m08.45s || -0m00.47s
0m07.89s | Specific/GF25519Reflective/Reified/Freeze     | 0m07.84s || +0m00.04s
0m06.87s | Specific/GF25519Reflective                    | 0m06.92s || -0m00.04s
0m03.53s | Specific/GF25519Reflective/Reified/CarrySub   | 0m03.63s || -0m00.10s
0m03.27s | Specific/GF25519Reflective/Reified/CarryAdd   | 0m03.28s || -0m00.00s
0m03.18s | Specific/GF25519Reflective/Reified/CarryOpp   | 0m03.15s || +0m00.03s
0m02.24s | Specific/GF25519Reflective/Reified/Unpack     | 0m02.21s || +0m00.03s
0m02.19s | Specific/GF25519Reflective/Reified/Pack       | 0m02.28s || -0m00.08s
0m02.16s | Specific/GF25519Reflective/Reified/Sub        | 0m02.15s || +0m00.01s
0m02.14s | Specific/GF25519Bounded                       | 0m02.07s || +0m00.07s
0m02.07s | Experiments/Ed25519Extraction                 | 0m02.16s || -0m00.09s
0m01.99s | Specific/GF25519Reflective/Reified/Add        | 0m01.81s || +0m00.17s
0m01.82s | Specific/GF25519Reflective/Reified/Opp        | 0m01.78s || +0m00.04s
0m01.76s | Specific/GF25519Reflective/Reified/GeModulus  | 0m01.71s || +0m00.05s
0m00.97s | Specific/GF25519Reflective/CommonUnOpFEToZ    |   N/A    || +0m00.97s
0m00.86s | Specific/GF25519Reflective/Reified            | 0m00.75s || +0m00.10s

18 files changed, 348 insertions, 246 deletions

diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 80932d4df..71267e96a 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,119 @@ 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 => 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) _ 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 +288,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 +306,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 +373,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.