TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Runtime

Default static-byte backend runtime #

A static-byte family's selected backend supplies six arithmetic operations and a shared cost estimate. Refinement theorems live in Backend.Proof; capability instances live in Backend.Construction.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.add {F : Type u} [Family F] (left right : ExecFloat F) :
ExecFloat F

Statically selected byte addition.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.sub {F : Type u} [Family F] (left right : ExecFloat F) :
    ExecFloat F

    Statically selected byte subtraction.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.mul {F : Type u} [Family F] (left right : ExecFloat F) :
      ExecFloat F

      Statically selected byte multiplication.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.div {F : Type u} [Family F] (left right : ExecFloat F) :
        ExecFloat F

        Statically selected byte division.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.sqrt {F : Type u} [Family F] (value : ExecFloat F) :
          ExecFloat F

          Statically selected byte square root.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.fma {F : Type u} [Family F] (left right addend : ExecFloat F) :
            ExecFloat F

            Statically selected byte fused multiply-add.

            Instances For
              source
              def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.familyEstimate (operation : String) :
              ExecFloat.Backend.Candidate

              Default estimate for a monomorphic direct-byte kernel supplied by a static family.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Table.binary {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) width_le_eight) modelSpec) (left right : ExecFloat F) :
                ExecFloat F

                Run any certified binary byte table directly on a nominal static-byte format.

                The table is an explicit argument so a closed format package can expose a first-order, monomorphic kernel without projecting a function from its Family dictionary.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Table.unary {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding (Family.format F) width_le_eight) modelSpec) (value : ExecFloat F) :
                  ExecFloat F

                  Run any certified unary byte table directly on a nominal static-byte format.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Table.ternary {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding (Family.format F) width_le_eight) modelSpec) (left right addend : ExecFloat F) :
                    ExecFloat F

                    Run any certified ternary byte table directly on a nominal static-byte format.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Model.ternary {F : Type u} [Family F] (width_le_eight : (Family.format F).bitWidth ≤ 8) (op : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)) (left right addend : ExecFloat F) :
                      ExecFloat F

                      Run a model-level ternary kernel through the direct byte carrier.

                      This is the shared table-free path for operations such as eight-bit FMA, where an exhaustive ternary table would be disproportionately large.

                      Instances For