TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Carrier

Binary-interchange descriptors in the universal carrier #

Descriptor format gives an arbitrary validated binary format a type-level identity. Its runtime code is the existing Model format, so packing and unpacking are representation-preserving.

This module intentionally contains no arithmetic backend. Carrier-only clients should not have to load word kernels, dispatch proofs, or planner machinery merely to name a descriptor.

source
inductive FloatLib.Floats.Formats.BinaryInterchange.Descriptor (_format : FloatFormat) :
Type

Type identity for one validated binary FloatFormat descriptor.

The descriptor is static in the type. Width, bias, and exceptional-value encoding therefore specialize independently for every IEEE, non-IEEE, or user-defined format.

    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.BinaryInterchange.encodedFormat (format : FloatFormat) :
      Numerics.EncodedFormat (Descriptor format)
      source
      @[instance_reducible]
      noncomputable instance FloatLib.Floats.Formats.BinaryInterchange.formatSemantics (format : FloatFormat) :
      Numerics.FormatSemantics (Descriptor format)
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.BinaryInterchange.descriptorModelCodec (format : FloatFormat) :
      ExecFloat.ModelCodec () (Model format) (Model format)

      The descriptor carrier stores its proof model directly, so encoding and decoding are identities.

      Registering that identity codec lets descriptor arithmetic use the same executable lifts and refinement theorems as every configured format.

      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.pack {format : FloatFormat} (value : Model format) :
      ExecFloat (Descriptor format)

      Inject a binary model value into the universal carrier without changing its code.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.unpack {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
        Model format

        Recover the binary model value without changing its representation.

        Instances For
          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.unpack_pack {format : FloatFormat} (value : Model format) :
          unpack (pack value) = value

          Packing and then unpacking a model value is the identity.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.pack_unpack {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
          pack (unpack value) = value

          Unpacking and then packing a descriptor value is the identity.