TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.BID.Runtime

Binary integer decimal encoding #

IEEE 754-2019 §3.5.2(c)(2) stores the decimal coefficient as a binary integer. The 11 steering bits move the exponent field and imply coefficient prefix 100. A finite coefficient exceeding 10^precision - 1 denotes zero, preserving its sign and quantum exponent. Excessive NaN payloads also denote zero. The decoder implements these rules rather than reducing the coefficient modulo a decimal power.

source
def FloatLib.Floats.Formats.DecimalInterchange.BID.encodeFinite (f : Format) (c e : ℕ) :
ℕ

Encode a finite coefficient and biased exponent using the BID steering bits.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.BID.rawCoefficient (f : Format) (n : ℕ) :
    ℕ

    Read the BID coefficient before checking its decimal precision bound.

    Instances For
      source
      def FloatLib.Floats.Formats.DecimalInterchange.BID.biasedExponent (f : Format) (n : ℕ) :
      ℕ

      Read the biased exponent; subtracting the steering prefix exposes its field.

      Instances For
        source
        def FloatLib.Floats.Formats.DecimalInterchange.BID.decodeFinite (f : Format) (n : ℕ) :
        ℕ × ℕ

        Decode finite fields. Oversized binary coefficients denote decimal zero.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.BID.decodePayload (f : Format) (n : ℕ) :
          ℕ

          A NaN payload outside the decimal payload range denotes zero (§3.5.2(a), (c)(2)).

          Instances For
            source
            def FloatLib.Floats.Formats.DecimalInterchange.BID.codec :
            Codec

            The complete BID interchange codec. Its laws are proved in BID.Proof.

            Instances For
              source
              def FloatLib.Floats.Formats.DecimalInterchange.BID.decode (f : Format) (word : BitVec f.bitWidth) :
              Datum

              Decode a BID word at the selected interchange layout.

              Instances For
                source
                def FloatLib.Floats.Formats.DecimalInterchange.BID.encode? (f : Format) (d : Datum) :
                Option (BitVec f.bitWidth)

                Encode a representable datum as BID, returning none instead of rounding when the selected width cannot represent it.

                Instances For
                  source
                  def FloatLib.Floats.Formats.DecimalInterchange.BID.canonicalize (f : Format) (word : BitVec f.bitWidth) :
                  BitVec f.bitWidth

                  Canonical BID encoding of the datum denoted by a word.

                  Instances For