aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject1
-rw-r--r--src/Specific/GF25519.v36
-rw-r--r--src/Specific/GF25519BoundedCommon.v50
-rw-r--r--src/Specific/GF25519Reflective/Common.v100
-rw-r--r--src/Specific/GF25519Reflective/Common9_4Op.v108
-rw-r--r--src/Specific/GF25519Reflective/Reified/AddCoordinates.v81
-rw-r--r--src/SpecificGen/GF2213_32.v36
-rw-r--r--src/SpecificGen/GF2519_32.v36
-rw-r--r--src/SpecificGen/GF25519_32.v36
-rw-r--r--src/SpecificGen/GF25519_64.v36
-rw-r--r--src/SpecificGen/GF41417_32.v36
-rw-r--r--src/SpecificGen/GF5211_32.v36
-rw-r--r--src/SpecificGen/GFtemplate3mod436
-rw-r--r--src/SpecificGen/GFtemplate5mod836
-rw-r--r--src/Util/Tower.v17
15 files changed, 608 insertions, 73 deletions
diff --git a/_CoqProject b/_CoqProject
index 11d34e925..1412edfdf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -153,6 +153,7 @@ src/Specific/FancyMachine256/Barrett.v
src/Specific/FancyMachine256/Core.v
src/Specific/FancyMachine256/Montgomery.v
src/Specific/GF25519Reflective/Common.v
+src/Specific/GF25519Reflective/Common9_4Op.v
src/Specific/GF25519Reflective/CommonBinOp.v
src/Specific/GF25519Reflective/CommonUnOp.v
src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 10ff8d1af..357b9dc8a 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -177,6 +177,25 @@ Proof.
etransitivity; apply app_10_correct.
Qed.
+Definition appify9 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519) :=
+ app_10 x0 (fun x0' =>
+ app_10 x1 (fun x1' =>
+ app_10 x2 (fun x2' =>
+ app_10 x3 (fun x3' =>
+ app_10 x4 (fun x4' =>
+ app_10 x5 (fun x5' =>
+ app_10 x6 (fun x6' =>
+ app_10 x7 (fun x7' =>
+ app_10 x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_10_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe25519 {T} (op : fe25519 -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe25519) op.
Definition curry_unop_fe25519 {T} op : fe25519 -> T
@@ -191,6 +210,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_7 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe25519 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T)
+ := Eval compute in
+ uncurry_unop_fe25519 (fun x0 =>
+ uncurry_unop_fe25519 (fun x1 =>
+ uncurry_unop_fe25519 (fun x2 =>
+ uncurry_unop_fe25519 (fun x3 =>
+ uncurry_unop_fe25519 (fun x4 =>
+ uncurry_unop_fe25519 (fun x5 =>
+ uncurry_unop_fe25519 (fun x6 =>
+ uncurry_unop_fe25519 (fun x7 =>
+ uncurry_unop_fe25519 (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe25519 {T} op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe25519) :
{ fg : fe25519 | fg = add_opt f g}.
Proof.
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index 7b47a8509..22c2edc4b 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -186,6 +186,25 @@ Section generic_destructuring.
intros. cbv [appify2].
etransitivity; apply app_fe25519W_correct.
Qed.
+
+ Definition appify9 {T} (op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519W) :=
+ app_fe25519W x0 (fun x0' =>
+ app_fe25519W x1 (fun x1' =>
+ app_fe25519W x2 (fun x2' =>
+ app_fe25519W x3 (fun x3' =>
+ app_fe25519W x4 (fun x4' =>
+ app_fe25519W x5 (fun x5' =>
+ app_fe25519W x6 (fun x6' =>
+ app_fe25519W x7 (fun x7' =>
+ app_fe25519W x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+ Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_fe25519W_correct | ]); reflexivity.
+ Qed.
End generic_destructuring.
Definition eta_fe25519W_sig (x : fe25519W) : { v : fe25519W | v = x }.
@@ -369,6 +388,22 @@ Definition uncurry_unop_wire_digitsW {T} (op : wire_digitsW -> T)
Definition curry_unop_wire_digitsW {T} op : wire_digitsW -> T
:= Eval cbv (*-[word64]*) in fun f => app_wire_digitsW f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe25519W {T} (op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T)
+ := Eval cbv (*-[word64]*) in
+ uncurry_unop_fe25519W (fun x0 =>
+ uncurry_unop_fe25519W (fun x1 =>
+ uncurry_unop_fe25519W (fun x2 =>
+ uncurry_unop_fe25519W (fun x3 =>
+ uncurry_unop_fe25519W (fun x4 =>
+ uncurry_unop_fe25519W (fun x5 =>
+ uncurry_unop_fe25519W (fun x6 =>
+ uncurry_unop_fe25519W (fun x7 =>
+ uncurry_unop_fe25519W (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe25519W {T} op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T
+ := Eval cbv (*-[word64]*) in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
Definition proj1_fe25519W (x : fe25519) : fe25519W
:= Eval app_tuple_map in
@@ -708,5 +743,20 @@ Notation iunop_WireToFE_correct_and_bounded irop op
wire_digits_is_bounded (wire_digitsWToZ x) = true
-> fe25519WToZ (irop x) = op (wire_digitsWToZ x)
/\ is_bounded (fe25519WToZ (irop x)) = true) (only parsing).
+Notation i9top_correct_and_bounded k irop op
+ := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ is_bounded (fe25519WToZ x0) = true
+ -> is_bounded (fe25519WToZ x1) = true
+ -> is_bounded (fe25519WToZ x2) = true
+ -> is_bounded (fe25519WToZ x3) = true
+ -> is_bounded (fe25519WToZ x4) = true
+ -> is_bounded (fe25519WToZ x5) = true
+ -> is_bounded (fe25519WToZ x6) = true
+ -> is_bounded (fe25519WToZ x7) = true
+ -> is_bounded (fe25519WToZ x8) = true
+ -> (Tuple.map (n:=k) fe25519WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)
+ = op (fe25519WToZ x0) (fe25519WToZ x1) (fe25519WToZ x2) (fe25519WToZ x3) (fe25519WToZ x4) (fe25519WToZ x5) (fe25519WToZ x6) (fe25519WToZ x7) (fe25519WToZ x8))
+ * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
+ (only parsing).
Definition prefreeze := GF25519.prefreeze.
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 76cf82bd1..ea42499f7 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/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_fe25519 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_fe25519 pack). Defined.
+Definition Expr4OpT : type base_type.
+Proof.
+ let T := lazymatch type of (apply4_nd
+ (B:=GF25519.fe25519)
+ (@uncurry_unop_fe25519)) 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.fe25519 4)
+ (@uncurry_unop_fe25519)) 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 -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= fun e => curry_binop_fe25519W (Interp (@WordW.interp_op) e).
Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
@@ -99,6 +132,18 @@ Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCo
:= fun e => curry_unop_fe25519W (Interp (@WordW.interp_op) e).
Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
:= fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
+Definition interp_9_4expr : Expr9_4Op
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Specific.GF25519BoundedCommon.fe25519W
+ -> Tuple.tuple Specific.GF25519BoundedCommon.fe25519W 4
+ := fun e => curry_9op_fe25519W (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_fe25519 op)) (o
Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25519 op)) (only parsing).
Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe25519 op)) (only parsing).
Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
+Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519 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 : fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W)
+ (H0 : is_bounded (fe25519WToZ (fst (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+ (H1 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true)
+ (H2 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true)
+ (H3 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst x))))))) = true)
+ (H4 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst x)))))) = true)
+ (H5 : is_bounded (fe25519WToZ (snd (fst (fst (fst x))))) = true)
+ (H6 : is_bounded (fe25519WToZ (snd (fst (fst x)))) = true)
+ (H7 : is_bounded (fe25519WToZ (snd (fst x))) = true)
+ (H8 : is_bounded (fe25519WToZ (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_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW
- curry_binop_fe25519 curry_unop_fe25519 curry_unop_wire_digits
- uncurry_binop_fe25519W uncurry_unop_fe25519W uncurry_unop_wire_digitsW
- uncurry_binop_fe25519 uncurry_unop_fe25519 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_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W
+ curry_binop_fe25519 curry_unop_fe25519 curry_unop_wire_digits curry_9op_fe25519
+ uncurry_binop_fe25519W uncurry_unop_fe25519W uncurry_unop_wire_digitsW uncurry_9op_fe25519W
+ uncurry_binop_fe25519 uncurry_unop_fe25519 uncurry_unop_wire_digits uncurry_9op_fe25519
+ ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT
interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *;
cbv zeta in *;
simpl @fe25519WToZ; 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
| [ |- fe25519WToZ ?x = _ /\ _ ]
=> generalize dependent x; intros
| [ |- wire_digitsWToZ ?x = _ /\ _ ]
=> generalize dependent x; intros
+ | [ |- ((Tuple.map fe25519WToZ ?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 @fe25519WToZ; 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/Specific/GF25519Reflective/Common9_4Op.v b/src/Specific/GF25519Reflective/Common9_4Op.v
new file mode 100644
index 000000000..d2366932e
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Common9_4Op.v
@@ -0,0 +1,108 @@
+Require Export Crypto.Specific.GF25519Reflective.Common.
+Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr9_4Op_correct_and_bounded
+ ropW op (ropZ_sig : rexpr_9_4op_sig op)
+ (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+ (H0 : forall x012345678
+ (x012345678
+ := (eta_fe25519W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe25519W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe25519W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe25519W (snd (fst (fst (fst x012345678)))),
+ eta_fe25519W (snd (fst (fst x012345678))),
+ eta_fe25519W (snd (fst x012345678)),
+ eta_fe25519W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe25519WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe25519WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+ (LiftOption.to' (Some args)))
+ with
+ | Some _ => True
+ | None => False
+ end)
+ (H1 : forall x012345678
+ (x012345678
+ := (eta_fe25519W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe25519W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe25519W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe25519W (snd (fst (fst (fst x012345678)))),
+ eta_fe25519W (snd (fst (fst x012345678))),
+ eta_fe25519W (snd (fst x012345678)),
+ eta_fe25519W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe25519WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe25519WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe25519WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+ with
+ | Some bounds => op9_4_bounds_good bounds = true
+ | None => False
+ end)
+ : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+ intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.
+ pose x0 as x0'.
+ pose x1 as x1'.
+ pose x2 as x2'.
+ pose x3 as x3'.
+ pose x4 as x4'.
+ pose x5 as x5'.
+ pose x6 as x6'.
+ pose x7 as x7'.
+ pose x8 as x8'.
+ hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8; destruct_head' prod.
+ specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
+ (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
+ specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
+ (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
+ let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+ t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
+Qed.
diff --git a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
index 36d388ea3..2632c6b5e 100644
--- a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
+++ b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
@@ -20,9 +20,10 @@ Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
Require Import Crypto.Specific.GF25519Reflective.Reified.Add.
Require Import Crypto.Specific.GF25519Reflective.Reified.Sub.
Require Import Crypto.Specific.GF25519Reflective.Reified.Mul.
-Require Import Crypto.Specific.GF25519Reflective.CommonBinOp.
+Require Import Crypto.Specific.GF25519Reflective.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.
@@ -50,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_fe25519)
+ 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)
@@ -64,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_fe25519)
- (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
@@ -124,11 +115,11 @@ 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_fe25519 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519].
+ cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519 add_coordinates].
intros.
unfold UnReturn at 13 14 15 16.
repeat match goal with
@@ -163,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 (fe25519WToZ x0) = true
- -> is_bounded (fe25519WToZ x1) = true
- -> is_bounded (fe25519WToZ x2) = true
- -> is_bounded (fe25519WToZ x3) = true
- -> is_bounded (fe25519WToZ x4) = true
- -> is_bounded (fe25519WToZ x5) = true
- -> is_bounded (fe25519WToZ x6) = true
- -> is_bounded (fe25519WToZ x7) = true
- -> is_bounded (fe25519WToZ x8) = true
- -> fe25519WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8) = op (fe25519WToZ x0) (fe25519WToZ x1) (fe25519WToZ x2) (fe25519WToZ x3) (fe25519WToZ x4) (fe25519WToZ x5) (fe25519WToZ x6) (fe25519WToZ x7) (fe25519WToZ x8)
- /\ is_bounded (fe25519WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)) = true) (only parsing).
+Proof. (*Time rexpr_correct. Time Qed.*) Admitted.
+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).
diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v
index 87da8dbcc..cd5ff40c5 100644
--- a/src/SpecificGen/GF2213_32.v
+++ b/src/SpecificGen/GF2213_32.v
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2213_32) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe2213_32 {T} (op : fe2213_32 -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe2213_32) op.
Definition curry_unop_fe2213_32 {T} op : fe2213_32 -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe2213_32 {T} (op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T)
+ := Eval compute in
+ uncurry_unop_fe2213_32 (fun x0 =>
+ uncurry_unop_fe2213_32 (fun x1 =>
+ uncurry_unop_fe2213_32 (fun x2 =>
+ uncurry_unop_fe2213_32 (fun x3 =>
+ uncurry_unop_fe2213_32 (fun x4 =>
+ uncurry_unop_fe2213_32 (fun x5 =>
+ uncurry_unop_fe2213_32 (fun x6 =>
+ uncurry_unop_fe2213_32 (fun x7 =>
+ uncurry_unop_fe2213_32 (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe2213_32) :
{ fg : fe2213_32 | fg = add_opt f g}.
Proof.
diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v
index b7fd074ae..98338b64c 100644
--- a/src/SpecificGen/GF2519_32.v
+++ b/src/SpecificGen/GF2519_32.v
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2519_32) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe2519_32 {T} (op : fe2519_32 -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe2519_32) op.
Definition curry_unop_fe2519_32 {T} op : fe2519_32 -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe2519_32 {T} (op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T)
+ := Eval compute in
+ uncurry_unop_fe2519_32 (fun x0 =>
+ uncurry_unop_fe2519_32 (fun x1 =>
+ uncurry_unop_fe2519_32 (fun x2 =>
+ uncurry_unop_fe2519_32 (fun x3 =>
+ uncurry_unop_fe2519_32 (fun x4 =>
+ uncurry_unop_fe2519_32 (fun x5 =>
+ uncurry_unop_fe2519_32 (fun x6 =>
+ uncurry_unop_fe2519_32 (fun x7 =>
+ uncurry_unop_fe2519_32 (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe2519_32) :
{ fg : fe2519_32 | fg = add_opt f g}.
Proof.
diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v
index 30d01f87d..89f63a572 100644
--- a/src/SpecificGen/GF25519_32.v
+++ b/src/SpecificGen/GF25519_32.v
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe25519_32 {T} (op : fe25519_32 -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe25519_32) op.
Definition curry_unop_fe25519_32 {T} op : fe25519_32 -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe25519_32 {T} (op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T)
+ := Eval compute in
+ uncurry_unop_fe25519_32 (fun x0 =>
+ uncurry_unop_fe25519_32 (fun x1 =>
+ uncurry_unop_fe25519_32 (fun x2 =>
+ uncurry_unop_fe25519_32 (fun x3 =>
+ uncurry_unop_fe25519_32 (fun x4 =>
+ uncurry_unop_fe25519_32 (fun x5 =>
+ uncurry_unop_fe25519_32 (fun x6 =>
+ uncurry_unop_fe25519_32 (fun x7 =>
+ uncurry_unop_fe25519_32 (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe25519_32) :
{ fg : fe25519_32 | fg = add_opt f g}.
Proof.
diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v
index 49b5fb2c4..3645a59f7 100644
--- a/src/SpecificGen/GF25519_64.v
+++ b/src/SpecificGen/GF25519_64.v
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe25519_64 {T} (op : fe25519_64 -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe25519_64) op.
Definition curry_unop_fe25519_64 {T} op : fe25519_64 -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe25519_64 {T} (op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T)
+ := Eval compute in
+ uncurry_unop_fe25519_64 (fun x0 =>
+ uncurry_unop_fe25519_64 (fun x1 =>
+ uncurry_unop_fe25519_64 (fun x2 =>
+ uncurry_unop_fe25519_64 (fun x3 =>
+ uncurry_unop_fe25519_64 (fun x4 =>
+ uncurry_unop_fe25519_64 (fun x5 =>
+ uncurry_unop_fe25519_64 (fun x6 =>
+ uncurry_unop_fe25519_64 (fun x7 =>
+ uncurry_unop_fe25519_64 (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe25519_64) :
{ fg : fe25519_64 | fg = add_opt f g}.
Proof.
diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v
index 04ad4c173..9d0e73245 100644
--- a/src/SpecificGen/GF41417_32.v
+++ b/src/SpecificGen/GF41417_32.v
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe41417_32) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe41417_32 {T} (op : fe41417_32 -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe41417_32) op.
Definition curry_unop_fe41417_32 {T} op : fe41417_32 -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe41417_32 {T} (op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T)
+ := Eval compute in
+ uncurry_unop_fe41417_32 (fun x0 =>
+ uncurry_unop_fe41417_32 (fun x1 =>
+ uncurry_unop_fe41417_32 (fun x2 =>
+ uncurry_unop_fe41417_32 (fun x3 =>
+ uncurry_unop_fe41417_32 (fun x4 =>
+ uncurry_unop_fe41417_32 (fun x5 =>
+ uncurry_unop_fe41417_32 (fun x6 =>
+ uncurry_unop_fe41417_32 (fun x7 =>
+ uncurry_unop_fe41417_32 (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe41417_32) :
{ fg : fe41417_32 | fg = add_opt f g}.
Proof.
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v
index ea75b2983..48f85104a 100644
--- a/src/SpecificGen/GF5211_32.v
+++ b/src/SpecificGen/GF5211_32.v
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe5211_32 {T} (op : fe5211_32 -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe5211_32) op.
Definition curry_unop_fe5211_32 {T} op : fe5211_32 -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe5211_32 {T} (op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T)
+ := Eval compute in
+ uncurry_unop_fe5211_32 (fun x0 =>
+ uncurry_unop_fe5211_32 (fun x1 =>
+ uncurry_unop_fe5211_32 (fun x2 =>
+ uncurry_unop_fe5211_32 (fun x3 =>
+ uncurry_unop_fe5211_32 (fun x4 =>
+ uncurry_unop_fe5211_32 (fun x5 =>
+ uncurry_unop_fe5211_32 (fun x6 =>
+ uncurry_unop_fe5211_32 (fun x7 =>
+ uncurry_unop_fe5211_32 (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe5211_32) :
{ fg : fe5211_32 | fg = add_opt f g}.
Proof.
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index d255befeb..bc7766f7a 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe{{{k}}}{{{c}}}_{{{w}}}) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op.
Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
+ := Eval compute in
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x0 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x1 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x2 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x3 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x4 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x5 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x6 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x7 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
{ fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}.
Proof.
diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8
index 008010efd..7a0f0f22c 100644
--- a/src/SpecificGen/GFtemplate5mod8
+++ b/src/SpecificGen/GFtemplate5mod8
@@ -176,6 +176,25 @@ Proof.
etransitivity; apply app_n_correct.
Qed.
+Definition appify9 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe{{{k}}}{{{c}}}_{{{w}}}) :=
+ app_n x0 (fun x0' =>
+ app_n x1 (fun x1' =>
+ app_n x2 (fun x2' =>
+ app_n x3 (fun x3' =>
+ app_n x4 (fun x4' =>
+ app_n x5 (fun x5' =>
+ app_n x6 (fun x6' =>
+ app_n x7 (fun x7' =>
+ app_n x8 (fun x8' =>
+ op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+ @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+ intros. cbv [appify9].
+ repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T)
:= Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op.
Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
Definition curry_unop_wire_digits {T} op : wire_digits -> T
:= Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
+Definition uncurry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
+ := Eval compute in
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x0 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x1 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x2 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x3 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x4 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x5 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x6 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x7 =>
+ uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x8 =>
+ op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
+ := Eval compute in
+ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+ => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8).
+
Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
{ fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}.
Proof.
diff --git a/src/Util/Tower.v b/src/Util/Tower.v
index 6bcd44bf4..e3f57f3ed 100644
--- a/src/Util/Tower.v
+++ b/src/Util/Tower.v
@@ -1,5 +1,22 @@
Require Export Crypto.Util.FixCoqMistakes.
+Definition apply4 {AK BK PA PB ARR}
+ (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B))
+ {A0 A1 A2 A3 : AK} {B : BK}
+ (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PB B)
+ : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 B)))).
+Proof.
+ repeat (apply F; intro); apply f; assumption.
+Defined.
+
+Definition apply4_nd {BK PA PB ARR}
+ (F : forall (B : BK), (PA -> PB B) -> PB (ARR B))
+ {B : BK}
+ (f : PA -> PA -> PA -> PA -> PB B)
+ : PB (ARR (ARR (ARR (ARR B))))
+ := @apply4 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F)
+ tt tt tt tt B f.
+
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}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 04:58:45 +0000