copy_bounds

18 files changed, 1128 insertions, 54 deletions

diff --git a/src/SpecificGen/GF2213_32BoundedCommon.v b/src/SpecificGen/GF2213_32BoundedCommon.v
index 7ec291046..2451f5f1d 100644
--- a/src/SpecificGen/GF2213_32BoundedCommon.v
+++ b/src/SpecificGen/GF2213_32BoundedCommon.v
@@ -871,5 +871,21 @@ Notation i9top_correct_and_bounded k irop op
               = op (fe2213_32WToZ x0) (fe2213_32WToZ x1) (fe2213_32WToZ x2) (fe2213_32WToZ x3) (fe2213_32WToZ x4) (fe2213_32WToZ x5) (fe2213_32WToZ x6) (fe2213_32WToZ x7) (fe2213_32WToZ x8))
              * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
        (only parsing).
+Notation i10top_correct_and_bounded k irop op
+  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+          is_bounded (fe2213_32WToZ x0) = true
+          -> is_bounded (fe2213_32WToZ x1) = true
+          -> is_bounded (fe2213_32WToZ x2) = true
+          -> is_bounded (fe2213_32WToZ x3) = true
+          -> is_bounded (fe2213_32WToZ x4) = true
+          -> is_bounded (fe2213_32WToZ x5) = true
+          -> is_bounded (fe2213_32WToZ x6) = true
+          -> is_bounded (fe2213_32WToZ x7) = true
+          -> is_bounded (fe2213_32WToZ x8) = true
+          -> is_bounded (fe2213_32WToZ x9) = true
+          -> (Tuple.map (n:=k) fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+              = op (fe2213_32WToZ x0) (fe2213_32WToZ x1) (fe2213_32WToZ x2) (fe2213_32WToZ x3) (fe2213_32WToZ x4) (fe2213_32WToZ x5) (fe2213_32WToZ x6) (fe2213_32WToZ x7) (fe2213_32WToZ x8) (fe2213_32WToZ x9))
+             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type)
+       (only parsing).
 
 Definition prefreeze := GF2213_32.prefreeze.
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index e5fab2a8d..884ae0fc3 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -55,6 +55,7 @@ Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe2213_32 pack). Defined.
 Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1.
 Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4.
+Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4.
 Definition ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -72,6 +73,7 @@ Definition ExprBinOp : Type := Expr ExprBinOpT.
 Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
+Definition Expr10_4Op : Type := Expr Expr10_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
@@ -82,6 +84,7 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t
 Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT.
 Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT.
 Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT.
+Definition expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_4OpT.
 Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
 Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT.
 Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET.
@@ -137,6 +140,8 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_
   := Eval compute in Expr_nm_Op_bounds 4 1.
 Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
   := Eval compute in Expr_nm_Op_bounds 9 4.
+Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 10 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
 
@@ -162,6 +167,19 @@ Definition interp_9_4expr : Expr9_4Op
                             -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
                             -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4
   := fun e => curry_9op_fe2213_32W (Interp (@WordW.interp_op) e).
+Definition interp_10_4expr : Expr10_4Op
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4
+  := fun e => curry_10op_fe2213_32W (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -175,6 +193,8 @@ Notation unop_WireToFE_correct_and_bounded rop op
   := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
 Notation op9_4_correct_and_bounded rop op
   := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing).
+Notation op10_4_correct_and_bounded rop op
+  := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing).
 
 Ltac rexpr_cbv :=
   lazymatch goal with
@@ -200,6 +220,7 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe22
 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe2213_32 op)) (only parsing).
 Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
 Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe2213_32 op)) (only parsing).
+Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe2213_32 op)) (only parsing).
 
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
@@ -394,6 +415,31 @@ Proof.
   let v := app_tuples (unop_args_to_bounded _ H0) v in
   exact v.
 Defined.
+Definition op10_args_to_bounded (x : fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W)
+           (H0 : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H1 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H2 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H3 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+           (H4 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+           (H5 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x)))))) = true)
+           (H6 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst x))))) = true)
+           (H7 : is_bounded (fe2213_32WToZ (snd (fst (fst x)))) = true)
+           (H8 : is_bounded (fe2213_32WToZ (snd (fst x))) = true)
+           (H9 : is_bounded (fe2213_32WToZ (snd x)) = true)
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT).
+Proof.
+  let v := constr:(unop_args_to_bounded _ H9) in
+  let v := app_tuples (unop_args_to_bounded _ H8) v in
+  let v := app_tuples (unop_args_to_bounded _ H7) v in
+  let v := app_tuples (unop_args_to_bounded _ H6) v in
+  let v := app_tuples (unop_args_to_bounded _ H5) v in
+  let v := app_tuples (unop_args_to_bounded _ H4) v in
+  let v := app_tuples (unop_args_to_bounded _ H3) v in
+  let v := app_tuples (unop_args_to_bounded _ H2) v in
+  let v := app_tuples (unop_args_to_bounded _ H1) v in
+  let v := app_tuples (unop_args_to_bounded _ H0) v in
+  exact v.
+Defined.
 
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
@@ -431,6 +477,8 @@ Proof.
 Defined.
 Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
 Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
+Definition op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_4OpT)) : bool.
+Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
 Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
   := fun x
@@ -469,12 +517,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Hbounds1 := fresh "Hbounds1" in
   let Hbounds2 := fresh "Hbounds2" in
   pose proof (proj2_sig ropZ_sig) as Heq;
-  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
-                    curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W
-                    curry_binop_fe2213_32 curry_unop_fe2213_32 curry_unop_wire_digits curry_9op_fe2213_32
-                    uncurry_binop_fe2213_32W uncurry_unop_fe2213_32W uncurry_unop_wire_digitsW uncurry_9op_fe2213_32W
-                    uncurry_binop_fe2213_32 uncurry_unop_fe2213_32 uncurry_unop_wire_digits uncurry_9op_fe2213_32
-                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
+  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr
+                    curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W curry_10op_fe2213_32W
+                    curry_binop_fe2213_32 curry_unop_fe2213_32 curry_unop_wire_digits curry_9op_fe2213_32 curry_10op_fe2213_32
+                    uncurry_binop_fe2213_32W uncurry_unop_fe2213_32W uncurry_unop_wire_digitsW uncurry_9op_fe2213_32W uncurry_10op_fe2213_32W
+                    uncurry_binop_fe2213_32 uncurry_unop_fe2213_32 uncurry_unop_wire_digits uncurry_9op_fe2213_32 uncurry_10op_fe2213_32
+                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT
                     interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
   cbv zeta in *;
   simpl @fe2213_32WToZ; simpl @wire_digitsWToZ;
@@ -505,7 +553,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   end;
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
-         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
+         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe2213_32WToZ ?x = _ /\ _ ]
@@ -523,8 +571,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
-           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good
-           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1;
+           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good
+           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1;
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe2213_32WToZ; simpl @wire_digitsWToZ;
diff --git a/src/SpecificGen/GF2213_32Reflective/Common10_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common10_4Op.v
new file mode 100644
index 000000000..26f1edaef
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Common10_4Op.v
@@ -0,0 +1,115 @@
+Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr10_4Op_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_10_4op_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe2213_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe2213_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe2213_32W (snd (fst (fst x0123456789))),
+                        eta_fe2213_32W (snd (fst x0123456789)),
+                        eta_fe2213_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe2213_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe2213_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe2213_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe2213_32W (snd (fst (fst x0123456789))),
+                        eta_fe2213_32W (snd (fst x0123456789)),
+                        eta_fe2213_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe2213_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => op10_4_bounds_good bounds = true
+          | None => False
+          end)
+  : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9.
+  pose x0 as x0'.
+  pose x1 as x1'.
+  pose x2 as x2'.
+  pose x3 as x3'.
+  pose x4 as x4'.
+  pose x5 as x5'.
+  pose x6 as x6'.
+  pose x7 as x7'.
+  pose x8 as x8'.
+  pose x9 as x9'.
+  hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod.
+  specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF2519_32BoundedCommon.v b/src/SpecificGen/GF2519_32BoundedCommon.v
index 42f7e2610..f8538a6fb 100644
--- a/src/SpecificGen/GF2519_32BoundedCommon.v
+++ b/src/SpecificGen/GF2519_32BoundedCommon.v
@@ -871,5 +871,21 @@ Notation i9top_correct_and_bounded k irop op
               = op (fe2519_32WToZ x0) (fe2519_32WToZ x1) (fe2519_32WToZ x2) (fe2519_32WToZ x3) (fe2519_32WToZ x4) (fe2519_32WToZ x5) (fe2519_32WToZ x6) (fe2519_32WToZ x7) (fe2519_32WToZ x8))
              * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
        (only parsing).
+Notation i10top_correct_and_bounded k irop op
+  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+          is_bounded (fe2519_32WToZ x0) = true
+          -> is_bounded (fe2519_32WToZ x1) = true
+          -> is_bounded (fe2519_32WToZ x2) = true
+          -> is_bounded (fe2519_32WToZ x3) = true
+          -> is_bounded (fe2519_32WToZ x4) = true
+          -> is_bounded (fe2519_32WToZ x5) = true
+          -> is_bounded (fe2519_32WToZ x6) = true
+          -> is_bounded (fe2519_32WToZ x7) = true
+          -> is_bounded (fe2519_32WToZ x8) = true
+          -> is_bounded (fe2519_32WToZ x9) = true
+          -> (Tuple.map (n:=k) fe2519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+              = op (fe2519_32WToZ x0) (fe2519_32WToZ x1) (fe2519_32WToZ x2) (fe2519_32WToZ x3) (fe2519_32WToZ x4) (fe2519_32WToZ x5) (fe2519_32WToZ x6) (fe2519_32WToZ x7) (fe2519_32WToZ x8) (fe2519_32WToZ x9))
+             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type)
+       (only parsing).
 
 Definition prefreeze := GF2519_32.prefreeze.
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index 729c79995..bf4be644f 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -55,6 +55,7 @@ Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe2519_32 pack). Defined.
 Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1.
 Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4.
+Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4.
 Definition ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -72,6 +73,7 @@ Definition ExprBinOp : Type := Expr ExprBinOpT.
 Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
+Definition Expr10_4Op : Type := Expr Expr10_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
@@ -82,6 +84,7 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t
 Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT.
 Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT.
 Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT.
+Definition expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_4OpT.
 Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
 Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT.
 Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET.
@@ -137,6 +140,8 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_
   := Eval compute in Expr_nm_Op_bounds 4 1.
 Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
   := Eval compute in Expr_nm_Op_bounds 9 4.
+Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 10 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
 
@@ -162,6 +167,19 @@ Definition interp_9_4expr : Expr9_4Op
                             -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
                             -> Tuple.tuple SpecificGen.GF2519_32BoundedCommon.fe2519_32W 4
   := fun e => curry_9op_fe2519_32W (Interp (@WordW.interp_op) e).
+Definition interp_10_4expr : Expr10_4Op
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
+                            -> Tuple.tuple SpecificGen.GF2519_32BoundedCommon.fe2519_32W 4
+  := fun e => curry_10op_fe2519_32W (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -175,6 +193,8 @@ Notation unop_WireToFE_correct_and_bounded rop op
   := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
 Notation op9_4_correct_and_bounded rop op
   := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing).
+Notation op10_4_correct_and_bounded rop op
+  := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing).
 
 Ltac rexpr_cbv :=
   lazymatch goal with
@@ -200,6 +220,7 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25
 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe2519_32 op)) (only parsing).
 Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
 Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe2519_32 op)) (only parsing).
+Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe2519_32 op)) (only parsing).
 
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
@@ -394,6 +415,31 @@ Proof.
   let v := app_tuples (unop_args_to_bounded _ H0) v in
   exact v.
 Defined.
+Definition op10_args_to_bounded (x : fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W)
+           (H0 : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H1 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H2 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H3 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+           (H4 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+           (H5 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x)))))) = true)
+           (H6 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst x))))) = true)
+           (H7 : is_bounded (fe2519_32WToZ (snd (fst (fst x)))) = true)
+           (H8 : is_bounded (fe2519_32WToZ (snd (fst x))) = true)
+           (H9 : is_bounded (fe2519_32WToZ (snd x)) = true)
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT).
+Proof.
+  let v := constr:(unop_args_to_bounded _ H9) in
+  let v := app_tuples (unop_args_to_bounded _ H8) v in
+  let v := app_tuples (unop_args_to_bounded _ H7) v in
+  let v := app_tuples (unop_args_to_bounded _ H6) v in
+  let v := app_tuples (unop_args_to_bounded _ H5) v in
+  let v := app_tuples (unop_args_to_bounded _ H4) v in
+  let v := app_tuples (unop_args_to_bounded _ H3) v in
+  let v := app_tuples (unop_args_to_bounded _ H2) v in
+  let v := app_tuples (unop_args_to_bounded _ H1) v in
+  let v := app_tuples (unop_args_to_bounded _ H0) v in
+  exact v.
+Defined.
 
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
@@ -431,6 +477,8 @@ Proof.
 Defined.
 Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
 Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
+Definition op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_4OpT)) : bool.
+Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
 Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
   := fun x
@@ -469,12 +517,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Hbounds1 := fresh "Hbounds1" in
   let Hbounds2 := fresh "Hbounds2" in
   pose proof (proj2_sig ropZ_sig) as Heq;
-  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
-                    curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W
-                    curry_binop_fe2519_32 curry_unop_fe2519_32 curry_unop_wire_digits curry_9op_fe2519_32
-                    uncurry_binop_fe2519_32W uncurry_unop_fe2519_32W uncurry_unop_wire_digitsW uncurry_9op_fe2519_32W
-                    uncurry_binop_fe2519_32 uncurry_unop_fe2519_32 uncurry_unop_wire_digits uncurry_9op_fe2519_32
-                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
+  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr
+                    curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W curry_10op_fe2519_32W
+                    curry_binop_fe2519_32 curry_unop_fe2519_32 curry_unop_wire_digits curry_9op_fe2519_32 curry_10op_fe2519_32
+                    uncurry_binop_fe2519_32W uncurry_unop_fe2519_32W uncurry_unop_wire_digitsW uncurry_9op_fe2519_32W uncurry_10op_fe2519_32W
+                    uncurry_binop_fe2519_32 uncurry_unop_fe2519_32 uncurry_unop_wire_digits uncurry_9op_fe2519_32 uncurry_10op_fe2519_32
+                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT
                     interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
   cbv zeta in *;
   simpl @fe2519_32WToZ; simpl @wire_digitsWToZ;
@@ -505,7 +553,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   end;
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
-         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
+         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe2519_32WToZ ?x = _ /\ _ ]
@@ -523,8 +571,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
-           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good
-           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1;
+           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good
+           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1;
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe2519_32WToZ; simpl @wire_digitsWToZ;
diff --git a/src/SpecificGen/GF2519_32Reflective/Common10_4Op.v b/src/SpecificGen/GF2519_32Reflective/Common10_4Op.v
new file mode 100644
index 000000000..cb762e1cb
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Common10_4Op.v
@@ -0,0 +1,115 @@
+Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr10_4Op_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_10_4op_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe2519_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe2519_32W (snd (fst (fst x0123456789))),
+                        eta_fe2519_32W (snd (fst x0123456789)),
+                        eta_fe2519_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe2519_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe2519_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe2519_32W (snd (fst (fst x0123456789))),
+                        eta_fe2519_32W (snd (fst x0123456789)),
+                        eta_fe2519_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe2519_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => op10_4_bounds_good bounds = true
+          | None => False
+          end)
+  : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9.
+  pose x0 as x0'.
+  pose x1 as x1'.
+  pose x2 as x2'.
+  pose x3 as x3'.
+  pose x4 as x4'.
+  pose x5 as x5'.
+  pose x6 as x6'.
+  pose x7 as x7'.
+  pose x8 as x8'.
+  pose x9 as x9'.
+  hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod.
+  specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v
index f28608623..43fc1be36 100644
--- a/src/SpecificGen/GF25519_32BoundedCommon.v
+++ b/src/SpecificGen/GF25519_32BoundedCommon.v
@@ -871,5 +871,21 @@ Notation i9top_correct_and_bounded k irop op
               = op (fe25519_32WToZ x0) (fe25519_32WToZ x1) (fe25519_32WToZ x2) (fe25519_32WToZ x3) (fe25519_32WToZ x4) (fe25519_32WToZ x5) (fe25519_32WToZ x6) (fe25519_32WToZ x7) (fe25519_32WToZ x8))
              * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
        (only parsing).
+Notation i10top_correct_and_bounded k irop op
+  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+          is_bounded (fe25519_32WToZ x0) = true
+          -> is_bounded (fe25519_32WToZ x1) = true
+          -> is_bounded (fe25519_32WToZ x2) = true
+          -> is_bounded (fe25519_32WToZ x3) = true
+          -> is_bounded (fe25519_32WToZ x4) = true
+          -> is_bounded (fe25519_32WToZ x5) = true
+          -> is_bounded (fe25519_32WToZ x6) = true
+          -> is_bounded (fe25519_32WToZ x7) = true
+          -> is_bounded (fe25519_32WToZ x8) = true
+          -> is_bounded (fe25519_32WToZ x9) = true
+          -> (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+              = op (fe25519_32WToZ x0) (fe25519_32WToZ x1) (fe25519_32WToZ x2) (fe25519_32WToZ x3) (fe25519_32WToZ x4) (fe25519_32WToZ x5) (fe25519_32WToZ x6) (fe25519_32WToZ x7) (fe25519_32WToZ x8) (fe25519_32WToZ x9))
+             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type)
+       (only parsing).
 
 Definition prefreeze := GF25519_32.prefreeze.
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index aad67f032..b1dbbd976 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -55,6 +55,7 @@ Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe25519_32 pack). Defined.
 Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1.
 Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4.
+Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4.
 Definition ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -72,6 +73,7 @@ Definition ExprBinOp : Type := Expr ExprBinOpT.
 Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
+Definition Expr10_4Op : Type := Expr Expr10_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
@@ -82,6 +84,7 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t
 Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT.
 Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT.
 Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT.
+Definition expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_4OpT.
 Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
 Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT.
 Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET.
@@ -137,6 +140,8 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_
   := Eval compute in Expr_nm_Op_bounds 4 1.
 Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
   := Eval compute in Expr_nm_Op_bounds 9 4.
+Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 10 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
 
@@ -162,6 +167,19 @@ Definition interp_9_4expr : Expr9_4Op
                             -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
                             -> Tuple.tuple SpecificGen.GF25519_32BoundedCommon.fe25519_32W 4
   := fun e => curry_9op_fe25519_32W (Interp (@WordW.interp_op) e).
+Definition interp_10_4expr : Expr10_4Op
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
+                            -> Tuple.tuple SpecificGen.GF25519_32BoundedCommon.fe25519_32W 4
+  := fun e => curry_10op_fe25519_32W (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -175,6 +193,8 @@ Notation unop_WireToFE_correct_and_bounded rop op
   := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
 Notation op9_4_correct_and_bounded rop op
   := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing).
+Notation op10_4_correct_and_bounded rop op
+  := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing).
 
 Ltac rexpr_cbv :=
   lazymatch goal with
@@ -200,6 +220,7 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25
 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe25519_32 op)) (only parsing).
 Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
 Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519_32 op)) (only parsing).
+Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe25519_32 op)) (only parsing).
 
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
@@ -394,6 +415,31 @@ Proof.
   let v := app_tuples (unop_args_to_bounded _ H0) v in
   exact v.
 Defined.
+Definition op10_args_to_bounded (x : fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W)
+           (H0 : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H1 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H2 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H3 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+           (H4 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+           (H5 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x)))))) = true)
+           (H6 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst x))))) = true)
+           (H7 : is_bounded (fe25519_32WToZ (snd (fst (fst x)))) = true)
+           (H8 : is_bounded (fe25519_32WToZ (snd (fst x))) = true)
+           (H9 : is_bounded (fe25519_32WToZ (snd x)) = true)
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT).
+Proof.
+  let v := constr:(unop_args_to_bounded _ H9) in
+  let v := app_tuples (unop_args_to_bounded _ H8) v in
+  let v := app_tuples (unop_args_to_bounded _ H7) v in
+  let v := app_tuples (unop_args_to_bounded _ H6) v in
+  let v := app_tuples (unop_args_to_bounded _ H5) v in
+  let v := app_tuples (unop_args_to_bounded _ H4) v in
+  let v := app_tuples (unop_args_to_bounded _ H3) v in
+  let v := app_tuples (unop_args_to_bounded _ H2) v in
+  let v := app_tuples (unop_args_to_bounded _ H1) v in
+  let v := app_tuples (unop_args_to_bounded _ H0) v in
+  exact v.
+Defined.
 
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
@@ -431,6 +477,8 @@ Proof.
 Defined.
 Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
 Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
+Definition op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_4OpT)) : bool.
+Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
 Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
   := fun x
@@ -469,12 +517,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Hbounds1 := fresh "Hbounds1" in
   let Hbounds2 := fresh "Hbounds2" in
   pose proof (proj2_sig ropZ_sig) as Heq;
-  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
-                    curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W
-                    curry_binop_fe25519_32 curry_unop_fe25519_32 curry_unop_wire_digits curry_9op_fe25519_32
-                    uncurry_binop_fe25519_32W uncurry_unop_fe25519_32W uncurry_unop_wire_digitsW uncurry_9op_fe25519_32W
-                    uncurry_binop_fe25519_32 uncurry_unop_fe25519_32 uncurry_unop_wire_digits uncurry_9op_fe25519_32
-                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
+  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr
+                    curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W curry_10op_fe25519_32W
+                    curry_binop_fe25519_32 curry_unop_fe25519_32 curry_unop_wire_digits curry_9op_fe25519_32 curry_10op_fe25519_32
+                    uncurry_binop_fe25519_32W uncurry_unop_fe25519_32W uncurry_unop_wire_digitsW uncurry_9op_fe25519_32W uncurry_10op_fe25519_32W
+                    uncurry_binop_fe25519_32 uncurry_unop_fe25519_32 uncurry_unop_wire_digits uncurry_9op_fe25519_32 uncurry_10op_fe25519_32
+                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT
                     interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
   cbv zeta in *;
   simpl @fe25519_32WToZ; simpl @wire_digitsWToZ;
@@ -505,7 +553,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   end;
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
-         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
+         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe25519_32WToZ ?x = _ /\ _ ]
@@ -523,8 +571,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
-           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good
-           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1;
+           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good
+           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1;
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe25519_32WToZ; simpl @wire_digitsWToZ;
diff --git a/src/SpecificGen/GF25519_32Reflective/Common10_4Op.v b/src/SpecificGen/GF25519_32Reflective/Common10_4Op.v
new file mode 100644
index 000000000..f94ed3446
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Common10_4Op.v
@@ -0,0 +1,115 @@
+Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr10_4Op_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_10_4op_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe25519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe25519_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe25519_32W (snd (fst (fst x0123456789))),
+                        eta_fe25519_32W (snd (fst x0123456789)),
+                        eta_fe25519_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe25519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe25519_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe25519_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe25519_32W (snd (fst (fst x0123456789))),
+                        eta_fe25519_32W (snd (fst x0123456789)),
+                        eta_fe25519_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe25519_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => op10_4_bounds_good bounds = true
+          | None => False
+          end)
+  : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9.
+  pose x0 as x0'.
+  pose x1 as x1'.
+  pose x2 as x2'.
+  pose x3 as x3'.
+  pose x4 as x4'.
+  pose x5 as x5'.
+  pose x6 as x6'.
+  pose x7 as x7'.
+  pose x8 as x8'.
+  pose x9 as x9'.
+  hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod.
+  specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v
index 519b90fac..90a107f9c 100644
--- a/src/SpecificGen/GF25519_64BoundedCommon.v
+++ b/src/SpecificGen/GF25519_64BoundedCommon.v
@@ -871,5 +871,21 @@ Notation i9top_correct_and_bounded k irop op
               = op (fe25519_64WToZ x0) (fe25519_64WToZ x1) (fe25519_64WToZ x2) (fe25519_64WToZ x3) (fe25519_64WToZ x4) (fe25519_64WToZ x5) (fe25519_64WToZ x6) (fe25519_64WToZ x7) (fe25519_64WToZ x8))
              * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_64WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
        (only parsing).
+Notation i10top_correct_and_bounded k irop op
+  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+          is_bounded (fe25519_64WToZ x0) = true
+          -> is_bounded (fe25519_64WToZ x1) = true
+          -> is_bounded (fe25519_64WToZ x2) = true
+          -> is_bounded (fe25519_64WToZ x3) = true
+          -> is_bounded (fe25519_64WToZ x4) = true
+          -> is_bounded (fe25519_64WToZ x5) = true
+          -> is_bounded (fe25519_64WToZ x6) = true
+          -> is_bounded (fe25519_64WToZ x7) = true
+          -> is_bounded (fe25519_64WToZ x8) = true
+          -> is_bounded (fe25519_64WToZ x9) = true
+          -> (Tuple.map (n:=k) fe25519_64WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+              = op (fe25519_64WToZ x0) (fe25519_64WToZ x1) (fe25519_64WToZ x2) (fe25519_64WToZ x3) (fe25519_64WToZ x4) (fe25519_64WToZ x5) (fe25519_64WToZ x6) (fe25519_64WToZ x7) (fe25519_64WToZ x8) (fe25519_64WToZ x9))
+             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_64WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type)
+       (only parsing).
 
 Definition prefreeze := GF25519_64.prefreeze.
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index f639aa0b6..eb90b67e5 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -55,6 +55,7 @@ Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe25519_64 pack). Defined.
 Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1.
 Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4.
+Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4.
 Definition ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -72,6 +73,7 @@ Definition ExprBinOp : Type := Expr ExprBinOpT.
 Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
+Definition Expr10_4Op : Type := Expr Expr10_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
@@ -82,6 +84,7 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t
 Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT.
 Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT.
 Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT.
+Definition expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_4OpT.
 Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
 Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT.
 Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET.
@@ -137,6 +140,8 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_
   := Eval compute in Expr_nm_Op_bounds 4 1.
 Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
   := Eval compute in Expr_nm_Op_bounds 9 4.
+Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 10 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
 
@@ -162,6 +167,19 @@ Definition interp_9_4expr : Expr9_4Op
                             -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
                             -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 4
   := fun e => curry_9op_fe25519_64W (Interp (@WordW.interp_op) e).
+Definition interp_10_4expr : Expr10_4Op
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
+                            -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 4
+  := fun e => curry_10op_fe25519_64W (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -175,6 +193,8 @@ Notation unop_WireToFE_correct_and_bounded rop op
   := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
 Notation op9_4_correct_and_bounded rop op
   := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing).
+Notation op10_4_correct_and_bounded rop op
+  := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing).
 
 Ltac rexpr_cbv :=
   lazymatch goal with
@@ -200,6 +220,7 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25
 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe25519_64 op)) (only parsing).
 Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
 Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519_64 op)) (only parsing).
+Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe25519_64 op)) (only parsing).
 
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
@@ -394,6 +415,31 @@ Proof.
   let v := app_tuples (unop_args_to_bounded _ H0) v in
   exact v.
 Defined.
+Definition op10_args_to_bounded (x : fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W)
+           (H0 : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H1 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H2 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H3 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+           (H4 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+           (H5 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x)))))) = true)
+           (H6 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst x))))) = true)
+           (H7 : is_bounded (fe25519_64WToZ (snd (fst (fst x)))) = true)
+           (H8 : is_bounded (fe25519_64WToZ (snd (fst x))) = true)
+           (H9 : is_bounded (fe25519_64WToZ (snd x)) = true)
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT).
+Proof.
+  let v := constr:(unop_args_to_bounded _ H9) in
+  let v := app_tuples (unop_args_to_bounded _ H8) v in
+  let v := app_tuples (unop_args_to_bounded _ H7) v in
+  let v := app_tuples (unop_args_to_bounded _ H6) v in
+  let v := app_tuples (unop_args_to_bounded _ H5) v in
+  let v := app_tuples (unop_args_to_bounded _ H4) v in
+  let v := app_tuples (unop_args_to_bounded _ H3) v in
+  let v := app_tuples (unop_args_to_bounded _ H2) v in
+  let v := app_tuples (unop_args_to_bounded _ H1) v in
+  let v := app_tuples (unop_args_to_bounded _ H0) v in
+  exact v.
+Defined.
 
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
@@ -431,6 +477,8 @@ Proof.
 Defined.
 Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
 Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
+Definition op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_4OpT)) : bool.
+Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
 Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
   := fun x
@@ -469,12 +517,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Hbounds1 := fresh "Hbounds1" in
   let Hbounds2 := fresh "Hbounds2" in
   pose proof (proj2_sig ropZ_sig) as Heq;
-  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
-                    curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W
-                    curry_binop_fe25519_64 curry_unop_fe25519_64 curry_unop_wire_digits curry_9op_fe25519_64
-                    uncurry_binop_fe25519_64W uncurry_unop_fe25519_64W uncurry_unop_wire_digitsW uncurry_9op_fe25519_64W
-                    uncurry_binop_fe25519_64 uncurry_unop_fe25519_64 uncurry_unop_wire_digits uncurry_9op_fe25519_64
-                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
+  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr
+                    curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W curry_10op_fe25519_64W
+                    curry_binop_fe25519_64 curry_unop_fe25519_64 curry_unop_wire_digits curry_9op_fe25519_64 curry_10op_fe25519_64
+                    uncurry_binop_fe25519_64W uncurry_unop_fe25519_64W uncurry_unop_wire_digitsW uncurry_9op_fe25519_64W uncurry_10op_fe25519_64W
+                    uncurry_binop_fe25519_64 uncurry_unop_fe25519_64 uncurry_unop_wire_digits uncurry_9op_fe25519_64 uncurry_10op_fe25519_64
+                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT
                     interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
   cbv zeta in *;
   simpl @fe25519_64WToZ; simpl @wire_digitsWToZ;
@@ -505,7 +553,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   end;
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
-         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
+         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe25519_64WToZ ?x = _ /\ _ ]
@@ -523,8 +571,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
-           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good
-           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1;
+           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good
+           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1;
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe25519_64WToZ; simpl @wire_digitsWToZ;
diff --git a/src/SpecificGen/GF25519_64Reflective/Common10_4Op.v b/src/SpecificGen/GF25519_64Reflective/Common10_4Op.v
new file mode 100644
index 000000000..6c4fde676
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Common10_4Op.v
@@ -0,0 +1,115 @@
+Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
+Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations128.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr10_4Op_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_10_4op_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe25519_64W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe25519_64W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe25519_64W (snd (fst (fst x0123456789))),
+                        eta_fe25519_64W (snd (fst x0123456789)),
+                        eta_fe25519_64W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe25519_64W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe25519_64W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe25519_64W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe25519_64W (snd (fst (fst x0123456789))),
+                        eta_fe25519_64W (snd (fst x0123456789)),
+                        eta_fe25519_64W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe25519_64WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => op10_4_bounds_good bounds = true
+          | None => False
+          end)
+  : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9.
+  pose x0 as x0'.
+  pose x1 as x1'.
+  pose x2 as x2'.
+  pose x3 as x3'.
+  pose x4 as x4'.
+  pose x5 as x5'.
+  pose x6 as x6'.
+  pose x7 as x7'.
+  pose x8 as x8'.
+  pose x9 as x9'.
+  hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod.
+  specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.128s) (successful) *)*)
diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v
index 5d9a7d209..15416433e 100644
--- a/src/SpecificGen/GF41417_32BoundedCommon.v
+++ b/src/SpecificGen/GF41417_32BoundedCommon.v
@@ -871,5 +871,21 @@ Notation i9top_correct_and_bounded k irop op
               = op (fe41417_32WToZ x0) (fe41417_32WToZ x1) (fe41417_32WToZ x2) (fe41417_32WToZ x3) (fe41417_32WToZ x4) (fe41417_32WToZ x5) (fe41417_32WToZ x6) (fe41417_32WToZ x7) (fe41417_32WToZ x8))
              * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe41417_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
        (only parsing).
+Notation i10top_correct_and_bounded k irop op
+  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+          is_bounded (fe41417_32WToZ x0) = true
+          -> is_bounded (fe41417_32WToZ x1) = true
+          -> is_bounded (fe41417_32WToZ x2) = true
+          -> is_bounded (fe41417_32WToZ x3) = true
+          -> is_bounded (fe41417_32WToZ x4) = true
+          -> is_bounded (fe41417_32WToZ x5) = true
+          -> is_bounded (fe41417_32WToZ x6) = true
+          -> is_bounded (fe41417_32WToZ x7) = true
+          -> is_bounded (fe41417_32WToZ x8) = true
+          -> is_bounded (fe41417_32WToZ x9) = true
+          -> (Tuple.map (n:=k) fe41417_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+              = op (fe41417_32WToZ x0) (fe41417_32WToZ x1) (fe41417_32WToZ x2) (fe41417_32WToZ x3) (fe41417_32WToZ x4) (fe41417_32WToZ x5) (fe41417_32WToZ x6) (fe41417_32WToZ x7) (fe41417_32WToZ x8) (fe41417_32WToZ x9))
+             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe41417_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type)
+       (only parsing).
 
 Definition prefreeze := GF41417_32.prefreeze.
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index 62d55b463..e63c29ce3 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -55,6 +55,7 @@ Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe41417_32 pack). Defined.
 Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1.
 Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4.
+Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4.
 Definition ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -72,6 +73,7 @@ Definition ExprBinOp : Type := Expr ExprBinOpT.
 Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
+Definition Expr10_4Op : Type := Expr Expr10_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
@@ -82,6 +84,7 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t
 Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT.
 Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT.
 Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT.
+Definition expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_4OpT.
 Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
 Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT.
 Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET.
@@ -137,6 +140,8 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_
   := Eval compute in Expr_nm_Op_bounds 4 1.
 Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
   := Eval compute in Expr_nm_Op_bounds 9 4.
+Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 10 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
 
@@ -162,6 +167,19 @@ Definition interp_9_4expr : Expr9_4Op
                             -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
                             -> Tuple.tuple SpecificGen.GF41417_32BoundedCommon.fe41417_32W 4
   := fun e => curry_9op_fe41417_32W (Interp (@WordW.interp_op) e).
+Definition interp_10_4expr : Expr10_4Op
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
+                            -> Tuple.tuple SpecificGen.GF41417_32BoundedCommon.fe41417_32W 4
+  := fun e => curry_10op_fe41417_32W (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -175,6 +193,8 @@ Notation unop_WireToFE_correct_and_bounded rop op
   := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
 Notation op9_4_correct_and_bounded rop op
   := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing).
+Notation op10_4_correct_and_bounded rop op
+  := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing).
 
 Ltac rexpr_cbv :=
   lazymatch goal with
@@ -200,6 +220,7 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe41
 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe41417_32 op)) (only parsing).
 Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
 Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe41417_32 op)) (only parsing).
+Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe41417_32 op)) (only parsing).
 
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
@@ -394,6 +415,31 @@ Proof.
   let v := app_tuples (unop_args_to_bounded _ H0) v in
   exact v.
 Defined.
+Definition op10_args_to_bounded (x : fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W)
+           (H0 : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H1 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H2 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H3 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+           (H4 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+           (H5 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x)))))) = true)
+           (H6 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst x))))) = true)
+           (H7 : is_bounded (fe41417_32WToZ (snd (fst (fst x)))) = true)
+           (H8 : is_bounded (fe41417_32WToZ (snd (fst x))) = true)
+           (H9 : is_bounded (fe41417_32WToZ (snd x)) = true)
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT).
+Proof.
+  let v := constr:(unop_args_to_bounded _ H9) in
+  let v := app_tuples (unop_args_to_bounded _ H8) v in
+  let v := app_tuples (unop_args_to_bounded _ H7) v in
+  let v := app_tuples (unop_args_to_bounded _ H6) v in
+  let v := app_tuples (unop_args_to_bounded _ H5) v in
+  let v := app_tuples (unop_args_to_bounded _ H4) v in
+  let v := app_tuples (unop_args_to_bounded _ H3) v in
+  let v := app_tuples (unop_args_to_bounded _ H2) v in
+  let v := app_tuples (unop_args_to_bounded _ H1) v in
+  let v := app_tuples (unop_args_to_bounded _ H0) v in
+  exact v.
+Defined.
 
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
@@ -431,6 +477,8 @@ Proof.
 Defined.
 Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
 Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
+Definition op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_4OpT)) : bool.
+Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
 Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
   := fun x
@@ -469,12 +517,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Hbounds1 := fresh "Hbounds1" in
   let Hbounds2 := fresh "Hbounds2" in
   pose proof (proj2_sig ropZ_sig) as Heq;
-  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
-                    curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W
-                    curry_binop_fe41417_32 curry_unop_fe41417_32 curry_unop_wire_digits curry_9op_fe41417_32
-                    uncurry_binop_fe41417_32W uncurry_unop_fe41417_32W uncurry_unop_wire_digitsW uncurry_9op_fe41417_32W
-                    uncurry_binop_fe41417_32 uncurry_unop_fe41417_32 uncurry_unop_wire_digits uncurry_9op_fe41417_32
-                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
+  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr
+                    curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W curry_10op_fe41417_32W
+                    curry_binop_fe41417_32 curry_unop_fe41417_32 curry_unop_wire_digits curry_9op_fe41417_32 curry_10op_fe41417_32
+                    uncurry_binop_fe41417_32W uncurry_unop_fe41417_32W uncurry_unop_wire_digitsW uncurry_9op_fe41417_32W uncurry_10op_fe41417_32W
+                    uncurry_binop_fe41417_32 uncurry_unop_fe41417_32 uncurry_unop_wire_digits uncurry_9op_fe41417_32 uncurry_10op_fe41417_32
+                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT
                     interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
   cbv zeta in *;
   simpl @fe41417_32WToZ; simpl @wire_digitsWToZ;
@@ -505,7 +553,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   end;
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
-         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
+         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe41417_32WToZ ?x = _ /\ _ ]
@@ -523,8 +571,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
-           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good
-           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1;
+           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good
+           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1;
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe41417_32WToZ; simpl @wire_digitsWToZ;
diff --git a/src/SpecificGen/GF41417_32Reflective/Common10_4Op.v b/src/SpecificGen/GF41417_32Reflective/Common10_4Op.v
new file mode 100644
index 000000000..46bb1211d
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Common10_4Op.v
@@ -0,0 +1,115 @@
+Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr10_4Op_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_10_4op_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe41417_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe41417_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe41417_32W (snd (fst (fst x0123456789))),
+                        eta_fe41417_32W (snd (fst x0123456789)),
+                        eta_fe41417_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe41417_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe41417_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe41417_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe41417_32W (snd (fst (fst x0123456789))),
+                        eta_fe41417_32W (snd (fst x0123456789)),
+                        eta_fe41417_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe41417_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => op10_4_bounds_good bounds = true
+          | None => False
+          end)
+  : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9.
+  pose x0 as x0'.
+  pose x1 as x1'.
+  pose x2 as x2'.
+  pose x3 as x3'.
+  pose x4 as x4'.
+  pose x5 as x5'.
+  pose x6 as x6'.
+  pose x7 as x7'.
+  pose x8 as x8'.
+  pose x9 as x9'.
+  hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod.
+  specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v
index 7ca03193f..82c577dfa 100644
--- a/src/SpecificGen/GF5211_32BoundedCommon.v
+++ b/src/SpecificGen/GF5211_32BoundedCommon.v
@@ -871,5 +871,21 @@ Notation i9top_correct_and_bounded k irop op
               = op (fe5211_32WToZ x0) (fe5211_32WToZ x1) (fe5211_32WToZ x2) (fe5211_32WToZ x3) (fe5211_32WToZ x4) (fe5211_32WToZ x5) (fe5211_32WToZ x6) (fe5211_32WToZ x7) (fe5211_32WToZ x8))
              * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
        (only parsing).
+Notation i10top_correct_and_bounded k irop op
+  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+          is_bounded (fe5211_32WToZ x0) = true
+          -> is_bounded (fe5211_32WToZ x1) = true
+          -> is_bounded (fe5211_32WToZ x2) = true
+          -> is_bounded (fe5211_32WToZ x3) = true
+          -> is_bounded (fe5211_32WToZ x4) = true
+          -> is_bounded (fe5211_32WToZ x5) = true
+          -> is_bounded (fe5211_32WToZ x6) = true
+          -> is_bounded (fe5211_32WToZ x7) = true
+          -> is_bounded (fe5211_32WToZ x8) = true
+          -> is_bounded (fe5211_32WToZ x9) = true
+          -> (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+              = op (fe5211_32WToZ x0) (fe5211_32WToZ x1) (fe5211_32WToZ x2) (fe5211_32WToZ x3) (fe5211_32WToZ x4) (fe5211_32WToZ x5) (fe5211_32WToZ x6) (fe5211_32WToZ x7) (fe5211_32WToZ x8) (fe5211_32WToZ x9))
+             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type)
+       (only parsing).
 
 Definition prefreeze := GF5211_32.prefreeze.
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index 977710173..6ef9d3c9f 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -55,6 +55,7 @@ Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe5211_32 pack). Defined.
 Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1.
 Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4.
+Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4.
 Definition ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -72,6 +73,7 @@ Definition ExprBinOp : Type := Expr ExprBinOpT.
 Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
+Definition Expr10_4Op : Type := Expr Expr10_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
@@ -82,6 +84,7 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t
 Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT.
 Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT.
 Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT.
+Definition expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_4OpT.
 Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
 Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT.
 Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET.
@@ -137,6 +140,8 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_
   := Eval compute in Expr_nm_Op_bounds 4 1.
 Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
   := Eval compute in Expr_nm_Op_bounds 9 4.
+Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 10 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
 
@@ -162,6 +167,19 @@ Definition interp_9_4expr : Expr9_4Op
                             -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
                             -> Tuple.tuple SpecificGen.GF5211_32BoundedCommon.fe5211_32W 4
   := fun e => curry_9op_fe5211_32W (Interp (@WordW.interp_op) e).
+Definition interp_10_4expr : Expr10_4Op
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
+                            -> Tuple.tuple SpecificGen.GF5211_32BoundedCommon.fe5211_32W 4
+  := fun e => curry_10op_fe5211_32W (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -175,6 +193,8 @@ Notation unop_WireToFE_correct_and_bounded rop op
   := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
 Notation op9_4_correct_and_bounded rop op
   := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing).
+Notation op10_4_correct_and_bounded rop op
+  := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing).
 
 Ltac rexpr_cbv :=
   lazymatch goal with
@@ -200,6 +220,7 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe52
 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe5211_32 op)) (only parsing).
 Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
 Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe5211_32 op)) (only parsing).
+Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe5211_32 op)) (only parsing).
 
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
@@ -394,6 +415,31 @@ Proof.
   let v := app_tuples (unop_args_to_bounded _ H0) v in
   exact v.
 Defined.
+Definition op10_args_to_bounded (x : fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W)
+           (H0 : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H1 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true)
+           (H2 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H3 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+           (H4 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+           (H5 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x)))))) = true)
+           (H6 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst x))))) = true)
+           (H7 : is_bounded (fe5211_32WToZ (snd (fst (fst x)))) = true)
+           (H8 : is_bounded (fe5211_32WToZ (snd (fst x))) = true)
+           (H9 : is_bounded (fe5211_32WToZ (snd x)) = true)
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT).
+Proof.
+  let v := constr:(unop_args_to_bounded _ H9) in
+  let v := app_tuples (unop_args_to_bounded _ H8) v in
+  let v := app_tuples (unop_args_to_bounded _ H7) v in
+  let v := app_tuples (unop_args_to_bounded _ H6) v in
+  let v := app_tuples (unop_args_to_bounded _ H5) v in
+  let v := app_tuples (unop_args_to_bounded _ H4) v in
+  let v := app_tuples (unop_args_to_bounded _ H3) v in
+  let v := app_tuples (unop_args_to_bounded _ H2) v in
+  let v := app_tuples (unop_args_to_bounded _ H1) v in
+  let v := app_tuples (unop_args_to_bounded _ H0) v in
+  exact v.
+Defined.
 
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
@@ -431,6 +477,8 @@ Proof.
 Defined.
 Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
 Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
+Definition op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_4OpT)) : bool.
+Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
 Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
   := fun x
@@ -469,12 +517,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Hbounds1 := fresh "Hbounds1" in
   let Hbounds2 := fresh "Hbounds2" in
   pose proof (proj2_sig ropZ_sig) as Heq;
-  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
-                    curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W
-                    curry_binop_fe5211_32 curry_unop_fe5211_32 curry_unop_wire_digits curry_9op_fe5211_32
-                    uncurry_binop_fe5211_32W uncurry_unop_fe5211_32W uncurry_unop_wire_digitsW uncurry_9op_fe5211_32W
-                    uncurry_binop_fe5211_32 uncurry_unop_fe5211_32 uncurry_unop_wire_digits uncurry_9op_fe5211_32
-                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
+  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr
+                    curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W curry_10op_fe5211_32W
+                    curry_binop_fe5211_32 curry_unop_fe5211_32 curry_unop_wire_digits curry_9op_fe5211_32 curry_10op_fe5211_32
+                    uncurry_binop_fe5211_32W uncurry_unop_fe5211_32W uncurry_unop_wire_digitsW uncurry_9op_fe5211_32W uncurry_10op_fe5211_32W
+                    uncurry_binop_fe5211_32 uncurry_unop_fe5211_32 uncurry_unop_wire_digits uncurry_9op_fe5211_32 uncurry_10op_fe5211_32
+                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT
                     interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
   cbv zeta in *;
   simpl @fe5211_32WToZ; simpl @wire_digitsWToZ;
@@ -505,7 +553,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   end;
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
-         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
+         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe5211_32WToZ ?x = _ /\ _ ]
@@ -523,8 +571,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
-           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good
-           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1;
+           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good
+           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1;
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe5211_32WToZ; simpl @wire_digitsWToZ;
diff --git a/src/SpecificGen/GF5211_32Reflective/Common10_4Op.v b/src/SpecificGen/GF5211_32Reflective/Common10_4Op.v
new file mode 100644
index 000000000..c595470e9
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Common10_4Op.v
@@ -0,0 +1,115 @@
+Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr10_4Op_correct_and_bounded
+      ropW op (ropZ_sig : rexpr_10_4op_sig op)
+      (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+      (H0 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe5211_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe5211_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe5211_32W (snd (fst (fst x0123456789))),
+                        eta_fe5211_32W (snd (fst x0123456789)),
+                        eta_fe5211_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+                                    (LiftOption.to' (Some args)))
+          with
+          | Some _ => True
+          | None => False
+          end)
+      (H1 : forall x0123456789
+                   (x0123456789
+                    := (eta_fe5211_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst (fst x0123456789)))))),
+                        eta_fe5211_32W (snd (fst (fst (fst (fst x0123456789))))),
+                        eta_fe5211_32W (snd (fst (fst (fst x0123456789)))),
+                        eta_fe5211_32W (snd (fst (fst x0123456789))),
+                        eta_fe5211_32W (snd (fst x0123456789)),
+                        eta_fe5211_32W (snd x0123456789)))
+                   (Hx0123456789
+                    : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst x0123456789))))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst (fst x0123456789)))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd (fst x0123456789))) = true
+                      /\ is_bounded (fe5211_32WToZ (snd x0123456789)) = true),
+          let (Hx0, Hx123456789) := (eta_and Hx0123456789) in
+          let (Hx1, Hx23456789) := (eta_and Hx123456789) in
+          let (Hx2, Hx3456789) := (eta_and Hx23456789) in
+          let (Hx3, Hx456789) := (eta_and Hx3456789) in
+          let (Hx4, Hx56789) := (eta_and Hx456789) in
+          let (Hx5, Hx6789) := (eta_and Hx56789) in
+          let (Hx6, Hx789) := (eta_and Hx6789) in
+          let (Hx7, Hx89) := (eta_and Hx789) in
+          let (Hx8, Hx9) := (eta_and Hx89) in
+          let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+          match LiftOption.of'
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+          with
+          | Some bounds => op10_4_bounds_good bounds = true
+          | None => False
+          end)
+  : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+  intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9.
+  pose x0 as x0'.
+  pose x1 as x1'.
+  pose x2 as x2'.
+  pose x3 as x3'.
+  pose x4 as x4'.
+  pose x5 as x5'.
+  pose x6 as x6'.
+  pose x7 as x7'.
+  pose x8 as x8'.
+  pose x9 as x9'.
+  hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod.
+  specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9')
+                 (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))).
+  Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)