TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Runtime.Autograd.Model.StateIO.Encoding

Scalar encodings for immutable model checkpoints #

The tensor container checks shapes and lengths; Checkpoint.Encoding checks scalar payloads. Native formats preserve the bits their values export; Lean canonicalizes native NaNs. Their decoders reject noncanonical NaN words instead of silently changing a payload. Configured binary formats preserve all encodings, including NaN payloads. Complex values encode both coordinates using the component encoding. No value passes through a narrower native format.

source
class TorchLean.Checkpoint.Encoding (α : Type) :
Type

A versioned scalar checkpoint representation, with explicit rejection of malformed values.

  • format : String

    Identifies the scalar format and schema. Different interpretations need different tags.

  • encode : α → Lean.Json

    Encode one scalar without changing its precision.

  • decode : Lean.Json → Except String α

    Decode one scalar, rejecting out-of-range or incorrectly shaped payloads.

Instances
    source
    def TorchLean.Checkpoint.Encoding.checkedWord (width : ℕ) (json : Lean.Json) :
    Except String ℕ

    Parse a storage word without silently reducing an out-of-range input modulo its width.

    Instances For
      source
      @[instance_reducible]
      instance TorchLean.Checkpoint.Encoding.instFloat :
      Encoding Float

      The existing binary64 JSON format, preserving compatibility with saved Float checkpoints.

      source
      @[instance_reducible]
      instance TorchLean.Checkpoint.Encoding.instFloat32 :
      Encoding Float32

      Exact binary32 words for immutable CPU state. Streamed runtime checkpoints remain separate.

      source
      @[instance_reducible]
      instance TorchLean.Checkpoint.Encoding.instExecFloatFamilyOfModelCodecStoragePlanModel {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] :
      Encoding (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan))

      Configured binary checkpoints include the complete numerical format, independently of storage plan.

      Exponent width, fraction width, bias, and exceptional-value encoding all participate in the tag. Two equal-width formats with different interpretations therefore cannot be confused on loading.

      source
      @[instance_reducible]
      instance TorchLean.Checkpoint.Encoding.instComplex {α : Type} [Encoding α] :
      Encoding (Complex α)

      A complex scalar is an ordered pair of independently encoded real and imaginary coordinates.