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.

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)

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