diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-06-27 19:11:36 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-06-27 19:11:36 -0400 |
commit | c003b54c8d3d92d3a2805d0469b1ee69af349764 (patch) | |
tree | f6d567fce900a1bc885f7af8eebefa2074e52ab6 /src | |
parent | 5397ade1bd1616de6658edc5322765b3c1c04d06 (diff) |
match C code in Jacobian addition
Diffstat (limited to 'src')
-rw-r--r-- | src/Curves/Weierstrass/Jacobian/Precomputed.v | 15 | ||||
-rw-r--r-- | src/Specific/NISTP256/AMD64/icc/measurements.txt | 1 | ||||
-rw-r--r-- | src/Specific/NISTP256/AMD64/measurements.txt | 1 | ||||
-rw-r--r-- | src/Specific/X25519/C64/measurements.txt | 2 |
4 files changed, 14 insertions, 5 deletions
diff --git a/src/Curves/Weierstrass/Jacobian/Precomputed.v b/src/Curves/Weierstrass/Jacobian/Precomputed.v index c52cbc7b8..75aa6bf53 100644 --- a/src/Curves/Weierstrass/Jacobian/Precomputed.v +++ b/src/Curves/Weierstrass/Jacobian/Precomputed.v @@ -72,26 +72,33 @@ Module Jacobian. let '(X1, Y1, Z1) := P in let '(X2, Y2) := Q in dlet ZZ : F := Z1^2 in + dlet P1z := if dec (Z1 = 0) then true else false in dlet U2 : F := ZZ * X2 in + dlet X2z := if dec (X2 = 0) then true else false in dlet ZZZ: F := ZZ * Z1 in dlet H : F := U2 - X1 in dlet Z3 : F := Z1 * H in + dlet P2z := if dec (Y2 = 0) then X2z else false in dlet S2 : F := ZZZ * Y2 in dlet R : F := S2 - Y1 in dlet HH : F := H^2 in dlet RR : F := R^2 in dlet HHH: F := HH*H in + dlet Z3 := if P1z then 1 else Z3 in + dlet Z3 := if P2z then Z1 else Z3 in dlet HHX : F := HH * X1 in dlet T10 : F := HHX + HHX in dlet E4 : F := RR - T10 in dlet X3 : F := E4 - HHH in + dlet X3 := if P1z then X2 else X3 in + dlet X3 := if P2z then X1 else X3 in dlet T13 : F := HHH * Y1 in dlet T11 : F := HHX - X3 in dlet T12 : F := T11 * R in dlet Y3 : F := T12 - T13 in - if dec (X2 = 0 /\ Y2 = 0) then P else - if dec (Z1 = 0) then (X2, Y2, 1) - else (X3, Y3, Z3). + dlet Y3 := if P1z then Y2 else Y3 in + dlet Y3 := if P2z then Y1 else Y3 in + (X3, Y3, Z3). Definition affine_of_table (P:F*F) := let '(x, y) := P in if dec (x = 0 /\ y = 0) then inr tt else inl (x,y). @@ -112,7 +119,7 @@ Module Jacobian. (HPQ:~ W.eq (to_affine P) Q) : let '(X, Y, Z) := add_affine_coordinates (proj1_sig P) q in if dec (Z = 0) then True else Y^2 = X^3 + a * X * (Z^2)^2 + b * (Z^3)^2. - Proof. prept; not_and_t. par: abstract fsatz. Qed. + Proof. prept; not_and_t. all: try abstract fsatz. Qed. Lemma add_affine_coordinates_correct (P:point) (q:F*F) pf (Q:=exist _ (affine_of_table q) pf) diff --git a/src/Specific/NISTP256/AMD64/icc/measurements.txt b/src/Specific/NISTP256/AMD64/icc/measurements.txt index 17abbfe2d..18729ea40 100644 --- a/src/Specific/NISTP256/AMD64/icc/measurements.txt +++ b/src/Specific/NISTP256/AMD64/icc/measurements.txt @@ -1 +1,2 @@ 1140 ashryn-noht-notb-noac-broadwell 2.60ghz 7.1.1 cac291e0 +1144 ashryn-noht-notb-ac-broadwell 2.60ghz 7.1.1 5397ade1 diff --git a/src/Specific/NISTP256/AMD64/measurements.txt b/src/Specific/NISTP256/AMD64/measurements.txt index 66745d40c..ac19ef2f4 100644 --- a/src/Specific/NISTP256/AMD64/measurements.txt +++ b/src/Specific/NISTP256/AMD64/measurements.txt @@ -1 +1,2 @@ +1576 ashryn-noht-notb-ac-broadwell 2.60ghz 7.1.1 5397ade1 1576 ashryn-noht-notb-noac-broadwell 2.60ghz 7.1.1 cac291e0 diff --git a/src/Specific/X25519/C64/measurements.txt b/src/Specific/X25519/C64/measurements.txt index 3782c59c5..2d8255c11 100644 --- a/src/Specific/X25519/C64/measurements.txt +++ b/src/Specific/X25519/C64/measurements.txt @@ -1,4 +1,4 @@ 156081 ashryn-ht-tb-ac-broadwell 2.78ghz 7.1.1 83ddc573 +168380 ashryn-noht-notb-ac-broadwell 2.60ghz 7.1.1 5397ade1 168628 ashryn-noht-notb-noac-broadwell 2.60ghz 7.1.1 cac291e0 -174300 ashryn-noht-notb-ac-broadwell 2.50ghz 7.1.1 4dc08623 187992 jgross-Leopard-WS-ht-tb-nops-haswell 3.70ghz 5.4.0 19a7001 |