def
definition
pointAdd
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cryptography.ECDLPWatch on GitHub at line 66.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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