chordSlope

formal source

  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
  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