Tensor helpers for verification artifacts

Verification tools often sit at the boundary between Lean tensors and external JSON artifacts. This module keeps those conversions in one place instead of reimplementing vector/matrix unpacking inside each checker.

def NN.Verification.Util.Tensor.boundsOrdered {n : ℕ} (lo hi : TorchLean.Tensor Float [n]) : Bool

Pointwise ordering of equally shaped bounds. NaN comparisons fail.

def NN.Verification.Util.Tensor.boxWithin {n : ℕ} (rootLo rootHi lo hi : TorchLean.Tensor Float [n]) : Bool

Check ordered leaf bounds contained in an equally shaped root box.

def NN.Verification.Util.Tensor.refutesThreshold {n : ℕ} (lowerBound threshold : TorchLean.Tensor Float [n]) : Bool

A strict lower-bound witness refutes its corresponding threshold.

def NN.Verification.Util.Tensor.refutesThresholdAt {n : ℕ} (lowerBound threshold : TorchLean.Tensor Float [n]) (witnessIdx : ℕ) : Bool

Check the supplied coordinate; out-of-range witnesses and NaN comparisons fail.

def NN.Verification.Util.Tensor.vecOfArray (n : ℕ) (xs : Array Float) : Option (TorchLean.Tensor Float [n])

Convert a float array into a length-n vector tensor, returning none on length mismatch.

def NN.Verification.Util.Tensor.matOfFlatArray (rows cols : ℕ) (xs : Array Float) : Option (TorchLean.Tensor Float [rows, cols])

Convert a row-major flat array into a rows × cols matrix tensor.

This is the common JSON-artifact shape: external tools often serialize matrices as one flat float array plus schema-level dimensions.

def NN.Verification.Util.Tensor.matOfArray (rows cols : ℕ) (xs : Array (Array Float)) : Option (TorchLean.Tensor Float [rows, cols])

Convert a rows × cols float matrix payload into a matrix tensor.

Both the row count and every row length are checked before the tensor is built.

def NN.Verification.Util.Tensor.vecToArray {n : ℕ} {storage : TorchLean.Storage Float} (x : TorchLean.Tensor Float [n]) : Array Float

Convert a vector tensor to a float array.

def NN.Verification.Util.Tensor.requireVecOfArray (ctx : String) (n : ℕ) (xs : Array Float) : IO (TorchLean.Tensor Float [n])

Load a length-checked vector tensor from a JSON float array, or raise a schema error.

def NN.Verification.Util.Tensor.requireMatOfFlatArray (ctx : String) (rows cols : ℕ) (xs : Array Float) : IO (TorchLean.Tensor Float [rows, cols])

Load a row-major matrix tensor from a JSON float array, or raise a schema error.