TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.Runtime

Direct exhaustive runtime kernels for configured byte formats #

Every binary-interchange descriptor occupying at most eight encoded bits admits the same format-independent tiny-table backend used by other finite encodings. Table generation evaluates the reference definition, while warm execution performs native indexing and one byte load.

The operation planner may reject a table when setup cost or resident memory is inappropriate for the selected workload. That policy does not affect the refinement proofs in ByteTable.Proof.

source
def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.encoding (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) :
ExecFloat.Backend.TinyTable.Encoding (Model format)

The exact binary-interchange model as a proved finite byte encoding.

Instances For

    Tables generated from reference model kernels #

    source
    def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.addTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) :
    ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.add

    Lazily generated direct addition table.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.subTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) :
      ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.sub

      Lazily generated direct subtraction table.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.mulTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) :
        ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.mul

        Lazily generated direct multiplication table.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.divTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) :
          ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.div

          Lazily generated direct division table.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.sqrtTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) :
            ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) Model.Spec.sqrt

            Lazily generated direct square-root table.

            Instances For
              source
              def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.fmaTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) :
              ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) Model.Spec.fma

              Lazily generated direct fused-multiply-add table.

              Instances For

                Direct configured-carrier execution #

                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runBinary {format : FloatFormat} {modelSpec : Model format → Model format → Model format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) modelSpec) (left right : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))) :
                ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))

                Execute one already-constructed certified binary table on the configured byte carrier.

                The explicit table argument ensures the selected capability captures one memoizing Thunk instead of constructing a fresh cell on every arithmetic call.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runUnary {format : FloatFormat} {modelSpec : Model format → Model format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) modelSpec) (value : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))) :
                  ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))

                  Execute one already-constructed certified unary table on the configured byte carrier.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runTernary {format : FloatFormat} {modelSpec : Model format → Model format → Model format → Model format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) modelSpec) (left right addend : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))) :
                    ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))

                    Execute one already-constructed certified ternary table on the configured byte carrier.

                    Instances For