Curve25519 as an abelian group #
Defines Curve25519 abstractly as an additive commutative group, with a
distinguished generator and an x-coordinate projection to the field
𝔽_p where p = 2²⁵⁵ − 19. The group structure itself is treated as a
black box — realising it from the curve equation requires Mathlib-level
Montgomery-curve algebraic geometry that is not in place yet.
This gives a concrete target for the ladder correctness theorem in
MontgomeryLadder.lean: specialising it to G = Curve25519 yields a
concrete statement about X25519 scalar multiplication.
What this file establishes #
curve25519Prime : ℕ = 2²⁵⁵ − 19, the Curve25519 base field prime.Fp25519, a type alias forZMod curve25519Prime.Curve25519— an abstract abelian group (assumed as a parameter).curve25519Generator : Curve25519— distinguished generator (u = 9).x25519 : ℕ → Curve25519 → Curve25519— scalar multiplication, defined viansmulfrom the group structure.x25519_eq_ladder— the ladder computes X25519 scalar multiplication.
What remains (the fiat-crypto trust edge) #
- Realising
Curve25519as{ P : Fp25519 × Fp25519 // y² = x³ + Ax² + x }with an explicit group law. ~3–6 weeks of Mathlib-style work, or trust the Rocq proof in fiat-crypto. - Connecting the abstract
Curve25519to the concreteFp25519-valuedxProjfromMontgomeryXOnly.MontyCurveGroup.
References #
- RFC 7748, "Elliptic Curves for Security" (defines X25519).
- Bernstein, "Curve25519: new Diffie-Hellman speed records", PKC 2006.
Base field #
Curve25519 base-field prime p = 2²⁵⁵ − 19.
Equations
- CatCrypt.Crypto.ECC.curve25519Prime = 2 ^ 255 - 19
Instances For
The prime is positive (for Fact (0 < p) instance).
Base field for Curve25519 arithmetic.
Instances For
Abstract group structure #
We take Curve25519 to be any abelian group together with a
distinguished generator. This abstracts the details of the
curve-point implementation. Security proofs reduce X25519 to DDH
on this abstract group.
x25519 k P computes k · P in the group G. For G = Curve25519
and P = generator, this is the X25519 scalar multiplication.
Equations
- CatCrypt.Crypto.ECC.x25519 k P = k • P
Instances For
The Montgomery ladder computes x25519. This is the corollary of
ladderFold_fst_eq_nsmul tailored to the X25519 setting.
Two X25519 scalar multiplications commute (DH property). This follows from commutativity of the abelian group action.
Concrete Curve25519 as a Weierstrass point group #
We instantiate Curve25519 concretely as the points on the Montgomery-form
Weierstrass curve y² = x³ + 486662·x² + x over Fp25519. The
AddCommGroup is inherited from Mathlib's proved group law on affine
Weierstrass points; the MontyCurveGroup instance is closed via
montgomeryW_MontyCurveGroup from MontgomeryAsWeierstrass.lean.
Trust edge #
Proving Nat.Prime (2²⁵⁵ − 19) in Lean requires a Pratt certificate
that is both costly to construct and kernel-check. Mirroring the Rocq
AUCurves development (which uses Spec/XEdDSA_Curve25519.v abstractly
over Z/pZ without discharging primality) and standard fiat-crypto
convention, we take primality as an axiom. It is one of four
AUCurves-bridged trust edges in this file — each documented at its
definition and imported across the Rocq↔Lean boundary:
curve25519Prime_prime (base-field prime), curve25519SubgroupOrder_prime
(the subgroup order l is prime), and curve25519_basepoint /
curve25519_basepoint_addOrder (the RFC 7748 base point and its order l).
Everything else — including the unconditional ladder capstone
x25519_ladder_correct_basepoint — is proved.
Trust edge: Curve25519's base-field modulus is prime. Registered
as an axiom because proving Nat.Prime (2²⁵⁵ − 19) in Lean requires
a costly Pocklington/Pratt certificate; this is already discharged
in the Rocq AUCurves development and we import it across the
Rocq↔Lean boundary.
curve25519Prime ≠ 2. Needed for (2 : Fp25519) ≠ 0.
(2 : Fp25519) ≠ 0 — follows from 2 < curve25519Prime.
Concrete Curve25519: points on the Montgomery-as-Weierstrass curve
over Fp25519. Inherits AddCommGroup from Mathlib's
WeierstrassCurve.Affine.Point.
Equations
Instances For
Concrete MontyCurveGroup instance for Curve25519. The x-only
formulas xdbl and xdadd correctly compute scalar multiplication
on Curve25519Point.
Equations
Instances For
xProj is negation-invariant on Curve25519 (instance specialisation of
xProjW_neg).
Field-level ladder correctness for Curve25519 #
xladderFold_curve25519_correct is the end-to-end algebraic theorem:
running the field-level x-only ladder on xProj P and a bit-list produces
a projective x-coordinate matching k • P where k = bitsToNat bits.
Requires nondegeneracy of the ladder's intermediate xdbl/xdadd outputs
along the entire scalar-multiplication path — a scalar-specific hypothesis
(on Curve25519's prime-order subgroup, this holds for non-identity base
points and non-zero scalars below the subgroup order).
Curve25519 subgroup order (AUCurves bridge) #
The order of Curve25519's prime-order subgroup — equivalently the order of the
RFC 7748 base point u = 9 — is
l = 2^252 + 27742317777372353535851937790883648493. It bounds the scalar range
the Montgomery ladder traverses, and its primality is what makes every
intermediate n • B (for 0 < n < l) non-identity, hence projectively
nondegenerate — the group-theoretic half of discharging LadderNondeg.
Order of Curve25519's prime-order subgroup / of the base point u = 9.
Equations
- CatCrypt.Crypto.ECC.curve25519SubgroupOrder = 2 ^ 252 + 27742317777372353535851937790883648493
Instances For
l is prime. Bridged across the Rocq↔Lean boundary from the AUCurves
development — E_basepoint_order in Spec/Curve25519_BasepointOrder.v
establishes l • B = 0 (Qed-sealed; its Montgomery-side link
scalarmult_l_eq_zero is tactic-complete but left Admitted there only
because the Coq kernel-check times out), and the quotient E/E[4] has prime
order l in fiat-crypto's Spec/Ristretto255.v. Imported here as an axiom
exactly as curve25519Prime_prime is. This underpins the cyclic-subgroup
argument that n • B ≠ 0 for 0 < n < l, the group-theoretic input to
discharging the LadderNondeg side-condition of x25519_ladder_correct.
The remaining, field-algebraic half — that xdbl/xdadd outputs on
non-identity affine points are (0,0)-free — plus a concrete
Curve25519Point basepoint of order l, together turn x25519_ladder_correct
unconditional in the intended regime; that proof is not yet carried here.
Combined nondegeneracy hypothesis over a list of bits: at every point of the ladder run, the intermediate projective outputs are nondegenerate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Field-level ladder correctness for Curve25519.
xladderFold, applied to xProj P and a bit-list, satisfies the
projective-equivalence invariant with the abstract-group ladder.
End-to-end X25519 field-level scalar-multiplication theorem
(conditional on ladder nondegeneracy).
The first component of the field-level Montgomery ladder run on
xProj P for bit-list bits is projectively equivalent to
xProj (x25519 (bitsToNat bits) P) — i.e., the x-coordinate of the
abstract-group scalar multiplication.
The hypothesis hND : LadderNondeg P bits is required and is left
undischarged here. It asserts that every intermediate xdbl/xdadd
output along the scalar-multiplication path is projectively nondegenerate.
On Curve25519's prime-order subgroup this holds for a non-identity base
point and scalars below the subgroup order curve25519SubgroupOrder (l),
so the theorem is unconditional in the intended regime. The group-theoretic
input to discharging it — that n • B ≠ 0 for 0 < n < l — follows from
curve25519SubgroupOrder_prime (the AUCurves order bridge); the remaining
field-algebraic step (xdbl/xdadd non-(0,0) on non-identity affine
points) plus a concrete order-l basepoint would remove hND entirely.
Until that lands, read this as correctness wherever the ladder path stays
nondegenerate, not as an unconditional identity.
Unconditional ladder nondegeneracy for the RFC 7748 basepoint #
The RFC 7748 base point B (u = 9) generates Curve25519's prime-order
subgroup of order l = curve25519SubgroupOrder. Because l is an odd prime,
no non-identity multiple n • B (0 < n < l) is a 4-torsion point, and this
is exactly what makes every intermediate xdbl/xdadd output along the ladder
path projectively nondegenerate. This section discharges LadderNondeg for the
base point unconditionally, removing the hND side condition from
x25519_ladder_correct.
Small field elements are nonzero: n < curve25519Prime for n ≤ 2000000.
16 · a24 ≠ 0 in Fp25519 (a24 = 121666).
16 · a24 − 16 ≠ 0 in Fp25519 (16·(121666−1)).
Curve25519 base point (AUCurves bridge) #
curve25519_basepoint is the RFC 7748 base point u = 9 as a concrete
Curve25519Point, and curve25519_basepoint_addOrder records that its order in
the Weierstrass group is l = curve25519SubgroupOrder. Both are bridged across
the Rocq↔Lean boundary from the AUCurves development: E_basepoint_order in
Spec/Curve25519_BasepointOrder.v establishes l • B = 0 (with l the prime
subgroup order of E/E[4] from fiat-crypto's Spec/Ristretto255.v), and the
minimality of l as the additive order follows there from primality of l
together with B ≠ 0. Imported here as axioms exactly as curve25519Prime_prime
and curve25519SubgroupOrder_prime are; everything downstream of them is proved.
AUCurves bridge: an order-l point of the Curve25519 group. Only its
additive order is constrained (by curve25519_basepoint_addOrder); nothing
here pins its x-coordinate. The intended instantiation is the RFC 7748 base
point u = 9, but because only the order is used, the capstone
x25519_ladder_correct_basepoint in fact holds for any order-l point
(u = 9 included) — a generalisation, not a weakening. Pinning xProj to
(9, 1) would need a further concrete-coordinate bridge, not present here.
AUCurves bridge: the base point has additive order l
(E_basepoint_order, Spec/Curve25519_BasepointOrder.v).
Non-vanishing of small multiples of a point of order l: for
0 < n < l, n • B ≠ 0.
curve25519_MontyCurveGroup.xProj unfolds to xProjW 486662.
If the first projective coordinate of Q vanishes, then Q is a
2-torsion point: Q + Q = 0. (Such a Q is the affine point (0, 0),
which is its own negation on a Montgomery curve.)
A point of x-coordinate 1 is a 4-torsion point: (R+R)+(R+R) = 0.
A point of x-coordinate −1 is a 4-torsion point: (R+R)+(R+R) = 0.
l is coprime to 4 (it is an odd prime > 4).
The 4-torsion multiple (4m)·B = 0 only when l ∣ m; hence for
0 < m < l the point m·B is not 4-torsion.
xdbl nondegeneracy. If Q is not a 4-torsion point, the xdbl
output at xProj Q is projectively nondegenerate.
The projective second coordinate of a nonzero point is 1.
The base point is not the identity.
The base point's projective second coordinate is 1 (it is affine).
The base point's projective first coordinate is nonzero (u = 9 ≠ 0);
equivalently, the base point is not the 2-torsion point (0, 0).
xdadd nondegeneracy. For a non-4-torsion point P0 and any P1, the
differential-addition output (with the base point as the difference input,
which is the ladder's invariant) is projectively nondegenerate. The base
point is affine with nonzero x-coordinate (u = 9), and the only way the
output could degenerate is if P0 had x-coordinate ±1 (a 4-torsion
point), excluded by hypothesis.
The base point discharges LadderNondeg for every in-range scalar.
For any bit-list whose value is below the subgroup order l, the entire
Montgomery-ladder path over the base point is projectively nondegenerate.
Unconditional X25519 field-level scalar-multiplication theorem for the
RFC 7748 base point. For any scalar below the subgroup order l, the
first component of the field-level Montgomery ladder run on xProj B is
projectively equivalent to xProj (k · B) — the x-coordinate of the
abstract-group scalar multiplication. This is x25519_ladder_correct
with the LadderNondeg side condition discharged (via
curve25519_basepoint_LadderNondeg), so it holds with no nondegeneracy
hypothesis, exactly on the RFC 7748 scalar range k < l.
Canonical X25519 scalar-clamp (RFC 7748 §5) #
X25519 clamps scalar bytes before treating as a scalar:
- Clear bits 0, 1, 2 of byte 0 (so bottom 3 bits of scalar are 0).
- Clear bit 7 of byte 31 (top bit).
- Set bit 6 of byte 31 (so scalar ≥ 2^254).
We model this as a scalar-level operation on ℕ.