End-to-end IBP soundness (graph dialect, over ℝ)

NN.MLTheory.CROWN.Proofs.GraphCertSoundness proves:

If a per-node IBP certificate is locally consistent (CertLocalOK) and the value semantics is locally consistent (SemLocalOK), then each certified box encloses the corresponding value.

This file supplies a concrete, total evaluator and a concrete, total IBP propagation and proves they satisfy the local-consistency predicates under the TopoSorted assumption (parents have smaller ids). Combining these results yields an end-to-end theorem.

The final section connects the proof-side pass runIBP? to the engine's executable runIBP (runIBP_eq_runIBP?) and derives the end-to-end theorem for the engine (runIBP_encloses_evalGraphRec).

Array helper lemmas (getElem! after setIfInBounds)

Total evaluators (Nat-recursive, prefix semantics)

We define fold-by-id evaluators using Nat.rec rather than List.foldl to keep proofs small and stable. The resulting arrays coincide with the intended “evaluate in node-id order” semantics.

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

Evaluate the first n nodes of g in id order, leaving the rest none.

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

Evaluate all nodes of g in id order, returning the final value array.

def NN.MLTheory.CROWN.Graph.CertSoundness.runIBPPrefix (g : Graph) (ps : ParamStore ℝ) : ℕ → Array (Option (FlatBox ℝ))

Prefix evaluator for the safe IBP checker step (certStepNode?).

noncomputable def NN.MLTheory.CROWN.Graph.CertSoundness.runIBP? (g : Graph) (ps : ParamStore ℝ) : Array (Option (FlatBox ℝ))

Run the safe IBP checker step across the full graph, producing a per-node certificate array.

Prefix size facts.

Prefix stability: later writes do not change earlier entries.

Congruence of the step functions under TopoSorted

If two arrays agree on all parent ids of node id, then the step function at id evaluates to the same result.

Local consistency of the total evaluators

theorem NN.MLTheory.CROWN.Graph.CertSoundness.evalGraphRec_SemLocalOK (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) (htopo : TopoSorted g) (hsupp : Supported g) : SemLocalOK g ps inputs (evalGraphRec g ps inputs)

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?_CertLocalOK (g : Graph) (ps : ParamStore ℝ) (htopo : TopoSorted g) : CertLocalOK g ps (runIBP? g ps)

Under topological order, the certificate produced by runIBP? satisfies CertLocalOK.

End-to-end theorem

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?_encloses_evalGraphRec (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) (htopo : TopoSorted g) (hsupp : Supported g) (hinputs : InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → match (runIBP? g ps)[id]!, (evalGraphRec g ps inputs)[id]! with | some B, some v => EnclosesBox B v | x, x_1 => True

The engine pass runIBP

runIBP (in NN.MLTheory.CROWN.Graph.Engine.IBP) is the executable pass that checkers call. It differs from the proof-side runIBP? above in the following ways.

• It folds propagateIBPNode over List.finRange instead of recursing on a prefix length.
• propagateIBPNode reads parent boxes with get!, so a missing parent box is replaced by the default box instead of producing none.
• It returns an all-none array when crownGraphSemanticsSupported rejects the graph.
• For tanh, sigmoid, sin, and cos it uses the NonlinearBoundOps enclosures, whereas certStepNode? uses the Runtime.Ops.IBP boxes. For sin and cos these are different boxes (both sound), so the two passes do not agree on those ops.

The first three differences are inessential. We identify the two passes on the op set where the per-node steps coincide (EngineCore), under the hypothesis that the proof-side pass produced a box at every node (IBPCovers), which rules out the get! default path. The engine's behaviour is not changed.

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

Node kinds on which propagateIBPNode and certStepNode? compute the same box.

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

Every node of a certificate array carries a box.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.supported_of_engineCore {g : Graph} (h : EngineCore g) : Supported g

The engine-core op set is contained in the op set of the IBP soundness theorem.

def NN.MLTheory.CROWN.Graph.CertSoundness.runIBPEnginePrefix (g : Graph) (ps : ParamStore ℝ) : ℕ → Array (Option (FlatBox ℝ))

Prefix of the engine's fold, by recursion on the number of processed nodes.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP_eq_runIBPEnginePrefix (g : Graph) (ps : ParamStore ℝ) (hguard : g.crownGraphSemanticsSupported ps = true) : g.runIBP ps = runIBPEnginePrefix g ps g.nodes.size

runIBP is the engine prefix recursion when the semantic guard accepts the graph.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP_eq_replicate_none (g : Graph) (ps : ParamStore ℝ) (hguard : g.crownGraphSemanticsSupported ps = false) : g.runIBP ps = Array.replicate g.nodes.size none

runIBP is all none when the semantic guard rejects the graph.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP_eq_runIBP? (g : Graph) (ps : ParamStore ℝ) (htopo : TopoSorted g) (hcore : EngineCore g) (hguard : g.crownGraphSemanticsSupported ps = true) (hcov : IBPCovers g (runIBP? g ps)) : g.runIBP ps = runIBP? g ps

The engine's runIBP computes exactly the proof-side runIBP? on engine-core graphs, provided the semantic guard accepts the graph and the proof-side pass produced a box at every node.

Coverage is needed because propagateIBPNode reads parents with get!: at a node whose parent box is missing, the engine would compute from a default box while certStepNode? returns none.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP_encloses_evalGraphRec (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) (htopo : TopoSorted g) (hcore : EngineCore g) (hcov : IBPCovers g (runIBP? g ps)) (hinputs : InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → ∀ (B : FlatBox ℝ) (v : Val), (g.runIBP ps)[id]! = some B → (evalGraphRec g ps inputs)[id]! = some v → EnclosesBox B v

End-to-end soundness of the engine's IBP pass: every box computed by runIBP encloses the value computed by the total evaluator evalGraphRec at the same node.

The statement quantifies over node ids at which the engine produced a box B and the evaluator a value v, so it cannot hold through a missing entry. The semantic guard needs no hypothesis: if crownGraphSemanticsSupported rejects the graph, runIBP produces no boxes and there is nothing to prove. Coverage of the proof-side pass is needed for the reason given at runIBP_eq_runIBP?.