TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Core.Construction

Static-byte table and kernel construction #

Lazy certified tables and complete family kernel bundles are constructed from the format-independent tiny-table backend. Proof terms are erased, while the generated tables remain memoized runtime values.

Standard binary-interchange tables #

source
def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Tables.add (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) :
ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.add

Lazily generated certified addition table for any static byte descriptor.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Tables.sub (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) :
    ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.sub

    Lazily generated certified subtraction table for any static byte descriptor.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Tables.mul (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) :
      ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.mul

      Lazily generated certified multiplication table for any static byte descriptor.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Tables.div (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) :
        ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.div

        Lazily generated certified division table for any static byte descriptor.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Tables.sqrt (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) :
          ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) Model.Spec.sqrt

          Lazily generated certified square-root table for any static byte descriptor.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Tables.fma (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) :
            ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) Model.Spec.fma

            Lazily generated certified fused-multiply-add table for any static byte descriptor.

            Instances For
              source
              def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Kernels.fromTables {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) (add : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.add) (sub : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.sub) (mul : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.mul) (div : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.div) (sqrt : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) Model.Spec.sqrt) (fma : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) Model.Spec.fma) :
              Kernels format

              Build all six direct kernels from the shared format-independent byte-table backend.

              Instances For
                source
                def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Kernels.fromTablesWithModelFma {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) (add : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.add) (sub : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.sub) (mul : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.mul) (div : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.div) (sqrt : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) Model.Spec.sqrt) (fmaModel : ModelValue format → ModelValue format → ModelValue format → ModelValue format) (fmaModel_eq_spec : ∀ (left right addend : ModelValue format), fmaModel left right addend = Model.Spec.fma left right addend) :
                Kernels format

                Build table-backed arithmetic with a certified model-level fused multiply-add.

                For an eight-bit format, the four binary tables contain 4 * 256² byte entries and the square-root table contains 256. Computing FMA with the supplied model kernel avoids a 256³-entry table.

                Instances For