NPY loaders for typed training tensors

This module implements the small, explicit .npy subset that TorchLean's native training examples need:

• NumPy format versions 1 and 2;
• little-endian float32 and float64 payloads (<f4, <f8);
• C-order arrays directly, and Fortran-order arrays converted to C-order at load time;
• typed 1D and 2D tensor views for vectors and matrices.

The loader stays narrow. It is a runtime bridge for trusted experiment artifacts, not a general NumPy parser and not part of the formal tensor semantics. Keeping it here, under Runtime.Autograd.Train, makes that boundary visible while still giving examples a convenient path from Python-produced arrays into TorchLean tensors.

Reference:

• NumPy .npy format documentation: https://numpy.org/doc/stable/reference/generated/numpy.lib.format.html

structure Runtime.Autograd.Train.NpyData : Type

In-memory representation of a loaded .npy file in TorchLean's supported subset.

values is always flattened in C-order. If the source file declares fortran_order = True, we reorder the payload during parsing and store fortran := false in the returned value so downstream tensor loaders never have to reason about storage order.

• dtype : String

  Dtype string as stored in the header, for example "<f4" or "<f8".

• shape : List ℕ

  Logical array shape as stored in the header.

• fortran : Bool

  Whether the returned flat payload is still Fortran-ordered. This loader returns false.

• values : Array Float

  Flattened numeric payload, converted to Lean Float values.

def Runtime.Autograd.Train.IoLoader.Internal.prefixProducts (shape : List ℕ) : List ℕ

Prefix products of a shape list.

For a shape [d₀, d₁, d₂], this returns [1, d₀, d₀*d₁], which are exactly the Fortran-order strides. We use these strides to convert Fortran storage into TorchLean's ordinary C-order flattening convention.

def Runtime.Autograd.Train.IoLoader.Internal.prefixProducts.go (acc : ℕ) : List ℕ → List ℕ

def Runtime.Autograd.Train.IoLoader.Internal.idxFortranOfCIdx (shape : List ℕ) (idxC : ℕ) : ℕ

Convert a linear C-order index to the corresponding linear Fortran-order index.

Both indices describe the same multi-dimensional coordinate. The difference is only how the coordinate is flattened into a one-dimensional payload.

def Runtime.Autograd.Train.IoLoader.Internal.idxFortranOfCIdx.go (dims strides : List ℕ) (idx acc : ℕ) : ℕ

def Runtime.Autograd.Train.IoLoader.Internal.reorderFortranToC (shape : List ℕ) (raw : Array Float) : Array Float

Reorder a Fortran-ordered flat array into C-order.

The function is total and defensive: if the file payload is malformed and an index is missing, the missing element is filled with 0.0. The parser checks payload length before calling this function, so that fallback should not happen for accepted files.

def Runtime.Autograd.Train.IoLoader.Internal.byteAt? (bs : ByteArray) (i : ℕ) : Option UInt8

Safe ByteArray indexing.

def Runtime.Autograd.Train.IoLoader.Internal.readUInt16LE (bs : ByteArray) (i : ℕ) : Option ℕ

Read a little-endian UInt16 at byte offset i, returning none on out-of-bounds input.

def Runtime.Autograd.Train.IoLoader.Internal.readUInt32LE (bs : ByteArray) (i : ℕ) : Option UInt32

Read a little-endian UInt32 at byte offset i, returning none on out-of-bounds input.

def Runtime.Autograd.Train.IoLoader.Internal.readUInt64LE (bs : ByteArray) (i : ℕ) : Option UInt64

Read a little-endian UInt64 at byte offset i, returning none on out-of-bounds input.

def Runtime.Autograd.Train.IoLoader.Internal.parseShapeValue (s : String) : Option (List ℕ)

Parse a shape tuple like (3, 4) or (3,) from a NumPy header fragment.

def Runtime.Autograd.Train.IoLoader.Internal.parseShapeValue.parseAll (xs : List String) (acc : List ℕ) : Option (List ℕ)

def Runtime.Autograd.Train.IoLoader.Internal.parseHeader (tag hdr : String) : Result (String × Bool × List ℕ)

Parse the NumPy header dictionary.

We only need three standard fields: descr, fortran_order, and shape. The header format is a Python-literal dictionary padded to an alignment boundary, so this parser stays field-oriented rather than trying to become a full Python parser.

structure Runtime.Autograd.Train.IoLoader.Internal.NpyHeaderMeta : Type

Parsed .npy metadata needed before reading the numeric payload.

• descr : String

  Dtype descriptor from the header, for example "<f4" or "<f8".

• fortran : Bool

  Whether the on-disk payload is Fortran-ordered.

• shape : List ℕ

  Logical array shape from the header.

• dataStart : ℕ

  Byte offset where the numeric payload begins.

def Runtime.Autograd.Train.IoLoader.Internal.parseNpyHeaderMeta (tag : String) (bs : ByteArray) : Result NpyHeaderMeta

Read and validate the NumPy magic/version/header block shared by all NPY loaders.

def Runtime.Autograd.Train.IoLoader.Internal.npyElementBytes (tag descr : String) : Result ℕ

Byte width for the dtypes supported by TorchLean's NPY loader.

def Runtime.Autograd.Train.IoLoader.Internal.readNpyElement (tag descr : String) (bs : ByteArray) (off : ℕ) : Result Float

Read one supported numeric element from an NPY payload.

def Runtime.Autograd.Train.parseNpy (tag : String) (bs : ByteArray) : Result NpyData

Parse the bytes of a .npy file into NpyData.

The parser rejects unsupported dtypes, malformed headers, and truncated payloads. That makes loader failures explicit at the trust boundary instead of silently producing tensors with the wrong shape or partial data.

def Runtime.Autograd.Train.parseNpyPrefixDim0 (tag : String) (expectedShape : List ℕ) (bs : ByteArray) : Result NpyData

Parse only the requested leading rows of a C-order .npy array.

This supports large exported tensors kept on disk while a run uses only the first n rows. The rank and trailing dimensions must match exactly; only dim 0 may be larger than requested.

The implementation shares header and dtype parsing with parseNpy, then decodes only the requested prefix. This avoids building a full Array Float when a command asks for a small leading slice of a real image or sequence dataset.

Why C-order only? In row-major NPY files, the first n rows are physically contiguous, so the prefix is exactly the first n * trailingSize elements. In Fortran-order files the same logical prefix is interleaved across the payload, so prefix decoding would be unsound. Rather than silently returning bad rows, we reject Fortran-order prefix loading and ask callers to convert the array to C-order first.

def Runtime.Autograd.Train.readNpy (path : System.FilePath) : IO (Result NpyData)

Read a .npy file from disk and parse it as NpyData.

def Runtime.Autograd.Train.readNpyPrefixDim0 (path : System.FilePath) (expectedShape : List ℕ) : IO (Result NpyData)

Read a .npy file but decode only the requested leading rows.

This is the file-system wrapper around parseNpyPrefixDim0. It still reads the file bytes into memory, but it avoids building a full Array Float for rows the run did not ask to use. The public API.Data layer uses this when a dataset source says "load the first n examples" from a larger exported NPY tensor.

def Runtime.Autograd.Train.readNpyVector (path : System.FilePath) (n : ℕ) : IO (Result (Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)))

Read a 1D .npy file as a typed TorchLean vector tensor.

The shape check is part of the loader contract: files with the wrong logical size are rejected instead of being reshaped implicitly.

def Runtime.Autograd.Train.readNpyMatrix (path : System.FilePath) (m n : ℕ) : IO (Result (Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))))

Read a 2D .npy file as a typed TorchLean matrix tensor.

The returned matrix uses the same row-major indexing convention as the rest of the runtime tensor helpers.