Array predicates for verification artifacts

Small checkers often receive vector data as JSON float arrays before converting anything into shape-indexed tensors. This module keeps the common pointwise predicates in one place.

def NN.Verification.Util.Array.floatLe (x y : Float) : Bool

Boolean $\leq$ on floats, for executable artifact checks.

def NN.Verification.Util.Array.floatLt (x y : Float) : Bool

Boolean < on floats, for executable artifact checks.

def NN.Verification.Util.Array.boxWithin (rootLo rootHi lo hi : Array Float) : Bool

Check pointwise containment $[\mathrm{lo},\mathrm{hi}]\subseteq[\mathrm{rootLo},\mathrm{rootHi}]$ for JSON-style float arrays.

The helper is strict about lengths through allPairwise: mismatched arrays are rejected.

def NN.Verification.Util.Array.refutesThreshold (lowerBound threshold : Array Float) : Bool

Check whether a lower-bound vector refutes a threshold vector at some coordinate.

This is the executable form of $\exists i,\ \mathrm{threshold}[i]<\mathrm{lowerBound}[i]$.

def NN.Verification.Util.Array.refutesThresholdAt (lowerBound threshold : Array Float) (witnessIdx : Nat) : Bool

Check a supplied witness coordinate for threshold refutation.

Out-of-range witnesses are rejected instead of silently falling back to another coordinate.