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 (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 FlatTensors (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.

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

Safe lookup of a previously computed parent value.

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

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.