IndisputableMonolith.Cryptography.ECDLPWatch

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# ECDLP Watch Surface
   6
   7This module defines a small, explicit surface for auditing elliptic-curve
   8discrete logarithm claims. It is not an attack module.
   9
  10The goal is to make the ordinary mathematical problem precise before testing
  11any RS candidate invariant: a finite carrier `ZMod p`, a short Weierstrass
  12curve, points including infinity, the chord-tangent group operation, scalar
  13multiplication, and an ECDLP solution predicate.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Cryptography
  18namespace ECDLPWatch
  19
  20open scoped Pointwise
  21
  22/-- Short Weierstrass curve over `ZMod p`: `y^2 = x^3 + a*x + b`. -/
  23structure ShortWeierstrassCurve (p : ℕ) where
  24  a : ZMod p
  25  b : ZMod p
  26
  27/-- Discriminant nonvanishing condition for `y^2 = x^3 + ax + b`. -/
  28def nonsingular {p : ℕ} (E : ShortWeierstrassCurve p) : Prop :=
  29  (4 : ZMod p) * E.a ^ 3 + (27 : ZMod p) * E.b ^ 2 ≠ 0
  30
  31/-- Projective point surface specialized to a short Weierstrass equation. -/
  32inductive ECPoint (p : ℕ) where
  33  | infinity : ECPoint p
  34  | affine : ZMod p → ZMod p → ECPoint p
  35deriving DecidableEq, Repr
  36
  37/-- The curve equation, with infinity admitted as the identity point. -/
  38def onCurve {p : ℕ} (E : ShortWeierstrassCurve p) : ECPoint p → Prop
  39  | ECPoint.infinity => True
  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
  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
  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
 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
 126  family := inst.family
 127
 128/-- A watch invariant is admissible only if it is computed from public data. -/
 129structure PublicInvariant where
 130  score : ∀ {p : ℕ}, PublicECDLPData p → ℝ
 131
 132/-- Known weak-curve classes must be separated from any standard-curve claim. -/
 133def isKnownWeakFamily : CurveFamily → Prop
 134  | CurveFamily.anomalous => True
 135  | CurveFamily.supersingular => True
 136  | CurveFamily.smallEmbeddingDegree => True
 137  | _ => False
 138
 139/-- Watch predicate: a candidate invariant is being tested only on public data
 140and against an explicitly tagged curve family. This carries no security claim. -/
 141structure InvariantWatchRecord (I : PublicInvariant) where
 142  family : CurveFamily
 143  weak_family_tagged : isKnownWeakFamily family ∨ ¬ isKnownWeakFamily family
 144
 145end ECDLPWatch
 146end Cryptography
 147end IndisputableMonolith
 148