TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.ByteTable.Runtime

Runtime support for byte-sized posit tables #

Byte-sized posit tables share a finite encoding and direct execution on their carrier. Certified table construction and correctness proofs are separate so consumers can depend on the smallest appropriate layer.

source
def FloatLib.Floats.Formats.Posit.Configured.ByteTable.encoding (format : Format) (width_le : format.bits ≤ 8) :
ExecFloat.Backend.TinyTable.Encoding (Model format)

The exact posit model as a proved finite byte encoding.

Instances For

    Direct configured-carrier execution #

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

    Execute a certified binary table on the public byte carrier.

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

      Execute a certified unary table on the public byte carrier.

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

        Execute a certified ternary table on the public byte carrier.

        Instances For