TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Runtime packing for configured posits #

Code.toModel and Code.ofModel form the canonical executable conversion pair for every static posit carrier. Closed plans reduce to primitive or fixed-limb operations; the wide branch is the identity on the exact-width proof model.

source
theorem FloatLib.Floats.Formats.Posit.Configured.bits_lt_storage_capacity (format : Format) (bits wordWidth : ℕ) (hbits : bits < format.modulus) (width_le : format.bits ≤ wordWidth) :
bits < 2 ^ wordWidth

A valid Posit encoding fits every storage width at least as wide as its format.

source
@[inline]
def FloatLib.Floats.Formats.Posit.Configured.Code.toModel {format : Format} {plan : StoragePlan format} :
Code plan → Model format

Decode a packed runtime code into the exact-width proof model.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.Posit.Configured.Code.ofModel {format : Format} {plan : StoragePlan format} :
    Model format → Code plan

    Pack an exact proof-model value into the selected runtime carrier.

    Instances For