  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
  69  | ECPoint.affine x₁ y₁, ECPoint.affine x₂ y₂ =>
  70      if _hx : x₁ = x₂ then
  71        if _hy : y₁ + y₂ = 0 then
  72          ECPoint.infinity
  73        else
  74          slopeAddPoint (tangentSlope E x₁ y₁) x₁ y₁ x₁
  75      else
  76        slopeAddPoint (chordSlope x₁ y₁ x₂ y₂) x₁ y₁ x₂
  77
  78/-- Scalar multiplication by repeated addition. This is the reference
  79specification, not an efficient implementation. -/
  80def scalarMul {p : ℕ} (E : ShortWeierstrassCurve p) : ℕ → ECPoint p → ECPoint p
  81  | 0, _P => ECPoint.infinity
  82  | n + 1, P => pointAdd E P (scalarMul E n P)
  83
  84/-- Curve-family tag used by the watch harness. -/
  85inductive CurveFamily where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.