TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.TwoWordMul.Runtime

Native two-word finite multiplication #

This is the executable 64 x 64 -> 128 normal-product tier for one-word IEEE formats whose significand product needs two words. Refinement proofs are in TwoWordMul.Proof.

source
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.Eligible (fmt : FloatFormat) :
Prop

Capacity contract for a one-storage-word format whose product needs two native words.

Instances For
    source
    @[instance_reducible, inline]
    instance FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.instDecidableEligible (fmt : FloatFormat) :
    Decidable (Eligible fmt)

    Two-word eligibility is decided from the descriptor fields. As for NativeSmallWord.StorageEligible, the conditional form is inlined and simplifies for a closed format.

    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.productLeading (fmt : FloatFormat) (product : Numerics.FixedWord.UInt128) :
    UInt64

    Leading-bit position 2 * fracWidth or 2 * fracWidth + 1 of a normalized two-word product.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.roundNormalProductWord? (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) :
      Option UInt64

      Round an exact two-word product of two normal finite significands, returning the packed storage word.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.roundNormalProduct? (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) :
        Option (Model fmt)

        roundNormalProductWord? as a model value.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.mulNormalWord? (fmt : FloatFormat) (xBits yBits : UInt64) :
          Option UInt64

          Decode two normal finite storage words and try the reusable two-word product path, returning the packed storage word of an accepted product. Carriers that store the encoding as a UInt64 call it on their words, so the product never becomes an exact-width model value.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.mulNormal? {fmt : FloatFormat} (x y : Model fmt) :
            Option (Model fmt)

            mulNormalWord? as a model value, on the operands' storage words.

            Instances For