structure Hex.ECPP.ImportBudget : Type

Limits on the input and work allowed when importing a primality certificate from PARI text. These bound parsing, point calculations and optional search for a proof of the last prime. Exceeding a limit returns an error; it does not imply that the intended integer is composite.

• maxInputBytes : Nat

  Maximum certificate text length in UTF-8 bytes, checked before parsing.

• maxDigits : Nat

  Maximum digits in a supplied decimal integer, checked before allocating it.

• maxRows : Nat

  Maximum number of elliptic curve steps in the supplied certificate.

• maxIntegerBits : Nat

  Maximum bit length of the magnitude of any supplied integer, including coordinates.

• maxScalarBits : Nat

  Maximum bit length of the cofactor or auxiliary prime used to multiply a point.

• maxInverseOps : Nat

  Maximum divisions requiring a modular inverse in one scalar multiplication.

• maxEndpointFuel : Nat

  Maximum search fuel a caller may request for proving the last prime in the chain.

@[instance_reducible]

instance Hex.ECPP.instReprImportBudget : Repr ImportBudget

Equations

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

def Hex.ECPP.instReprImportBudget.repr : ImportBudget → Nat → Std.Format

Equations

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

def Hex.ECPP.defaultImportBudget : ImportBudget

Standard limits used to import saved primality certificates: 16 KiB of text, 170 decimal digits per integer, 20 elliptic rows, 512-bit integers and scalars, 1200 divisions per scalar multiplication and 200 units of search fuel for the last prime. Callers may choose smaller limits.

Equations

• Hex.ECPP.defaultImportBudget = { maxInputBytes := 16384, maxDigits := 170, maxRows := 20, maxIntegerBits := 512, maxScalarBits := 512, maxInverseOps := 1200, maxEndpointFuel := 200 }

inductive Hex.ECPP.ImportErrorKind : Type

Conversion failures distinguish allocation, format and arithmetic errors.

• malformed : ImportErrorKind
• exhausted : ImportErrorKind
• unsupported : ImportErrorKind
• invalidArithmetic : ImportErrorKind
• nonunitProjective : ImportErrorKind
• subjectMismatch : ImportErrorKind
• invalidEndpoint : ImportErrorKind

@[instance_reducible]

instance Hex.ECPP.instReprImportErrorKind : Repr ImportErrorKind

Equations

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

def Hex.ECPP.instReprImportErrorKind.repr : ImportErrorKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.ECPP.instBEqImportErrorKind : BEq ImportErrorKind

Equations

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

def Hex.ECPP.instBEqImportErrorKind.beq : ImportErrorKind → ImportErrorKind → Bool

Equations

• Hex.ECPP.instBEqImportErrorKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Hex.ECPP.ImportError : Type

A conversion diagnostic with an original row index; the endpoint follows the rows.

• row : Nat

  Original zero-based vector index; input-wide text errors use zero and may carry parser details.

• kind : ImportErrorKind

  The allocation, format or arithmetic failure.

• offset : Option Nat

  Zero-based ASCII offset for a text preflight failure, when available.

• detail : Option String

  Generic parser diagnostic, including its source location.

@[instance_reducible]

instance Hex.ECPP.instReprImportError : Repr ImportError

Equations

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

def Hex.ECPP.instReprImportError.repr : ImportError → Nat → Std.Format

Equations

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

structure Hex.ECPP.Projective : Type

Supplied signed homogeneous coordinates; normalization requires a unit denominator.

• x : Int

  Signed first homogeneous coordinate.

• y : Int

  Signed second homogeneous coordinate.

• z : Int

  Signed denominator, checked as a unit before normalization.

@[instance_reducible]

instance Hex.ECPP.instReprProjective : Repr Projective

Equations

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

def Hex.ECPP.instReprProjective.repr : Projective → Nat → Std.Format

Equations

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

structure Hex.ECPP.PariRow : Type

One supplied PARI row: subject, trace encoding, cofactor, curve coefficient and point.

• n : Nat

  Claimed subject of this row.

• t : Int

  Signed order encoding: the proposed order is n + 1 - t.

• s : Int

  Positive exact cofactor dividing the proposed order.

• a : Int

  Signed short Weierstrass coefficient.

• point : Projective

  Supplied affine or homogeneous point.

@[instance_reducible]

instance Hex.ECPP.instReprPariRow : Repr PariRow

Equations

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

def Hex.ECPP.instReprPariRow.repr : PariRow → Nat → Std.Format

Equations

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

structure Hex.ECPP.PariCertificate : Type

Parsed rows and the terminal subject to replace with a checked Hex certificate.

• rows : List PariRow

  Rows in parent-to-child order.

• endpoint : Nat

  Terminal subject requiring an accepted Hex primality certificate.

@[instance_reducible]

instance Hex.ECPP.instReprPariCertificate : Repr PariCertificate

Equations

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

def Hex.ECPP.instReprPariCertificate.repr : PariCertificate → Nat → Std.Format

Equations

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

def Hex.ECPP.PariCertificate.subject (input : PariCertificate) : Nat

Subject represented by the outer row, or by the endpoint for an empty vector.

Equations

• input.subject = (Option.map Hex.ECPP.PariRow.n input.rows.head?).getD input.endpoint

def Hex.ECPP.residue (n : Nat) (z : Int) : Nat

Reduce a supplied signed integer to a natural residue.

Equations

• Hex.ECPP.residue n z = (z % ↑n).toNat

def Hex.ECPP.inverse? (n d : Nat) : Option Nat

Conversion may search for inverses, unlike the proof checker. Each proposal is still verified before it enters the raw certificate.

Equations

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

def Hex.ECPP.normalizeProjective (n : Nat) (P : Projective) : Except ImportErrorKind Point

Normalize homogeneous coordinates only after checking a unit inverse of z.

Equations

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

def Hex.ECPP.proposeWithInverse (n a : Nat) (P Q : Point) (d : Nat) : Except ImportErrorKind (Point × Option Nat)

Compute and check the inverse for one affine division branch.

Equations

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

def Hex.ECPP.proposeAdd (n a : Nat) (P Q : Point) : Except ImportErrorKind (Point × Option Nat)

Untrusted affine addition used only while converting supplied rows.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.proposeAdd n a Hex.ECPP.Point.infinity Q = pure (Q, none)
• Hex.ECPP.proposeAdd n a P Hex.ECPP.Point.infinity = pure (P, none)

def Hex.ECPP.proposeBits (budget : ImportBudget) (n a q : Nat) (Q : Point) : Nat → Point → List Nat → Nat → Except ImportErrorKind (Point × List Nat)

Generate a canonical proposal and its inverse transcript. The structural recursor visits the same scalar bits as the proof checker.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.proposeBits budget n a q Q 0 x✝² x✝¹ x✝ = pure (x✝², x✝¹.reverse)

def Hex.ECPP.proposeScalar (budget : ImportBudget) (n a q : Nat) (Q : Point) : Except ImportErrorKind (Point × List Nat)

Generate a bounded scalar proposal and its complete inverse transcript.

Equations

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

def Hex.ECPP.checkRowLimits (budget : ImportBudget) (row : PariRow) : Except ImportErrorKind Unit

Check every supplied integer before arithmetic or endpoint construction.

Equations

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

def Hex.ECPP.preflight (budget : ImportBudget) (input : PariCertificate) : Except ImportError Unit

Check the number of rows and the sizes of their integers before doing curve arithmetic or proving the last prime. An error identifies the original row, or the position after the rows for that last integer. parsePari separately checks text length and decimal digit limits.

Equations

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

def Hex.ECPP.convertRow (budget : ImportBudget) (row : PariRow) (child : Cert) : Except ImportErrorKind Cert

Convert one row against its supplied child and check the local step. The complete child chain is checked at the public conversion boundary.

Equations

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

def Hex.ECPP.convertRows (budget : ImportBudget) : Nat → List PariRow → Cert → Except ImportError Cert

Convert from the terminal row outward, preserving original row indices on failure.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.convertRows budget x✝¹ [] x✝ = pure x✝

def Hex.ECPP.convert (budget : ImportBudget) (input : PariCertificate) (leaf : Nat.PrimeCert) : Except ImportError Cert

Convert parsed PARI rows into a checked ECPP primality certificate. leaf must pass the HexPrimality checker and certify exactly the last integer in the PARI chain. Conversion verifies the curve and point calculations, then checks the resulting complete certificate.

Equations

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

def Hex.ECPP.parsePari (budget : ImportBudget) (source : String) : Except ImportErrorKind PariCertificate

Read PARI primality certificate text: either an integer ending the proof chain or a vector of [n,t,s,a,P] elliptic curve rows. Here n + 1 - t is a proposed order, s its cofactor, a a curve coefficient, and P a point. Points may have two affine or three homogeneous coordinates. Parsing is not a primality proof; convertText completes the arithmetic checks and retains the failing row's location if conversion fails.

Equations

• Hex.ECPP.parsePari budget source = Except.mapError Hex.ECPP.ImportError.kind (Hex.ECPP.parseLocated✝ budget source)

def Hex.ECPP.convertText (budget : ImportBudget) (source : String) (leaf : Nat.PrimeCert) : Except ImportError Cert

Read PARI certificate text and convert it to a checked Hex primality certificate. Supply leaf as a HexPrimality certificate for the last prime in the chain. Return an error for invalid data or exceeded limits. Conversion does not call GP or search for leaf; a successful result is accepted by the ECPP checker for the integer recorded in the text.

Equations

• Hex.ECPP.convertText budget source leaf = do let input ← Hex.ECPP.parseLocated✝ budget source Hex.ECPP.convert budget input leaf

def Hex.ECPP.convertCounted (budget : ImportBudget) (primeBudget : Nat.PrimeCertBudget) (rand : Rand) (fuel : Nat) (input : PariCertificate) : Except ImportError (Cert × Rand)

Import parsed PARI rows while searching for a proof of their last prime. The resulting complete certificate is checked before it is returned, together with the advanced random state. The requested fuel must fit budget; an exhausted search does not establish compositeness.

Equations

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

theorem Hex.ECPP.convert_ok {budget : ImportBudget} {input : PariCertificate} {leaf : Nat.PrimeCert} {c : Cert} (h : convert budget input leaf = Except.ok c) : checkAt input.subject c = true

Supplied conversion returns only certificates accepted by the raw checker; parsing and proposal generation are outside the proof boundary.