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.
• Agreement is checked with a tolerance because the JSON uses decimal serialization.
• This checker validates an exported artifact against Lean execution. The theorem-backed path is separate: use NN.Entrypoint.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) (tol : Float := 1e-5) : IO Bool

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

Returns true iff bounds match componentwise (within tolerance). On mismatch, prints both Lean and JSON bounds for debugging.

def NN.Verification.IBPCert.checkOrThrow (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (outId : ℕ) (path : String) (tol : Float := 1e-5) : 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.