TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E8M0.Semantics

Numerical semantics of E8M0 scaling #

E8M0 is an exponent-only scale rather than a sign/exponent/fraction float. Its runtime carrier remains one byte. The contracts in this module relate that byte and the existing exact decoders to the same NumericalSystem and Operation interfaces used by ordinary floats and other numerical representations.

source
def FloatLib.Floats.Formats.OCP.MX.E8M0.numericalSystem :
Numerics.NumericalSystem

E8M0 codes interpreted as exact positive dyadic scales, with 0xff denoting NaN.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.Formats.OCP.MX.E8M0.AtFinite (value : Numerics.Dyadic) :
    Type

    An E8M0 code with an erased proof of its exact finite scale.

    Instances For
      source
      theorem FloatLib.Floats.Formats.OCP.MX.E8M0.numericalSystem_represents_iff (scale : E8M0) (value : Numerics.Dyadic) :
      numericalSystem.Represents scale value ↔ scale.toDyadic? = some value

      Finite E8M0 representation is exactly successful dyadic decoding.

      source
      theorem FloatLib.Floats.Formats.OCP.MX.E8M0.toDyadic?_eq_some_of_represents {scale : E8M0} {value : Numerics.Dyadic} (hscale : numericalSystem.Represents scale value) :
      scale.toDyadic? = some value

      Recover successful E8M0 decoding from a finite representation proof.

      source
      @[inline]
      def FloatLib.Floats.Formats.OCP.MX.E8M0.scaledValue (scale value : Numerics.Dyadic) :
      Numerics.Dyadic

      Apply the exponent carried by an E8M0 scale to an exact dyadic.

      Instances For
        source
        theorem FloatLib.Floats.Formats.OCP.MX.E8M0.scaleDyadic_refines :
        Numerics.Operation.Checked2 numericalSystem (Numerics.NumericalSystem.exact Numerics.Dyadic) (Numerics.NumericalSystem.exact Numerics.Dyadic) scaleDyadic? fun (scale : numericalSystem.Scalar) (value : (Numerics.NumericalSystem.exact Numerics.Dyadic).Scalar) => Numerics.NumericalValue.finite (scaledValue scale value)

        E8M0 scaling is exact on every represented finite scale.

        source
        theorem FloatLib.Floats.Formats.OCP.MX.E8M0.decodeElement_refines (fmt : BinaryInterchange.FloatFormat) :
        Numerics.Operation.Checked2 numericalSystem (BinaryInterchange.Model.exactNumericalSystem fmt) (Numerics.NumericalSystem.exact Numerics.Dyadic) decodeElement? fun (scale : numericalSystem.Scalar) (value : (BinaryInterchange.Model.exactNumericalSystem fmt).Scalar) => Numerics.NumericalValue.finite (scaledValue scale value)

        Decoding one block element applies the represented E8M0 scale exactly.