Centralized certificate verification (trust choke point)

Every LeanCert reflective tactic ultimately closes a decidable certificate proposition, normally of the form check … = true. This module is the single place where that goal gets closed, and therefore the single place where the trusted base of the resulting proof is decided:

Mode	Closes with	Trusted base
.native	nativeEqTrue	kernel + compiler/runtime (native auxiliary axiom)
.kernel	cached kernel proof	kernel only (foundational axioms)
.auto	kernel, then native	kernel when it succeeds; fallback is reported

Design rules:

• .kernel never falls back to native verification. Failure is a hard error telling the user how to opt in to native trust explicitly.
• .auto may fall back, and reports when it does (trace[leancert.verification] always; one logInfo per process on first fallback).
• The typed boundary reduces the Decidable instance first, so a conclusive false result is data rather than an exception. Successful kernel proofs still go through mkAuxLemma for eager kernel validation and per-module caching.
• Native mode uses Lean's structured nativeEqTrue primitive directly: .notTrue is rejection, while compilation/evaluation exceptions are infrastructure failures.

Select the mode globally with set_option leancert.trust "kernel" (likewise "native", "auto"), or per invocation with (trust := kernel|native|auto). The per-invocation setting takes precedence.

Caveat for .auto: the heartbeat budget bounds elaboration-side work, but kernel reduction itself is not heartbeat-interruptible; a pathologically large certificate can exceed the budget wall-clock. Calibrated cost gates therefore route predictably large finite sums, integrations, and optimization certificates directly to native verification.

opaque leancert.trust : Lean.Option String

opaque leancert.trust.kernelHeartbeats : Lean.Option Nat

opaque leancert.trust.autoGate : Lean.Option Bool

opaque leancert.trust.autoMaxSumTerms : Lean.Option Nat

opaque leancert.trust.autoMaxPartitions : Lean.Option Nat

opaque leancert.trust.autoMaxOptIterations : Lean.Option Nat

opaque LeanCert.Tactic.autoFallbackReported : IO.Ref Bool

Reported once per process on the first .auto-mode native fallback, so a file with hundreds of certificate checks does not produce hundreds of messages. Per-invocation detail is always available under trace[leancert.verification].

inductive LeanCert.Tactic.VerificationMode : Type

How a certificate goal is allowed to be verified.

• native : VerificationMode

  Close with native_decide; the proof additionally trusts the Lean compiler and runtime (Lean.ofReduceBool).

• kernel : VerificationMode

  Close with decide +kernel; kernel-only trusted base. Never falls back to native verification.

• auto : VerificationMode

  Try the kernel route first, fall back to native_decide, reporting the fallback.

@[instance_reducible]

instance LeanCert.Tactic.instDecidableEqVerificationMode : DecidableEq VerificationMode

Equations

• LeanCert.Tactic.instDecidableEqVerificationMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanCert.Tactic.instReprVerificationMode.repr : VerificationMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationMode : Repr VerificationMode

Equations

• LeanCert.Tactic.instReprVerificationMode = { reprPrec := LeanCert.Tactic.instReprVerificationMode.repr }

@[instance_reducible]

instance LeanCert.Tactic.instInhabitedVerificationMode : Inhabited VerificationMode

Equations

• LeanCert.Tactic.instInhabitedVerificationMode = { default := LeanCert.Tactic.instInhabitedVerificationMode.default }

inductive LeanCert.Tactic.VerificationUsed : Type

Which route actually closed a certificate goal.

• kernel : VerificationUsed
• native : VerificationUsed

@[instance_reducible]

instance LeanCert.Tactic.instDecidableEqVerificationUsed : DecidableEq VerificationUsed

Equations

• LeanCert.Tactic.instDecidableEqVerificationUsed x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationUsed : Repr VerificationUsed

Equations

• LeanCert.Tactic.instReprVerificationUsed = { reprPrec := LeanCert.Tactic.instReprVerificationUsed.repr }

def LeanCert.Tactic.instReprVerificationUsed.repr : VerificationUsed → Nat → Std.Format

Equations

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

inductive LeanCert.Tactic.VerificationCause : Type

Why a particular verification route was used.

This distinguishes an explicit native request from the two reasons that .auto can use native verification.

• explicitNative : VerificationCause

  The caller explicitly requested native verification.

• explicitKernel : VerificationCause

  The caller explicitly requested kernel verification.

• autoKernel : VerificationCause

  Auto mode successfully used kernel verification.

• autoNativeGate : VerificationCause

  Auto mode selected native verification before attempting the kernel because a calibrated cost gate fired.

• autoNativeFallback : VerificationCause

  Auto mode used native verification after its kernel attempt failed.

@[instance_reducible]

instance LeanCert.Tactic.instDecidableEqVerificationCause : DecidableEq VerificationCause

Equations

• LeanCert.Tactic.instDecidableEqVerificationCause x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationCause : Repr VerificationCause

Equations

• LeanCert.Tactic.instReprVerificationCause = { reprPrec := LeanCert.Tactic.instReprVerificationCause.repr }

def LeanCert.Tactic.instReprVerificationCause.repr : VerificationCause → Nat → Std.Format

Equations

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

structure LeanCert.Tactic.VerificationEvent : Type

Structured telemetry for one successfully closed certificate goal.

The event is returned directly to the caller. It is not stored globally, so speculative tactic attempts can discard it together with their proof state.

• requested : VerificationMode

  The resolved policy in force for this certificate closure.

• used : VerificationUsed

  The route that actually closed the certificate.

• cause : VerificationCause

  Why that route was selected.

• gateReason : Option String

  Human-readable auto-gate explanation, present exactly for autoNativeGate events.

def LeanCert.Tactic.instReprVerificationEvent.repr : VerificationEvent → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationEvent : Repr VerificationEvent

Equations

• LeanCert.Tactic.instReprVerificationEvent = { reprPrec := LeanCert.Tactic.instReprVerificationEvent.repr }

structure LeanCert.Tactic.VerificationUsage : Type

Verification telemetry for zero or more retained certificate closures.

• events : Array VerificationEvent

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationUsage : Repr VerificationUsage

Equations

• LeanCert.Tactic.instReprVerificationUsage = { reprPrec := LeanCert.Tactic.instReprVerificationUsage.repr }

def LeanCert.Tactic.instReprVerificationUsage.repr : VerificationUsage → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instInhabitedVerificationUsage : Inhabited VerificationUsage

Equations

• LeanCert.Tactic.instInhabitedVerificationUsage = { default := LeanCert.Tactic.instInhabitedVerificationUsage.default }

inductive LeanCert.Tactic.VerificationFailure : Type

Infrastructure failures while checking a Boolean certificate.

An ordinary checker result of false is deliberately not represented here: it is the .rejected case of VerificationResult.

• malformedCertificateGoal (detail : String) : VerificationFailure

  The proposed certificate goal was not a closed decidable proposition.

• kernelFailure (detail : String) : VerificationFailure

  Kernel reduction could not determine or validate the checker result.

• nativeFailure (detail : String) : VerificationFailure

  Native compilation or evaluation failed before producing a result.

• internalError (detail : String) : VerificationFailure

  The verification protocol itself encountered an unexpected invariant failure.

def LeanCert.Tactic.instReprVerificationFailure.repr : VerificationFailure → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationFailure : Repr VerificationFailure

Equations

• LeanCert.Tactic.instReprVerificationFailure = { reprPrec := LeanCert.Tactic.instReprVerificationFailure.repr }

inductive LeanCert.Tactic.VerificationResult : Type

Typed result of attempting to close one Boolean certificate goal.

Only .accepted mutates the retained tactic state. Both .rejected and .failed restore the complete state saved on entry.

• accepted (event : VerificationEvent) : VerificationResult

  The checker evaluated to true; the certificate goal is assigned.

• rejected : VerificationResult

  The checker conclusively evaluated to false.

• failed (failure : VerificationFailure) : VerificationResult

  The checker could not be evaluated or its proof could not be retained.

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationResult : Repr VerificationResult

Equations

• LeanCert.Tactic.instReprVerificationResult = { reprPrec := LeanCert.Tactic.instReprVerificationResult.repr }

def LeanCert.Tactic.instReprVerificationResult.repr : VerificationResult → Nat → Std.Format

Equations

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

def LeanCert.Tactic.VerificationEvent.toUsage (event : VerificationEvent) : VerificationUsage

Regard one successful certificate closure as aggregate usage.

Equations

• event.toUsage = { events := #[event] }

def LeanCert.Tactic.VerificationUsage.singleton (event : VerificationEvent) : VerificationUsage

Aggregate usage containing one successful certificate closure.

Equations

• LeanCert.Tactic.VerificationUsage.singleton event = event.toUsage

def LeanCert.Tactic.VerificationUsage.combine (left right : VerificationUsage) : VerificationUsage

Combine independently retained verification events, preserving order.

Equations

• left.combine right = { events := left.events ++ right.events }

def LeanCert.Tactic.VerificationUsage.kernelChecks (usage : VerificationUsage) : Nat

Number of retained certificates closed by kernel reduction.

Equations

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

def LeanCert.Tactic.VerificationUsage.nativeChecks (usage : VerificationUsage) : Nat

Number of retained certificates closed by native reduction.

Equations

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

def LeanCert.Tactic.VerificationUsage.autoGateReasons (usage : VerificationUsage) : Array String

Reasons for auto-mode decisions that bypassed kernel verification.

Equations

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

def LeanCert.Tactic.VerificationMode.ofString? : String → Option VerificationMode

Equations

• LeanCert.Tactic.VerificationMode.ofString? "native" = some LeanCert.Tactic.VerificationMode.native
• LeanCert.Tactic.VerificationMode.ofString? "kernel" = some LeanCert.Tactic.VerificationMode.kernel
• LeanCert.Tactic.VerificationMode.ofString? "auto" = some LeanCert.Tactic.VerificationMode.auto
• LeanCert.Tactic.VerificationMode.ofString? x✝ = none

def LeanCert.Tactic.VerificationMode.asString : VerificationMode → String

Option-value spelling of the mode ("kernel" / "native" / "auto").

Equations

• LeanCert.Tactic.VerificationMode.native.asString = "native"
• LeanCert.Tactic.VerificationMode.kernel.asString = "kernel"
• LeanCert.Tactic.VerificationMode.auto.asString = "auto"

structure LeanCert.Tactic.VerificationConfig : Type

Configuration for certificate verification. Tactics resolve this from options via VerificationConfig.current; public (trust := …) syntax overrides it per invocation.

• mode : VerificationMode
• kernelHeartbeats : Nat

  Heartbeat budget for the kernel attempt in .auto mode.

@[instance_reducible]

instance LeanCert.Tactic.instReprVerificationConfig : Repr VerificationConfig

Equations

• LeanCert.Tactic.instReprVerificationConfig = { reprPrec := LeanCert.Tactic.instReprVerificationConfig.repr }

def LeanCert.Tactic.instReprVerificationConfig.repr : VerificationConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instInhabitedVerificationConfig : Inhabited VerificationConfig

Equations

• LeanCert.Tactic.instInhabitedVerificationConfig = { default := LeanCert.Tactic.instInhabitedVerificationConfig.default }

def LeanCert.Tactic.VerificationConfig.current : Lean.CoreM VerificationConfig

Read the verification configuration from the current options (leancert.trust, leancert.trust.kernelHeartbeats).

Equations

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

Auto-mode cost gate

Thresholds come from scripts/bench-trust/baselines/ (see the README there): kernel reduction is essentially free for point/bound/Newton certificates, cheap for moderate partition/subdivision counts, and crosses over to "markedly worse than native" around 10^4 finite-sum terms (superlinear time, +1.5 GiB RSS). The gate reads scale parameters syntactically off the certificate goal; anything it does not recognize is attempted normally.

The checker names below are unresolved Name literals because this module deliberately imports only Lean (everything in LeanCert imports it back). LeanCert/Test/TrustModes.lean builds these applications with resolved names and asserts the gate fires, so a checker rename breaks CI rather than silently disabling the gate.

def LeanCert.Tactic.autoGateReason? (opts : Lean.Options) (certType : Lean.Expr) : Option String

If the certificate is predictably past the kernel/native crossover, return a human-readable reason to skip the kernel attempt in auto mode. none means "attempt the kernel".

Equations

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

def LeanCert.Tactic.closeCertificateGoalTyped (cfg : VerificationConfig) (certGoal : Lean.MVarId) (tacticName : String := "leancert") : Lean.Elab.Tactic.TacticM VerificationResult

Close a decidable certificate goal (normally check … = true) according to the verification mode and return a typed result.

Only .accepted retains state changes. Rejection, malformed goals, and verification infrastructure failures restore the complete tactic state saved on entry, including environment declarations and messages.

Equations

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

def LeanCert.Tactic.VerificationFailure.message (tacticName : String) : VerificationFailure → String

Equations

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

def LeanCert.Tactic.tacticLeancert_verify_cert : Lean.ParserDescr

Close the current goal as a LeanCert certificate check according to the configured verification route (leancert.trust, or a (trust := …) override active via withTrustMode). For tactic implementations that embed certificate obligations inside quoted proof terms — (by leancert_verify_cert) — where the typed boundary cannot be called directly. Not intended for end users.

Equations

• LeanCert.Tactic.tacticLeancert_verify_cert = Lean.ParserDescr.node `LeanCert.Tactic.tacticLeancert_verify_cert 1024 (Lean.ParserDescr.nonReservedSymbol "leancert_verify_cert" false)

Public per-invocation syntax: (trust := kernel|native|auto)

Tactics accept an optional trailing leancertTrustItem; when present it overrides the leancert.trust option for that invocation only (implemented by running the tactic core under withOptions, so every certificate check in the invocation — including nested fallback strategies — honors it).

def LeanCert.Tactic.leancertTrustMode.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.leancertTrustMode : Category

Parser category for verification modes. auto needs an explicit branch because it is a reserved Lean token rather than an ident.

Equations

• Lean.Parser.Category.leancertTrustMode = { }

def LeanCert.Tactic.leancertTrustMode_ : Lean.ParserDescr

Equations

• LeanCert.Tactic.leancertTrustMode_ = Lean.ParserDescr.node `LeanCert.Tactic.leancertTrustMode_ 1022 (Lean.ParserDescr.const `ident)

def LeanCert.Tactic.leancertTrustModeAuto : Lean.ParserDescr

Equations

• LeanCert.Tactic.leancertTrustModeAuto = Lean.ParserDescr.node `LeanCert.Tactic.leancertTrustModeAuto 1022 (Lean.ParserDescr.nonReservedSymbol "auto" false)

def LeanCert.Tactic.leancertTrustItem : Lean.ParserDescr

Per-invocation verification route for LeanCert tactics: (trust := kernel), (trust := native), or (trust := auto).

Equations

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

def LeanCert.Tactic.elabTrustItem? : Option (Lean.TSyntax `LeanCert.Tactic.leancertTrustItem) → Lean.Elab.Tactic.TacticM (Option VerificationMode)

Elaborate an optional (trust := …) item.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Tactic.elabTrustItem? none = pure none

def LeanCert.Tactic.withTrustMode {α : Type} (mode? : Option VerificationMode) (act : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

Run act with leancert.trust overridden to mode? when provided.

Equations

• LeanCert.Tactic.withTrustMode none act = act
• LeanCert.Tactic.withTrustMode (some m) act = Lean.withOptions (fun (o : Lean.Options) => o.set `leancert.trust m.asString) act

#assert_trust: CI trust manifests

#assert_trust kernel thm / #assert_trust native thm pin a theorem's trust class. Drift in either direction fails: a kernel-clean theorem acquiring native-compiler trust is a regression, and a native-pinned theorem losing its native dependency means the manifest should be tightened to kernel. sorryAx and unrecognized axioms always fail.

inductive LeanCert.Tactic.TrustClass : Type

Trust classification of a single axiom.

• foundational : TrustClass

  propext, Classical.choice, Quot.sound.

• nativeCompiler : TrustClass

  Lean.ofReduceBool / Lean.ofReduceNat / Lean.trustCompiler, or a per-declaration native_decide auxiliary (<decl>._native.native_decide.ax_*).

• sorryAx : TrustClass

  sorryAx.

• custom : TrustClass

  Anything else.

@[instance_reducible]

instance LeanCert.Tactic.instDecidableEqTrustClass : DecidableEq TrustClass

Equations

• LeanCert.Tactic.instDecidableEqTrustClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanCert.Tactic.instReprTrustClass.repr : TrustClass → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instReprTrustClass : Repr TrustClass

Equations

• LeanCert.Tactic.instReprTrustClass = { reprPrec := LeanCert.Tactic.instReprTrustClass.repr }

def LeanCert.Tactic.classifyAxiom (n : Lean.Name) : TrustClass

Classify an axiom name into its trust class.

Equations

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

def LeanCert.Tactic.«command#assert_trust__» : Lean.ParserDescr

#assert_trust kernel thm: thm depends on foundational axioms only. #assert_trust native thm: thm additionally depends on native-compiler trust (and nothing worse). Any sorryAx or unrecognized axiom fails both.

Equations

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