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. Each decimal endpoint is rounded once into binary64, the lower endpoint toward -∞ and the upper toward +∞, and containment is checked exactly on those values. An endpoint inward of Lean's by one binary64 ulp or more is rejected; one that is closer reads as Lean's value.
• Acceptance here compares bounds with Lean execution; it does not itself prove a universal real-input enclosure. Cert.CROWNQuery.Json.acceptsText_sound proves an output property for its separate exact-rational dense/ReLU format. Cert.FiniteArtifactSemantics.accepts_graph_sound handles finite binary32 affine artifacts with additional exact-real dominance checks.

References (informal):

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

def NN.Verification.Cert.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.Cert.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.