diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-07 20:53:32 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-07 20:54:39 -0500 |
| commit | 66b63b406d9c78a0cecbbf89e5baf282231215c5 (patch) | |
| tree | 896390a751dc0f618997784b6f007102d8f9ed17 /src/SpecificGen/GF25519_64BoundedCommon.v | |
| parent | 579cd835006e0cd57c640d0195a507861aaed0b0 (diff) | |
Add appify10
Grrrrrr, code duplication for ladderstep
Diffstat (limited to 'src/SpecificGen/GF25519_64BoundedCommon.v')
| -rw-r--r-- | src/SpecificGen/GF25519_64BoundedCommon.v | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v index b4c8e47ca..519b90fac 100644 --- a/src/SpecificGen/GF25519_64BoundedCommon.v +++ b/src/SpecificGen/GF25519_64BoundedCommon.v @@ -206,6 +206,26 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe25519_64W_correct | ]); reflexivity. Qed. + + Definition appify10 {T} (op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_64W) := + app_fe25519_64W x0 (fun x0' => + app_fe25519_64W x1 (fun x1' => + app_fe25519_64W x2 (fun x2' => + app_fe25519_64W x3 (fun x3' => + app_fe25519_64W x4 (fun x4' => + app_fe25519_64W x5 (fun x5' => + app_fe25519_64W x6 (fun x6' => + app_fe25519_64W x7 (fun x7' => + app_fe25519_64W x8 (fun x8' => + app_fe25519_64W 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_fe25519_64W_correct | ]); reflexivity. + Qed. End generic_destructuring. Definition eta_fe25519_64W_sig (x : fe25519_64W) : { v : fe25519_64W | v = x }. @@ -406,6 +426,24 @@ Definition curry_9op_fe25519_64W {T} op : fe25519_64W -> fe25519_64W -> fe25519_ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W op x0) x1) x2) x3) x4) x5) x6) x7) x8). +Definition uncurry_10op_fe25519_64W {T} (op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T) + := Eval cbv (*-[word128]*) in + uncurry_unop_fe25519_64W (fun x0 => + uncurry_unop_fe25519_64W (fun x1 => + uncurry_unop_fe25519_64W (fun x2 => + uncurry_unop_fe25519_64W (fun x3 => + uncurry_unop_fe25519_64W (fun x4 => + uncurry_unop_fe25519_64W (fun x5 => + uncurry_unop_fe25519_64W (fun x6 => + uncurry_unop_fe25519_64W (fun x7 => + uncurry_unop_fe25519_64W (fun x8 => + uncurry_unop_fe25519_64W (fun x9 => + op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). +Definition curry_10op_fe25519_64W {T} op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T + := Eval cbv (*-[word128]*) in + appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 + => curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). + Definition proj1_fe25519_64W (x : fe25519_64) : fe25519_64W := Eval app_tuple_map in app_fe25519_64 x (HList.mapt (fun _ => (@proj_word _ _))). |