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.vecOfArray (n : ℕ) (xs : Array Float) : Option (Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar))

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 (Spec.Tensor Float (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

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 (Spec.Tensor Float (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

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 : ℕ} (x : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) : Array Float

Convert a vector tensor to a float array.

def NN.Verification.Util.Tensor.boundsToArrays {n : ℕ} (lo hi : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) : Array Float × Array Float

Convert lower/upper vector tensors into arrays for artifact checkers.

def NN.Verification.Util.Tensor.flatBoxBoundsToArrays (B : MLTheory.CROWN.FlatBox Float) : Array Float × Array Float

Convert a FlatBox Float into lower/upper arrays.

def NN.Verification.Util.Tensor.boxBoundsToArrays {n : ℕ} (B : MLTheory.CROWN.Box Float (Spec.Shape.dim n Spec.Shape.scalar)) : Array Float × Array Float

Convert a shape-indexed vector Box Float into lower/upper arrays.

def NN.Verification.Util.Tensor.requireVecOfArray (ctx : String) (n : ℕ) (xs : Array Float) : IO (Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar))

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 (Spec.Tensor Float (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

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