NPY Loader

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

• 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;
• deterministic conversion to a flat Array Float in C order.

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. Tensor construction happens in NN.API.Data.Sources, which keeps this file-format boundary independent of model training.

Reference:

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

structure TorchLean.Data.IO.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 : Array Nat

  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.

structure TorchLean.Data.IO.NpyHeader : Type

Validated NPY metadata, without reading or allocating the numeric payload.

Dimensions and the element count fit an addressable Array Float. Payload availability is checked separately by full or prefix readers; a valid header alone does not certify a complete file.

• dtype : String

  Supported dtype descriptor, either "<f4" or "<f8".

• shape : Array Nat

  Logical array shape from the header.

• fortran : Bool

  Whether the on-disk payload is Fortran-ordered.

• dataStart : Nat

  Byte offset where the numeric payload begins.

• elementBytes : Nat

  Number of bytes occupied by one on-disk element.

• elementCount : Nat

  Product of the validated dimensions; scalar arrays contain one element.

def TorchLean.Data.IO.Internal.prefixProducts (shape : Array Nat) : Array Nat

Prefix products of a shape array.

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 TorchLean.Data.IO.Internal.idxFortranOfCIdx (shape : Array Nat) (idxC : Nat) : Nat

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 TorchLean.Data.IO.Internal.reorderFortranToC (tag : String) (shape : Array Nat) (raw : Array Float) : Except String (Array Float)

Reorder a Fortran-ordered flat array into C-order, rejecting an inconsistent payload.

def TorchLean.Data.IO.Internal.byteAt? (bs : ByteArray) (i : Nat) : Option UInt8

Safe ByteArray indexing.

def TorchLean.Data.IO.Internal.readUInt16LE (bs : ByteArray) (i : Nat) : Option Nat

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

def TorchLean.Data.IO.Internal.readUInt32LE (bs : ByteArray) (i : Nat) : Option UInt32

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

def TorchLean.Data.IO.Internal.readUInt64LE (bs : ByteArray) (i : Nat) : Option UInt64

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

def TorchLean.Data.IO.Internal.parseShapeValue (s : String) : Option (Array Nat)

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

def TorchLean.Data.IO.Internal.parseHeader (tag hdr : String) : Except String (String × Bool × Array Nat)

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.

def TorchLean.Data.IO.Internal.maxNpyHeaderBytes : Nat

Bound header allocation before interpreting an untrusted version-2 header length.

def TorchLean.Data.IO.Internal.npyHeaderLayout (tag : String) (bs : ByteArray) : Except String (Nat × Nat)

Validate the magic and version, returning the header offset and its bounded byte length.

def TorchLean.Data.IO.Internal.npyElementBytes (tag descr : String) : Except String Nat

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

def TorchLean.Data.IO.Internal.npyElementCount (tag : String) (shape : Array Nat) : Except String Nat

Bound each dimension and the shape product before allocating a decoded Array Float.

def TorchLean.Data.IO.Internal.parseNpyHeaderMeta (tag : String) (bs : ByteArray) : Except String NpyHeader

Parse and validate the metadata shared by in-memory and file-backed NPY readers.

def TorchLean.Data.IO.Internal.readNpyElement (tag descr : String) (bs : ByteArray) (off : Nat) : Except String Float

Read one supported numeric element from an NPY payload.

def TorchLean.Data.IO.Internal.npyPrefixHeader (tag : String) (hdr : NpyHeader) (expectedShape : Array Nat) : Except String NpyHeader

Validate a C-order leading prefix and retain only its requested shape and element count.

def TorchLean.Data.IO.Internal.decodeNpyPayload (tag : String) (hdr : NpyHeader) (bs : ByteArray) : Except String NpyData

Decode a validated full or prefix payload, checking its byte range before reserving values.

def TorchLean.Data.IO.Internal.readNpyBytes (handle : IO.FS.Handle) (count : Nat) : IO (Except String ByteArray)

Read exactly the requested bytes using bounded allocations, rejecting an early end of file.

The buffer grows only with bytes actually read. An untrusted element count never becomes the capacity of a read buffer before the corresponding file contents have been observed.

partial def TorchLean.Data.IO.Internal.readNpyBytes.loop (handle : IO.FS.Handle) (remaining : Nat) (bytes : ByteArray) : IO (Except String ByteArray)

def TorchLean.Data.IO.Internal.readNpyHeaderFromHandle (handle : IO.FS.Handle) : IO (Except String NpyHeader)

Read only the bounded NPY preamble and header, leaving the handle at the numeric payload.

def TorchLean.Data.IO.Internal.readNpyPayload (handle : IO.FS.Handle) (hdr : NpyHeader) : IO (Except String NpyData)

Read and decode the validated payload at the handle's current position.

def TorchLean.Data.IO.parseNpy (tag : String) (bs : ByteArray) : Except String NpyData

Parse the bytes of a .npy file into NpyData.

The parser rejects unsupported dtypes, missing or malformed required header fields, and truncated payloads. Header parsing recognizes the three required fields; it is not a general Python parser. That makes loader failures explicit at the trust boundary instead of silently producing tensors with the wrong shape or partial data.

def TorchLean.Data.IO.parseNpyLeadingAxisPrefix (tag : String) (expectedShape : Array Nat) (bs : ByteArray) : Except String 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 the leading axis 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. Only the requested range must be present; unused trailing rows are not checked for truncation.

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 TorchLean.Data.IO.readNpyHeader (path : System.FilePath) : IO (Except String NpyHeader)

Read validated metadata without reading the payload.

Supports version 1 and 2 headers up to one MiB. Dtype, storage-order syntax, dimensions, and shape products are validated; payload completeness belongs to readNpy or readNpyLeadingAxisPrefix.

def TorchLean.Data.IO.readNpy (path : System.FilePath) : IO (Except String NpyData)

Read the full declared NPY payload, rejecting truncation and converting Fortran to C order.

def TorchLean.Data.IO.readNpyLeadingAxisPrefix (path : System.FilePath) (expectedShape : Array Nat) : IO (Except String NpyData)

Read only the header and requested leading rows of a C-order .npy file.

Unrequested rows are neither read nor decoded. The requested range must be complete, and rank and trailing dimensions must match exactly. Reads use bounded chunks so a malformed claimed size cannot trigger a correspondingly large allocation before any bytes have been read.