TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeDispatch

First-order dispatch for binary32 and binary64 #

Binary32 and binary64 use first-order operation instances that name their fixed-format specializations. The public type constructor lives in Configured.Type, while the generic table, word, limb, and baseline instances live in Configured.Plan.Instances.

Each instance names the fixed-format certificate it executes. Plan.selectCertified_binary32AddCandidates and its siblings prove that the planner selects this certificate under every Policy. The kernel that runs is therefore the proved kernel #float_info reports, whichever PolicyFor instance is in scope.

The guarded host operations live in Configured.NativeFPU.Unchecked, and no compiler substitution or certified candidate puts them behind these capabilities.

source
@[instance_reducible, always_inline, instance 400]
instance FloatLib.Floats.ExecFloat.Binary.binary32AddCapability [planning : Backend.PolicyFor (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)] :
Add (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)

Configured IEEE binary32 and binary64 operations name their first-order software kernels.

These instances are attached to the public parameterized families, not to a storage-plan constructor, because Lean's typeclass index keeps Binary.Family 8 23 and Binary.Family 11 52 but does not always unfold their computed forKnownWidth plans during instance search. All six operations execute the proved fixed-format word kernels.

source
@[instance_reducible, always_inline, instance 400]
instance FloatLib.Floats.ExecFloat.Binary.binary32SubCapability [planning : Backend.PolicyFor (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)] :
Sub (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)
source
@[instance_reducible, always_inline, instance 400]
instance FloatLib.Floats.ExecFloat.Binary.binary32MulCapability [planning : Backend.PolicyFor (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)] :
Mul (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)
source
@[instance_reducible, always_inline, instance 400]
instance FloatLib.Floats.ExecFloat.Binary.binary32DivCapability [planning : Backend.PolicyFor (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)] :
Div (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)
source
@[instance_reducible, always_inline, instance 400]
instance FloatLib.Floats.ExecFloat.Binary.binary32SqrtCapability [planning : Backend.PolicyFor (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)] :
Sqrt (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)
source
@[instance_reducible, always_inline, instance 400]
instance FloatLib.Floats.ExecFloat.Binary.binary32FmaCapability [planning : Backend.PolicyFor (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)] :
Fma (Family 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) binary32AddCapability._proof_1 binary32AddCapability._proof_2 binary32AddCapability._proof_3 binary32AddCapability._proof_4)
source
def FloatLib.Floats.ExecFloat.Binary.Internal.binary64Add (left right : ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)) :
ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)

Binary64 addition on the stored words, compiled once as a specialized function. The instance calls it rather than inlining the word kernel into every caller, which keeps arithmetic loops small.

Instances For
    source
    def FloatLib.Floats.ExecFloat.Binary.Internal.binary64Sub (left right : ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)) :
    ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)

    Binary64 subtraction on the stored words, compiled once as a specialized function.

    Instances For
      source
      def FloatLib.Floats.ExecFloat.Binary.Internal.binary64Mul (left right : ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)) :
      ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)

      Binary64 multiplication on the stored words, compiled once as a specialized function.

      Instances For
        source
        def FloatLib.Floats.ExecFloat.Binary.Internal.binary64Div (left right : ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)) :
        ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)

        Binary64 division on the stored words, compiled once as a specialized function.

        Instances For
          source
          def FloatLib.Floats.ExecFloat.Binary.Internal.binary64Fma (left right addend : ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)) :
          ExecFloat (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) binary64Add._proof_1 binary64Add._proof_2 binary64Add._proof_3 binary64Add._proof_4)

          Binary64 fused multiply-add on the stored words, compiled once as a specialized function.

          Instances For
            source
            @[instance_reducible, always_inline, instance 400]
            instance FloatLib.Floats.ExecFloat.Binary.binary64AddCapability [planning : Backend.PolicyFor (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)] :
            Add (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)
            source
            @[instance_reducible, always_inline, instance 400]
            instance FloatLib.Floats.ExecFloat.Binary.binary64SubCapability [planning : Backend.PolicyFor (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)] :
            Sub (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)
            source
            @[instance_reducible, always_inline, instance 400]
            instance FloatLib.Floats.ExecFloat.Binary.binary64MulCapability [planning : Backend.PolicyFor (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)] :
            Mul (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)
            source
            @[instance_reducible, always_inline, instance 400]
            instance FloatLib.Floats.ExecFloat.Binary.binary64DivCapability [planning : Backend.PolicyFor (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)] :
            Div (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)
            source
            @[instance_reducible, always_inline, instance 400]
            instance FloatLib.Floats.ExecFloat.Binary.binary64SqrtCapability [planning : Backend.PolicyFor (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)] :
            Sqrt (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)
            source
            @[instance_reducible, always_inline, instance 400]
            instance FloatLib.Floats.ExecFloat.Binary.binary64FmaCapability [planning : Backend.PolicyFor (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)] :
            Fma (Family 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) Internal.binary64Add._proof_1 Internal.binary64Add._proof_2 Internal.binary64Add._proof_3 Internal.binary64Add._proof_4)