diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-07 21:18:51 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-07 21:19:17 -0500 |
| commit | 4d3d21d604243bc63774f4931f2313e20cdaf515 (patch) | |
| tree | 59de4cc802de57b13128cda7905845200ab0df10 /src/Specific/GF25519.v | |
| parent | fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b (diff) | |
Revert "Add apply10"
This reverts commit fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b.
Revert "copy_bounds"
This reverts commit 4c395e83de3c0baf7f8639fa2fbe2b62ba509682.
Revert "Add Common10_4Op"
This reverts commit 677733838139ff09d4a2dd9ff82258492a9a5bab.
Revert "Add Expr10_4Op"
This reverts commit 540740e8a423d0ec9d1dddb173f772c441dc0a1a.
Revert "Add i10top_correct_and_bounded"
This reverts commit bc4184ce6086971799630a0419881c8d344811ca.
Revert "Add appify10"
This reverts commit 66b63b406d9c78a0cecbbf89e5baf282231215c5.
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index fea289d78..361cc83a7 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -197,26 +197,6 @@ Proof. repeat (etransitivity; [ apply app_10_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : 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' => - app_10 x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - 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 @@ -250,13 +230,6 @@ Definition curry_9op_fe25519 {T} op : fe25519 -> fe25519 -> fe25519 -> fe25519 - 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 uncurry_10op_fe25519 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T) - := Eval compute in uncurry_n_op_fe25519 10 op. -Definition curry_10op_fe25519 {T} op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => 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 (curry_unop_fe25519 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe25519) : { fg : fe25519 | fg = add_opt f g}. Proof. |