TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Storage.Pair.Runtime

Two-limb runtime access for configured posits #

Formats from 65 through 128 bits use a persistent UInt128 pair by default. These operations expose and pack that carrier directly, without constructing a model at the storage boundary.

source
@[inline]
def FloatLib.Floats.Formats.Posit.Configured.PairCode.word {format : Format} (code : PairCode format) :
Numerics.FixedWord.UInt128

Read the two persistent limbs without reconstructing the exact-width proof model.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.Posit.Configured.PairCode.packWord {format : Format} (word : Numerics.FixedWord.UInt128) (hword : word.toNat < format.modulus) :
    PairCode format

    Store one already-range-checked two-limb encoding directly.

    Unlike pack, this carrier-native boundary performs no natural-number conversion. It is the result constructor for arithmetic kernels whose complete code already resides in UInt128.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.Posit.Configured.PairCode.pack {format : Format} (width_le : format.bits ≤ 128) (bits : ℕ) (hbits : bits < format.modulus) :
      PairCode format

      Pack one already-range-checked complete encoding into two persistent limbs.

      The format-width premise proves that conversion to UInt128 is exact rather than modular.

      Instances For