  82  | n + 1, P => pointAdd E P (scalarMul E n P)
  83
  84/-- Curve-family tag used by the watch harness. -/
  85inductive CurveFamily where
  86  | toy
  87  | anomalous
  88  | supersingular
  89  | smallEmbeddingDegree
  90  | ordinaryPrimeOrder
  91  | standardLike
  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

papers checked against this theorem

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