4.4. Bounded native production🔗

Hex.ECPP.produce accepts a subject, deterministic seed and Hex.ECPP.SearchBudget. Its finite CM portfolio proposes roots, curves and orders; checking remains the authority. Shared allocations survive local retries and recursive backtracking. Failed point proposals leave other twists and orders available. Complete local portfolio exhaustion and an unresolved recursive child have distinct diagnostics.

#guard (produce 17 0).result.toOption.any (checkAt 17)
def bitsExhausted : Bool :=
  match (produce 17 0 { maxBits := 4 }).result with
  | .error e => e.resource == .inputBits
  | _ => false
#guard bitsExhausted
def depthExhausted : Bool :=
  match (produce 17 0 { maxDepth := 0 }).result with
  | .error e => e.resource == .depth
  | _ => false
#guard depthExhausted

end HexECPPChapter

Exhaustion is not a compositeness verdict. The supported native policy admits subjects through 256 bits. Supplied-certificate checking and conversion have separate evidence through 512 bits; that does not extend native search to those sizes. Callers can inspect cumulative resource charges and backtracking statistics in the returned search state.

def

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

Native production accepts only the subject, seed and resource allocation. Every success is complete raw certificate data accepted by checkAt.

theorem

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

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

structure

Hex.ECPP.SearchBudget : Type
Hex.ECPP.SearchBudget : Type

Finite shared search allocations, with separate local retry ceilings.

Constructor

Hex.ECPP.SearchBudget.mk

Fields

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.