diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 22:40:56 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 22:41:17 -0500 |
| commit | 53f706757c81a1a57b479c6700b518965f32e862 (patch) | |
| tree | 34facaaa024248326d9c232ffea04045685dab36 /src/Specific | |
| parent | 2045f9ffb67c72363871c7cae2a1d1fb996e0306 (diff) | |
Better extraction
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519BoundedAddCoordinates.v | 20 | ||||
| -rw-r--r-- | src/Specific/GF25519BoundedExtendedAddCoordinates.v | 9 |
2 files changed, 18 insertions, 11 deletions
diff --git a/src/Specific/GF25519BoundedAddCoordinates.v b/src/Specific/GF25519BoundedAddCoordinates.v index 141c950bb..cbc8666ea 100644 --- a/src/Specific/GF25519BoundedAddCoordinates.v +++ b/src/Specific/GF25519BoundedAddCoordinates.v @@ -27,16 +27,16 @@ Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coo Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed. Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem := - refine (HList.mapt exist_fe25519W - (ts:=opW (proj1_fe25519W x0) - (proj1_fe25519W x1) - (proj1_fe25519W x2) - (proj1_fe25519W x3) - (proj1_fe25519W x4) - (proj1_fe25519W x5) - (proj1_fe25519W x6) - (proj1_fe25519W x7) - (proj1_fe25519W x8)) _); + refine (let ts := opW (proj1_fe25519W x0) + (proj1_fe25519W x1) + (proj1_fe25519W x2) + (proj1_fe25519W x3) + (proj1_fe25519W x4) + (proj1_fe25519W x5) + (proj1_fe25519W x6) + (proj1_fe25519W x7) + (proj1_fe25519W x8) in + HList.mapt exist_fe25519W (ts:=ts) _); abstract ( rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe25519WToZ)); apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe25519 diff --git a/src/Specific/GF25519BoundedExtendedAddCoordinates.v b/src/Specific/GF25519BoundedExtendedAddCoordinates.v index 3910edab8..cb42b9e7f 100644 --- a/src/Specific/GF25519BoundedExtendedAddCoordinates.v +++ b/src/Specific/GF25519BoundedExtendedAddCoordinates.v @@ -41,12 +41,19 @@ Proof. end. Qed. -Definition add_coordinates twice_d P1 P2 +Definition add_coordinates' twice_d P1 P2 := let '(P10, P11, P12, P13) := P1 in let '(P20, P21, P22, P23) := P2 in @GF25519BoundedAddCoordinates.add_coordinates twice_d P10 P11 P12 P13 P20 P21 P22 P23. +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF25519BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF25519BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + Lemma add_coordinates_correct_full twice_d P1 P2 : Tuple.fieldwise GF25519BoundedCommon.eq |