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

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: the write at step n (in or out of bounds) leaves earlier entries alone.

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) : SemLocalOK g ps inputs (evalGraphRec g ps inputs)

Under topological order, the total evaluator evalGraphRec satisfies SemLocalOK.

No restriction on node kinds is needed: evalNode? consults the table only at parents, which precede the node, so the value written at step id + 1 from the prefix equals the value evalNode? reads off the final table.

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.
• 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.

Both passes propagate missing parent boxes through Option. We identify them on the op set where the per-node steps coincide (EngineCore), using the coverage hypothesis (IBPCovers) of the end-to-end enclosure theorem.

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 supplies a successful certificate step at each prefix of the induction.

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?.