def Hex.ECPP.checkStep (n a b x y discrInv : Nat) (inverses : List Nat) (q : Nat) : Bool

Check the elliptic curve conditions that establish n prime once q is known prime: a nonsingular short Weierstrass curve, a finite point (x,y), verified divisions in q • (x,y) = O, and a sufficiently large q < n. This function checks the local arithmetic; it does not itself prove q prime. check additionally checks the nested certificate for q.

Equations

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

def Hex.ECPP.check : Cert → Bool

Verify a primality certificate, including every smaller prime it uses.

For an elliptic curve step, verify the curve equation, nonsingularity, the strict size bound on the auxiliary prime, and scalar multiplication to infinity using the supplied modular inverses. For a HexPrimality certificate, use its existing primality checker.

In HexECPPTheory, natPrime_of_check proves that a true result implies Nat.Prime cert.subject.

Equations

• Hex.ECPP.check (Hex.ECPP.Cert.base cert) = Hex.Nat.checkPrime cert
• Hex.ECPP.check (Hex.ECPP.Cert.step n a b x_1 y discrInv inverses child) = (Hex.ECPP.check child && Hex.ECPP.checkStep n a b x_1 y discrInv inverses child.subject)

def Hex.ECPP.checkAt (n : Nat) (cert : Cert) : Bool

Verify that cert is a valid primality certificate for the integer n. Return false if it records a different integer, even when its own certificate is valid. In HexECPPTheory, natPrime_of_checkAt turns a true result into a theorem of Nat.Prime n.

Equations

• Hex.ECPP.checkAt n cert = (cert.subject == n && Hex.ECPP.check cert)

@[simp]

theorem Hex.ECPP.check_base (cert : Nat.PrimeCert) : check (Cert.base cert) = Nat.checkPrime cert

A certificate ending with HexPrimality data is checked by its existing primality checker.

theorem Hex.ECPP.check_step (n a b x y d : Nat) (ws : List Nat) (child : Cert) : check (Cert.step n a b x y d ws child) = (check child && checkStep n a b x y d ws child.subject)

Checking an elliptic step checks its smaller prime's certificate and uses exactly that prime as the scalar in the point multiplication.

@[simp]

theorem Hex.ECPP.checkAt_eq_true_iff {n : Nat} {cert : Cert} : checkAt n cert = true ↔ cert.subject = n ∧ check cert = true

Checking a certificate for n succeeds exactly when its recorded integer is n and the certificate itself passes the primality checker.

theorem Hex.ECPP.checkStep_canonical {n a b x y discrInv q : Nat} {inverses : List Nat} (h : checkStep n a b x y discrInv inverses q = true) : a < n ∧ b < n ∧ x < n ∧ y < n ∧ discrInv < n

Accepted step data uses canonical curve, point and discriminant residues.

theorem Hex.ECPP.checkStep_facts {n a b x y discrInv q : Nat} {inverses : List Nat} (h : checkStep n a b x y discrInv inverses q = true) : 3 < n ∧ (n % 6 = 1 ∨ n % 6 = 5) ∧ 2 ≤ q ∧ q < n ∧ onCurve n a b x y = true ∧ (4 * a * a * a + 27 * b * b) * discrInv % n = 1 ∧ sizeBound n q = true ∧ replay n a b q (Point.affine x y) inverses = some (Point.infinity, [])

An accepted step satisfies the curve, inverse and size conditions, and its scalar multiplication reaches infinity with no unused inverse witnesses.

theorem Hex.ECPP.checkAt_subject {n : Nat} {cert : Cert} (h : checkAt n cert = true) : cert.subject = n

A certificate accepted for n records n as its intended prime.

theorem Hex.ECPP.checkAt_check {n : Nat} {cert : Cert} (h : checkAt n cert = true) : check cert = true

A certificate accepted for n also passes the certificate checker alone.