TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.Runtime

Direct-carrier software FMA for binary32 and binary64 #

These binary32 and binary64 FMA entry points execute the proved fixed-word kernel in both Lean's logic and compiled code, with carrier conversion fixed statically. Addition, subtraction, multiplication, division, and square root use the generic configured Backend.word* entry points.

Guarded Float32 and Float experiments live in the separate Configured.NativeFPU.Unchecked module. Importing this runtime does not expose them or pull native floating-point primitives into certified clients.

Binary32 #

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.Binary32Value (width_le : FloatFormat.binary32.bitWidth ≤ 32) :
Type

Configured IEEE binary32 value stored in a direct UInt32 carrier.

Instances For
    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.binary32Bits_lt (bits : UInt32) :
    bits.toNat < 2 ^ FloatFormat.binary32.bitWidth

    Every UInt32 bit pattern fits the complete binary32 interchange width.

    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.ofBinary32Bits {width_le : FloatFormat.binary32.bitWidth ≤ 32} (bits : UInt32) :
    Binary32Value width_le

    Rewrap one complete binary32 interchange word in its configured carrier.

    Instances For

      Direct-carrier fused multiply-add #

      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.softwareFma32 {width_le : FloatFormat.binary32.bitWidth ≤ 32} (left right addend : Binary32Value width_le) :
      Binary32Value width_le

      Proved software binary32 FMA with the UInt32 carrier adapter fixed statically.

      This uses the proved fixed-word FMA kernel. Spelling the carrier conversion directly avoids retaining a ModelCodec structure and four indirect closure applications in compiled monomorphic code.

      Instances For

        Binary64 #

        source
        @[reducible, inline]
        abbrev FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.Binary64Value (width_le : FloatFormat.binary64.bitWidth ≤ 64) :
        Type

        Configured IEEE binary64 value stored in a direct UInt64 carrier.

        Instances For
          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.binary64Bits_lt (bits : UInt64) :
          bits.toNat < 2 ^ FloatFormat.binary64.bitWidth

          Every UInt64 bit pattern fits the complete binary64 interchange width.

          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.ofBinary64Bits {width_le : FloatFormat.binary64.bitWidth ≤ 64} (bits : UInt64) :
          Binary64Value width_le

          Rewrap one complete binary64 interchange word in its configured carrier.

          Instances For

            Direct-carrier fused multiply-add #

            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.softwareFma64 {width_le : FloatFormat.binary64.bitWidth ≤ 64} (left right addend : Binary64Value width_le) :
            Binary64Value width_le

            Proved software binary64 FMA with the UInt64 carrier adapter fixed statically.

            As for binary32, the arithmetic uses the proved fixed-word kernel. The specialization exists to make carrier conversion first-order in generated code, independently of the generic codec used by arbitrary configured formats.

            Instances For