diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-25 13:02:06 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-25 13:02:06 -0500 |
| commit | fbdd082f2b7fab1fb5b074e193f1072d2ecdb2f7 (patch) | |
| tree | 12d81977e0c454de17f63eb357144ca1fe31d9cb /src/Specific/GF25519.v | |
| parent | c51d5c4af858fb38946546b8d47f9d9dbb481cc0 (diff) | |
uncurry_n_op_fe25519
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 357b9dc8a..361cc83a7 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Tower. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. @@ -200,8 +201,20 @@ 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 := Eval compute in fun f => app_10 f (Tuple.curry (n:=length_fe25519) op). + +Fixpoint uncurry_n_op_fe25519 {T} n + : forall (op : Tower.tower_nd fe25519 T n), + Tower.tower_nd Z T (n * length_fe25519) + := match n + return (forall (op : Tower.tower_nd fe25519 T n), + Tower.tower_nd Z T (n * length_fe25519)) + with + | O => fun x => x + | S n' => fun f => uncurry_unop_fe25519 (fun x => @uncurry_n_op_fe25519 _ n' (f x)) + end. + Definition uncurry_binop_fe25519 {T} (op : fe25519 -> fe25519 -> T) - := Eval compute in uncurry_unop_fe25519 (fun f => uncurry_unop_fe25519 (op f)). + := Eval compute in uncurry_n_op_fe25519 2 op. Definition curry_binop_fe25519 {T} op : fe25519 -> fe25519 -> T := Eval compute in appify2 (fun f => curry_unop_fe25519 (curry_unop_fe25519 op f)). @@ -211,17 +224,7 @@ 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))))))))). + := Eval compute in uncurry_n_op_fe25519 9 op. 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 |