4.3. Supplied PARI conversion🔗

Hex.ECPP.ImportBudget bounds text bytes and decimal digits, every supplied integer magnitude, rows, scalar bits, inverse operations and endpoint search fuel. Parsed-input preflight precedes endpoint construction. Row errors preserve their original vector index; the endpoint occupies the index immediately after the rows.

#guard (convertText defaultImportBudget
  "[[17,7,1,2,[3,6]]]" (.small 11)).isOk
#guard (convertText defaultImportBudget
  "17" (.small 17)).isOk

def importExhausted : Bool := match convertCounted
    { defaultImportBudget with maxIntegerBits := 2 }
    Hex.Nat.defaultPrimeCertBudget
    (Hex.Rand.ofSeed 1) 10 ⟨[], 15⟩ with
  | .error e => e.kind == .exhausted
  | _ => false
#guard importExhausted

Signed PARI coordinates are reduced during conversion. Homogeneous coordinates require a unit denominator. Raw certificates themselves must already contain canonical residues. PARI's integer terminal representation is replaced with an accepted Hex primality certificate, never assumed prime because it lies below PARI's cutoff.

def

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

Parse a PARI integer or a vector of [n,t,s,a,P] rows. An affine P has two coordinates; the three-coordinate form is also accepted so its projective z is checked as a unit. convertText retains row locations.

def

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

Preflight parsed input before checking or searching for a terminal certificate. Row errors retain their original vector index; the endpoint uses the index immediately after the last row. Text byte and digit limits are enforced separately by parsePari.

def

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

Parse and convert a supplied PARI certificate under explicit limits.

def

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

Complete a partial PARI endpoint with Hex's bounded, checked terminal certificate search. Supplied fuel above the conversion allocation is rejected.

theorem

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

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