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 interval-box refutation check used by VNN-COMP style safety certificates.

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 mat * y <= 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 mat * y <= rhs over the network output vector y.

• id : Nat

  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_j * y_j over y_j ∈ [lo_j, hi_j] is the smaller of the endpoint products.

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

Lower-bound one linear row, returning 0 when the row and interval dimensions do not match.

Use rowLowerBoundOnBox? at checker boundaries when mismatch must be reported explicitly.

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.