TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.WideLimbCandidates

Certified wide-limb candidates for the limb carrier #

An explicit StoragePlan.limbs stores formats wider than 128 bits in limb arrays. Its arithmetic candidates enter through this carrier and are proved equal to the configured reference operation through Model.WideLimb.toModel_add and its siblings together with the codec laws. Division and square root use arbitrary-precision integer quotients and roots after reading the stored fields; the other kernels operate on the limbs themselves. A candidate is offered only when Model.WideLimb.Eligible holds, a decidable test on the descriptor.

source
def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbEstimate (format : FloatFormat) (operation : ExecFloat.Backend.Operation) :
ExecFloat.Backend.Candidate

Estimate for a direct limb-carrier entry, including any internal integer conversions.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbAdd (format : FloatFormat) (width_gt : 128 < format.bitWidth) (h : Model.WideLimb.Eligible format) :
    ExecFloat.Backend.Certified Spec.add

    Certified wide-limb addition on the limb carrier.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbSub (format : FloatFormat) (width_gt : 128 < format.bitWidth) (h : Model.WideLimb.Eligible format) :
      ExecFloat.Backend.Certified Spec.sub

      Certified wide-limb subtraction on the limb carrier.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbMul (format : FloatFormat) (width_gt : 128 < format.bitWidth) (h : Model.WideLimb.Eligible format) :
        ExecFloat.Backend.Certified Spec.mul

        Certified wide-limb multiplication on the limb carrier.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbDiv (format : FloatFormat) (width_gt : 128 < format.bitWidth) (h : Model.WideLimb.Eligible format) :
          ExecFloat.Backend.Certified Spec.div

          Certified wide-limb division on the limb carrier.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbSqrt (format : FloatFormat) (width_gt : 128 < format.bitWidth) (h : Model.WideLimb.Eligible format) :
            ExecFloat.Backend.Certified Spec.sqrt

            Certified wide-limb square root on the limb carrier.

            Instances For
              source
              def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbFma (format : FloatFormat) (width_gt : 128 < format.bitWidth) (h : Model.WideLimb.Eligible format) :
              ExecFloat.Backend.Certified Spec.fma

              Certified wide-limb fused multiply-add on the limb carrier.

              Instances For
                source
                def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbAdd? (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
                Option (ExecFloat.Backend.Certified Spec.add)

                Offer wide-limb addition exactly when the descriptor is eligible.

                Instances For
                  source
                  def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbSub? (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
                  Option (ExecFloat.Backend.Certified Spec.sub)

                  Offer wide-limb subtraction exactly when the descriptor is eligible.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbMul? (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
                    Option (ExecFloat.Backend.Certified Spec.mul)

                    Offer wide-limb multiplication exactly when the descriptor is eligible.

                    Instances For
                      source
                      def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbDiv? (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
                      Option (ExecFloat.Backend.Certified Spec.div)

                      Offer wide-limb division exactly when the descriptor is eligible.

                      Instances For
                        source
                        def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbSqrt? (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
                        Option (ExecFloat.Backend.Certified Spec.sqrt)

                        Offer wide-limb square root exactly when the descriptor is eligible.

                        Instances For
                          source
                          def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.wideLimbFma? (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
                          Option (ExecFloat.Backend.Certified Spec.fma)

                          Offer wide-limb fused multiply-add exactly when the descriptor is eligible.

                          Instances For