TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.Byte.Runtime

Configured UInt8 runtime for packed posits #

These wrappers rebuild the statically selected byte carrier around unboxed raw kernels. Range proofs are erased during compilation; semantic refinement is isolated in Byte.Proof.

The visible monomorphic boundary is intentional: it preserves the compiler's direct UInt8 calling convention. Arithmetic itself is shared in FixedWords.Kernels, so this file contains no byte-only algorithm or fallback, only the small adapter required by the configured carrier.

source
@[always_inline]
def FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.add {format : Format} (width_le : format.bits ≤ 8) (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))

Add two posits stored directly in a UInt8 carrier.

Instances For
    source
    @[always_inline]
    def FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.sub {format : Format} (width_le : format.bits ≤ 8) (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))

    Subtract two posits stored directly in a UInt8 carrier.

    Instances For
      source
      @[always_inline]
      def FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.mul {format : Format} (width_le : format.bits ≤ 8) (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))

      Multiply two posits stored directly in a UInt8 carrier.

      Instances For
        source
        @[always_inline]
        def FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.div {format : Format} (width_le : format.bits ≤ 8) (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))

        Divide two posits stored directly in a UInt8 carrier.

        Instances For
          source
          @[always_inline]
          def FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.sqrt {format : Format} (width_le : format.bits ≤ 8) (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))

          Take the square root of a posit stored directly in a UInt8 carrier.

          Instances For
            source
            @[always_inline]
            def FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.fma {format : Format} (width_le : format.bits ≤ 8) (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))

            Fused multiply-add for posits stored directly in a UInt8 carrier.

            Instances For