Montgomery curve x-only formulas (Costello–Smith §4)

For a Montgomery curve

E : B y² = x³ + A x² + x

over a field F, the x-only differential-addition and doubling formulas operate on projective pairs (X, Z) representing the x-coordinate X/Z. The formulas use only field operations (no y).

What this file provides

1. The formulas xdbl, xdadd over any commutative ring F.

2. Basic algebraic properties of the formulas (projective invariance, commutativity of xdbl's output shape, etc.).

3. MontyParams structure capturing the curve parameters (A, B, p).

4. The Costello–Smith §4 key identities stated as a hypothesis class MontyCurveGroup, which axiomatises the correspondence between the x-only formulas and scalar multiplication on the abstract group.

   • xdbl_eq: xdbl(X/Z) = x(2 · P) when x(P) = X/Z
   • xdadd_eq: xdadd(x(P), x(Q), x(P-Q)) = x(P + Q)

Why this is a hypothesis, not a theorem (yet)

Proving xdbl_eq and xdadd_eq from first principles requires

• The Montgomery-form group law in affine coordinates (~2 pages of polynomial algebra).
• A birational map to Weierstrass form (or a direct point-addition formula).
• Case analysis for the point at infinity / doubling singularities.

This is the classical Costello–Smith §4 algebra. It's a page of polynomial manipulation, doable in Lean in a few dozen lines once the affine-coordinate group law is set up, but the group law itself requires a Montgomery-curve structure in Mathlib that does not yet exist (Mathlib has WeierstrassCurve but not MontgomeryCurve).

The correspondence is axiomatised and connected to the ladder correctness proof in MontgomeryLadder.lean.

References

• Costello, Smith, "Montgomery curves and the Montgomery ladder", IACR eprint 2017/212, §4 (equations 8, 9, 12, 13).
• Bernstein, "Curve25519: new Diffie-Hellman speed records", PKC 2006.

x-only formulas as pure field computation

def CatCrypt.Crypto.ECC.xdbl {F : Type u_1} [CommRing F] (a24 : F) (XZ : F × F) : F × F

Projective x-only doubling (Costello–Smith eq. 12). Given (X, Z) with X/Z = x(P), returns (X', Z') with X'/Z' = x(2 · P). Formula:

X' = (X + Z)² · (X − Z)² Z' = 4·X·Z · ((X − Z)² + ((A + 2)/4) · 4·X·Z)

We use the equivalent form with a single curve-parameter a24 = (A+2)/4.

Equations

• CatCrypt.Crypto.ECC.xdbl a24 (X, Z) = ((X + Z) * (X + Z) * ((X - Z) * (X - Z)), ((X + Z) * (X + Z) - (X - Z) * (X - Z)) * ((X - Z) * (X - Z) + a24 * ((X + Z) * (X + Z) - (X - Z) * (X - Z))))

def CatCrypt.Crypto.ECC.xdadd {F : Type u_1} [CommRing F] (PZ QZ DZ : F × F) : F × F

Projective x-only differential addition (Costello–Smith eq. 13). Given (XP, ZP) for P, (XQ, ZQ) for Q, and (XD, ZD) for P−Q, returns the projective x-coordinate of P + Q. Formula:

DA = (XP − ZP)(XQ + ZQ) CB = (XP + ZP)(XQ − ZQ) X' = ZD · (DA + CB)² Z' = XD · (DA − CB)²

Equations

• CatCrypt.Crypto.ECC.xdadd (X, Z) (X_1, Z_1) (X_2, Z_2) = (Z_2 * ((X - Z) * (X_1 + Z_1) + (X + Z) * (X_1 - Z_1)) ^ 2, X_2 * ((X - Z) * (X_1 + Z_1) - (X + Z) * (X_1 - Z_1)) ^ 2)

Algebraic properties

theorem CatCrypt.Crypto.ECC.xdadd_symm {F : Type u_1} [CommRing F] (PZ QZ DZ : F × F) : xdadd PZ QZ DZ = xdadd QZ PZ DZ

xdadd is symmetric in its first two arguments up to the sign of the "DA − CB" term, which is squared, so full symmetry holds.

theorem CatCrypt.Crypto.ECC.xdbl_infinity {F : Type u_1} [CommRing F] (a24 X : F) : xdbl a24 (X, 0) = (X ^ 4, 0)

If Z = 0, the projective point (X, 0) represents the point at infinity. Doubling the point at infinity gives the point at infinity.

Curve parameters

structure CatCrypt.Crypto.ECC.MontyParams (F : Type u_2) [CommRing F] : Type u_2

A Montgomery curve parameter triple (A, p) over a field F, plus the common derived constant a24 = (A + 2) / 4. Kept as an independent field to avoid division in the representation.

• A : F

  Curve equation: y² = x³ + A x² + x.

• a24 : F

  The derived constant (A + 2) / 4 used in xdbl. The invariant 4 * a24 = A + 2 is part of the well-formedness hypothesis.

def CatCrypt.Crypto.ECC.curve25519Params (F : Type u_2) [CommRing F] : MontyParams F

Curve25519 parameters: A = 486662, a24 = 121666 = (486662 + 2)/4.

Note: some implementations use the constant 121665 = (A − 2)/4 with a different doubling-formula variant. Here we use the (A + 2)/4 variant corresponding to Costello–Smith eq. 12.

Equations

• CatCrypt.Crypto.ECC.curve25519Params F = { A := ↑486662, a24 := ↑121666 }

theorem CatCrypt.Crypto.ECC.curve25519Params_wf (F : Type u_2) [CommRing F] : 4 * (curve25519Params F).a24 = (curve25519Params F).A + 2

Well-formedness: 4 * a24 = A + 2. Verifies for Curve25519 over any field where the characteristic doesn't divide the value.

Costello–Smith §4 — polynomial identities

The identities below are the algebraic content of Costello–Smith §4. Each is a pure field identity, provable by the ring tactic. They state that the x-only projective formulas compute the same values as the affine slope-based formulas evaluated under the Montgomery curve equation y² = x³ + A x² + x.

Once a Montgomery-curve group structure is in place (with affine point addition), these identities are the core algebraic fact needed to prove MontyCurveGroup.xdbl_spec and xdadd_spec.

theorem CatCrypt.Crypto.ECC.xdbl_affine_numerator_identity {F : Type u_1} [CommRing F] (A x : F) : (3 * x ^ 2 + 2 * A * x + 1) ^ 2 - 4 * (A + 2 * x) * (x ^ 3 + A * x ^ 2 + x) = (x ^ 2 - 1) ^ 2

xdbl polynomial identity (Costello–Smith §4, doubling). The projective x-coordinate numerator xdbl.1 at input (x, 1) equals (x² − 1)², matching the affine formula x(2P) = λ² − A − 2x with λ = (3x² + 2Ax + 1) / (2y).

Specifically, over any commutative ring, the identity (3x² + 2Ax + 1)² − 4(A + 2x)(x³ + Ax² + x) = (x² − 1)² holds. This is the numerator identity that falls out of clearing the common denominator 4(x³ + Ax² + x) = 4y² from the affine expression for x(2P).

theorem CatCrypt.Crypto.ECC.xdbl_numerator {F : Type u_1} [CommRing F] (a24 x : F) : (xdbl a24 (x, 1)).1 = (x ^ 2 - 1) ^ 2

The xdbl numerator matches (x² − 1)² — direct from the formula.

theorem CatCrypt.Crypto.ECC.xdbl_denominator {F : Type u_1} [CommRing F] (A a24 x : F) (h : 4 * a24 = A + 2) : (xdbl a24 (x, 1)).2 = 4 * x * (x ^ 2 + A * x + 1)

The xdbl denominator, in the a24 = (A + 2) / 4 convention, matches 4x · (x² + A x + 1) under the constraint 4 a24 = A + 2.

theorem CatCrypt.Crypto.ECC.xdadd_affine_num_simpl {F : Type u_1} [CommRing F] (xP xQ : F) : ((xP - 1) * (xQ + 1) + (xP + 1) * (xQ - 1)) ^ 2 = (2 * (xP * xQ - 1)) ^ 2

xdadd polynomial identity (Costello–Smith §4, differential addition). Given points P, Q with x-coordinates xP, xQ and their difference P − Q with x-coordinate xD, the projective output of xdadd has numerator ((xP − 1)(xQ + 1) + (xP + 1)(xQ − 1))² = (2(xP xQ − 1))² and denominator xD · ((xP − 1)(xQ + 1) − (xP + 1)(xQ − 1))² = xD · (2(xQ − xP))² when Z coordinates are all normalised to 1.

theorem CatCrypt.Crypto.ECC.xdadd_affine_den_simpl {F : Type u_1} [CommRing F] (xP xQ : F) : ((xP - 1) * (xQ + 1) - (xP + 1) * (xQ - 1)) ^ 2 = (2 * (xQ - xP)) ^ 2

theorem CatCrypt.Crypto.ECC.xdadd_normalised {F : Type u_1} [CommRing F] (xP xQ xD : F) : xdadd (xP, 1) (xQ, 1) (xD, 1) = ((2 * (xP * xQ - 1)) ^ 2, xD * (2 * (xQ - xP)) ^ 2)

The xdadd output with Z = 1 for all three projective inputs simplifies to (2(xP xQ − 1))² · 1 and xD · (2(xQ − xP))² — the classical form.

Costello–Smith §4 correspondence (hypothesised group form)

class CatCrypt.Crypto.ECC.MontyCurveGroup (F : Type u_2) [CommRing F] (params : MontyParams F) (G : Type u_3) [AddCommGroup G] : Type (max u_2 u_3)

A Montgomery curve with a distinguished abelian group of points and an x-coordinate map. The key hypotheses encode Costello–Smith §4 §4.

xdbl_spec and xdadd_spec state that the x-only formulas agree with scalar multiplication (equivalently: group addition) on the abstract group. Proving these from the affine Montgomery curve group law is the remaining work; see the header.

• xProj : G → F × F

  Project a curve point to its projective x-coordinate (X, Z).

• xdbl_spec (P : G) : match xdbl params.a24 (xProj params P) with | (Xd, Zd) => match xProj params (P + P) with | (X2, Z2) => Xd * Z2 = X2 * Zd

  xdbl computes the x-coordinate of doubling, up to projective equivalence (both outputs represent the same X/Z).

• xdadd_spec (P Q : G) : match xdadd (xProj params P) (xProj params Q) (xProj params (P - Q)) with | (Xs, Zs) => match xProj params (P + Q) with | (Xa, Za) => Xs * Za = Xa * Zs

  xdadd computes the x-coordinate of addition, up to projective equivalence, given the difference as auxiliary input.

Field-level x-only ladder

The ladder below is the actual program a Jasmin (or bedrock2, or Rust) implementation runs: pure field operations on projective pairs (X, Z), no points, no y-coordinates, no group law. Connect it to the abstract-group ladder via MontyCurveGroup using ProjEquiv.

def CatCrypt.Crypto.ECC.ProjEquiv {F : Type u_1} [CommRing F] (p q : F × F) : Prop

Projective equivalence on F × F: (X₁, Z₁) ∼ (X₂, Z₂) iff their x-coordinates agree (X₁/Z₁ = X₂/Z₂ in the field of fractions).

Equations

• CatCrypt.Crypto.ECC.ProjEquiv p q = (p.1 * q.2 = q.1 * p.2)

theorem CatCrypt.Crypto.ECC.ProjEquiv.refl {F : Type u_1} [CommRing F] (p : F × F) : ProjEquiv p p

theorem CatCrypt.Crypto.ECC.ProjEquiv.symm {F : Type u_1} [CommRing F] {p q : F × F} (h : ProjEquiv p q) : ProjEquiv q p

def CatCrypt.Crypto.ECC.xladderStep {F : Type u_1} [CommRing F] (a24 : F) (xP : F × F) (acc : (F × F) × F × F) (b : Bool) : (F × F) × F × F

One step of the field-level x-only ladder. Takes the projective x-coordinate of the base point xP (as the invariant difference) and the current (R₀_proj, R₁_proj) state, steps on bit b via xdbl and xdadd.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Crypto.ECC.xladderFold {F : Type u_1} [CommRing F] (a24 : F) (xP : F × F) : List Bool → (F × F) × F × F

Run the field-level ladder over a list of bits (MSB first) starting from projective (1, 0) (infinity) and xP (the base point).

Equations

• CatCrypt.Crypto.ECC.xladderFold a24 xP [] = ((1, 0), xP)
• CatCrypt.Crypto.ECC.xladderFold a24 xP (b :: bs) = CatCrypt.Crypto.ECC.xladderStep a24 xP (CatCrypt.Crypto.ECC.xladderFold a24 xP bs) b

theorem CatCrypt.Crypto.ECC.xdbl_projEquiv {F : Type u_1} [CommRing F] (a24 : F) {p q : F × F} (h : ProjEquiv p q) : ProjEquiv (xdbl a24 p) (xdbl a24 q)

xdbl respects projective equivalence: if two projective inputs represent the same x-coordinate, their xdbl outputs do too. Both numerator and denominator of xdbl are homogeneous polynomials of degree 4 in (X, Z), so scaling both coordinates by a common factor scales the output uniformly — ProjEquiv is preserved.

theorem CatCrypt.Crypto.ECC.xdadd_projEquiv {F : Type u_1} [CommRing F] {p p' q q' d d' : F × F} (hp : ProjEquiv p p') (hq : ProjEquiv q q') (hd : ProjEquiv d d') : ProjEquiv (xdadd p q d) (xdadd p' q' d')

xdadd respects projective equivalence in all three arguments. Key algebraic fact: DA + CB = 2(XPXQ − ZPZQ) and DA − CB = 2(XPZQ − XQZP), and each of these is homogeneous of degree 1 in each of (XP, ZP) and (XQ, ZQ). The ZD/XD factors cancel under ProjEquiv (d, d').

Field-level ladder correctness

Combines MontyCurveGroup.{xdbl_spec, xdadd_spec} with the invariant (R₀, R₁) ∼ (xProj (n·P), xProj ((n+1)·P)) from MontgomeryLadder.ladderFold_correct, where ∼ is projective equivalence.

def CatCrypt.Crypto.ECC.XLadderInv {F : Type u_2} [CommRing F] {params : MontyParams F} {G : Type u_3} [AddCommGroup G] [h : MontyCurveGroup F params G] (P : G) (n : ℕ) (st : (F × F) × F × F) : Prop

The field-level ladder invariant: the state (R₀, R₁) projectively represents (n · P, (n + 1) · P) for some running scalar n.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Crypto.ECC.ProjEquiv.trans {F : Type u_2} [Field F] {p q r : F × F} (hpq : ProjEquiv p q) (hqr : ProjEquiv q r) (hq : q.1 ≠ 0 ∨ q.2 ≠ 0) : ProjEquiv p r

Restricted ProjEquiv transitivity over an integral domain. ProjEquiv is transitive when the middle term is nondegenerate (not both coordinates zero). Over a CommRing that isn't an integral domain, transitivity can fail; we specialise to the Field case (integral domain) and require nondegeneracy explicitly.

theorem CatCrypt.Crypto.ECC.ProjEquiv_xdbl_of_inv {F : Type u_2} [Field F] {params : MontyParams F} {G : Type u_3} [AddCommGroup G] [h : MontyCurveGroup F params G] (P : G) (n : ℕ) {r : F × F} (hr : ProjEquiv r (MontyCurveGroup.xProj params (n • P))) (hND : (xdbl params.a24 (MontyCurveGroup.xProj params (n • P))).1 ≠ 0 ∨ (xdbl params.a24 (MontyCurveGroup.xProj params (n • P))).2 ≠ 0) : ProjEquiv (xdbl params.a24 r) (MontyCurveGroup.xProj params (n • P + n • P))

Doubling step preserves ProjEquiv, given the intermediate xdbl (xProj (n·P)) is nondegenerate (Z ≠ 0). This is the composition of xdbl_projEquiv, xdbl_spec, and ProjEquiv.trans.

theorem CatCrypt.Crypto.ECC.ProjEquiv_xdadd_of_inv {F : Type u_2} [Field F] {params : MontyParams F} {G : Type u_3} [AddCommGroup G] [h : MontyCurveGroup F params G] (P Q D : G) {r s d : F × F} (hr : ProjEquiv r (MontyCurveGroup.xProj params P)) (hs : ProjEquiv s (MontyCurveGroup.xProj params Q)) (hd : ProjEquiv d (MontyCurveGroup.xProj params D)) (hDeq : MontyCurveGroup.xProj params D = MontyCurveGroup.xProj params (P - Q)) (hND : (xdadd (MontyCurveGroup.xProj params P) (MontyCurveGroup.xProj params Q) (MontyCurveGroup.xProj params (P - Q))).1 ≠ 0 ∨ (xdadd (MontyCurveGroup.xProj params P) (MontyCurveGroup.xProj params Q) (MontyCurveGroup.xProj params (P - Q))).2 ≠ 0) : ProjEquiv (xdadd r s d) (MontyCurveGroup.xProj params (P + Q))

Differential-addition step preserves ProjEquiv, given the intermediate xdadd output is nondegenerate, and that xProj is negation-invariant (xProj (-X) = xProj X).

theorem CatCrypt.Crypto.ECC.xladderStep_preserves_invariant {F : Type u_2} [Field F] {params : MontyParams F} {G : Type u_3} [AddCommGroup G] [h : MontyCurveGroup F params G] (P : G) (n : ℕ) (st : (F × F) × F × F) (b : Bool) (hNeg : ∀ (X : G), MontyCurveGroup.xProj params (-X) = MontyCurveGroup.xProj params X) (hND0 : (xdbl params.a24 (MontyCurveGroup.xProj params (n • P))).1 ≠ 0 ∨ (xdbl params.a24 (MontyCurveGroup.xProj params (n • P))).2 ≠ 0) (hND1 : (xdbl params.a24 (MontyCurveGroup.xProj params ((n + 1) • P))).1 ≠ 0 ∨ (xdbl params.a24 (MontyCurveGroup.xProj params ((n + 1) • P))).2 ≠ 0) (hNDa : (xdadd (MontyCurveGroup.xProj params (n • P)) (MontyCurveGroup.xProj params ((n + 1) • P)) (MontyCurveGroup.xProj params (n • P - (n + 1) • P))).1 ≠ 0 ∨ (xdadd (MontyCurveGroup.xProj params (n • P)) (MontyCurveGroup.xProj params ((n + 1) • P)) (MontyCurveGroup.xProj params (n • P - (n + 1) • P))).2 ≠ 0) (hInv : XLadderInv P n st) : XLadderInv P (2 * n + if b = true then 1 else 0) (xladderStep params.a24 (MontyCurveGroup.xProj params P) st b)

Field-level ladder step preserves the invariant.

For bit b, scalar n advances to 2n + (if b then 1 else 0).

Requires:

• Field F (for ProjEquiv transitivity);
• hNeg: xProj is negation-invariant (holds on montgomeryW via xProjW_neg);
• hND0/hND1: nondegeneracy of the two intermediate outputs (xdbl (xProj (n·P)) and xdadd (xProj (n·P)) (xProj ((n+1)·P)) (xProj (-P))).