VNNLIB-style output specifications

This module contains the benchmark-independent part of the VNN-COMP artifact boundary:

• an input box plus a disjunction-of-conjunctions output spec,
• a JSON loader for the compact vnnlib_suite_v0_1 export format,
• the outward-rounded interval-box refutation check used by the executable VNN-COMP runner.

Model-specific checkers, such as MNIST-FC, build a graph and output bounds. The arithmetic for interpreting the VNNLIB rows lives here.

@[reducible, inline]

abbrev NN.Verification.VNNComp.VNNLib.Term : Type

One conjunction term $\mathrm{mat}\,y\leq\mathrm{rhs}$ in a VNNLIB disjunction.

@[reducible, inline]

abbrev NN.Verification.VNNComp.VNNLib.Spec : Type

A VNNLIB-style unsafe-region spec: a disjunction of conjunction terms.

structure NN.Verification.VNNComp.VNNLib.Instance : Type

One exported VNN-COMP instance.

spec is a disjunction-of-conjunctions: each term is a conjunction $\mathrm{mat}\,y\leq\mathrm{rhs}$ over the network output vector y.

• id : ℕ

  Instance id copied from the exported suite JSON.

• inputLo : Array Float

  Lower bound for the input box.

• inputHi : Array Float

  Upper bound for the input box.

• spec : Spec

  Unsafe output-region specification.

def NN.Verification.VNNComp.VNNLib.loadSuite (path : String) : IO (Array Instance)

Load the compact VNNLIB suite JSON format used by TorchLean checkers.

Expected top-level format: vnnlib_suite_v0_1.

def NN.Verification.VNNComp.VNNLib.rowLowerBoundOnBox? (row yLo yHi : Array Float) : Option Float

Lower-bound one linear row over an output interval box.

For each coefficient $a_j$, the minimum of $a_jy_j$ over $y_j\in[\mathrm{lo}_j,\mathrm{hi}_j]$ is the smaller of the endpoint products.

def NN.Verification.VNNComp.VNNLib.termRefutedByOutputBox (yLo yHi : Array Float) (term : Term) : Bool

Check whether a conjunction term is refuted by the output interval box.

def NN.Verification.VNNComp.VNNLib.refutedByOutputBox (yLo yHi : Array Float) (spec : Spec) : Bool

Check whether an unsafe VNNLIB spec is refuted by an output interval box.

The spec is a disjunction of conjunctions. To prove the unsafe region is empty, every disjunct must be refuted. For a conjunction, it is enough for one row lower bound to exceed its right-hand side. This executable predicate uses the explicit host-Float BoundOps boundary; its Boolean result is not itself a Lean theorem about real-valued graph semantics.