Graph Certificate Semantics

Value semantics for the verifier graph dialect over ℝ, together with the local semantic consistency predicate used by certificate soundness proofs.

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

A value flowing along a graph edge in the semantics: a real flat tensor.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.CertSoundness.encloses (B : FlatBox ℝ) (x : TorchLean.Tensor ℝ [B.dim]) : Prop

Componentwise enclosure predicate for a tensor point inside a FlatBox.

def NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) (v : FlatTensor α) : Prop

A flat box encloses a flat tensor when their dimensions agree and every coordinate is bounded.

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.

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.evalBinaryMatmul? (leftShape rightShape : Spec.Shape) (left right : Val) : Option Val

Binary matmul uses the runtime's broadcast layout and ordered scalar contraction.

def NN.MLTheory.CROWN.Graph.CertSoundness.evalSomeTensorUnary? (shape : Spec.Shape) (op : Spec.SomeTensor ℝ → Except String (Spec.SomeTensor ℝ)) (x : Val) : Option Val

Reconstruct a shaped value, run a generic unary tensor operation, and flatten its result.

noncomputable def NN.MLTheory.CROWN.Graph.CertSoundness.evalConvNode? (configuration : IR.ConvConfig) (parentShape outShape : Spec.Shape) (id : ℕ) (ps : ParamStore ℝ) (input : Val) : Option Val

Value evaluation of the same checked grouped convolution used by the interval transfer.

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 ℝ).

theorem NN.MLTheory.CROWN.Graph.CertSoundness.array_mapM_congr_of_mem {α β : Type} {f g : α → Option β} (xs : Array α) (h : ∀ x ∈ xs, f x = g x) : Array.mapM f xs = Array.mapM g xs

Optional traversal depends only on the callback values at array members.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.evalNode?_congr (nodes : Array Node) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) (vals₁ vals₂ : Array (Option Val)) (id : ℕ) (h : ∀ p ∈ nodes[id]!.parents, getVal? vals₁ p = getVal? vals₂ p) : evalNode? nodes ps inputs vals₁ id = evalNode? nodes ps inputs vals₂ id

evalNode? reads the value table only at the node's parents, through getVal?. Every arm decodes its parents with unaryParent?, binaryParents?, or a traversal of parents.

The main soundness theorem does not fix a particular graph evaluator. It is stated 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. Concrete total evaluators (evalGraphRec in NN.MLTheory.CROWN.Proofs.GraphRunibpEndToEnd) are then shown to satisfy this predicate.

This separates 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

vals is a full semantic interpretation of g: one entry per node, each equal to what the node's own evaluation rule produces from its parents' entries.

This is stated as a local condition rather than built by a recursive evaluator so the soundness theorem applies to any interpretation, however it was obtained.