ShortWeierstrassCurve

formal source

  20open scoped Pointwise
  21
  22/-- Short Weierstrass curve over `ZMod p`: `y^2 = x^3 + a*x + b`. -/
  23structure ShortWeierstrassCurve (p : ℕ) where
  24  a : ZMod p
  25  b : ZMod p
  26
  27/-- Discriminant nonvanishing condition for `y^2 = x^3 + ax + b`. -/
  28def nonsingular {p : ℕ} (E : ShortWeierstrassCurve p) : Prop :=
  29  (4 : ZMod p) * E.a ^ 3 + (27 : ZMod p) * E.b ^ 2 ≠ 0
  30
  31/-- Projective point surface specialized to a short Weierstrass equation. -/
  32inductive ECPoint (p : ℕ) where
  33  | infinity : ECPoint p
  34  | affine : ZMod p → ZMod p → ECPoint p
  35deriving DecidableEq, Repr
  36
  37/-- The curve equation, with infinity admitted as the identity point. -/
  38def onCurve {p : ℕ} (E : ShortWeierstrassCurve p) : ECPoint p → Prop
  39  | ECPoint.infinity => True
  40  | ECPoint.affine x y => y ^ 2 = x ^ 3 + E.a * x + E.b
  41
  42/-- Negation in the elliptic-curve group law. -/
  43def neg {p : ℕ} : ECPoint p → ECPoint p
  44  | ECPoint.infinity => ECPoint.infinity
  45  | ECPoint.affine x y => ECPoint.affine x (-y)
  46
  47instance {p : ℕ} : Neg (ECPoint p) where
  48  neg := neg
  49
  50/-- Chord slope for two distinct affine x-coordinates. -/
  51def chordSlope {p : ℕ} (x₁ y₁ x₂ y₂ : ZMod p) : ZMod p :=
  52  (y₂ - y₁) * (x₂ - x₁)⁻¹
  53