slopeAddPoint
slopeAddPoint computes the third affine point on a short Weierstrass curve over ZMod p from the chord slope m together with the x-coordinates of the two summands. Cryptographers auditing ECDLP instances in the watch module cite this helper when checking group-law implementations. The definition is a direct algebraic expansion of the standard addition formulas with no side-condition checks.
claimLet $p$ be a natural number. Given slope $m$ and coordinates $x_1,y_1,x_2$ in the prime field $ZMod p$, the third point is the affine point whose coordinates satisfy $x_3 = m^2 - x_1 - x_2$ and $y_3 = m(x_1 - x_3) - y_1$.
background
The ECDLP Watch module supplies an explicit surface for auditing discrete-logarithm claims on elliptic curves. It fixes a finite carrier ZMod p, a short Weierstrass curve, the set of points including infinity, the chord-tangent group law, scalar multiplication, and an ECDLP solution predicate. ECPoint is the inductive type with constructors infinity and affine x y that packages these points.
proof idea
The definition directly evaluates the usual addition formulas: it sets the new x-coordinate to the square of the slope minus the sum of the input x-coordinates, computes the new y-coordinate from the slope and the difference of x-coordinates, and constructs the affine ECPoint.
why it matters in Recognition Science
This helper is invoked by pointAdd to realize the full chord-tangent addition on the curve. It contributes to the precise mathematical formulation of the ECDLP instance before any Recognition Science invariant is tested. The module isolates ordinary elliptic-curve arithmetic so that downstream checks can be performed cleanly.
scope and limits
- Does not verify that the input points lie on the curve.
- Does not handle doubling, vertical lines, or the point at infinity.
- Does not enforce that m equals the actual chord slope.
- Does not guarantee the output point is nonsingular.
Lean usage
slopeAddPoint m x1 y1 x2formal statement (Lean)
59def slopeAddPoint {p : ℕ} (m x₁ y₁ x₂ : ZMod p) : ECPoint p :=
proof body
Definition body.
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. -/