structure Hex.ECPP.DataBudget : Type

Finite admission policy for constructor data enclosing certificates. Extra names must be the enclosing type's trusted constructors and instances.

• maxNodes : Nat

  Maximum visited syntax nodes, including expanded let occurrences.

• numeralBits : Nat

  Maximum numeral size; certificate fields are admitted separately.

• extraNames : List Lean.Name

  Additional constructors and numeral instances for an enclosing type.

def Hex.ECPP.reifyCert : Cert → Lean.Expr

Reify a bounded raw proposal as kernel-checkable constructor data. Call validateCert first when the proposal has not already passed replay preflight.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.reifyCert (Hex.ECPP.Cert.base c) = Lean.mkApp (Lean.mkConst `Hex.ECPP.Cert.base) (Hex.PrimalityTactic.reifyPrimeCert c)

def Hex.ECPP.auditData (e : Lean.Expr) (b : DataBudget := { }) : Lean.MetaM Lean.Expr

Audit exposed constructor data and bounded let expansion before evaluation. No compiled override or executable body enters the returned expression.

Equations

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

def Hex.ECPP.readCert (e : Lean.Expr) : Lean.MetaM Cert

Build a proof from a supplied exposed certificate. The evaluated producer is discarded; the kernel checks the reified raw data and checker reduction.

Equations

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

def Hex.ECPP.validateCert (cert : Cert) : Lean.MetaM Unit

Validate a raw proposal against the finite replay policy.

Equations

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