End-to-end CROWN certificate-checking framework (graph dialect)

This file provides the reusable end-to-end CROWN certificate-checking framework for graph dialects:

• an "end-to-end" enclosure theorem that composes:
  • a value semantics (evalNode? / SemLocalOK)
  • a per-node CROWN certificate (FlatAffineBounds)
  • a checker predicate (local consistency + per-op transfer soundness)

The main theorem is phrased in the standard "if the checker accepts, the bound holds" style.

Relation to auto_LiRPA / alpha-beta-CROWN

This file is written in a producer/checker style that matches common workflows:

• an external engine (e.g. the LiRPA engine in auto_LiRPA, or the verifier in alpha-beta-CROWN) can act as an untrusted producer of per-node affine bounds;
• Lean hosts the checker theorem: given a concrete step function and proved CrownTransferSound rules, accepted per-node affine bounds imply an end-to-end enclosure against the Lean graph denotation.

We deliberately state the main theorem schematically in terms of an abstract step function: plain CROWN and α-CROWN, with or without ReLU phases, can all share the same end-to-end checker theorem once their transfer rules are proved sound.

Trust boundary for transcendental ops

IEEE-754 does not standardize libm transcendental functions. For ops like exp, log, tanh, and sigmoid, soundness is therefore expressed as an explicit assumption in the checker predicate. A concrete checker may discharge that assumption with a proved approximation or a validated external interval enclosure, but it may not infer it from a particular libm implementation.

References (code)

• auto_LiRPA: https://github.com/Verified-Intelligence/auto_LiRPA
• alpha-beta-CROWN: https://github.com/Verified-Intelligence/alpha-beta-CROWN

Pointwise interpretation of affine bounds

A FlatAffineBounds α represents (componentwise) affine lower/upper functions of a fixed flattened input vector. To compare it to a concrete semantic value, we evaluate the affine maps at the chosen input point.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt {α : Type} [TorchLean.Storage α] [Context α] {inDim outDim : ℕ} (aff : AffineVec α inDim outDim) (x : TorchLean.Tensor α [inDim]) : TorchLean.Tensor α [outDim]

Evaluate an affine form A x + c at a concrete input point.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.boundsEvalAt {α : Type} [TorchLean.Storage α] [Context α] (b : FlatAffineBounds α) (x : TorchLean.Tensor α [b.inDim]) : FlatBox α

Evaluate affine lower/upper bounds at a concrete input point, yielding a FlatBox.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput {α : Type} [TorchLean.Storage α] [Context α] (ctx : AffineCtx) (x : TorchLean.Tensor α [ctx.inputDim]) (b : FlatAffineBounds α) (v : FlatTensor α) : Prop

Enclosure of a node value v under an affine bound b, evaluated at the designated input x.

This is a well-typed variant of EnclosesBox (boundsEvalAt b x) v that guards the dependent dimension b.inDim.

In a well-formed CROWN certificate, every bound satisfies b.inDim = ctx.inputDim, so the guard branch is the one that matters.

Local semantic consistency

We reuse the real-valued graph dialect evaluator from NN.MLTheory.CROWN.Proofs.GraphCertSoundness.Semantics, but we keep the definition abstract: the CROWN enclosure theorem below holds for any locally-consistent semantic interpretation vals (provided the graph is topologically sorted).

The real-valued theorem uses SemLocalOK. The IEEE32 section below supplies a separate interface for a caller-proved binary32 trace and transfer rules.

A CROWN certificate "step function" (checker interface)

The runtime runCROWN produces nodewise FlatAffineBounds. For a certificate/checker architecture, we treat the producer as untrusted and phrase correctness as a local step condition:

• CrownCertLocalOK: the certificate is locally consistent with a (trusted) step function.
• CrownTransferSound: each node kind's step function is sound w.r.t. the semantics.

This file separates the generic checker theorem from per-operator transfer proofs. In particular, transcendental operators are represented by explicit transfer-soundness assumptions supplied by the backend or checker workflow.

crownStepNode? is a parameter to the checker theorem: different certificate formats (plain CROWN, phased α-CROWN, split certificates) can share the same end-to-end theorem as long as they provide a step function and discharge transfer soundness.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK {α : Type} [TorchLean.Storage α] [Context α] (g : Graph) (step : Array (Option (FlatAffineBounds α)) → ℕ → Option (FlatAffineBounds α)) (cert : Array (Option (FlatAffineBounds α))) : Prop

The certificate is exactly what the step rule recomputes at every node: a local fixed point.

Replay checks local consistency with the chosen step rule. Its cost depends on that rule; this predicate alone does not establish transfer soundness or complete node coverage.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertCovers {α : Type} [TorchLean.Storage α] [Context α] (g : Graph) (cert : Array (Option (FlatAffineBounds α))) (vals : Array (Option (FlatTensor α))) : Prop

Every graph node has both a certificate entry and a semantic value.

Transfer-rule soundness assumptions

CrownTransferSound is the kernel of the checker theorem: it states that the certificate's local step rule is sound for each supported node kind.

For transcendental ops, this assumption is where you connect to an oracle model (e.g. Arb).

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound (g : Graph) (_ps : ParamStore ℝ) (_inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (step : Array (Option (FlatAffineBounds ℝ)) → ℕ → Option (FlatAffineBounds ℝ)) (cert : Array (Option (FlatAffineBounds ℝ))) : Prop

Each node's step rule is sound: parents enclosing their values force the node to enclose its own. This is the assumption a certificate format has to discharge to reuse the checker theorem.

Checker implies enclosure

If a certificate is locally consistent and the transfer rules are sound, then every certified node encloses the graph value computed at that node.

This theorem does not pick a certificate producer or a nonlinear backend. Those details come in through step and CrownTransferSound.

theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_semantics_match (g : Graph) (ps : ParamStore ℝ) (step : Array (Option (FlatAffineBounds ℝ)) → ℕ → Option (FlatAffineBounds ℝ)) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (_hsem : CertSoundness.SemLocalOK g ps inputs vals) (hcert : CrownCertLocalOK g step cert) (hsound : CrownTransferSound g ps inputs vals ctx x step cert) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some b, some v => EnclosesAtInput ctx x b v | x, x_1 => True

theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_semantics (g : Graph) (ps : ParamStore ℝ) (step : Array (Option (FlatAffineBounds ℝ)) → ℕ → Option (FlatAffineBounds ℝ)) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hcert : CrownCertLocalOK g step cert) (hsound : CrownTransferSound g ps inputs vals ctx x step cert) (id : ℕ) : id < g.nodes.size → ∀ (b : FlatAffineBounds ℝ) (v : CertSoundness.Val), cert[id]! = some b → vals[id]! = some v → EnclosesAtInput ctx x b v

Wherever both a certificate entry and a semantic value are present, the entry encloses the value.

This is the partial form of the main theorem: it says nothing about nodes the checker skipped, which is exactly why crown_checker_encloses_all_nodes below also takes a coverage hypothesis.

theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_all_nodes (g : Graph) (ps : ParamStore ℝ) (step : Array (Option (FlatAffineBounds ℝ)) → ℕ → Option (FlatAffineBounds ℝ)) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hcert : CrownCertLocalOK g step cert) (hcoverage : CrownCertCovers g cert vals) (hsound : CrownTransferSound g ps inputs vals ctx x step cert) (id : ℕ) : id < g.nodes.size → ∃ (b : FlatAffineBounds ℝ) (v : CertSoundness.Val), cert[id]! = some b ∧ vals[id]! = some v ∧ EnclosesAtInput ctx x b v

Complete certificate coverage turns local replay and transfer soundness into an enclosure theorem for every graph node. Unlike the partial match theorem above, this result cannot succeed through a missing certificate entry or missing semantic value.

IEEE32Exec specialization

For IEEE32 we still leave the node evaluator to the caller. The caller supplies the evaluator, proves that vals is its trace, and proves that evaluating node id does not read vals[id]!. The floating-point refinement theorem itself lives outside this checker lemma.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32.Val : Type

A flat node value in the binary32 executable semantics.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32.EvalNode : Type

Type of a caller-supplied binary32 node evaluator: nodes, parameters, inputs, partial trace, node id, and an optional result.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32.EvalNoSelfDependency (evalNode? : EvalNode) : Prop

The IEEE32 node evaluator may inspect already-computed values, but not the slot it is supposed to compute.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32.SemLocalOK (evalNode? : EvalNode) (g : Graph) (ps : ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4)) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) : Prop

The binary32 counterpart of SemLocalOK: vals is a full-length trace of evalNode?, and the evaluator does not read the slot it writes.

theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32.crown_checker_encloses_semantics_match (g : Graph) (_ps : ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4)) (step : Array (Option (FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4))) → ℕ → Option (FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4))) (cert : Array (Option (FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4)))) (evalNode? : EvalNode) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) (ctx : AffineCtx) (x : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4) [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (_hsem : SemLocalOK evalNode? g _ps inputs vals) (hcert : CrownCertLocalOK g step cert) (hsound : ∀ id < g.nodes.size, (∀ p ∈ g.nodes[id]!.parents, match cert[p]!, vals[p]! with | some bp, some vp => EnclosesAtInput ctx x bp vp | x, x_1 => True) → match step cert id, vals[id]! with | some b, some v => EnclosesAtInput ctx x b v | x, x_1 => True) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some b, some v => EnclosesAtInput ctx x b v | x, x_1 => True

Checker-implies-enclosure for ExecFloat.Binary 8 23 certificates, in the partial match form.

The proof is a pure topological induction: it only rewrites certificate entries with the step function and passes parent enclosures to hsound. In particular it never compares two ExecFloat.Binary 8 23 values, so no order structure on ExecFloat.Binary 8 23 is assumed; the enclosure predicate itself uses the LE supplied by the Context IEEE32Exec instance, which is not a lawful order because of NaN. Any order reasoning belongs in the transfer proofs discharging hsound.

theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32.crown_checker_encloses_semantics (g : Graph) (ps : ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4)) (step : Array (Option (FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4))) → ℕ → Option (FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4))) (cert : Array (Option (FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4)))) (evalNode? : EvalNode) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) (ctx : AffineCtx) (x : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4) [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : SemLocalOK evalNode? g ps inputs vals) (hcert : CrownCertLocalOK g step cert) (hsound : ∀ id < g.nodes.size, (∀ p ∈ g.nodes[id]!.parents, match cert[p]!, vals[p]! with | some bp, some vp => EnclosesAtInput ctx x bp vp | x, x_1 => True) → match step cert id, vals[id]! with | some b, some v => EnclosesAtInput ctx x b v | x, x_1 => True) (id : ℕ) : id < g.nodes.size → ∀ (b : FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Val._proof_1 Val._proof_2 Val._proof_3 Val._proof_4)) (v : Val), cert[id]! = some b → vals[id]! = some v → EnclosesAtInput ctx x b v

Checker-implies-enclosure for ExecFloat.Binary 8 23 certificates, quantified over the node ids at which both a certificate entry and a semantic value are present. See crown_checker_encloses_semantics_match for why no order on ExecFloat.Binary 8 23 is assumed.