Copy bounds, fix a typo

24 files changed, 1620 insertions, 162 deletions

diff --git a/src/SpecificGen/GF2213_32BoundedAddCoordinates.v b/src/SpecificGen/GF2213_32BoundedAddCoordinates.v
new file mode 100644
index 000000000..6079aadc9
--- /dev/null
+++ b/src/SpecificGen/GF2213_32BoundedAddCoordinates.v
@@ -0,0 +1,77 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.SpecificGen.GF2213_32.
+Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
+Require Import Crypto.SpecificGen.GF2213_32ReflectiveAddCoordinates.
+Require Import Crypto.Util.LetIn.
+Local Open Scope Z.
+
+Local Ltac bounded_t opW blem :=
+  apply blem; apply is_bounded_proj1_fe2213_32.
+
+Local Ltac define_binop f g opW blem :=
+  refine (exist_fe2213_32W (opW (proj1_fe2213_32W f) (proj1_fe2213_32W g)) _);
+  abstract bounded_t opW blem.
+
+Local Opaque Let_In.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64.
+Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
+Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2213_32W) : Tuple.tuple fe2213_32W 4
+  := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8.
+
+Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
+  change opW with (interp_rop);
+  rewrite pre_rewrite;
+  intros; apply rop_cb; assumption.
+
+Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates.
+Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed.
+
+Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem :=
+  refine (let ts := opW (proj1_fe2213_32W x0)
+                        (proj1_fe2213_32W x1)
+                        (proj1_fe2213_32W x2)
+                        (proj1_fe2213_32W x3)
+                        (proj1_fe2213_32W x4)
+                        (proj1_fe2213_32W x5)
+                        (proj1_fe2213_32W x6)
+                        (proj1_fe2213_32W x7)
+                        (proj1_fe2213_32W x8) in
+          HList.mapt exist_fe2213_32W (ts:=ts) _);
+  abstract (
+      rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe2213_32WToZ));
+      apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe2213_32
+    ).
+Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2213_32) : Tuple.tuple fe2213_32 4.
+Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined.
+
+Local Ltac op_correct_t op opW_correct_and_bounded :=
+  cbv [op];
+  rewrite ?HList.map_mapt;
+  lazymatch goal with
+  | [ |- context[proj1_fe2213_32 (exist_fe2213_32W _ _)] ]
+    => rewrite proj1_fe2213_32_exist_fe2213_32W || setoid_rewrite proj1_fe2213_32_exist_fe2213_32W
+  | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ]
+    => rewrite proj1_wire_digits_exist_wire_digitsW
+  | _ => idtac
+  end;
+  rewrite <- ?HList.map_is_mapt;
+  apply opW_correct_and_bounded;
+  lazymatch goal with
+  | [ |- is_bounded _ = true ]
+    => apply is_bounded_proj1_fe2213_32
+  | [ |- wire_digits_is_bounded _ = true ]
+    => apply is_bounded_proj1_wire_digits
+  end.
+
+Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2213_32)
+  : Tuple.map (n:=4) proj1_fe2213_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8)
+    = Reified.AddCoordinates.add_coordinates (proj1_fe2213_32 x0)
+                                             (proj1_fe2213_32 x1)
+                                             (proj1_fe2213_32 x2)
+                                             (proj1_fe2213_32 x3)
+                                             (proj1_fe2213_32 x4)
+                                             (proj1_fe2213_32 x5)
+                                             (proj1_fe2213_32 x6)
+                                             (proj1_fe2213_32 x7)
+                                             (proj1_fe2213_32 x8).
+Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed.
diff --git a/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v
new file mode 100644
index 000000000..58c297578
--- /dev/null
+++ b/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v
@@ -0,0 +1,67 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.SpecificGen.GF2213_32Bounded.
+Require Import Crypto.SpecificGen.GF2213_32ExtendedAddCoordinates.
+Require Import Crypto.SpecificGen.GF2213_32BoundedAddCoordinates.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+
+Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
+  : Tuple.fieldwise
+      (n:=4) GF2213_32BoundedCommon.eq
+      (@GF2213_32BoundedAddCoordinates.add_coordinates
+         twice_d P10 P11 P12 P13 P20 P21 P22 P23)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF2213_32BoundedCommon.fe2213_32
+         GF2213_32Bounded.add GF2213_32Bounded.sub GF2213_32Bounded.mul twice_d
+         (P10, P11, P12, P13) (P20, P21, P22, P23)).
+Proof.
+  unfold GF2213_32BoundedCommon.eq.
+  apply -> (fieldwise_map_iff (n:=4) eq GF2213_32BoundedCommon.proj1_fe2213_32 GF2213_32BoundedCommon.proj1_fe2213_32).
+  rewrite add_coordinates_correct.
+  cbv [AddCoordinates.add_coordinates].
+  setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
+  unfold edwards_extended_carry_add_coordinates.
+  match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
+  apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF2213_32BoundedCommon.proj1_fe2213_32).
+  apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
+    intros;
+    repeat match goal with
+           | [ |- context[add _ _] ]
+             => rewrite add_correct
+           | [ |- context[sub _ _] ]
+             => rewrite sub_correct
+           | [ |- context[mul _ _] ]
+             => rewrite mul_correct
+           | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
+           | [ |- and _ _ ] => split
+           | [ |- ?x = ?x ] => reflexivity
+           | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
+           | _ => congruence
+           end.
+Qed.
+
+Definition add_coordinates' twice_d P1 P2
+  := let '(P10, P11, P12, P13) := P1 in
+     let '(P20, P21, P22, P23) := P2 in
+     @GF2213_32BoundedAddCoordinates.add_coordinates
+       twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Definition add_coordinates twice_d P1 P2
+  := Eval cbv beta iota delta [GF2213_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in
+      let '(P10, P11, P12, P13) := P1 in
+      let '(P20, P21, P22, P23) := P2 in
+      @GF2213_32BoundedAddCoordinates.add_coordinates
+        twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Lemma add_coordinates_correct_full twice_d P1 P2
+  : Tuple.fieldwise
+      GF2213_32BoundedCommon.eq
+      (add_coordinates twice_d P1 P2)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF2213_32BoundedCommon.fe2213_32
+         GF2213_32Bounded.add GF2213_32Bounded.sub GF2213_32Bounded.mul twice_d P1 P2).
+Proof.
+  destruct_head' prod.
+  rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
+Qed.
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index ea4539963..52f488f2e 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
   make_type_from' T.
 
-Definition ExprBinOpT : type base_type.
-Proof. make_type_from (uncurry_binop_fe2213_32 carry_add). Defined.
-Definition ExprUnOpT : type base_type.
-Proof. make_type_from (uncurry_unop_fe2213_32 carry_opp). Defined.
+Definition fe2213_32T : flat_type base_type.
+Proof.
+  let T := (eval compute in GF2213_32.fe2213_32) in
+  let T := reify_flat_type T in
+  exact T.
+Defined.
+Definition Expr_n_OpT (count_out : nat) : flat_type base_type
+  := Eval cbv [Syntax.tuple Syntax.tuple' fe2213_32T] in
+      Syntax.tuple fe2213_32T count_out.
+Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
+  := match count_in with
+     | 0 => Expr_n_OpT count_out
+     | S n => SmartArrow base_type fe2213_32T (Expr_nm_OpT n count_out)
+     end.
+Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
+Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
 Definition ExprUnOpFEToZT : type base_type.
 Proof. make_type_from (uncurry_unop_fe2213_32 ge_modulus). Defined.
 Definition ExprUnOpWireToFET : type base_type.
 Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
 Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe2213_32 pack). Defined.
-Definition Expr4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply4_nd
-                                (B:=GF2213_32.fe2213_32)
-                                (@uncurry_unop_fe2213_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-Defined.
-Definition Expr9_4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply9_nd
-                                (B:=Tuple.tuple GF2213_32.fe2213_32 4)
-                                (@uncurry_unop_fe2213_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-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 ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type
 Definition ExprArgWireRevT : flat_type base_type
   := Eval compute in all_binders_for ExprUnOpWireToFET.
 Definition ExprZ : Type := Expr (Tbase TZ).
-Definition ExprBinOp : Type := Expr ExprBinOpT.
-Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out).
+Definition ExprBinOp : Type := Expr ExprBinOpT.
+Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
 Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
-Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
+Definition expr_nm_Op count_in count_out interp_base_type var : Type
+  := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out).
 Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT.
 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 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.
 Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT.
-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 exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT.
 Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT.
 Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT.
 Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT.
 
+Local Ltac bounds_from_list_cps ls :=
+  lazymatch (eval hnf in ls) with
+  | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra))
+  | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in
+                        constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
+  end.
+
+Local Ltac make_bounds_cps ls :=
+  let v := bounds_from_list_cps (List.rev ls) in
+  let v := (eval compute in v) in
+  pose v.
+
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
   | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
@@ -105,6 +116,18 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
+(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Proof.
+  refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
+         | 0 => tt
+         | S n => let v := Expr_nm_Op_bounds n count_out in
+                  _
+         end; simpl.
+  make_bounds_cps (Tuple.to_list _ bounds).
+  pose (p _ v).
+  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
+  exact p0.
+*)
 Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
 Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
diff --git a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v
new file mode 100644
index 000000000..3b95ae5c4
--- /dev/null
+++ b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v
@@ -0,0 +1,76 @@
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Export Crypto.SpecificGen.GF2213_32.
+Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
+Require Import Crypto.Reflection.Reify.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Reify.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.AddCoordinates.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
+Require Import Coq.Lists.List Crypto.Util.ListUtil.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Algebra.
+Import ListNotations.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Local Open Scope Z.
+
+Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW.
+
+Declare Reduction asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
+Ltac asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
+
+
+Time Definition interp_radd_coordinates : 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
+  := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates).
+(*Print interp_radd_coordinates.*)
+Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.
+
+Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates.
+Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed.
diff --git a/src/SpecificGen/GF2519_32BoundedAddCoordinates.v b/src/SpecificGen/GF2519_32BoundedAddCoordinates.v
new file mode 100644
index 000000000..68b97f000
--- /dev/null
+++ b/src/SpecificGen/GF2519_32BoundedAddCoordinates.v
@@ -0,0 +1,77 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.SpecificGen.GF2519_32.
+Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
+Require Import Crypto.SpecificGen.GF2519_32ReflectiveAddCoordinates.
+Require Import Crypto.Util.LetIn.
+Local Open Scope Z.
+
+Local Ltac bounded_t opW blem :=
+  apply blem; apply is_bounded_proj1_fe2519_32.
+
+Local Ltac define_binop f g opW blem :=
+  refine (exist_fe2519_32W (opW (proj1_fe2519_32W f) (proj1_fe2519_32W g)) _);
+  abstract bounded_t opW blem.
+
+Local Opaque Let_In.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64.
+Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
+Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2519_32W) : Tuple.tuple fe2519_32W 4
+  := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8.
+
+Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
+  change opW with (interp_rop);
+  rewrite pre_rewrite;
+  intros; apply rop_cb; assumption.
+
+Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates.
+Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed.
+
+Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem :=
+  refine (let ts := opW (proj1_fe2519_32W x0)
+                        (proj1_fe2519_32W x1)
+                        (proj1_fe2519_32W x2)
+                        (proj1_fe2519_32W x3)
+                        (proj1_fe2519_32W x4)
+                        (proj1_fe2519_32W x5)
+                        (proj1_fe2519_32W x6)
+                        (proj1_fe2519_32W x7)
+                        (proj1_fe2519_32W x8) in
+          HList.mapt exist_fe2519_32W (ts:=ts) _);
+  abstract (
+      rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe2519_32WToZ));
+      apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe2519_32
+    ).
+Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2519_32) : Tuple.tuple fe2519_32 4.
+Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined.
+
+Local Ltac op_correct_t op opW_correct_and_bounded :=
+  cbv [op];
+  rewrite ?HList.map_mapt;
+  lazymatch goal with
+  | [ |- context[proj1_fe2519_32 (exist_fe2519_32W _ _)] ]
+    => rewrite proj1_fe2519_32_exist_fe2519_32W || setoid_rewrite proj1_fe2519_32_exist_fe2519_32W
+  | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ]
+    => rewrite proj1_wire_digits_exist_wire_digitsW
+  | _ => idtac
+  end;
+  rewrite <- ?HList.map_is_mapt;
+  apply opW_correct_and_bounded;
+  lazymatch goal with
+  | [ |- is_bounded _ = true ]
+    => apply is_bounded_proj1_fe2519_32
+  | [ |- wire_digits_is_bounded _ = true ]
+    => apply is_bounded_proj1_wire_digits
+  end.
+
+Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2519_32)
+  : Tuple.map (n:=4) proj1_fe2519_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8)
+    = Reified.AddCoordinates.add_coordinates (proj1_fe2519_32 x0)
+                                             (proj1_fe2519_32 x1)
+                                             (proj1_fe2519_32 x2)
+                                             (proj1_fe2519_32 x3)
+                                             (proj1_fe2519_32 x4)
+                                             (proj1_fe2519_32 x5)
+                                             (proj1_fe2519_32 x6)
+                                             (proj1_fe2519_32 x7)
+                                             (proj1_fe2519_32 x8).
+Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed.
diff --git a/src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v
new file mode 100644
index 000000000..309a62324
--- /dev/null
+++ b/src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v
@@ -0,0 +1,67 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.SpecificGen.GF2519_32Bounded.
+Require Import Crypto.SpecificGen.GF2519_32ExtendedAddCoordinates.
+Require Import Crypto.SpecificGen.GF2519_32BoundedAddCoordinates.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+
+Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
+  : Tuple.fieldwise
+      (n:=4) GF2519_32BoundedCommon.eq
+      (@GF2519_32BoundedAddCoordinates.add_coordinates
+         twice_d P10 P11 P12 P13 P20 P21 P22 P23)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF2519_32BoundedCommon.fe2519_32
+         GF2519_32Bounded.add GF2519_32Bounded.sub GF2519_32Bounded.mul twice_d
+         (P10, P11, P12, P13) (P20, P21, P22, P23)).
+Proof.
+  unfold GF2519_32BoundedCommon.eq.
+  apply -> (fieldwise_map_iff (n:=4) eq GF2519_32BoundedCommon.proj1_fe2519_32 GF2519_32BoundedCommon.proj1_fe2519_32).
+  rewrite add_coordinates_correct.
+  cbv [AddCoordinates.add_coordinates].
+  setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
+  unfold edwards_extended_carry_add_coordinates.
+  match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
+  apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF2519_32BoundedCommon.proj1_fe2519_32).
+  apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
+    intros;
+    repeat match goal with
+           | [ |- context[add _ _] ]
+             => rewrite add_correct
+           | [ |- context[sub _ _] ]
+             => rewrite sub_correct
+           | [ |- context[mul _ _] ]
+             => rewrite mul_correct
+           | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
+           | [ |- and _ _ ] => split
+           | [ |- ?x = ?x ] => reflexivity
+           | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
+           | _ => congruence
+           end.
+Qed.
+
+Definition add_coordinates' twice_d P1 P2
+  := let '(P10, P11, P12, P13) := P1 in
+     let '(P20, P21, P22, P23) := P2 in
+     @GF2519_32BoundedAddCoordinates.add_coordinates
+       twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Definition add_coordinates twice_d P1 P2
+  := Eval cbv beta iota delta [GF2519_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in
+      let '(P10, P11, P12, P13) := P1 in
+      let '(P20, P21, P22, P23) := P2 in
+      @GF2519_32BoundedAddCoordinates.add_coordinates
+        twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Lemma add_coordinates_correct_full twice_d P1 P2
+  : Tuple.fieldwise
+      GF2519_32BoundedCommon.eq
+      (add_coordinates twice_d P1 P2)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF2519_32BoundedCommon.fe2519_32
+         GF2519_32Bounded.add GF2519_32Bounded.sub GF2519_32Bounded.mul twice_d P1 P2).
+Proof.
+  destruct_head' prod.
+  rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
+Qed.
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index d23856c4b..4be893f8f 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
   make_type_from' T.
 
-Definition ExprBinOpT : type base_type.
-Proof. make_type_from (uncurry_binop_fe2519_32 carry_add). Defined.
-Definition ExprUnOpT : type base_type.
-Proof. make_type_from (uncurry_unop_fe2519_32 carry_opp). Defined.
+Definition fe2519_32T : flat_type base_type.
+Proof.
+  let T := (eval compute in GF2519_32.fe2519_32) in
+  let T := reify_flat_type T in
+  exact T.
+Defined.
+Definition Expr_n_OpT (count_out : nat) : flat_type base_type
+  := Eval cbv [Syntax.tuple Syntax.tuple' fe2519_32T] in
+      Syntax.tuple fe2519_32T count_out.
+Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
+  := match count_in with
+     | 0 => Expr_n_OpT count_out
+     | S n => SmartArrow base_type fe2519_32T (Expr_nm_OpT n count_out)
+     end.
+Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
+Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
 Definition ExprUnOpFEToZT : type base_type.
 Proof. make_type_from (uncurry_unop_fe2519_32 ge_modulus). Defined.
 Definition ExprUnOpWireToFET : type base_type.
 Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
 Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe2519_32 pack). Defined.
-Definition Expr4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply4_nd
-                                (B:=GF2519_32.fe2519_32)
-                                (@uncurry_unop_fe2519_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-Defined.
-Definition Expr9_4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply9_nd
-                                (B:=Tuple.tuple GF2519_32.fe2519_32 4)
-                                (@uncurry_unop_fe2519_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-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 ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type
 Definition ExprArgWireRevT : flat_type base_type
   := Eval compute in all_binders_for ExprUnOpWireToFET.
 Definition ExprZ : Type := Expr (Tbase TZ).
-Definition ExprBinOp : Type := Expr ExprBinOpT.
-Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out).
+Definition ExprBinOp : Type := Expr ExprBinOpT.
+Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
 Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
-Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
+Definition expr_nm_Op count_in count_out interp_base_type var : Type
+  := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out).
 Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT.
 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 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.
 Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT.
-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 exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT.
 Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT.
 Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT.
 Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT.
 
+Local Ltac bounds_from_list_cps ls :=
+  lazymatch (eval hnf in ls) with
+  | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra))
+  | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in
+                        constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
+  end.
+
+Local Ltac make_bounds_cps ls :=
+  let v := bounds_from_list_cps (List.rev ls) in
+  let v := (eval compute in v) in
+  pose v.
+
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
   | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
@@ -105,6 +116,18 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
+(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Proof.
+  refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
+         | 0 => tt
+         | S n => let v := Expr_nm_Op_bounds n count_out in
+                  _
+         end; simpl.
+  make_bounds_cps (Tuple.to_list _ bounds).
+  pose (p _ v).
+  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
+  exact p0.
+*)
 Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
 Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
diff --git a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v
new file mode 100644
index 000000000..a400a893a
--- /dev/null
+++ b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v
@@ -0,0 +1,76 @@
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Export Crypto.SpecificGen.GF2519_32.
+Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
+Require Import Crypto.Reflection.Reify.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Reify.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.AddCoordinates.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
+Require Import Coq.Lists.List Crypto.Util.ListUtil.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Algebra.
+Import ListNotations.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Local Open Scope Z.
+
+Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW.
+
+Declare Reduction asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
+Ltac asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
+
+
+Time Definition interp_radd_coordinates : 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
+  := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates).
+(*Print interp_radd_coordinates.*)
+Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.
+
+Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates.
+Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed.
diff --git a/src/SpecificGen/GF25519_32BoundedAddCoordinates.v b/src/SpecificGen/GF25519_32BoundedAddCoordinates.v
new file mode 100644
index 000000000..5a1fd12b3
--- /dev/null
+++ b/src/SpecificGen/GF25519_32BoundedAddCoordinates.v
@@ -0,0 +1,77 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.SpecificGen.GF25519_32.
+Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
+Require Import Crypto.SpecificGen.GF25519_32ReflectiveAddCoordinates.
+Require Import Crypto.Util.LetIn.
+Local Open Scope Z.
+
+Local Ltac bounded_t opW blem :=
+  apply blem; apply is_bounded_proj1_fe25519_32.
+
+Local Ltac define_binop f g opW blem :=
+  refine (exist_fe25519_32W (opW (proj1_fe25519_32W f) (proj1_fe25519_32W g)) _);
+  abstract bounded_t opW blem.
+
+Local Opaque Let_In.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64.
+Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
+Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32W) : Tuple.tuple fe25519_32W 4
+  := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8.
+
+Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
+  change opW with (interp_rop);
+  rewrite pre_rewrite;
+  intros; apply rop_cb; assumption.
+
+Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates.
+Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed.
+
+Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem :=
+  refine (let ts := opW (proj1_fe25519_32W x0)
+                        (proj1_fe25519_32W x1)
+                        (proj1_fe25519_32W x2)
+                        (proj1_fe25519_32W x3)
+                        (proj1_fe25519_32W x4)
+                        (proj1_fe25519_32W x5)
+                        (proj1_fe25519_32W x6)
+                        (proj1_fe25519_32W x7)
+                        (proj1_fe25519_32W x8) in
+          HList.mapt exist_fe25519_32W (ts:=ts) _);
+  abstract (
+      rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe25519_32WToZ));
+      apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe25519_32
+    ).
+Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32) : Tuple.tuple fe25519_32 4.
+Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined.
+
+Local Ltac op_correct_t op opW_correct_and_bounded :=
+  cbv [op];
+  rewrite ?HList.map_mapt;
+  lazymatch goal with
+  | [ |- context[proj1_fe25519_32 (exist_fe25519_32W _ _)] ]
+    => rewrite proj1_fe25519_32_exist_fe25519_32W || setoid_rewrite proj1_fe25519_32_exist_fe25519_32W
+  | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ]
+    => rewrite proj1_wire_digits_exist_wire_digitsW
+  | _ => idtac
+  end;
+  rewrite <- ?HList.map_is_mapt;
+  apply opW_correct_and_bounded;
+  lazymatch goal with
+  | [ |- is_bounded _ = true ]
+    => apply is_bounded_proj1_fe25519_32
+  | [ |- wire_digits_is_bounded _ = true ]
+    => apply is_bounded_proj1_wire_digits
+  end.
+
+Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32)
+  : Tuple.map (n:=4) proj1_fe25519_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8)
+    = Reified.AddCoordinates.add_coordinates (proj1_fe25519_32 x0)
+                                             (proj1_fe25519_32 x1)
+                                             (proj1_fe25519_32 x2)
+                                             (proj1_fe25519_32 x3)
+                                             (proj1_fe25519_32 x4)
+                                             (proj1_fe25519_32 x5)
+                                             (proj1_fe25519_32 x6)
+                                             (proj1_fe25519_32 x7)
+                                             (proj1_fe25519_32 x8).
+Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed.
diff --git a/src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v
new file mode 100644
index 000000000..c23bcea4a
--- /dev/null
+++ b/src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v
@@ -0,0 +1,67 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.SpecificGen.GF25519_32Bounded.
+Require Import Crypto.SpecificGen.GF25519_32ExtendedAddCoordinates.
+Require Import Crypto.SpecificGen.GF25519_32BoundedAddCoordinates.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+
+Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
+  : Tuple.fieldwise
+      (n:=4) GF25519_32BoundedCommon.eq
+      (@GF25519_32BoundedAddCoordinates.add_coordinates
+         twice_d P10 P11 P12 P13 P20 P21 P22 P23)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF25519_32BoundedCommon.fe25519_32
+         GF25519_32Bounded.add GF25519_32Bounded.sub GF25519_32Bounded.mul twice_d
+         (P10, P11, P12, P13) (P20, P21, P22, P23)).
+Proof.
+  unfold GF25519_32BoundedCommon.eq.
+  apply -> (fieldwise_map_iff (n:=4) eq GF25519_32BoundedCommon.proj1_fe25519_32 GF25519_32BoundedCommon.proj1_fe25519_32).
+  rewrite add_coordinates_correct.
+  cbv [AddCoordinates.add_coordinates].
+  setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
+  unfold edwards_extended_carry_add_coordinates.
+  match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
+  apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF25519_32BoundedCommon.proj1_fe25519_32).
+  apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
+    intros;
+    repeat match goal with
+           | [ |- context[add _ _] ]
+             => rewrite add_correct
+           | [ |- context[sub _ _] ]
+             => rewrite sub_correct
+           | [ |- context[mul _ _] ]
+             => rewrite mul_correct
+           | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
+           | [ |- and _ _ ] => split
+           | [ |- ?x = ?x ] => reflexivity
+           | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
+           | _ => congruence
+           end.
+Qed.
+
+Definition add_coordinates' twice_d P1 P2
+  := let '(P10, P11, P12, P13) := P1 in
+     let '(P20, P21, P22, P23) := P2 in
+     @GF25519_32BoundedAddCoordinates.add_coordinates
+       twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Definition add_coordinates twice_d P1 P2
+  := Eval cbv beta iota delta [GF25519_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in
+      let '(P10, P11, P12, P13) := P1 in
+      let '(P20, P21, P22, P23) := P2 in
+      @GF25519_32BoundedAddCoordinates.add_coordinates
+        twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Lemma add_coordinates_correct_full twice_d P1 P2
+  : Tuple.fieldwise
+      GF25519_32BoundedCommon.eq
+      (add_coordinates twice_d P1 P2)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF25519_32BoundedCommon.fe25519_32
+         GF25519_32Bounded.add GF25519_32Bounded.sub GF25519_32Bounded.mul twice_d P1 P2).
+Proof.
+  destruct_head' prod.
+  rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
+Qed.
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index 4801c64fd..3389f908a 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
   make_type_from' T.
 
-Definition ExprBinOpT : type base_type.
-Proof. make_type_from (uncurry_binop_fe25519_32 carry_add). Defined.
-Definition ExprUnOpT : type base_type.
-Proof. make_type_from (uncurry_unop_fe25519_32 carry_opp). Defined.
+Definition fe25519_32T : flat_type base_type.
+Proof.
+  let T := (eval compute in GF25519_32.fe25519_32) in
+  let T := reify_flat_type T in
+  exact T.
+Defined.
+Definition Expr_n_OpT (count_out : nat) : flat_type base_type
+  := Eval cbv [Syntax.tuple Syntax.tuple' fe25519_32T] in
+      Syntax.tuple fe25519_32T count_out.
+Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
+  := match count_in with
+     | 0 => Expr_n_OpT count_out
+     | S n => SmartArrow base_type fe25519_32T (Expr_nm_OpT n count_out)
+     end.
+Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
+Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
 Definition ExprUnOpFEToZT : type base_type.
 Proof. make_type_from (uncurry_unop_fe25519_32 ge_modulus). Defined.
 Definition ExprUnOpWireToFET : type base_type.
 Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
 Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe25519_32 pack). Defined.
-Definition Expr4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply4_nd
-                                (B:=GF25519_32.fe25519_32)
-                                (@uncurry_unop_fe25519_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-Defined.
-Definition Expr9_4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply9_nd
-                                (B:=Tuple.tuple GF25519_32.fe25519_32 4)
-                                (@uncurry_unop_fe25519_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-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 ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type
 Definition ExprArgWireRevT : flat_type base_type
   := Eval compute in all_binders_for ExprUnOpWireToFET.
 Definition ExprZ : Type := Expr (Tbase TZ).
-Definition ExprBinOp : Type := Expr ExprBinOpT.
-Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out).
+Definition ExprBinOp : Type := Expr ExprBinOpT.
+Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
 Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
-Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
+Definition expr_nm_Op count_in count_out interp_base_type var : Type
+  := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out).
 Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT.
 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 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.
 Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT.
-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 exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT.
 Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT.
 Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT.
 Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT.
 
+Local Ltac bounds_from_list_cps ls :=
+  lazymatch (eval hnf in ls) with
+  | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra))
+  | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in
+                        constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
+  end.
+
+Local Ltac make_bounds_cps ls :=
+  let v := bounds_from_list_cps (List.rev ls) in
+  let v := (eval compute in v) in
+  pose v.
+
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
   | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
@@ -105,6 +116,18 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
+(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Proof.
+  refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
+         | 0 => tt
+         | S n => let v := Expr_nm_Op_bounds n count_out in
+                  _
+         end; simpl.
+  make_bounds_cps (Tuple.to_list _ bounds).
+  pose (p _ v).
+  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
+  exact p0.
+*)
 Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
 Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
diff --git a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v
new file mode 100644
index 000000000..b13c07f44
--- /dev/null
+++ b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v
@@ -0,0 +1,76 @@
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Export Crypto.SpecificGen.GF25519_32.
+Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
+Require Import Crypto.Reflection.Reify.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Reify.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.AddCoordinates.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
+Require Import Coq.Lists.List Crypto.Util.ListUtil.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Algebra.
+Import ListNotations.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Local Open Scope Z.
+
+Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW.
+
+Declare Reduction asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
+Ltac asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
+
+
+Time Definition interp_radd_coordinates : 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
+  := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates).
+(*Print interp_radd_coordinates.*)
+Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.
+
+Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates.
+Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed.
diff --git a/src/SpecificGen/GF25519_64BoundedAddCoordinates.v b/src/SpecificGen/GF25519_64BoundedAddCoordinates.v
new file mode 100644
index 000000000..a1ba335c8
--- /dev/null
+++ b/src/SpecificGen/GF25519_64BoundedAddCoordinates.v
@@ -0,0 +1,77 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.SpecificGen.GF25519_64.
+Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
+Require Import Crypto.SpecificGen.GF25519_64ReflectiveAddCoordinates.
+Require Import Crypto.Util.LetIn.
+Local Open Scope Z.
+
+Local Ltac bounded_t opW blem :=
+  apply blem; apply is_bounded_proj1_fe25519_64.
+
+Local Ltac define_binop f g opW blem :=
+  refine (exist_fe25519_64W (opW (proj1_fe25519_64W f) (proj1_fe25519_64W g)) _);
+  abstract bounded_t opW blem.
+
+Local Opaque Let_In.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord128.
+Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
+Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64W) : Tuple.tuple fe25519_64W 4
+  := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8.
+
+Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
+  change opW with (interp_rop);
+  rewrite pre_rewrite;
+  intros; apply rop_cb; assumption.
+
+Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates.
+Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed.
+
+Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem :=
+  refine (let ts := opW (proj1_fe25519_64W x0)
+                        (proj1_fe25519_64W x1)
+                        (proj1_fe25519_64W x2)
+                        (proj1_fe25519_64W x3)
+                        (proj1_fe25519_64W x4)
+                        (proj1_fe25519_64W x5)
+                        (proj1_fe25519_64W x6)
+                        (proj1_fe25519_64W x7)
+                        (proj1_fe25519_64W x8) in
+          HList.mapt exist_fe25519_64W (ts:=ts) _);
+  abstract (
+      rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe25519_64WToZ));
+      apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe25519_64
+    ).
+Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64) : Tuple.tuple fe25519_64 4.
+Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined.
+
+Local Ltac op_correct_t op opW_correct_and_bounded :=
+  cbv [op];
+  rewrite ?HList.map_mapt;
+  lazymatch goal with
+  | [ |- context[proj1_fe25519_64 (exist_fe25519_64W _ _)] ]
+    => rewrite proj1_fe25519_64_exist_fe25519_64W || setoid_rewrite proj1_fe25519_64_exist_fe25519_64W
+  | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ]
+    => rewrite proj1_wire_digits_exist_wire_digitsW
+  | _ => idtac
+  end;
+  rewrite <- ?HList.map_is_mapt;
+  apply opW_correct_and_bounded;
+  lazymatch goal with
+  | [ |- is_bounded _ = true ]
+    => apply is_bounded_proj1_fe25519_64
+  | [ |- wire_digits_is_bounded _ = true ]
+    => apply is_bounded_proj1_wire_digits
+  end.
+
+Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64)
+  : Tuple.map (n:=4) proj1_fe25519_64 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8)
+    = Reified.AddCoordinates.add_coordinates (proj1_fe25519_64 x0)
+                                             (proj1_fe25519_64 x1)
+                                             (proj1_fe25519_64 x2)
+                                             (proj1_fe25519_64 x3)
+                                             (proj1_fe25519_64 x4)
+                                             (proj1_fe25519_64 x5)
+                                             (proj1_fe25519_64 x6)
+                                             (proj1_fe25519_64 x7)
+                                             (proj1_fe25519_64 x8).
+Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed.
diff --git a/src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v
new file mode 100644
index 000000000..d5e92dfac
--- /dev/null
+++ b/src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v
@@ -0,0 +1,67 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.SpecificGen.GF25519_64Bounded.
+Require Import Crypto.SpecificGen.GF25519_64ExtendedAddCoordinates.
+Require Import Crypto.SpecificGen.GF25519_64BoundedAddCoordinates.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+
+Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
+  : Tuple.fieldwise
+      (n:=4) GF25519_64BoundedCommon.eq
+      (@GF25519_64BoundedAddCoordinates.add_coordinates
+         twice_d P10 P11 P12 P13 P20 P21 P22 P23)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF25519_64BoundedCommon.fe25519_64
+         GF25519_64Bounded.add GF25519_64Bounded.sub GF25519_64Bounded.mul twice_d
+         (P10, P11, P12, P13) (P20, P21, P22, P23)).
+Proof.
+  unfold GF25519_64BoundedCommon.eq.
+  apply -> (fieldwise_map_iff (n:=4) eq GF25519_64BoundedCommon.proj1_fe25519_64 GF25519_64BoundedCommon.proj1_fe25519_64).
+  rewrite add_coordinates_correct.
+  cbv [AddCoordinates.add_coordinates].
+  setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
+  unfold edwards_extended_carry_add_coordinates.
+  match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
+  apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF25519_64BoundedCommon.proj1_fe25519_64).
+  apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
+    intros;
+    repeat match goal with
+           | [ |- context[add _ _] ]
+             => rewrite add_correct
+           | [ |- context[sub _ _] ]
+             => rewrite sub_correct
+           | [ |- context[mul _ _] ]
+             => rewrite mul_correct
+           | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
+           | [ |- and _ _ ] => split
+           | [ |- ?x = ?x ] => reflexivity
+           | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
+           | _ => congruence
+           end.
+Qed.
+
+Definition add_coordinates' twice_d P1 P2
+  := let '(P10, P11, P12, P13) := P1 in
+     let '(P20, P21, P22, P23) := P2 in
+     @GF25519_64BoundedAddCoordinates.add_coordinates
+       twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Definition add_coordinates twice_d P1 P2
+  := Eval cbv beta iota delta [GF25519_64BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in
+      let '(P10, P11, P12, P13) := P1 in
+      let '(P20, P21, P22, P23) := P2 in
+      @GF25519_64BoundedAddCoordinates.add_coordinates
+        twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Lemma add_coordinates_correct_full twice_d P1 P2
+  : Tuple.fieldwise
+      GF25519_64BoundedCommon.eq
+      (add_coordinates twice_d P1 P2)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF25519_64BoundedCommon.fe25519_64
+         GF25519_64Bounded.add GF25519_64Bounded.sub GF25519_64Bounded.mul twice_d P1 P2).
+Proof.
+  destruct_head' prod.
+  rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
+Qed.
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index 58764461e..bbdccaf26 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
   make_type_from' T.
 
-Definition ExprBinOpT : type base_type.
-Proof. make_type_from (uncurry_binop_fe25519_64 carry_add). Defined.
-Definition ExprUnOpT : type base_type.
-Proof. make_type_from (uncurry_unop_fe25519_64 carry_opp). Defined.
+Definition fe25519_64T : flat_type base_type.
+Proof.
+  let T := (eval compute in GF25519_64.fe25519_64) in
+  let T := reify_flat_type T in
+  exact T.
+Defined.
+Definition Expr_n_OpT (count_out : nat) : flat_type base_type
+  := Eval cbv [Syntax.tuple Syntax.tuple' fe25519_64T] in
+      Syntax.tuple fe25519_64T count_out.
+Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
+  := match count_in with
+     | 0 => Expr_n_OpT count_out
+     | S n => SmartArrow base_type fe25519_64T (Expr_nm_OpT n count_out)
+     end.
+Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
+Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
 Definition ExprUnOpFEToZT : type base_type.
 Proof. make_type_from (uncurry_unop_fe25519_64 ge_modulus). Defined.
 Definition ExprUnOpWireToFET : type base_type.
 Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
 Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe25519_64 pack). Defined.
-Definition Expr4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply4_nd
-                                (B:=GF25519_64.fe25519_64)
-                                (@uncurry_unop_fe25519_64)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-Defined.
-Definition Expr9_4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply9_nd
-                                (B:=Tuple.tuple GF25519_64.fe25519_64 4)
-                                (@uncurry_unop_fe25519_64)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-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 ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type
 Definition ExprArgWireRevT : flat_type base_type
   := Eval compute in all_binders_for ExprUnOpWireToFET.
 Definition ExprZ : Type := Expr (Tbase TZ).
-Definition ExprBinOp : Type := Expr ExprBinOpT.
-Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out).
+Definition ExprBinOp : Type := Expr ExprBinOpT.
+Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
 Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
-Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
+Definition expr_nm_Op count_in count_out interp_base_type var : Type
+  := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out).
 Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT.
 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 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.
 Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT.
-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 exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT.
 Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT.
 Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT.
 Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT.
 
+Local Ltac bounds_from_list_cps ls :=
+  lazymatch (eval hnf in ls) with
+  | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra))
+  | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in
+                        constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
+  end.
+
+Local Ltac make_bounds_cps ls :=
+  let v := bounds_from_list_cps (List.rev ls) in
+  let v := (eval compute in v) in
+  pose v.
+
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
   | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
@@ -105,6 +116,18 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
+(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Proof.
+  refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
+         | 0 => tt
+         | S n => let v := Expr_nm_Op_bounds n count_out in
+                  _
+         end; simpl.
+  make_bounds_cps (Tuple.to_list _ bounds).
+  pose (p _ v).
+  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
+  exact p0.
+*)
 Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
 Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
diff --git a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v
new file mode 100644
index 000000000..e9067cee8
--- /dev/null
+++ b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v
@@ -0,0 +1,76 @@
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Export Crypto.SpecificGen.GF25519_64.
+Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
+Require Import Crypto.Reflection.Reify.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Reflection.Z.Interpretations128.
+Require Crypto.Reflection.Z.Interpretations128.Relations.
+Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Reify.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Common.
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.AddCoordinates.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
+Require Import Coq.Lists.List Crypto.Util.ListUtil.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Algebra.
+Import ListNotations.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Local Open Scope Z.
+
+Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW.
+
+Declare Reduction asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize
+            Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
+Ltac asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
+
+
+Time Definition interp_radd_coordinates : 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
+  := Eval asm_interp_add_coordinates in interp_9_4expr (rword128ize radd_coordinates).
+(*Print interp_radd_coordinates.*)
+Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.
+
+Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates.
+Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed.
diff --git a/src/SpecificGen/GF41417_32BoundedAddCoordinates.v b/src/SpecificGen/GF41417_32BoundedAddCoordinates.v
new file mode 100644
index 000000000..e7d5842ce
--- /dev/null
+++ b/src/SpecificGen/GF41417_32BoundedAddCoordinates.v
@@ -0,0 +1,77 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.SpecificGen.GF41417_32.
+Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
+Require Import Crypto.SpecificGen.GF41417_32ReflectiveAddCoordinates.
+Require Import Crypto.Util.LetIn.
+Local Open Scope Z.
+
+Local Ltac bounded_t opW blem :=
+  apply blem; apply is_bounded_proj1_fe41417_32.
+
+Local Ltac define_binop f g opW blem :=
+  refine (exist_fe41417_32W (opW (proj1_fe41417_32W f) (proj1_fe41417_32W g)) _);
+  abstract bounded_t opW blem.
+
+Local Opaque Let_In.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64.
+Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
+Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe41417_32W) : Tuple.tuple fe41417_32W 4
+  := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8.
+
+Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
+  change opW with (interp_rop);
+  rewrite pre_rewrite;
+  intros; apply rop_cb; assumption.
+
+Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates.
+Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed.
+
+Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem :=
+  refine (let ts := opW (proj1_fe41417_32W x0)
+                        (proj1_fe41417_32W x1)
+                        (proj1_fe41417_32W x2)
+                        (proj1_fe41417_32W x3)
+                        (proj1_fe41417_32W x4)
+                        (proj1_fe41417_32W x5)
+                        (proj1_fe41417_32W x6)
+                        (proj1_fe41417_32W x7)
+                        (proj1_fe41417_32W x8) in
+          HList.mapt exist_fe41417_32W (ts:=ts) _);
+  abstract (
+      rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe41417_32WToZ));
+      apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe41417_32
+    ).
+Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe41417_32) : Tuple.tuple fe41417_32 4.
+Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined.
+
+Local Ltac op_correct_t op opW_correct_and_bounded :=
+  cbv [op];
+  rewrite ?HList.map_mapt;
+  lazymatch goal with
+  | [ |- context[proj1_fe41417_32 (exist_fe41417_32W _ _)] ]
+    => rewrite proj1_fe41417_32_exist_fe41417_32W || setoid_rewrite proj1_fe41417_32_exist_fe41417_32W
+  | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ]
+    => rewrite proj1_wire_digits_exist_wire_digitsW
+  | _ => idtac
+  end;
+  rewrite <- ?HList.map_is_mapt;
+  apply opW_correct_and_bounded;
+  lazymatch goal with
+  | [ |- is_bounded _ = true ]
+    => apply is_bounded_proj1_fe41417_32
+  | [ |- wire_digits_is_bounded _ = true ]
+    => apply is_bounded_proj1_wire_digits
+  end.
+
+Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe41417_32)
+  : Tuple.map (n:=4) proj1_fe41417_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8)
+    = Reified.AddCoordinates.add_coordinates (proj1_fe41417_32 x0)
+                                             (proj1_fe41417_32 x1)
+                                             (proj1_fe41417_32 x2)
+                                             (proj1_fe41417_32 x3)
+                                             (proj1_fe41417_32 x4)
+                                             (proj1_fe41417_32 x5)
+                                             (proj1_fe41417_32 x6)
+                                             (proj1_fe41417_32 x7)
+                                             (proj1_fe41417_32 x8).
+Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed.
diff --git a/src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v
new file mode 100644
index 000000000..dc99e0b11
--- /dev/null
+++ b/src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v
@@ -0,0 +1,67 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.SpecificGen.GF41417_32Bounded.
+Require Import Crypto.SpecificGen.GF41417_32ExtendedAddCoordinates.
+Require Import Crypto.SpecificGen.GF41417_32BoundedAddCoordinates.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+
+Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
+  : Tuple.fieldwise
+      (n:=4) GF41417_32BoundedCommon.eq
+      (@GF41417_32BoundedAddCoordinates.add_coordinates
+         twice_d P10 P11 P12 P13 P20 P21 P22 P23)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF41417_32BoundedCommon.fe41417_32
+         GF41417_32Bounded.add GF41417_32Bounded.sub GF41417_32Bounded.mul twice_d
+         (P10, P11, P12, P13) (P20, P21, P22, P23)).
+Proof.
+  unfold GF41417_32BoundedCommon.eq.
+  apply -> (fieldwise_map_iff (n:=4) eq GF41417_32BoundedCommon.proj1_fe41417_32 GF41417_32BoundedCommon.proj1_fe41417_32).
+  rewrite add_coordinates_correct.
+  cbv [AddCoordinates.add_coordinates].
+  setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
+  unfold edwards_extended_carry_add_coordinates.
+  match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
+  apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF41417_32BoundedCommon.proj1_fe41417_32).
+  apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
+    intros;
+    repeat match goal with
+           | [ |- context[add _ _] ]
+             => rewrite add_correct
+           | [ |- context[sub _ _] ]
+             => rewrite sub_correct
+           | [ |- context[mul _ _] ]
+             => rewrite mul_correct
+           | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
+           | [ |- and _ _ ] => split
+           | [ |- ?x = ?x ] => reflexivity
+           | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
+           | _ => congruence
+           end.
+Qed.
+
+Definition add_coordinates' twice_d P1 P2
+  := let '(P10, P11, P12, P13) := P1 in
+     let '(P20, P21, P22, P23) := P2 in
+     @GF41417_32BoundedAddCoordinates.add_coordinates
+       twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Definition add_coordinates twice_d P1 P2
+  := Eval cbv beta iota delta [GF41417_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in
+      let '(P10, P11, P12, P13) := P1 in
+      let '(P20, P21, P22, P23) := P2 in
+      @GF41417_32BoundedAddCoordinates.add_coordinates
+        twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Lemma add_coordinates_correct_full twice_d P1 P2
+  : Tuple.fieldwise
+      GF41417_32BoundedCommon.eq
+      (add_coordinates twice_d P1 P2)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF41417_32BoundedCommon.fe41417_32
+         GF41417_32Bounded.add GF41417_32Bounded.sub GF41417_32Bounded.mul twice_d P1 P2).
+Proof.
+  destruct_head' prod.
+  rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
+Qed.
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index e40dd0c53..40089d503 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
   make_type_from' T.
 
-Definition ExprBinOpT : type base_type.
-Proof. make_type_from (uncurry_binop_fe41417_32 carry_add). Defined.
-Definition ExprUnOpT : type base_type.
-Proof. make_type_from (uncurry_unop_fe41417_32 carry_opp). Defined.
+Definition fe41417_32T : flat_type base_type.
+Proof.
+  let T := (eval compute in GF41417_32.fe41417_32) in
+  let T := reify_flat_type T in
+  exact T.
+Defined.
+Definition Expr_n_OpT (count_out : nat) : flat_type base_type
+  := Eval cbv [Syntax.tuple Syntax.tuple' fe41417_32T] in
+      Syntax.tuple fe41417_32T count_out.
+Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
+  := match count_in with
+     | 0 => Expr_n_OpT count_out
+     | S n => SmartArrow base_type fe41417_32T (Expr_nm_OpT n count_out)
+     end.
+Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
+Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
 Definition ExprUnOpFEToZT : type base_type.
 Proof. make_type_from (uncurry_unop_fe41417_32 ge_modulus). Defined.
 Definition ExprUnOpWireToFET : type base_type.
 Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
 Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe41417_32 pack). Defined.
-Definition Expr4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply4_nd
-                                (B:=GF41417_32.fe41417_32)
-                                (@uncurry_unop_fe41417_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-Defined.
-Definition Expr9_4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply9_nd
-                                (B:=Tuple.tuple GF41417_32.fe41417_32 4)
-                                (@uncurry_unop_fe41417_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-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 ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type
 Definition ExprArgWireRevT : flat_type base_type
   := Eval compute in all_binders_for ExprUnOpWireToFET.
 Definition ExprZ : Type := Expr (Tbase TZ).
-Definition ExprBinOp : Type := Expr ExprBinOpT.
-Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out).
+Definition ExprBinOp : Type := Expr ExprBinOpT.
+Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
 Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
-Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
+Definition expr_nm_Op count_in count_out interp_base_type var : Type
+  := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out).
 Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT.
 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 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.
 Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT.
-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 exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT.
 Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT.
 Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT.
 Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT.
 
+Local Ltac bounds_from_list_cps ls :=
+  lazymatch (eval hnf in ls) with
+  | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra))
+  | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in
+                        constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
+  end.
+
+Local Ltac make_bounds_cps ls :=
+  let v := bounds_from_list_cps (List.rev ls) in
+  let v := (eval compute in v) in
+  pose v.
+
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
   | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
@@ -105,6 +116,18 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
+(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Proof.
+  refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
+         | 0 => tt
+         | S n => let v := Expr_nm_Op_bounds n count_out in
+                  _
+         end; simpl.
+  make_bounds_cps (Tuple.to_list _ bounds).
+  pose (p _ v).
+  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
+  exact p0.
+*)
 Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
 Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
diff --git a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v
new file mode 100644
index 000000000..6d4dd60bb
--- /dev/null
+++ b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v
@@ -0,0 +1,76 @@
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Export Crypto.SpecificGen.GF41417_32.
+Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
+Require Import Crypto.Reflection.Reify.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Reify.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.AddCoordinates.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
+Require Import Coq.Lists.List Crypto.Util.ListUtil.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Algebra.
+Import ListNotations.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Local Open Scope Z.
+
+Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW.
+
+Declare Reduction asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
+Ltac asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
+
+
+Time Definition interp_radd_coordinates : 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
+  := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates).
+(*Print interp_radd_coordinates.*)
+Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.
+
+Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates.
+Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed.
diff --git a/src/SpecificGen/GF5211_32BoundedAddCoordinates.v b/src/SpecificGen/GF5211_32BoundedAddCoordinates.v
new file mode 100644
index 000000000..17189f4d0
--- /dev/null
+++ b/src/SpecificGen/GF5211_32BoundedAddCoordinates.v
@@ -0,0 +1,77 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.SpecificGen.GF5211_32.
+Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
+Require Import Crypto.SpecificGen.GF5211_32ReflectiveAddCoordinates.
+Require Import Crypto.Util.LetIn.
+Local Open Scope Z.
+
+Local Ltac bounded_t opW blem :=
+  apply blem; apply is_bounded_proj1_fe5211_32.
+
+Local Ltac define_binop f g opW blem :=
+  refine (exist_fe5211_32W (opW (proj1_fe5211_32W f) (proj1_fe5211_32W g)) _);
+  abstract bounded_t opW blem.
+
+Local Opaque Let_In.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64.
+Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
+Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32W) : Tuple.tuple fe5211_32W 4
+  := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8.
+
+Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
+  change opW with (interp_rop);
+  rewrite pre_rewrite;
+  intros; apply rop_cb; assumption.
+
+Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates.
+Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed.
+
+Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem :=
+  refine (let ts := opW (proj1_fe5211_32W x0)
+                        (proj1_fe5211_32W x1)
+                        (proj1_fe5211_32W x2)
+                        (proj1_fe5211_32W x3)
+                        (proj1_fe5211_32W x4)
+                        (proj1_fe5211_32W x5)
+                        (proj1_fe5211_32W x6)
+                        (proj1_fe5211_32W x7)
+                        (proj1_fe5211_32W x8) in
+          HList.mapt exist_fe5211_32W (ts:=ts) _);
+  abstract (
+      rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe5211_32WToZ));
+      apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe5211_32
+    ).
+Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32) : Tuple.tuple fe5211_32 4.
+Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined.
+
+Local Ltac op_correct_t op opW_correct_and_bounded :=
+  cbv [op];
+  rewrite ?HList.map_mapt;
+  lazymatch goal with
+  | [ |- context[proj1_fe5211_32 (exist_fe5211_32W _ _)] ]
+    => rewrite proj1_fe5211_32_exist_fe5211_32W || setoid_rewrite proj1_fe5211_32_exist_fe5211_32W
+  | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ]
+    => rewrite proj1_wire_digits_exist_wire_digitsW
+  | _ => idtac
+  end;
+  rewrite <- ?HList.map_is_mapt;
+  apply opW_correct_and_bounded;
+  lazymatch goal with
+  | [ |- is_bounded _ = true ]
+    => apply is_bounded_proj1_fe5211_32
+  | [ |- wire_digits_is_bounded _ = true ]
+    => apply is_bounded_proj1_wire_digits
+  end.
+
+Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32)
+  : Tuple.map (n:=4) proj1_fe5211_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8)
+    = Reified.AddCoordinates.add_coordinates (proj1_fe5211_32 x0)
+                                             (proj1_fe5211_32 x1)
+                                             (proj1_fe5211_32 x2)
+                                             (proj1_fe5211_32 x3)
+                                             (proj1_fe5211_32 x4)
+                                             (proj1_fe5211_32 x5)
+                                             (proj1_fe5211_32 x6)
+                                             (proj1_fe5211_32 x7)
+                                             (proj1_fe5211_32 x8).
+Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed.
diff --git a/src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v
new file mode 100644
index 000000000..f6ba06ec6
--- /dev/null
+++ b/src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v
@@ -0,0 +1,67 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.SpecificGen.GF5211_32Bounded.
+Require Import Crypto.SpecificGen.GF5211_32ExtendedAddCoordinates.
+Require Import Crypto.SpecificGen.GF5211_32BoundedAddCoordinates.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+
+Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
+  : Tuple.fieldwise
+      (n:=4) GF5211_32BoundedCommon.eq
+      (@GF5211_32BoundedAddCoordinates.add_coordinates
+         twice_d P10 P11 P12 P13 P20 P21 P22 P23)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF5211_32BoundedCommon.fe5211_32
+         GF5211_32Bounded.add GF5211_32Bounded.sub GF5211_32Bounded.mul twice_d
+         (P10, P11, P12, P13) (P20, P21, P22, P23)).
+Proof.
+  unfold GF5211_32BoundedCommon.eq.
+  apply -> (fieldwise_map_iff (n:=4) eq GF5211_32BoundedCommon.proj1_fe5211_32 GF5211_32BoundedCommon.proj1_fe5211_32).
+  rewrite add_coordinates_correct.
+  cbv [AddCoordinates.add_coordinates].
+  setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
+  unfold edwards_extended_carry_add_coordinates.
+  match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
+  apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF5211_32BoundedCommon.proj1_fe5211_32).
+  apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
+    intros;
+    repeat match goal with
+           | [ |- context[add _ _] ]
+             => rewrite add_correct
+           | [ |- context[sub _ _] ]
+             => rewrite sub_correct
+           | [ |- context[mul _ _] ]
+             => rewrite mul_correct
+           | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
+           | [ |- and _ _ ] => split
+           | [ |- ?x = ?x ] => reflexivity
+           | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
+           | _ => congruence
+           end.
+Qed.
+
+Definition add_coordinates' twice_d P1 P2
+  := let '(P10, P11, P12, P13) := P1 in
+     let '(P20, P21, P22, P23) := P2 in
+     @GF5211_32BoundedAddCoordinates.add_coordinates
+       twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Definition add_coordinates twice_d P1 P2
+  := Eval cbv beta iota delta [GF5211_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in
+      let '(P10, P11, P12, P13) := P1 in
+      let '(P20, P21, P22, P23) := P2 in
+      @GF5211_32BoundedAddCoordinates.add_coordinates
+        twice_d P10 P11 P12 P13 P20 P21 P22 P23.
+
+Lemma add_coordinates_correct_full twice_d P1 P2
+  : Tuple.fieldwise
+      GF5211_32BoundedCommon.eq
+      (add_coordinates twice_d P1 P2)
+      (@ExtendedCoordinates.Extended.add_coordinates
+         GF5211_32BoundedCommon.fe5211_32
+         GF5211_32Bounded.add GF5211_32Bounded.sub GF5211_32Bounded.mul twice_d P1 P2).
+Proof.
+  destruct_head' prod.
+  rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
+Qed.
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index 1db5efcd0..2ad555057 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
   make_type_from' T.
 
-Definition ExprBinOpT : type base_type.
-Proof. make_type_from (uncurry_binop_fe5211_32 carry_add). Defined.
-Definition ExprUnOpT : type base_type.
-Proof. make_type_from (uncurry_unop_fe5211_32 carry_opp). Defined.
+Definition fe5211_32T : flat_type base_type.
+Proof.
+  let T := (eval compute in GF5211_32.fe5211_32) in
+  let T := reify_flat_type T in
+  exact T.
+Defined.
+Definition Expr_n_OpT (count_out : nat) : flat_type base_type
+  := Eval cbv [Syntax.tuple Syntax.tuple' fe5211_32T] in
+      Syntax.tuple fe5211_32T count_out.
+Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
+  := match count_in with
+     | 0 => Expr_n_OpT count_out
+     | S n => SmartArrow base_type fe5211_32T (Expr_nm_OpT n count_out)
+     end.
+Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
+Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
 Definition ExprUnOpFEToZT : type base_type.
 Proof. make_type_from (uncurry_unop_fe5211_32 ge_modulus). Defined.
 Definition ExprUnOpWireToFET : type base_type.
 Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
 Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe5211_32 pack). Defined.
-Definition Expr4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply4_nd
-                                (B:=GF5211_32.fe5211_32)
-                                (@uncurry_unop_fe5211_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-Defined.
-Definition Expr9_4OpT : type base_type.
-Proof.
-  let T := lazymatch type of (apply9_nd
-                                (B:=Tuple.tuple GF5211_32.fe5211_32 4)
-                                (@uncurry_unop_fe5211_32)) with
-           | _ -> ?T => T
-           end in
-  make_type_from' T.
-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 ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type
 Definition ExprArgWireRevT : flat_type base_type
   := Eval compute in all_binders_for ExprUnOpWireToFET.
 Definition ExprZ : Type := Expr (Tbase TZ).
-Definition ExprBinOp : Type := Expr ExprBinOpT.
-Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out).
+Definition ExprBinOp : Type := Expr ExprBinOpT.
+Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition Expr4Op : Type := Expr Expr4OpT.
 Definition Expr9_4Op : Type := Expr Expr9_4OpT.
 Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
 Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
-Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
+Definition expr_nm_Op count_in count_out interp_base_type var : Type
+  := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out).
 Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT.
 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 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.
 Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT.
-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 exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT.
 Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT.
 Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT.
 Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT.
 
+Local Ltac bounds_from_list_cps ls :=
+  lazymatch (eval hnf in ls) with
+  | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra))
+  | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in
+                        constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
+  end.
+
+Local Ltac make_bounds_cps ls :=
+  let v := bounds_from_list_cps (List.rev ls) in
+  let v := (eval compute in v) in
+  pose v.
+
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
   | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
@@ -105,6 +116,18 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
+(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Proof.
+  refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
+         | 0 => tt
+         | S n => let v := Expr_nm_Op_bounds n count_out in
+                  _
+         end; simpl.
+  make_bounds_cps (Tuple.to_list _ bounds).
+  pose (p _ v).
+  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
+  exact p0.
+*)
 Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
 Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
diff --git a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v
new file mode 100644
index 000000000..ddba2a199
--- /dev/null
+++ b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v
@@ -0,0 +1,76 @@
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Export Crypto.SpecificGen.GF5211_32.
+Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
+Require Import Crypto.Reflection.Reify.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Reify.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.AddCoordinates.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
+Require Import Coq.Lists.List Crypto.Util.ListUtil.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Algebra.
+Import ListNotations.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Local Open Scope Z.
+
+Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW.
+
+Declare Reduction asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
+Ltac asm_interp_add_coordinates
+  := cbv beta iota delta
+         [id
+            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+            radd_coordinates
+            curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W
+            WordW.interp_op WordW.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
+
+
+Time Definition interp_radd_coordinates : 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
+  := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates).
+(*Print interp_radd_coordinates.*)
+Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.
+
+Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates.
+Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed.