ECDLPInstance

formal source

  92deriving DecidableEq, Repr
  93
  94/-- Minimal ECDLP instance: recover `k` from `Q = kP`. -/
  95structure ECDLPInstance (p : ℕ) where
  96  curve : ShortWeierstrassCurve p
  97  base : ECPoint p
  98  target : ECPoint p
  99  order : ℕ
 100  cofactor : ℕ
 101  family : CurveFamily
 102  curve_ok : nonsingular curve
 103  base_on_curve : onCurve curve base
 104  target_on_curve : onCurve curve target
 105
 106/-- Candidate solution predicate for the elliptic-curve discrete log problem. -/
 107def isSolution {p : ℕ} (inst : ECDLPInstance p) (k : ℕ) : Prop :=
 108  k < inst.order ∧ scalarMul inst.curve k inst.base = inst.target
 109
 110/-- Public data available to an adversary. This structure exists to keep later
 111RS invariants honest: they may depend only on these fields. -/
 112structure PublicECDLPData (p : ℕ) where
 113  curve : ShortWeierstrassCurve p
 114  base : ECPoint p
 115  target : ECPoint p
 116  order : ℕ
 117  cofactor : ℕ
 118  family : CurveFamily
 119
 120def ECDLPInstance.publicData {p : ℕ} (inst : ECDLPInstance p) : PublicECDLPData p where
 121  curve := inst.curve
 122  base := inst.base
 123  target := inst.target
 124  order := inst.order
 125  cofactor := inst.cofactor