Proof-level IBP certificate soundness for the graph dialect

This file is the “strong” version of IBP certificate checking:

• NN.Verification.IBPNodeCert checks (at runtime, with floats) that a Python certificate matches Lean’s computed per-node bounds.
• Here we prove (at theorems level, over ℝ) that a per-node certificate implies enclosure of the graph semantics.

Verifier Graph Semantics

The current verifier graph dialect uses a slightly non-standard convention for .matmul: instead of a 2-parent matrix multiply node, the weight matrix is supplied externally via ParamStore.matmulW, and the node behaves like a bias-free linear layer y = W x.

So in this file we define a semantics that matches that convention:

• .linear uses ParamStore.linearWB and means y = W x + b.
• .matmul uses ParamStore.matmulW and means y = W x (bias = 0).

This semantics is stated on flattened vectors (a FlatVec), matching what runIBP computes.

Scope

To keep the proof manageable while matching the LiRPA graph patterns used by the verifier, we prove soundness for the following node kinds:

• .input, .const, .detach
• .add, .sub, .mul_elem, .relu
• .linear, .matmul (the ParamStore-based dialect)
• .tanh, .sigmoid, .sin, .cos

All other ops are considered unsupported in this theorem file.

What is actually proven?

We prove:

If a certificate cert satisfies the local IBP step equation at every node (i.e. every node’s box is exactly what IBP would compute from its parents’ boxes and params), and if the concrete inputs used by the semantics are enclosed by the input boxes, then every node’s concrete semantic value is enclosed by its certified interval box.

This is the standard “local soundness + induction over a topological order” proof structure used in certified verifiers.

Basic types and predicates

We work over ℝ because it has the right order structure for “true” soundness theorems. The runtime checkers operate over Float (fast, executable), and can be used to connect a Python-produced floating certificate to the same computations in Lean.

@[reducible, inline]

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

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.CertSoundness.encloses (B : FlatBox ℝ) (x : Spec.Tensor ℝ (Spec.Shape.dim B.dim Spec.Shape.scalar)) : Prop

Componentwise enclosure predicate for a tensor point inside a FlatBox.

def NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox (B : FlatBox ℝ) (v : Val) : Prop

EnclosesBox B v means the value vector v lies inside the interval box B.

We phrase enclosure using the existing Sem.encloses predicate, but our semantic values are FlatVecs (carrying their dimension as a Nat), so we also carry a dimension equality witness.

Denotational (value) semantics for the verifier graph dialect

The semantics is defined as a safe Option evaluator:

• If required parameters are missing, it returns none.
• If parents are missing (not yet evaluated) or dimensions mismatch, it returns none.

This keeps the semantic definition total, and avoids the partial get! used in the runtime propagation code.

def NN.MLTheory.CROWN.Graph.CertSoundness.getVal? (vals : Array (Option Val)) (pid : ℕ) : Option Val

Safe lookup of a previously computed parent value.

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

Value semantics for a single node in the supported dialect (over ℝ).

noncomputable def NN.MLTheory.CROWN.Graph.CertSoundness.evalGraph? (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) : Array (Option Val)

Evaluate an entire graph in node-id order using evalNode?.

Even though we provided an executable evalGraph?, the main soundness theorem below does not depend on it.

Reason: proving properties about the foldl evaluator would introduce a lot of “bookkeeping” lemmas about Array.set! and list folds.

Instead, we state soundness for any array vals that is a local model of the semantics step: each node’s value must equal evalNode? computed from its parents’ values.

This is a standard technique in proof engineering: separate “semantic consistency” from “the particular implementation of the evaluator”.

Local semantic consistency (SemLocalOK)

SemLocalOK g ps inputs vals means:

• vals has the correct length, and
• each entry vals[id] equals evalNode? computed from the full array vals.

For a DAG (and only for a DAG), this is exactly the property that vals is a valid interpretation of the graph semantics.

Existence and uniqueness of vals are evaluator-correctness facts. This file proves the certificate theorem in the reusable form: for any semantic interpretation vals, a locally-correct certificate encloses it.

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

The IBP “certificate step” (safe, total)

This is a safe version of propagateIBPNode tailored to the subset of ops we prove soundness for. It defines what it means for a per-node certificate to be “locally well-formed”.

Important: the runtime implementation propagateIBPNode uses get! on parent boxes; it assumes topological order and that earlier boxes exist. Here we avoid partiality by returning none whenever parents are missing.

def NN.MLTheory.CROWN.Graph.CertSoundness.getBox? (cert : Array (Option (FlatBox ℝ))) (pid : ℕ) : Option (FlatBox ℝ)

noncomputable def NN.MLTheory.CROWN.Graph.CertSoundness.certStepNode? (nodes : Array Node) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) (id : ℕ) : Option (FlatBox ℝ)

Safe per-node IBP step for the checker semantics.

This is the total (option-returning) analogue of the runtime propagateIBPNode, restricted to the ops handled in the soundness development.

def NN.MLTheory.CROWN.Graph.CertSoundness.CertLocalOK (g : Graph) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) : Prop

A certificate is locally consistent if every node equals certStepNode? at that node.

Op-level soundness lemmas (enclosure for each supported step)

These lemmas are the building blocks for the final “certificate ⇒ semantics enclosure” theorem.

This proof reuses the following existing components:

• Linear IBP soundness over ℝ is already proved in NN.MLTheory.CROWN.mlp as NN.MLTheory.CROWN.Theorems.ibp_linear_sound_real.
• For add/sub/relu on FlatBox, the graph file already contains enclosure lemmas in NN.MLTheory.CROWN.Graph.Theorems.Semantics.

Helpers: our bound propagation uses BoundOps.min2/max2, which are defined via decide (a > b). For ℝ these coincide with min/max.

Casting lemmas (avoid cases on B.dim = v.n)

FlatBox and FlatVec carry their dimensions in dependent types, so it is tempting to cases equalities like h : B.dim = v.n to “align” types. In Lean this can easily trigger dependent elimination failures when the equality mentions fields of dependent records.

Instead, we keep such equalities as data and move tensors/boxes across them using castDimScalar / castBoxDim. The following small lemmas are proved once (by cases on fresh Nat equalities) and then used throughout the main proof without ever cases-ing on B.dim = v.n directly.

Point Boxes Always Enclose Their Point

This is used in the .const case, where a constant node certifies a point box [v,v] and the semantics returns exactly the same v.

Sigmoid monotonicity (via Mathlib’s Real.sigmoid)

Our Activation.Math.sigmoid_spec definition over ℝ is exactly the Mathlib sigmoid function. So we can reuse its monotonicity lemma.

Tanh monotonicity (proved from calculus in Mathlib)

Mathlib does not expose a Real.tanh_monotone lemma under that name. We prove it here:

1. Use the identity tanh x = sinh x / cosh x.
2. Differentiate the quotient, using d/dx sinh = cosh and d/dx cosh = sinh.
3. Simplify the derivative using cosh^2 - sinh^2 = 1.
4. Conclude strict monotonicity from deriv > 0, hence monotonicity.

Soundness of Runtime.Ops.IBP.map_minmax for monotone scalar functions

Runtime.Ops.IBP.sigmoid and Runtime.Ops.IBP.tanh are defined using map_minmax. If the activation is monotone, then the min/max of the endpoints is a correct enclosure.

Soundness of the 1-Lipschitz sin/cos enclosures

Runtime.Ops.IBP.sin / Runtime.Ops.IBP.cos use a midpoint enclosure with radius r=(u-l)/2, clamped to [-1,1]. This avoids periodic case splits while remaining sound.

Main theorem: local IBP certificate implies semantic enclosure (supported subset)

We use strong induction on node id, assuming a topological order: every parent id is strictly smaller than the node id.

def NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted (g : Graph) : Prop

Topological order assumption: all parent ids are strictly smaller than the node id.

def NN.MLTheory.CROWN.Graph.CertSoundness.Supported (g : Graph) : Prop

A graph is supported by this soundness theorem if every node kind is in our supported subset.

def NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) : Prop

Inputs are well-formed if every .input node has a value, and that value is enclosed by its input box from ParamStore.inputBoxes.

The enclosure theorem

Assumptions:

• TopoSorted g: induction works (parents are earlier).
• Supported g: every node kind is handled by the proof.
• CertLocalOK g ps cert: the certificate is locally consistent with the IBP step.
• InputsEnclosed g ps inputs: semantic inputs are inside the certified input boxes.
• SemLocalOK g ps inputs vals: vals is a locally-consistent semantic interpretation.

Conclusion:

• For every node id, if the semantics produces a value v and the certificate has a box B, then B encloses v.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics (g : Graph) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) (htopo : TopoSorted g) (hsupp : Supported g) (hcert : CertLocalOK g ps cert) (hsem : SemLocalOK g ps inputs vals) (hinputs : InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some B, some v => EnclosesBox B v | x, x_1 => True