Remove admits, fill templates, copy bounds

2 files changed, 111 insertions, 92 deletions

diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index a8199fd5c..f88a801af 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -14,6 +14,7 @@ Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
 Require Import Crypto.Reflection.MapInterpWf.
 Require Import Crypto.Reflection.WfReflective.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
@@ -21,11 +22,13 @@ Require Import Crypto.Util.Notations.
 
 Notation Expr := (Expr base_type WordW.interp_base_type op).
 
-Local Ltac make_type_from uncurried_op :=
-  let T := (type of uncurried_op) in
+Local Ltac make_type_from' T :=
   let T := (eval compute in T) in
   let rT := reify_type T in
   exact rT.
+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.
@@ -37,6 +40,24 @@ 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 ExprArgT : flat_type base_type
   := Eval compute in remove_all_binders ExprUnOpT.
 Definition ExprArgWireT : flat_type base_type
@@ -51,6 +72,8 @@ Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+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.
@@ -61,6 +84,8 @@ Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_ty
 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.
@@ -89,6 +114,14 @@ Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZB
 Proof. make_bounds (Tuple.to_list _ bounds). Defined.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
+Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type.
+Proof.
+  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)).
+Defined.
+Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type.
+Proof.
+  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)).
+Defined.
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
   := fun e => curry_binop_fe2213_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
@@ -99,6 +132,18 @@ Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF2213_32Boun
   := fun e => curry_unop_fe2213_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF2213_32BoundedCommon.wire_digitsW -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
   := fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
+Definition interp_9_4expr : Expr9_4Op
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
+                            -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4
+  := fun e => curry_9op_fe2213_32W (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -110,6 +155,8 @@ Notation unop_FEToWire_correct_and_bounded rop op
   := (iunop_FEToWire_correct_and_bounded (interp_uexpr_FEToWire rop) op) (only parsing).
 Notation unop_WireToFE_correct_and_bounded rop op
   := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
+Notation op9_4_correct_and_bounded rop op
+  := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing).
 
 Ltac rexpr_cbv :=
   lazymatch goal with
@@ -134,6 +181,7 @@ Notation rexpr_unop_sig op := (rexpr_sig ExprUnOpT (uncurry_unop_fe2213_32 op))
 Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe2213_32 op)) (only parsing).
 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe2213_32 op)) (only parsing).
 Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
+Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe2213_32 op)) (only parsing).
 
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
@@ -305,6 +353,29 @@ Proof.
   let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in
   exact v.
 Defined.
+Definition op9_args_to_bounded (x : fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W)
+           (H0 : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H1 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+           (H2 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+           (H3 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+           (H4 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x)))))) = true)
+           (H5 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst x))))) = true)
+           (H6 : is_bounded (fe2213_32WToZ (snd (fst (fst x)))) = true)
+           (H7 : is_bounded (fe2213_32WToZ (snd (fst x))) = true)
+           (H8 : is_bounded (fe2213_32WToZ (snd x)) = true)
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr9_4OpT).
+Proof.
+  let v := constr:(unop_args_to_bounded _ H8) in
+  let v := app_tuples (unop_args_to_bounded _ H7) v in
+  let v := app_tuples (unop_args_to_bounded _ H6) v in
+  let v := app_tuples (unop_args_to_bounded _ H5) v in
+  let v := app_tuples (unop_args_to_bounded _ H4) v in
+  let v := app_tuples (unop_args_to_bounded _ H3) v in
+  let v := app_tuples (unop_args_to_bounded _ H2) v in
+  let v := app_tuples (unop_args_to_bounded _ H1) v in
+  let v := app_tuples (unop_args_to_bounded _ H0) v in
+  exact v.
+Defined.
 
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
@@ -340,6 +411,8 @@ Definition unopFEToZ_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bo
 Proof.
   refine (let (l, u) := bounds in ((0 <=? l) && (u <=? 1))%Z%bool).
 Defined.
+Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
+Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
 Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
   := fun x
@@ -378,12 +451,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   let Hbounds1 := fresh "Hbounds1" in
   let Hbounds2 := fresh "Hbounds2" in
   pose proof (proj2_sig ropZ_sig) as Heq;
-  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
-                    curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW
-                    curry_binop_fe2213_32 curry_unop_fe2213_32 curry_unop_wire_digits
-                    uncurry_binop_fe2213_32W uncurry_unop_fe2213_32W uncurry_unop_wire_digitsW
-                    uncurry_binop_fe2213_32 uncurry_unop_fe2213_32 uncurry_unop_wire_digits
-                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET
+  cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
+                    curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W
+                    curry_binop_fe2213_32 curry_unop_fe2213_32 curry_unop_wire_digits curry_9op_fe2213_32
+                    uncurry_binop_fe2213_32W uncurry_unop_fe2213_32W uncurry_unop_wire_digitsW uncurry_9op_fe2213_32W
+                    uncurry_binop_fe2213_32 uncurry_unop_fe2213_32 uncurry_unop_wire_digits uncurry_9op_fe2213_32
+                    ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
                     interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
   cbv zeta in *;
   simpl @fe2213_32WToZ; simpl @wire_digitsWToZ;
@@ -414,13 +487,15 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   end;
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
-         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded
+         binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe2213_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
   | [ |- wire_digitsWToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
+  | [ |- ((Tuple.map fe2213_32WToZ ?x = _) * _)%type ]
+    => generalize dependent x; intros
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
@@ -430,15 +505,16 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
-           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good
-           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds] in H1;
+           binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good
+           ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1;
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe2213_32WToZ; simpl @wire_digitsWToZ;
   destruct_head' and;
   Z.ltb_to_lt;
   change WordW.wordWToZ with word64ToZ in *;
-  unfold_is_bounded;
+  cbv [Tuple.map HList.hlist Tuple.on_tuple Tuple.from_list Tuple.from_list' Tuple.to_list Tuple.to_list' List.map HList.hlist' fst snd];
+  repeat split; unfold_is_bounded;
   Z.ltb_to_lt;
   try omega; try reflexivity.
 
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
index aa4bf49e7..a00c068ad 100644
--- a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
@@ -20,30 +20,15 @@ Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Add.
 Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Sub.
 Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Mul.
-Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonBinOp.
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Common9_4Op.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.HList.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 Require Import Bedrock.Word.
 
-Definition apply9 {AK BK PA PB ARR}
-           (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B))
-           {A0 A1 A2 A3 A4 A5 A6 A7 A8 : AK} {B : BK}
-           (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PA A4 -> PA A5 -> PA A6 -> PA A7 -> PA A8 -> PB B)
-  : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 (ARR A4 (ARR A5 (ARR A6 (ARR A7 (ARR A8 B))))))))).
-Proof.
-  repeat (apply F; intro); apply f; assumption.
-Defined.
-
-Definition apply9_nd {BK PA PB ARR}
-           (F : forall (B : BK), (PA -> PB B) -> PB (ARR B))
-           {B : BK}
-           (f : PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PB B)
-  : PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B)))))))))
-  := @apply9 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F)
-             tt tt tt tt tt tt tt tt tt B f.
-
 Definition radd_coordinatesZ' var twice_d P1 P2
   := @Extended.add_coordinates_gen
        _
@@ -66,12 +51,16 @@ Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _
                            (Return P10, Return P11, Return P12, Return P13)
                            (Return P20, Return P21, Return P22, Return P23))).
 
-Definition radd_coordinatesT : type base_type.
-Proof.
-  match type of radd_coordinatesZ'' with
-  | Syntax.Expr _ _ _ ?T => exact T
-  end.
-Defined.
+Definition add_coordinates
+  := fun twice_d P10 P11 P12 P13 P20 P21 P22 P23
+     => @Extended.add_coordinates
+          _ add sub mul
+          twice_d (P10, P11, P12, P13) (P20, P21, P22, P23).
+
+Definition uncurried_add_coordinates
+  := apply9_nd
+       (@uncurry_unop_fe2213_32)
+       add_coordinates.
 
 Local Notation rexpr_sigP T uncurried_op rexprZ :=
   (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op)
@@ -80,20 +69,6 @@ Local Notation rexpr_sig T uncurried_op :=
   { rexprZ | rexpr_sigP T uncurried_op rexprZ }
     (only parsing).
 
-Definition uncurried_add_coordinates
-  := apply9_nd
-       (@uncurry_unop_fe2213_32)
-       (fun twice_d P10 P11 P12 P13 P20 P21 P22 P23
-        => @Extended.add_coordinates
-             _ add sub mul
-             twice_d (P10, P11, P12, P13) (P20, P21, P22, P23)).
-
-
-Local Ltac fold_interpf_at_1 :=
-  let k := (eval unfold interpf in (@interpf base_type interp_base_type op interp_op)) in
-  change k with (@interpf base_type interp_base_type op interp_op) at 1.
-Local Ltac step_interpf :=
-  unfold interpf_step at 1; fold_interpf_at_1.
 Local Ltac repeat_step_interpf :=
   let k := (eval unfold interpf in (@interpf base_type interp_base_type op interp_op)) in
   let k' := fresh in
@@ -140,12 +115,13 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma radd_coordinatesZ_sigP : rexpr_sigP radd_coordinatesT uncurried_add_coordinates radd_coordinatesZ''.
+Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
   etransitivity; [ apply Interp_Linearize | ].
-  cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise radd_coordinatesT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe2213_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32].
+  cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe2213_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 add_coordinates].
   intros.
+  unfold UnReturn at 13 14 15 16.
   repeat match goal with
          | [ |- appcontext[@proj1_sig ?A ?B ?v] ]
            => let k := fresh "f" in
@@ -154,10 +130,9 @@ Proof.
               set (k := v);
                 set (k' := @proj1_sig A B k);
                 pose proof (proj2_sig k) as H;
-                change (proj1_sig k) with k' in H(*;
-                cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe2213_32] in H*)
+                change (proj1_sig k) with k' in H;
+                clearbody k'; clear k
          end.
-  unfold UnReturn at 13 14 15 16.
   unfold interpf; repeat_step_interpf.
   unfold interpf at 13 14 15; unfold interpf_step.
   cbv beta iota delta [Extended.add_coordinates].
@@ -179,55 +154,23 @@ Proof.
            end.
 Time Qed.
 
-Definition radd_coordinatesZ_sig : rexpr_sig radd_coordinatesT uncurried_add_coordinates.
+Definition radd_coordinatesZ_sig : rexpr_9_4op_sig add_coordinates.
 Proof.
   eexists.
   apply radd_coordinatesZ_sigP.
 Defined.
 
-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 |})
-  | (?x :: ?xs)%list => let bs := bounds_from_list xs in
-                        constr:((Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs))
-  end.
-
-Local Ltac make_bounds ls :=
-  compute;
-  let v := bounds_from_list (List.rev ls) in
-  let v := (eval compute in v) in
-  exact v.
-
-Definition ExprAC_bounds : interp_all_binders_for radd_coordinatesT ZBounds.interp_base_type.
-Proof.
-  make_bounds ((Tuple.to_list _ bounds)
-                 ++ Tuple.to_list _ bounds ++ Tuple.to_list _ bounds ++ Tuple.to_list _ bounds ++ Tuple.to_list _ bounds
-                 ++ Tuple.to_list _ bounds ++ Tuple.to_list _ bounds ++ Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list.
-Defined.
-
 Time Definition radd_coordinatesW := Eval vm_compute in rword_of_Z radd_coordinatesZ_sig.
 Lemma radd_coordinatesW_correct_and_bounded_gen : correct_and_bounded_genT radd_coordinatesW radd_coordinatesZ_sig.
 Proof. Time rexpr_correct. Time Qed.
-Definition radd_coordinates_output_bounds := Eval vm_compute in compute_bounds radd_coordinatesW ExprAC_bounds.
-(*Notation i9op_correct_and_bounded irop op
-  := (forall x0 x1 x2 x3 x4 x5 x6 x7 x8,
-         is_bounded (fe2213_32WToZ x0) = true
-         -> is_bounded (fe2213_32WToZ x1) = true
-         -> is_bounded (fe2213_32WToZ x2) = true
-         -> is_bounded (fe2213_32WToZ x3) = true
-         -> is_bounded (fe2213_32WToZ x4) = true
-         -> is_bounded (fe2213_32WToZ x5) = true
-         -> is_bounded (fe2213_32WToZ x6) = true
-         -> is_bounded (fe2213_32WToZ x7) = true
-         -> is_bounded (fe2213_32WToZ x8) = true
-         -> fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8) = op (fe2213_32WToZ x0) (fe2213_32WToZ x1) (fe2213_32WToZ x2) (fe2213_32WToZ x3) (fe2213_32WToZ x4) (fe2213_32WToZ x5) (fe2213_32WToZ x6) (fe2213_32WToZ x7) (fe2213_32WToZ x8)
-            /\ is_bounded (fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)) = true) (only parsing).
+Definition radd_coordinates_output_bounds := Eval vm_compute in compute_bounds radd_coordinatesW Expr9Op_bounds.
 
 Local Obligation Tactic := intros; vm_compute; constructor.
+
 Program Definition radd_coordinatesW_correct_and_bounded
-  := ExprBinOp_correct_and_bounded
+  := Expr9_4Op_correct_and_bounded
        radd_coordinatesW add_coordinates radd_coordinatesZ_sig radd_coordinatesW_correct_and_bounded_gen
-       _ _.*)
+       _ _.
 
 Local Open Scope string_scope.
 Compute ("Add_Coordinates", compute_bounds_for_display radd_coordinatesW ExprAC_bounds).