TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Instances

Capability instances for configured binary formats #

Representation-independent instances serve custom carriers. Higher-priority instances for Configured.Code expose byte tables after dependent elimination of the selected storage plan, and give the other non-limb plans a direct entry point to the selected structural or generic kernel. A closed ExecFloat.Binary call can therefore specialize that kernel to its descriptor.

The priorities encode capability preference and carry no numerical meaning, because every candidate must supply the same refinement contract before it can be selected. All of this wiring lives in this module, so storage-specific instances do not leak into the rest of the configured API.

source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.addCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Add (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.subCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Sub (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.mulCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Mul (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.divCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Div (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.sqrtCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Sqrt (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.fmaCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Fma (Family format code plan)

Higher-priority built-in-carrier instances match Code plan before inspecting the plan. This works for every statically computed precision, including a forKnownWidth expression that has not yet reduced to a storage constructor during typeclass indexing. The dependent candidate helpers then add direct byte tables exactly when the selected plan is .byte.

Families with a custom carrier use the representation-independent instances above.

First-order entry points #

A machine-word or pair plan calls its structural kernel directly when that candidate wins against the generic kernel under the policy in scope. Non-byte, non-limb plans also expose a direct call when the generic kernel wins. Byte tables, limb candidates, and the remaining structural routes execute the memoized selection.

The guard stays inside execute so closed callers can specialize the selected kernel. A match around the capability record would prevent the compiler from reducing the projection before kernel specialization. The proofs below unfold candidate selection, including the choice between word and fixed-limb square root and FMA. Numerical equivalence alone never justifies a route.

source
@[always_inline]
def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.directSqrt {format : FloatFormat} {plan : StoragePlan format} :
ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan)

The direct square root for a built-in carrier: stored two-word codes where the NativePair layout allows, otherwise the structural candidate.

Instances For
    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.directSqrt_eq {format : FloatFormat} {plan : StoragePlan format} (value : ExecFloat (Family format (Code plan) plan)) :
    directSqrt value = structuralSqrt value

    The direct square root computes the structural candidate's result.

    source
    @[always_inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.directFma {format : FloatFormat} {plan : StoragePlan format} :
    ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan)

    The direct fused multiply-add for a built-in carrier: stored two-word codes where the NativePair layout allows, otherwise the structural candidate.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.directFma_eq {format : FloatFormat} {plan : StoragePlan format} (left right addend : ExecFloat (Family format (Code plan) plan)) :
      directFma left right addend = structuralFma left right addend

      The direct fused multiply-add computes the structural candidate's result.

      source
      @[instance_reducible, always_inline, instance 200]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticAddCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
      ExecFloat.Add (Family format (Code plan) plan)
      source
      @[instance_reducible, always_inline, instance 200]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticSubCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
      ExecFloat.Sub (Family format (Code plan) plan)
      source
      @[instance_reducible, always_inline, instance 200]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticMulCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
      ExecFloat.Mul (Family format (Code plan) plan)
      source
      @[instance_reducible, always_inline, instance 200]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticDivCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
      ExecFloat.Div (Family format (Code plan) plan)
      source
      @[instance_reducible, always_inline, instance 200]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticSqrtCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
      ExecFloat.Sqrt (Family format (Code plan) plan)
      source
      @[instance_reducible, always_inline, instance 200]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticFmaCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
      ExecFloat.Fma (Family format (Code plan) plan)

      Closed limb plans expose their concrete carrier during typeclass indexing. These instances forward to the automatic portfolios so ExecFloat.BinaryLimbs retains the policy in scope, its certified candidates, and the generic fallback.

      source
      @[instance_reducible, instance 900]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbCodec (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
      ExecFloat.ModelCodec (StoragePlan.limbs width_gt) (Model format) (Model.WideLimb.Value format)

      The canonical lossless codec for the concrete limb carrier.

      Its priority is below codecForPlan because ModelCodec.Code is an output parameter, so unresolved codec goals must try the generic plan before the concrete limb carrier. That keeps inference working for conversions between definitionally equal descriptors such as Binary.descriptor 8 23 and binary32.

      source
      @[instance_reducible, always_inline, instance 210]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbAddCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
      ExecFloat.Add (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

      Policy-selected addition for the concrete limb carrier.

      source
      @[instance_reducible, always_inline, instance 210]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbSubCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
      ExecFloat.Sub (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

      Policy-selected subtraction for the concrete limb carrier.

      source
      @[instance_reducible, always_inline, instance 210]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbMulCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
      ExecFloat.Mul (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

      Policy-selected multiplication for the concrete limb carrier.

      source
      @[instance_reducible, always_inline, instance 210]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbDivCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
      ExecFloat.Div (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

      Policy-selected division for the concrete limb carrier.

      source
      @[instance_reducible, always_inline, instance 210]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbSqrtCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
      ExecFloat.Sqrt (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

      Policy-selected square root for the concrete limb carrier.

      source
      @[instance_reducible, always_inline, instance 210]
      instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbFmaCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
      ExecFloat.Fma (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

      Policy-selected fused multiply-add for the concrete limb carrier.