inductive Hex.ECPP.Point : Type

Coordinates used when checking a primality certificate's scalar multiplication: either the point at infinity or a finite pair of natural numbers. Curve membership and reduced coordinates are checked separately.

• infinity : Point
• affine (x y : Nat) : Point

@[instance_reducible]

instance Hex.ECPP.instReprPoint : Repr Point

Equations

• Hex.ECPP.instReprPoint = { reprPrec := Hex.ECPP.instReprPoint.repr }

def Hex.ECPP.instReprPoint.repr : Point → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.instReprPoint.repr Hex.ECPP.Point.infinity prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Point.infinity")).group prec✝

def Hex.ECPP.instBEqPoint.beq : Point → Point → Bool

Equations

• Hex.ECPP.instBEqPoint.beq Hex.ECPP.Point.infinity Hex.ECPP.Point.infinity = true
• Hex.ECPP.instBEqPoint.beq (Hex.ECPP.Point.affine a a_1) (Hex.ECPP.Point.affine b b_1) = (a == b && a_1 == b_1)
• Hex.ECPP.instBEqPoint.beq x✝¹ x✝ = false

@[instance_reducible]

instance Hex.ECPP.instBEqPoint : BEq Point

Equations

• Hex.ECPP.instBEqPoint = { beq := Hex.ECPP.instBEqPoint.beq }

@[instance_reducible]

instance Hex.ECPP.instDecidableEqPoint : DecidableEq Point

Equations

• Hex.ECPP.instDecidableEqPoint = Hex.ECPP.instDecidableEqPoint.decEq

def Hex.ECPP.instDecidableEqPoint.decEq (x✝ x✝¹ : Point) : Decidable (x✝ = x✝¹)

Equations

• Hex.ECPP.instDecidableEqPoint.decEq Hex.ECPP.Point.infinity Hex.ECPP.Point.infinity = isTrue ⋯
• Hex.ECPP.instDecidableEqPoint.decEq Hex.ECPP.Point.infinity (Hex.ECPP.Point.affine x_2 y) = isFalse ⋯
• Hex.ECPP.instDecidableEqPoint.decEq (Hex.ECPP.Point.affine x_2 y) Hex.ECPP.Point.infinity = isFalse ⋯
• Hex.ECPP.instDecidableEqPoint.decEq (Hex.ECPP.Point.affine a a_1) (Hex.ECPP.Point.affine b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Hex.ECPP.modSub (n a b : Nat) : Nat

Natural subtraction interpreted modulo n, for canonical operands.

Equations

• Hex.ECPP.modSub n a b = (a % n + n - b % n) % n

def Hex.ECPP.onCurve (n a b x y : Nat) : Bool

The equation of the short Weierstrass curve.

Equations

• Hex.ECPP.onCurve n a b x y = (y * y % n == (x * x * x + a * x + b) % n)

def Hex.ECPP.Point.canonical (n : Nat) : Point → Bool

A canonical point has both coordinates below the modulus.

Equations

• Hex.ECPP.Point.canonical n Hex.ECPP.Point.infinity = true
• Hex.ECPP.Point.canonical n (Hex.ECPP.Point.affine x_1 y) = (decide (x_1 < n) && decide (y < n))

def Hex.ECPP.Point.onCurve (n a b : Nat) : Point → Bool

Infinity belongs to every short curve; finite points satisfy its equation.

Equations

• Hex.ECPP.Point.onCurve n a b Hex.ECPP.Point.infinity = true
• Hex.ECPP.Point.onCurve n a b (Hex.ECPP.Point.affine x_1 y) = Hex.ECPP.onCurve n a b x_1 y

def Hex.ECPP.addWithInverse (n x₁ y₁ x₂ d v : Nat) (inverses : List Nat) : Option (Point × List Nat)

Complete one division branch, consuming exactly one inverse witness.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.addWithInverse n x₁ y₁ x₂ d v inverses = none

def Hex.ECPP.add? (n a : Nat) (P Q : Point) (inverses : List Nat) : Option (Point × List Nat)

Partial affine addition with explicit inverse witnesses.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.add? n a Hex.ECPP.Point.infinity Q inverses = some (Q, inverses)
• Hex.ECPP.add? n a P Hex.ECPP.Point.infinity inverses = some (P, inverses)

def Hex.ECPP.checkedAdd? (n a b : Nat) (P Q : Point) (inverses : List Nat) : Option (Point × List Nat)

Replay accepts only canonical points on the supplied curve after each addition. This makes both arithmetic invariants local, executable checks.

Equations

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

theorem Hex.ECPP.checkedAdd_facts {n a b : Nat} {P Q R : Point} {ws rest : List Nat} (h : checkedAdd? n a b P Q ws = some (R, rest)) : add? n a P Q ws = some (R, rest) ∧ Point.canonical n R = true ∧ Point.onCurve n a b R = true

Accepted checked additions satisfy the raw branch and both local arithmetic invariants.

theorem Hex.ECPP.modSub_lt {n a b : Nat} (hn : 0 < n) : modSub n a b < n

Modular subtraction returns a canonical residue for a positive modulus.

theorem Hex.ECPP.addWithInverse_canonical {n x₁ y₁ x₂ d v : Nat} {ws rest : List Nat} {R : Point} (hn : 0 < n) (h : addWithInverse n x₁ y₁ x₂ d v ws = some (R, rest)) : Point.canonical n R = true

A successful division branch returns canonical coordinates.

theorem Hex.ECPP.addWithInverse_spec {n x₁ y₁ x₂ d v : Nat} {ws rest : List Nat} {R : Point} (h : addWithInverse n x₁ y₁ x₂ d v ws = some (R, rest)) : ∃ (u : Nat), ws = u :: rest ∧ u < n ∧ d * u % n = 1 ∧ R = Point.affine (modSub n (modSub n (v * u % n * (v * u % n) % n) x₁) x₂) (modSub n (v * u % n * modSub n x₁ (modSub n (modSub n (v * u % n * (v * u % n) % n) x₁) x₂) % n) y₁)

A successful division branch used exactly the next checked witness.