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. This matches the repo's existing design: rigorous transcendental enclosures are handled via an oracle boundary (e.g. Arb-backed interval enclosures), not by assuming a particular libm.

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 α] [Preorder α] (B : FlatBox α) (v : FlatVec α) : Prop

def NN.MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput {α : Type} [Context α] [Preorder α] (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" theorem (end-to-end)

This is the theorem you want to use in the paper:

If a certificate is locally consistent and the transfer rules are sound, then the certificate enforces enclosure of the full graph semantics.

This theorem is deliberately generic: it does not commit to a particular certificate producer (plain CROWN vs α/β-CROWN) nor to a particular transcendental backend.

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 → match cert[id]!, vals[id]! with | some b, some v => EnclosesAtInput ctx x b v | x, x_1 => True

IEEE32Exec specialization (statement only)

The repository has a rich IEEE32 executable semantics (IEEE32Exec) and directed rounding lemmas for interval endpoints. However, a full end-to-end theorem connecting the float-running CROWN engine to IEEE32Exec execution requires a separate refinement theorem (rounding + libm/oracle).

For the paper, the right way to expose that dependency is to keep the theorem schematic: instantiate CrownTransferSound with the appropriate backend assumptions (e.g. Arb for transcendentals), and then the generic checker theorem applies.

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))) (_inputs : Std.HashMap ℕ (FlatVec TorchLean.Floats.IEEE754.IEEE32Exec)) (vals : Array (Option (FlatVec TorchLean.Floats.IEEE754.IEEE32Exec))) (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 : vals.size = g.nodes.size ∧ ∀ id < g.nodes.size, vals[id]! = vals[id]!) (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