ECDLPInstance
plain-language theorem explainer
An ECDLPInstance packages a short Weierstrass curve over ZMod p, base point P, target point Q, order, cofactor and curve-family tag together with proofs that the curve is nonsingular and both points lie on it. Auditors of elliptic-curve discrete-log claims cite the structure to fix the public data before any Recognition Science invariant is applied. The declaration is a plain record type that collects the instance data and the three validity conditions.
Claim. An ECDLP instance over modulus $p$ consists of a short Weierstrass curve $E: y^2 = x^3 + a x + b$ with $a,b$ in $ZMod p$, points $P$ and $Q$ on $E$, integers $n$ (order) and $h$ (cofactor), and a curve-family tag, together with proofs that the discriminant $4a^3 + 27b^2$ is nonzero and that both $P$ and $Q$ satisfy the curve equation.
background
The ECDLP Watch module supplies a minimal surface for stating elliptic-curve discrete-log instances before any Recognition Science test is applied. A ShortWeierstrassCurve is the equation $y^2 = x^3 + a x + b$ over $ZMod p$. ECPoint is either the point at infinity or an affine pair $(x,y)$. The predicate nonsingular requires the discriminant $4a^3 + 27b^2$ to be nonzero in $ZMod p$, while onCurve checks that a point satisfies the curve equation or is infinity. CurveFamily supplies tags such as toy, anomalous or supersingular.
proof idea
The declaration is a structure definition that packages the curve, base and target points, order, cofactor and family tag together with the three proof obligations curve_ok, base_on_curve and target_on_curve. No lemmas are invoked; the structure simply records the data and the validity predicates nonsingular and onCurve.
why it matters
This structure supplies the concrete instance that the downstream predicate isSolution consumes to test whether a candidate scalar $k$ satisfies scalarMul curve $k$ base = target with $k < order$. It appears in the ECDLP Watch Surface whose purpose is to make the ordinary ECDLP precise before any RS candidate invariant is tested. The construction ensures that later invariants can be stated using only the public data fields exposed by PublicECDLPData.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.