`scalarMul`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cryptography.ECDLPWatch on GitHub at line 80.

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

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

papers checked against this theorem

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