`neg`

definition

show as: view math explainer →

module: IndisputableMonolith.Cryptography.ECDLPWatch
domain: Cryptography
line: 43 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cryptography.ECDLPWatch on GitHub at line 43.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

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

papers checked against this theorem

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