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 live 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; the conditional form is inlined and can be simplified for a closed format (see NativeSmallWord.StorageEligible).

    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.roundNormalProduct? (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) :
      Option (Model fmt)

      Round an exact two-word product of two normal finite significands.

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

        Decode two normal finite values and try the reusable two-word product path.

        Instances For