onCurve

formal source

  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
  54/-- Tangent slope for point doubling. -/
  55def tangentSlope {p : ℕ} (E : ShortWeierstrassCurve p) (x y : ZMod p) : ZMod p :=
  56  ((3 : ZMod p) * x ^ 2 + E.a) * ((2 : ZMod p) * y)⁻¹
  57
  58/-- Third point obtained from the usual slope formula. -/
  59def slopeAddPoint {p : ℕ} (m x₁ y₁ x₂ : ZMod p) : ECPoint p :=
  60  let x₃ := m ^ 2 - x₁ - x₂
  61  let y₃ := m * (x₁ - x₃) - y₁
  62  ECPoint.affine x₃ y₃
  63
  64/-- Total chord-tangent addition formula. The usual prime-field side
  65conditions are carried separately by benchmark code and hypotheses. -/
  66def pointAdd {p : ℕ} (E : ShortWeierstrassCurve p) : ECPoint p → ECPoint p → ECPoint p
  67  | ECPoint.infinity, Q => Q
  68  | P, ECPoint.infinity => P