inductive Hex.ECPP.Resource : Type

The work limit or unsuccessful search stage reported when certificate search cannot complete a primality proof.

• inputBits : Resource
• depth : Resource
• candidates : Resource
• roots : Resource
• nonresidues : Resource
• points : Resource
• factorWork : Resource
• scalarWork : Resource
• outputBits : Resource
• memo : Resource
• portfolio : Resource
• screening : Resource
• nonresidueRetries : Resource
• pointRetries : Resource
• rows : Resource
• nodes : Resource
• factorPolicy : Resource
• polynomialWork : Resource
• rootWork : Resource

@[instance_reducible]

instance Hex.ECPP.instReprResource : Repr Resource

Equations

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

def Hex.ECPP.instReprResource.repr : Resource → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.inputBits prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.inputBits")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.depth prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.depth")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.roots prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.roots")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.points prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.points")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.memo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.memo")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.portfolio prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.portfolio")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.screening prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.screening")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.rows prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.rows")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.nodes prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.nodes")).group prec✝
• Hex.ECPP.instReprResource.repr Hex.ECPP.Resource.rootWork prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ECPP.Resource.rootWork")).group prec✝

@[instance_reducible]

instance Hex.ECPP.instBEqResource : BEq Resource

Equations

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

def Hex.ECPP.instBEqResource.beq : Resource → Resource → Bool

Equations

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

@[instance_reducible]

instance Hex.ECPP.instDecidableEqResource : DecidableEq Resource

Equations

• Hex.ECPP.instDecidableEqResource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Hex.ECPP.SearchBudget : Type

Limits for finding an elliptic curve primality certificate. The counters bound the entire search, including recursive proofs of auxiliary primes; trying another curve does not restore work already spent. Retry limits also bound the number of choices tried on each curve. Neither a bit-length limit nor the other allowances guarantee that search succeeds for every prime.

• maxBits : Nat

  Maximum subject bit length.

• maxDepth : Nat

  Maximum recursive certificate depth.

• maxCandidates : Nat

  Shared discriminant and order candidate allowance.

• maxRoots : Nat

  Shared modular-root call allowance.

• maxNonresidues : Nat

  Shared nonresidue-draw allowance.

• maxPoints : Nat

  Shared point-draw allowance.

• maxFactorWork : Nat

  Shared reserved factor-attempt packages.

• maxScalarWork : Nat

  Shared maximum scalar additions, including checker replays.

• maxOutputBits : Nat

  Maximum literal bits per retained certificate.

• maxMemo : Nat

  Maximum retained successful certificates.

• pointRetries : Nat

  Local retries are also charged to the shared allocations.

• nonresidueRetries : Nat

  Local nonresidue draws, also charged to the shared allowance.

• terminal : Option Nat.ConstructionBudget

  Select a finite terminal package; omission retains the 256-bit policy.

• order : Option Nat.FactorSearchBudget

  Select a finite order package; its attempt limit must be explicit.

• maxRows : Option Nat

  Public output limits include ancestral rows and embedded terminal nodes.

• maxNodes : Option Nat

  Total nodes include the ECPP base wrapper.

• backtrackOutput : Bool

  Reject oversized candidates locally, retaining all charged work.

• extendedCM : Bool

  Opt in to the attributed fixed linear/quadratic class polynomial table.

• maxPolynomialWork : Nat

  Shared reserved polynomial-root modular operations.

• maxRootWork : Nat

  Per-call modular-operation ceiling; closed-form roots need no splits.

@[instance_reducible]

instance Hex.ECPP.instReprSearchBudget : Repr SearchBudget

Equations

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

def Hex.ECPP.instReprSearchBudget.repr : SearchBudget → Nat → Std.Format

Equations

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

def Hex.ECPP.leafBudget : Nat.ConstructionBudget

Fixed per-attempt ceiling for terminal construction. It is deliberately smaller than the full primality? route used by capability comparisons.

Equations

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

def Hex.ECPP.orderBudget : Nat.FactorSearchBudget

Fixed partial-factor package for one CM order.

Equations

• Hex.ECPP.orderBudget = { primeBudget := { rhoRestarts := 1, rhoSteps := 2048 }, primeFuel := 1, factorFuel := 16, smoothBounds := [64, 512], smoothBases := [2], attemptLimit := some 4 }

def Hex.ECPP.native512Budget : SearchBudget

Larger search policy for integers through 512 bits, with additional fixed complex multiplication class polynomials. Select it explicitly; produce defaults to the 256-bit policy. Search can still fail within this size range. Use public512Budget when the result must fit the public proof commands' certificate limits.

Equations

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

def Hex.ECPP.public512Budget : SearchBudget

The 512-bit search policy used by the public tactic and export command. It restricts output to 20 elliptic rows and 32 total certificate nodes, including the wrapper and all nodes of the last HexPrimality certificate.

Equations

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

def Hex.ECPP.public256Budget : SearchBudget

Explicit output-bounded 256-bit allocation for mixed factor completion. The ordinary producer and existing Native 256-bit policy retain their defaults.

Equations

• Hex.ECPP.public256Budget = { maxDepth := 21, maxRows := some 20, maxNodes := some 32, backtrackOutput := true }

structure Hex.ECPP.SearchError : Type

An integer whose primality certificate was not found, together with the work limit or search stage that stopped the attempt.

• subject : Nat

  Integer whose primality certificate remains unfound.

• resource : Resource

  Work limit or search stage responsible for stopping the search.

@[instance_reducible]

instance Hex.ECPP.instReprSearchError : Repr SearchError

Equations

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

def Hex.ECPP.instReprSearchError.repr : SearchError → Nat → Std.Format

Equations

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

structure Hex.ECPP.SearchStats : Type

Cumulative charged work and backtracking diagnostics.

• candidates : Nat

  Charged discriminant and order candidates.

• roots : Nat

  Charged modular-root calls.

• nonresidues : Nat

  Charged nonresidue draws.

• points : Nat

  Charged point draws.

• factorWork : Nat

  Reserved factor-work units, never refunded.

• scalarWork : Nat

  Reserved scalar additions, never refunded.

• backtracks : Nat

  Checked proposals rejected when their recursive child could not be built.

• terminalCalls : Nat

  Terminal package invocations and their checked successes.

• terminalSuccesses : Nat
• terminalBitRejects : Nat

  Terminal calls outside the selected package's subject limit.

• terminalObligation : Option Nat

  Last unproved terminal obligation, distinct from CM child failures.

• norms : Nat

  Successful norm equations, orders and eligible large prime factors.

• orders : Nat
• largeFactors : Nat
• proposals : Nat

  Checked elliptic step proposals, before recursive child construction.

• outputRejects : Nat

  Output candidates rejected after their search work was charged.

• outputBits : Option Nat

  Actual last literal-bit count; none records traversal exhaustion.

• polynomialWork : Nat

  Reserved modular-operation bounds for class polynomial roots.

• polynomialRoots : Nat

  Checked j-roots admitted from the class polynomial table.

• unresolved : Option SearchError

  Retained failure. Smaller unresolved children and complete portfolios supersede local retries.

• lastRetry : Option SearchError

  Last local retry exhaustion, retained even when the final diagnosis is portfolio exhaustion.

@[instance_reducible]

instance Hex.ECPP.instReprSearchStats : Repr SearchStats

Equations

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

def Hex.ECPP.instReprSearchStats.repr : SearchStats → Nat → Std.Format

Equations

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

structure Hex.ECPP.SearchState : Type

The advanced random stream, cumulative counters and checked success memo.

• rand : Rand

  Advanced deterministic random stream.

• stats : SearchStats

  Cumulative counters and diagnostics; stateful callers can reset them independently of the memo.

• memo : List Cert

  Only successes are cached; a failed branch may depend on remaining depth.

@[instance_reducible]

instance Hex.ECPP.instReprSearchState : Repr SearchState

Equations

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

def Hex.ECPP.instReprSearchState.repr : SearchState → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Hex.ECPP.SearchM (α : Type) : Type

Search errors preserve the advanced random stream, memo and charged work.

Equations

• Hex.ECPP.SearchM = ExceptT Hex.ECPP.SearchError (StateM Hex.ECPP.SearchState)

def Hex.ECPP.charge (budget : SearchBudget) (n : Nat) (resource : Resource) (amount : Nat := 1) : SearchM Unit

Charge before running any work; no backtracking restores counters.

Equations

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

def Hex.ECPP.primeBits : Nat → Nat.PrimeCert → Option Nat

Count terminal literal bits under an explicit traversal fuel. Exhaustion is explicit and cannot bypass a caller's larger output allocation.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.primeBits 0 x✝ = none
• Hex.ECPP.primeBits n.succ (Hex.Nat.PrimeCert.small n_1) = some (1 + HexArith.bitLength n_1)

def Hex.ECPP.certBitsAt (terminalFuel : Nat) : Cert → Option Nat

Count raw chain bits, including a terminal within the fixed leaf-depth profile. Reject deeper supplied terminals instead of undercounting them.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.certBitsAt terminalFuel (Hex.ECPP.Cert.base c) = Option.map (fun (x : Nat) => 1 + x) (Hex.ECPP.primeBits terminalFuel c)

def Hex.ECPP.certBits (c : Cert) : Option Nat

Literal bits under the original terminal profile.

Equations

• Hex.ECPP.certBits c = Hex.ECPP.certBitsAt (Hex.ECPP.leafBudget.maxDepth + 1) c

def Hex.ECPP.primeShape : Nat → Nat.PrimeCert → Option (Nat × Nat)

Embedded terminal node count and height; exhaustion rejects the candidate.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.primeShape 0 x✝ = none
• Hex.ECPP.primeShape n.succ (Hex.Nat.PrimeCert.small n_1) = some (1, 1)

def Hex.ECPP.certShape (terminalFuel : Nat) : Cert → Option (Nat × Nat × Nat)

Rows, total nodes (including the base wrapper), and terminal height.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.certShape terminalFuel (Hex.ECPP.Cert.base c) = do let __x ← Hex.ECPP.primeShape terminalFuel c match __x with | (nodes, height) => pure (0, 1 + nodes, height)

def Hex.ECPP.replayWork : Cert → Nat

Maximum scalar additions performed by a complete checker replay.

Equations

• Hex.ECPP.replayWork (Hex.ECPP.Cert.base c) = 0
• Hex.ECPP.replayWork (Hex.ECPP.Cert.step n a b x_1 y d ws child) = 2 * HexArith.bitLength child.subject + Hex.ECPP.replayWork child

def Hex.ECPP.search (budget : SearchBudget) : Nat → Nat → SearchM (Option Cert)

Structurally bounded recursion; failure of a child resumes the parent's remaining CM orders, without resetting any allocation or random state. This stateful worker requires a memo of previously checked successes admitted under the same allocations and sufficient remaining depth. Caller-supplied states are not validated here; produce starts fresh and checks its result.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.search budget 0 x✝ = do Hex.ECPP.unresolved✝ x✝ Hex.ECPP.Resource.depth pure none

structure Hex.ECPP.SearchResult : Type

The outcome of certificate search, together with its final random state and statistics. An error reports an unsuccessful attempt, not a proof that the input is composite.

• result : Except SearchError Cert

  A complete checked primality certificate, or the integer and reason for which the search stopped.

• state : SearchState

  Final random stream, counters and successful memo.

@[instance_reducible]

instance Hex.ECPP.instReprSearchResult : Repr SearchResult

Equations

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

def Hex.ECPP.instReprSearchResult.repr : SearchResult → Nat → Std.Format

Equations

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

def Hex.ECPP.produce (n seed : Nat) (budget : SearchBudget := { }) : SearchResult

Search for a primality certificate for n, using seed to choose the deterministic random sequence and budget to limit the work. Return a certificate and search statistics, or an error explaining why search stopped. Every .ok c result satisfies checkAt n c = true; failure to find a certificate does not imply that n is composite.

The default policy admits inputs through 256 bits. native512Budget and public512Budget explicitly select 512-bit search. For a theorem of Mathlib's Nat.Prime n, use HexECPPTheory.Native or apply the companion's soundness theorem to a kernel-checked checker equation.

Equations

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

theorem Hex.ECPP.produce_ok {n seed : Nat} {budget : SearchBudget} {c : Cert} (h : (produce n seed budget).result = Except.ok c) : checkAt n c = true

Every successful production result is accepted at the requested subject, independently of seed, allocation and arithmetic proposals.

def Hex.ECPP.frozenRows (c : Cert) : String

Freeze only replay inputs. Each row uses the already found q-order point and cofactor one, so conversion need not repeat any CM or factor search. The stored t = n + 1 - q is an encoding field, not a Frobenius trace.

Equations

• Hex.ECPP.frozenRows c = match Hex.ECPP.rows✝ c with | [] => toString c.subject | rows => "[" ++ ",".intercalate rows ++ "]"