Documentation

Cryptlib.Primitives.Sign.Ed25519_identities

Field identities behind the Edwards/Montgomery transport #

Polynomial identities over ZMod p, proved by linear_combination against v² = u³ + 486662u² + u and c² = -486664. The Edwards image of (u, v) is (x, y) = (-c·u/v, (u-1)/(u+1)).

source
theorem Cryptlib.Primitives.Sign.Ed25519Identities.psi_curve_aux (u v : Ed25519Facts.F) (hv : v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u) (hv0 : v ≠ 0) (hu1 : u + 1 ≠ 0) :
-(-Ed25519Facts.c * u / v) ^ 2 + ((u - 1) / (u + 1)) ^ 2 = 1 + Ed25519Facts.d * (-Ed25519Facts.c * u / v) ^ 2 * ((u - 1) / (u + 1)) ^ 2

The map lands on the Edwards curve.

source
theorem Cryptlib.Primitives.Sign.Ed25519Identities.gen_y (u1 u2 v1 v2 : Ed25519Facts.F) (hv1 : v1 ^ 2 = u1 ^ 3 + 486662 * u1 ^ 2 + u1) (hv2 : v2 ^ 2 = u2 ^ 3 + 486662 * u2 ^ 2 + u2) (hu : u1 - u2 ≠ 0) (hv1' : v1 ≠ 0) (hv2' : v2 ≠ 0) (hu1 : u1 + 1 ≠ 0) (hu2 : u2 + 1 ≠ 0) (h1t : 1 - Ed25519Facts.d * (-Ed25519Facts.c * u1 / v1) * (-Ed25519Facts.c * u2 / v2) * ((u1 - 1) / (u1 + 1)) * ((u2 - 1) / (u2 + 1)) ≠ 0) (hu3 : ((v1 - v2) / (u1 - u2)) ^ 2 - 486662 - u1 - u2 + 1 ≠ 0) :
((u1 - 1) / (u1 + 1) * ((u2 - 1) / (u2 + 1)) + -Ed25519Facts.c * u1 / v1 * (-Ed25519Facts.c * u2 / v2)) / (1 - Ed25519Facts.d * (-Ed25519Facts.c * u1 / v1) * (-Ed25519Facts.c * u2 / v2) * ((u1 - 1) / (u1 + 1)) * ((u2 - 1) / (u2 + 1))) = (((v1 - v2) / (u1 - u2)) ^ 2 - 486662 - u1 - u2 - 1) / (((v1 - v2) / (u1 - u2)) ^ 2 - 486662 - u1 - u2 + 1)

Generic addition (u₁ ≠ u₂), y-coordinate.

source
theorem Cryptlib.Primitives.Sign.Ed25519Identities.gen_x (u1 u2 v1 v2 : Ed25519Facts.F) (hv1 : v1 ^ 2 = u1 ^ 3 + 486662 * u1 ^ 2 + u1) (hv2 : v2 ^ 2 = u2 ^ 3 + 486662 * u2 ^ 2 + u2) (hu : u1 - u2 ≠ 0) (hv1' : v1 ≠ 0) (hv2' : v2 ≠ 0) (hu1 : u1 + 1 ≠ 0) (hu2 : u2 + 1 ≠ 0) (h1t : 1 + Ed25519Facts.d * (-Ed25519Facts.c * u1 / v1) * (-Ed25519Facts.c * u2 / v2) * ((u1 - 1) / (u1 + 1)) * ((u2 - 1) / (u2 + 1)) ≠ 0) (hv3 : -((v1 - v2) / (u1 - u2) * (((v1 - v2) / (u1 - u2)) ^ 2 - 486662 - u1 - u2 - u1) + v1) ≠ 0) :
(-Ed25519Facts.c * u1 / v1 * ((u2 - 1) / (u2 + 1)) + (u1 - 1) / (u1 + 1) * (-Ed25519Facts.c * u2 / v2)) / (1 + Ed25519Facts.d * (-Ed25519Facts.c * u1 / v1) * (-Ed25519Facts.c * u2 / v2) * ((u1 - 1) / (u1 + 1)) * ((u2 - 1) / (u2 + 1))) = -Ed25519Facts.c * (((v1 - v2) / (u1 - u2)) ^ 2 - 486662 - u1 - u2) / -((v1 - v2) / (u1 - u2) * (((v1 - v2) / (u1 - u2)) ^ 2 - 486662 - u1 - u2 - u1) + v1)

Generic addition (u₁ ≠ u₂), x-coordinate.

source
theorem Cryptlib.Primitives.Sign.Ed25519Identities.dbl_y (u v : Ed25519Facts.F) (hv : v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u) (hv' : v ≠ 0) (hu : u + 1 ≠ 0) (h1t : 1 - Ed25519Facts.d * (-Ed25519Facts.c * u / v) * (-Ed25519Facts.c * u / v) * ((u - 1) / (u + 1)) * ((u - 1) / (u + 1)) ≠ 0) (hu3 : ((3 * u ^ 2 + 973324 * u + 1) / (2 * v)) ^ 2 - 486662 - u - u + 1 ≠ 0) :
((u - 1) / (u + 1) * ((u - 1) / (u + 1)) + -Ed25519Facts.c * u / v * (-Ed25519Facts.c * u / v)) / (1 - Ed25519Facts.d * (-Ed25519Facts.c * u / v) * (-Ed25519Facts.c * u / v) * ((u - 1) / (u + 1)) * ((u - 1) / (u + 1))) = (((3 * u ^ 2 + 973324 * u + 1) / (2 * v)) ^ 2 - 486662 - u - u - 1) / (((3 * u ^ 2 + 973324 * u + 1) / (2 * v)) ^ 2 - 486662 - u - u + 1)

Doubling, y-coordinate and x-coordinate.

source
theorem Cryptlib.Primitives.Sign.Ed25519Identities.dbl_x (u v : Ed25519Facts.F) (hv : v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u) (hv' : v ≠ 0) (hu : u + 1 ≠ 0) (h1t : 1 + Ed25519Facts.d * (-Ed25519Facts.c * u / v) * (-Ed25519Facts.c * u / v) * ((u - 1) / (u + 1)) * ((u - 1) / (u + 1)) ≠ 0) (hv3 : -((3 * u ^ 2 + 973324 * u + 1) / (2 * v) * (((3 * u ^ 2 + 973324 * u + 1) / (2 * v)) ^ 2 - 486662 - u - u - u) + v) ≠ 0) :
(-Ed25519Facts.c * u / v * ((u - 1) / (u + 1)) + (u - 1) / (u + 1) * (-Ed25519Facts.c * u / v)) / (1 + Ed25519Facts.d * (-Ed25519Facts.c * u / v) * (-Ed25519Facts.c * u / v) * ((u - 1) / (u + 1)) * ((u - 1) / (u + 1))) = -Ed25519Facts.c * (((3 * u ^ 2 + 973324 * u + 1) / (2 * v)) ^ 2 - 486662 - u - u) / -((3 * u ^ 2 + 973324 * u + 1) / (2 * v) * (((3 * u ^ 2 + 973324 * u + 1) / (2 * v)) ^ 2 - 486662 - u - u - u) + v)