TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.FirstOrder

Direct calls to selected structural kernels #

Word and pair storage can call a structural kernel without projecting a certificate closure. The guard below uses the same eligibility and cost comparison as the complete portfolio. Its selection proofs unfold that portfolio; they do not identify different algorithms through their common numerical specification.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.firstOrderDispatch {format : FloatFormat} :
StoragePlan format → Bool

Storage plans whose structural candidate can be called without a carrier-specific table or limb closure. This is a storage eligibility test, not a selection decision.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.structuralSelected {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (operation : ExecFloat.Backend.Operation) :
    Bool

    Whether the structural candidate wins its comparison with the generic kernel.

    Instances For
      source
      @[noinline]
      def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.firstOrderSelected {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (operation : ExecFloat.Backend.Operation) :
      Bool

      Whether a direct structural call executes the winner of the complete configured portfolio.

      Keep this decision out of the arithmetic body: closed format/plan/policy applications are cached by the compiler, while the selected structural branch remains available for specialization.

      Instances For
        source
        @[always_inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.structuralSqrt {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) :
        ExecFloat (Family format code plan)

        The square-root function stored in the descriptor's structural candidate.

        Instances For
          source
          @[always_inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.structuralFma {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) :
          ExecFloat (Family format code plan)

          The fused-multiply-add function stored in the descriptor's structural candidate.

          Instances For
            source
            theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_add_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.add = true) :
            (ExecFloat.Backend.selectCertified policy (automaticAddCandidates format plan)).run = Backend.wordAdd

            A direct add call names the selected candidate's function.

            source
            theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_sub_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.sub = true) :
            (ExecFloat.Backend.selectCertified policy (automaticSubCandidates format plan)).run = Backend.wordSub

            A direct sub call names the selected candidate's function.

            source
            theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_mul_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.mul = true) :
            (ExecFloat.Backend.selectCertified policy (automaticMulCandidates format plan)).run = Backend.wordMul

            A direct mul call names the selected candidate's function.

            source
            theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_div_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.div = true) :
            (ExecFloat.Backend.selectCertified policy (automaticDivCandidates format plan)).run = Backend.wordDiv

            A direct div call names the selected candidate's function.

            source
            theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_sqrt_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.sqrt = true) :
            (ExecFloat.Backend.selectCertified policy (automaticSqrtCandidates format plan)).run = structuralSqrt

            A direct sqrt call names the selected candidate's function.

            source
            theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_fma_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.fma = true) :
            (ExecFloat.Backend.selectCertified policy (automaticFmaCandidates format plan)).run = structuralFma

            A direct fma call names the selected candidate's function.