IBPCert

IBP “output bounds” certificate checking.

This is the simplest certificate checker in the repo: given a graph g and parameters ps, we:

1. recompute IBP bounds in Lean (runIBP), and
2. compare the final output interval [lo,hi] against a Python-exported JSON certificate.

This is primarily used by the small LiRPA-style artifacts under NN/Examples/Verification/LiRPA/*.

Certificate shape:

{ "result": { "lo": [...], "hi": [...] } }

Notes on trust boundaries:

• The JSON is an untrusted artifact; we only accept it if Lean recomputation agrees.
• Each serialized interval must contain the interval recomputed by TorchLean. An inward endpoint is rejected; an outward endpoint is allowed.
• This checker validates an exported artifact against Lean execution. The theorem-backed path is separate: use NN.Verification when you need a Lean theorem connecting checker hypotheses to semantic enclosure.

References (informal):

• IBP: Gowal et al. (2018).
• CROWN/LiRPA param-store model: see NN.MLTheory.CROWN.*.

def NN.Verification.IBPCert.check (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (outId : ℕ) (path : String) (refinement : Option (ℕ × ℕ) := none) : IO Bool

Run IBP on (g, ps) and compare the output box at outId against the JSON certificate at path.

Returns true iff the serialized bounds contain the recomputed bounds componentwise. On mismatch, prints both Lean and JSON bounds for debugging.

refinement := some (inputId, splitBudget) optionally subdivides the chosen graph input before comparing bounds. Every branch is included; the default keeps the original single-pass behavior.

def NN.Verification.IBPCert.checkOrThrow (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (outId : ℕ) (path : String) (refinement : Option (ℕ × ℕ) := none) : IO Unit

Run check and raise a readable error on mismatch.

Verification examples use this entrypoint when the surrounding artifact should fail loudly rather than returning a Boolean that a caller might ignore.