Ed25519's group law, by transport from Curve25519 #

Transports Mathlib's group on NIKE.X25519.Point across the birational map

ψ : Curve25519 → Edwards,   (u, v) ↦ (x, y) = (-c·u/v, (u-1)/(u+1)),   c² = -486664,

and proves ψ (P + Q) = Ed25519Math.add (ψ P) (ψ Q) for all P Q, including the identity and the order-2 point T = (0,0), which ψ sends to (0,-1).

source

@[reducible, inline]

abbrev Cryptlib.Primitives.Sign.Ed25519Group.W :

Type

Equations

Cryptlib.Primitives.Sign.Ed25519Group.W = Cryptlib.Primitives.NIKE.X25519.Point

Instances For

source

@[reducible, inline]

abbrev Cryptlib.Primitives.Sign.Ed25519Group.curve :

WeierstrassCurve.Affine (ZMod NIKE.X25519Common.p)

Equations

Cryptlib.Primitives.Sign.Ed25519Group.curve = Cryptlib.Primitives.NIKE.X25519.curve

Instances For

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.w_eq {u v : Ed25519Facts.F} (h : curve.Nonsingular u v) :

v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u

The curve equation on the Curve25519 side.

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.w_ns {u v : Ed25519Facts.F} (h : v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u) :

curve.Nonsingular u v

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.u_add_one_ne {u v : Ed25519Facts.F} (hv : v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u) :

u + 1 ≠ 0

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.u_eq_zero_of_v_eq_zero {u v : Ed25519Facts.F} (hv : v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u) (h0 : v = 0) :

u = 0

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.v_ne_zero_of_u_ne_zero {u v : Ed25519Facts.F} (hv : v ^ 2 = u ^ 3 + 486662 * u ^ 2 + u) (hu : u ≠ 0) :

v ≠ 0

source

def Cryptlib.Primitives.Sign.Ed25519Group.psi :

W → Ed25519Math.Point

The map Curve25519 → Edwards. Sends infinity to the identity and (0,0) to (0,-1).

Equations

Cryptlib.Primitives.Sign.Ed25519Group.psi WeierstrassCurve.Affine.Point.zero = { x := 0, y := 1 }
Cryptlib.Primitives.Sign.Ed25519Group.psi (WeierstrassCurve.Affine.Point.some u v h) = { x := -Cryptlib.Primitives.Sign.Ed25519Facts.c * u / v, y := (u - 1) / (u + 1) }

Instances For

source

@[simp]

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_zero :

psi 0 = { x := 0, y := 1 }

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_some {u v : Ed25519Facts.F} (h : curve.Nonsingular u v) :

psi (WeierstrassCurve.Affine.Point.some u v h) = { x := -Ed25519Facts.c * u / v, y := (u - 1) / (u + 1) }

source

def Cryptlib.Primitives.Sign.Ed25519Group.T :

The order-2 point (0, 0).

Equations

Cryptlib.Primitives.Sign.Ed25519Group.T = WeierstrassCurve.Affine.Point.some 0 0 Cryptlib.Primitives.Sign.Ed25519Group.T._proof_1

Instances For

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_T :

psi T = { x := 0, y := -1 }

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_onCurve (P : W) :

Ed25519Math.onCurve (psi P)

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_neg (P : W) :

psi (-P) = { x := -(psi P).x, y := (psi P).y }

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.some_congr {x x' y y' : Ed25519Facts.F} {h : curve.Nonsingular x y} {h' : curve.Nonsingular x' y'} (hx : x = x') (hy : y = y') :

WeierstrassCurve.Affine.Point.some x y h = WeierstrassCurve.Affine.Point.some x' y' h'

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.curve_a₁ :

curve.a₁ = 0

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.curve_a₂ :

curve.a₂ = 486662

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.curve_a₃ :

curve.a₃ = 0

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.curve_a₄ :

curve.a₄ = 1

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.addX_eq (x1 x2 l : Ed25519Facts.F) :

curve.addX x1 x2 l = l ^ 2 - 486662 - x1 - x2

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.addY_eq (x1 x2 y1 l : Ed25519Facts.F) :

curve.addY x1 x2 y1 l = -(l * (l ^ 2 - 486662 - x1 - x2 - x1) + y1)

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.negY_eq (x y : Ed25519Facts.F) :

curve.negY x y = -y

source

def Cryptlib.Primitives.Sign.Ed25519Group.U3 (u1 u2 v1 v2 : Ed25519Facts.F) :

Ed25519Facts.F

u-coordinate of P + Q for u₁ ≠ u₂.

Equations

Cryptlib.Primitives.Sign.Ed25519Group.U3 u1 u2 v1 v2 = ((v1 - v2) / (u1 - u2)) ^ 2 - 486662 - u1 - u2

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Group.V3 (u1 u2 v1 v2 : Ed25519Facts.F) :

Ed25519Facts.F

v-coordinate of P + Q for u₁ ≠ u₂.

Equations

Cryptlib.Primitives.Sign.Ed25519Group.V3 u1 u2 v1 v2 = -((v1 - v2) / (u1 - u2) * (Cryptlib.Primitives.Sign.Ed25519Group.U3 u1 u2 v1 v2 - u1) + v1)

Instances For

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.add_X_ne_eq {u1 v1 u2 v2 : Ed25519Facts.F} (h1 : curve.Nonsingular u1 v1) (h2 : curve.Nonsingular u2 v2) (hne : u1 ≠ u2) :

∃ (h3 : curve.Nonsingular (U3 u1 u2 v1 v2) (V3 u1 u2 v1 v2)), WeierstrassCurve.Affine.Point.some u1 v1 h1 + WeierstrassCurve.Affine.Point.some u2 v2 h2 = WeierstrassCurve.Affine.Point.some (U3 u1 u2 v1 v2) (V3 u1 u2 v1 v2) h3

source

def Cryptlib.Primitives.Sign.Ed25519Group.U3d (u v : Ed25519Facts.F) :

Ed25519Facts.F

u-coordinate of 2P.

Equations

Cryptlib.Primitives.Sign.Ed25519Group.U3d u v = ((3 * u ^ 2 + 973324 * u + 1) / (2 * v)) ^ 2 - 486662 - u - u

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Group.V3d (u v : Ed25519Facts.F) :

Ed25519Facts.F

v-coordinate of 2P.

Equations

Cryptlib.Primitives.Sign.Ed25519Group.V3d u v = -((3 * u ^ 2 + 973324 * u + 1) / (2 * v) * (Cryptlib.Primitives.Sign.Ed25519Group.U3d u v - u) + v)

Instances For

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.add_double_eq {u v : Ed25519Facts.F} (h : curve.Nonsingular u v) (hv : v ≠ 0) :

∃ (h3 : curve.Nonsingular (U3d u v) (V3d u v)), WeierstrassCurve.Affine.Point.some u v h + WeierstrassCurve.Affine.Point.some u v h = WeierstrassCurve.Affine.Point.some (U3d u v) (V3d u v) h3

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.T_add_T :

T + T = 0

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_add_T (P : W) :

psi (P + T) = { x := -(psi P).x, y := -(psi P).y }

Adding the order-2 point T negates both Edwards coordinates.

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.eq_T_of_v_zero {u v : Ed25519Facts.F} (h : curve.Nonsingular u v) (hv0 : v = 0) :

WeierstrassCurve.Affine.Point.some u v h = T

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_add_of_sum_zero {P Q : W} (hs : P + Q = 0) :

psi (P + Q) = Ed25519Math.add (psi P) (psi Q)

If P + Q = 0 then Q = -P, and Edwards add of a point with its negative is the identity.

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_add_of_sum_T {P Q : W} (hs : P + Q = T) :

psi (P + Q) = Ed25519Math.add (psi P) (psi Q)

If P + Q = T then Q = -P + T, so ψ Q = (x, -y), and Edwards add gives (0,-1) = ψ T.

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_add_gen {u1 v1 u2 v2 : Ed25519Facts.F} (h1 : curve.Nonsingular u1 v1) (h2 : curve.Nonsingular u2 v2) (hne : u1 ≠ u2) (hv1' : v1 ≠ 0) (hv2' : v2 ≠ 0) (hV : V3 u1 u2 v1 v2 ≠ 0) :

psi (WeierstrassCurve.Affine.Point.some u1 v1 h1 + WeierstrassCurve.Affine.Point.some u2 v2 h2) = Ed25519Math.add (psi (WeierstrassCurve.Affine.Point.some u1 v1 h1)) (psi (WeierstrassCurve.Affine.Point.some u2 v2 h2))

Generic addition of two points with u₁ ≠ u₂, neither of order 2, sum not of order 2.

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_add_dbl {u v : Ed25519Facts.F} (h : curve.Nonsingular u v) (hv' : v ≠ 0) (hV : V3d u v ≠ 0) :

psi (WeierstrassCurve.Affine.Point.some u v h + WeierstrassCurve.Affine.Point.some u v h) = Ed25519Math.add (psi (WeierstrassCurve.Affine.Point.some u v h)) (psi (WeierstrassCurve.Affine.Point.some u v h))

Doubling a point not of order 2, when 2P is not of order 2.

source

theorem Cryptlib.Primitives.Sign.Ed25519Group.psi_add (P Q : W) :

psi (P + Q) = Ed25519Math.add (psi P) (psi Q)

ψ is a homomorphism.

Documentation

Cryptlib.Primitives.Sign.Ed25519_group

Ed25519's group law, by transport from Curve25519 #