Binary Checkpoint IO

Internal framing utilities shared by TorchLean's binary checkpoint formats. Integer fields use an explicit little-endian encoding. Replacement writes use a fresh sibling file and close its handle before renaming it over the destination. On filesystems with atomic same-directory replacement, this prevents readers from observing a partially written checkpoint.

Every binary format starts with a stable family magic followed by an explicit unsigned 64-bit version. Keeping these fields separate lets readers distinguish a foreign file from a known checkpoint written by an unsupported format version.

structure Runtime.Autograd.Torch.Internal.CheckpointIO.Format : Type

Stable identity and current version of one binary checkpoint family.

• name : String

  Name used in diagnostics.

• magic : ByteArray

  Stable byte prefix shared by every version of this format.

• version : Nat

  Version written immediately after magic.

def Runtime.Autograd.Torch.Internal.CheckpointIO.nat64LE (n : Nat) : ByteArray

Encode a natural number as an unsigned 64-bit little-endian field.

def Runtime.Autograd.Torch.Internal.CheckpointIO.writeNat64 (formatName : String) (handle : IO.FS.Handle) (n : Nat) : IO Unit

Write one natural number after checking that it fits in an unsigned 64-bit field.

def Runtime.Autograd.Torch.Internal.CheckpointIO.nat64FromLE (formatName : String) (bytes : ByteArray) : Except String Nat

Decode an unsigned 64-bit little-endian field.

partial def Runtime.Autograd.Torch.Internal.CheckpointIO.readExact (formatName : String) (handle : IO.FS.Handle) (count : Nat) (acc : ByteArray := ByteArray.empty) : IO ByteArray

Read exactly count bytes or report a truncated checkpoint.

def Runtime.Autograd.Torch.Internal.CheckpointIO.readNat64 (formatName : String) (handle : IO.FS.Handle) : IO Nat

Read one unsigned 64-bit little-endian field.

def Runtime.Autograd.Torch.Internal.CheckpointIO.writeFormat (format : Format) (handle : IO.FS.Handle) : IO Unit

Write the stable family magic and explicit version of a binary checkpoint.

def Runtime.Autograd.Torch.Internal.CheckpointIO.readFormat (format : Format) (handle : IO.FS.Handle) : IO Unit

Read and validate a binary checkpoint header.

A wrong magic identifies a different file family. A matching magic with a different version gives an explicit version diagnostic instead of being misreported as malformed payload data.

def Runtime.Autograd.Torch.Internal.CheckpointIO.hasFormatMagic (format : Format) (path : System.FilePath) : IO Bool

Test whether a file belongs to a binary checkpoint family, without checking its version.

def Runtime.Autograd.Torch.Internal.CheckpointIO.writeAtomically (path : System.FilePath) (write : IO.FS.Handle → IO Unit) : IO Unit

Write a checkpoint through a temporary sibling and rename it after the handle has been closed.

If writing or renaming fails, the temporary file is removed. The destination is never exposed as a partially written checkpoint on filesystems with atomic same-directory replacement.