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, α-CROWN, and α/β-CROWN 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} [Context α] {inDim outDim : ℕ} (aff : AffineVec α inDim outDim) (x : Spec.Tensor α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Spec.Tensor α (Spec.Shape.dim outDim Spec.Shape.scalar)

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

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

Enclosure predicate

We reuse Semantics.encloses from NN.MLTheory.CROWN.Graph for componentwise enclosure.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesVec {α : Type} [Context α] (B : FlatBox α) (v : FlatVec α) : Prop

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput {α : Type} [Context α] (ctx : AffineCtx) (x : Spec.Tensor α (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) (b : FlatAffineBounds α) (v : FlatVec α) : 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 EnclosesVec (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 graph_cert_soundness.lean, 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).

For IEEE32Exec, a separate evaluator can be plugged in later; the theorem below is stated for any vals satisfying SemLocalOK.

@[reducible, inline]

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

Alias for the semantic value record used by CertSoundness.

@[reducible, inline]

noncomputable abbrev NN.MLTheory.CROWN.Graph.CrownCertSoundness.evalNode? (nodes : Array Node) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (id : ℕ) : Option CertSoundness.Val

Alias for the partial node evaluator used by CertSoundness.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.CrownCertSoundness.SemLocalOK (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) : Prop

Alias for the local semantic consistency predicate used by CertSoundness.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.CrownCertSoundness.TopoSorted (g : Graph) : Prop

Alias for the topological-sorting predicate used by CertSoundness.

A CROWN certificate "step function" (checker interface)

The runtime runCROWN produces FlatAffineBounds by a forward pass. 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.

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.getAff? {α : Type} [Context α] (cert : Array (Option (FlatAffineBounds α))) (pid : ℕ) : Option (FlatAffineBounds α)

crownStepNode? is a parameter to the checker theorem: different certificate formats (plain CROWN, α/β-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} [Context α] (g : Graph) (step : Array (Option (FlatAffineBounds α)) → ℕ → Option (FlatAffineBounds α)) (cert : Array (Option (FlatAffineBounds α))) : Prop

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 ℕ Val) (vals : Array (Option Val)) (ctx : AffineCtx) (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) (step : Array (Option (FlatAffineBounds ℝ)) → ℕ → Option (FlatAffineBounds ℝ)) (cert : Array (Option (FlatAffineBounds ℝ))) : Prop

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 ℕ Val) (vals : Array (Option Val)) (ctx : AffineCtx) (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) (htopo : TopoSorted g) (_hsem : 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 ℕ Val) (vals : Array (Option Val)) (ctx : AffineCtx) (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) (htopo : TopoSorted g) (hsem : 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 : Val), cert[id]! = some b → vals[id]! = some v → EnclosesAtInput ctx x b v

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.IEEE32Val : Type

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32EvalNode? : Type

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.IEEE32EvalNoSelfDependency (evalNode? : IEEE32EvalNode?) : 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.IEEE32SemLocalOK (evalNode? : IEEE32EvalNode?) (g : Graph) (ps : ParamStore TorchLean.Floats.IEEE754.IEEE32Exec) (inputs : Std.HashMap ℕ IEEE32Val) (vals : Array (Option IEEE32Val)) : Prop

theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_semantics_ieee32exec_match (g : Graph) (_ps : ParamStore TorchLean.Floats.IEEE754.IEEE32Exec) (step : Array (Option (FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec)) → ℕ → Option (FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec)) (cert : Array (Option (FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec))) (evalNode? : IEEE32EvalNode?) (inputs : Std.HashMap ℕ IEEE32Val) (vals : Array (Option IEEE32Val)) (ctx : AffineCtx) (x : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) [Preorder TorchLean.Floats.IEEE754.IEEE32Exec] (htopo : TopoSorted g) (_hsem : IEEE32SemLocalOK 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

theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_semantics_ieee32exec (g : Graph) (ps : ParamStore TorchLean.Floats.IEEE754.IEEE32Exec) (step : Array (Option (FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec)) → ℕ → Option (FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec)) (cert : Array (Option (FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec))) (evalNode? : IEEE32EvalNode?) (inputs : Std.HashMap ℕ IEEE32Val) (vals : Array (Option IEEE32Val)) (ctx : AffineCtx) (x : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) [Preorder TorchLean.Floats.IEEE754.IEEE32Exec] (htopo : TopoSorted g) (hsem : IEEE32SemLocalOK 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 TorchLean.Floats.IEEE754.IEEE32Exec) (v : IEEE32Val), cert[id]! = some b → vals[id]! = some v → EnclosesAtInput ctx x b v