Edwards-side facts: completeness and the special sums

Because d is not a square, the denominators of Ed25519Math.add never vanish on curve points.

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.d_eq : Ed25519Math.d = Ed25519Facts.d

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.onCurve_iff {q : Ed25519Math.Point} : Ed25519Math.onCurve q ↔ -q.x ^ 2 + q.y ^ 2 = 1 + Ed25519Facts.d * q.x ^ 2 * q.y ^ 2

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.d_add_one_ne_zero : Ed25519Facts.d + 1 ≠ 0

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.one_add_d_sq_ne {x y : Ed25519Facts.F} (h : -x ^ 2 + y ^ 2 = 1 + Ed25519Facts.d * x ^ 2 * y ^ 2) : 1 + Ed25519Facts.d * y ^ 2 ≠ 0

On a curve point 1 + d y² ≠ 0.

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.complete {x1 y1 x2 y2 : Ed25519Facts.F} (h1 : -x1 ^ 2 + y1 ^ 2 = 1 + Ed25519Facts.d * x1 ^ 2 * y1 ^ 2) (h2 : -x2 ^ 2 + y2 ^ 2 = 1 + Ed25519Facts.d * x2 ^ 2 * y2 ^ 2) : (Ed25519Facts.d * x1 * x2 * y1 * y2) ^ 2 ≠ 1

Completeness of the Edwards law: the denominators 1 ± d x₁x₂y₁y₂ never vanish on curve points.

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.one_sub_sq_ne {q r : Ed25519Math.Point} (hq : Ed25519Math.onCurve q) (hr : Ed25519Math.onCurve r) : 1 - (Ed25519Facts.d * q.x * r.x * q.y * r.y) ^ 2 ≠ 0

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.one_add_ne {q r : Ed25519Math.Point} (hq : Ed25519Math.onCurve q) (hr : Ed25519Math.onCurve r) : 1 + Ed25519Facts.d * q.x * r.x * q.y * r.y ≠ 0

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.one_sub_ne {q r : Ed25519Math.Point} (hq : Ed25519Math.onCurve q) (hr : Ed25519Math.onCurve r) : 1 - Ed25519Facts.d * q.x * r.x * q.y * r.y ≠ 0

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.add_def (q r : Ed25519Math.Point) : Ed25519Math.add q r = { x := (q.x * r.y + q.y * r.x) / (1 + Ed25519Facts.d * q.x * r.x * q.y * r.y), y := (q.y * r.y + q.x * r.x) / (1 - Ed25519Facts.d * q.x * r.x * q.y * r.y) }

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.add_comm' (q r : Ed25519Math.Point) : Ed25519Math.add q r = Ed25519Math.add r q

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.add_two_torsion (q : Ed25519Math.Point) : Ed25519Math.add q { x := 0, y := -1 } = { x := -q.x, y := -q.y }

Adding the order-2 point (0, -1) negates both coordinates.

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.add_zero' (q : Ed25519Math.Point) : Ed25519Math.add q Ed25519Math.zero = q

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.zero_add' (q : Ed25519Math.Point) : Ed25519Math.add Ed25519Math.zero q = q

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.add_neg (q : Ed25519Math.Point) (hq : Ed25519Math.onCurve q) : Ed25519Math.add q { x := -q.x, y := q.y } = Ed25519Math.zero

q + (-x, y) = (0, 1): the negative of (x, y) is (-x, y).

theorem Cryptlib.Primitives.Sign.Ed25519Edwards.add_conj (q : Ed25519Math.Point) (hq : Ed25519Math.onCurve q) : Ed25519Math.add q { x := q.x, y := -q.y } = { x := 0, y := -1 }

q + (x, -y) = (0, -1).