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 for the abstract group #
- 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.
Primality and trust edges #
Both primes are theorems proved by Pratt certificates that the kernel checks
(CatCrypt.PrattCertificate.pratt_prime): curve25519Prime_prime
(base-field prime, from P25519PrimeCert.p25519lit_prime) and
curve25519SubgroupOrder_prime (the subgroup order l, from
Ed25519LPrimeCert.ed25519Llit_prime). The remaining three trust edges are
axioms bridged across the Rocq↔Lean boundary from the AUCurves development,
each documented at its definition: curve25519_basepoint /
curve25519_basepoint_order_nsmul / curve25519_basepoint_ne_zero (the
RFC 7748 base point, its annihilation l • B = 0, and its non-identity).
The exact order addOrderOf B = l is the theorem
curve25519_basepoint_addOrder, derived from those two facts and the
primality of l. Everything else — including the unconditional ladder
capstone x25519_ladder_correct_basepoint — is proved.
Curve25519's base-field modulus 2²⁵⁵ − 19 is prime, by the Pratt
certificate P25519PrimeCert.p25519lit_prime checked by kernel reduction.
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, by the Pratt certificate
Ed25519LPrimeCert.ed25519Llit_prime (the Ed25519 group order is the same
l) checked by kernel reduction. 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 (a Pratt certificate); 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. Two of its properties are bridged across the Rocq↔Lean
boundary from the AUCurves development, each as an axiom:
curve25519_basepoint_order_nsmul records the annihilation l • B = 0
(E_basepoint_order in Spec/Curve25519_BasepointOrder.v, with l the prime
subgroup order of E/E[4] from fiat-crypto's Spec/Ristretto255.v — the Rocq
lemma is Qed, but its key input scalarmult_l_eq_zero in the same file is
Admitted: the tactic chain closes interactively and its Qed kernel check
exhausts memory at ~40 GB), and
curve25519_basepoint_ne_zero records that the base point is affine, hence not
the group identity. The exact additive order addOrderOf B = l is not bridged:
curve25519_basepoint_addOrder derives it from the two axioms and the
primality of l (a point annihilated by a prime and distinct from the identity
has that prime as its order). Everything downstream of these is proved.
AUCurves bridge: an order-l point of the Curve25519 group. Only its
additive order is constrained (by curve25519_basepoint_order_nsmul and
curve25519_basepoint_ne_zero via 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: l • B = 0 for the base point
(E_basepoint_order, Spec/Curve25519_BasepointOrder.v). The cited lemma
establishes exactly this annihilation and does not speak to minimality.
It is Qed, but rests on scalarmult_l_eq_zero in the same file, which
is Admitted upstream: its tactic chain closes interactively and the
Qed kernel check exhausts memory at ~40 GB.
AUCurves bridge: the base point is not the identity. RFC 7748's base
point is the affine point u = 9; the identity of the Weierstrass point
group is the point at infinity.
The base point has additive order exactly l: it is annihilated by the
prime l (curve25519_basepoint_order_nsmul) and is not the identity
(curve25519_basepoint_ne_zero), so addOrderOf_eq_prime pins the order.
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'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 ℕ.