def
definition
tangentSlope
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 55.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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