Configured posit backend runtime

The posit planner selects from representation-independent exact-dyadic backends, two-limb model-valued backends, and direct packed-storage kernels that read UInt64 words or UInt64 pairs.

Packed carriers pair a code with a proof that it lies below the format modulus. Their constructors use the arithmetic kernels' range theorems; these proof arguments are erased during compilation. Semantic refinement of the configured entry points is proved in FloatLib.Floats.Formats.Posit.Configured.Backend.Proof.

Representation-independent exact-dyadic kernels

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicAdd {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Exact-dyadic addition backend.

Finite inputs are aligned, added, and rounded entirely as signed binary integers.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicSub {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Exact-dyadic subtraction backend.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicMul {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Exact-dyadic multiplication backend.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicDiv {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Width-generic quotient-prefix division backend.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicSqrt {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Rational-free square-root backend.

The kernel is DirectDyadicSquareRoot: one destination-width integer root prefix, with the exact square remainder jammed into the sticky bit before the single rounding step.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicFma {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Exact-dyadic fused multiply-add backend with one final rounding step.

Representation-independent two-limb kernels

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbAdd {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Two-limb-rounded addition for formats of at most 128 bits.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbSub {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Two-limb-rounded subtraction for formats of at most 128 bits.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbMul {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Two-limb-rounded multiplication for formats of at most 128 bits.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbFma {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right third : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Two-limb-rounded fused multiply-add for formats of at most 128 bits.

Direct built-in packed-storage kernels

These are the native kernels: addWordsCodeFlatValid, subWordsCodeFlatValid, fmaWordsCodeFlatValid, PackedProduct.mulWordsCodeValid, PackedQuotient.divWordsCodeValid, and PackedSquareRoot.sqrtWordCodeValid operate on UInt64 words and consume the eligibility witness.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordAdd {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : ExecFloat (Family format (Code plan) plan)

Native-word addition that reads built-in packed storage directly.

Unlike dyadicAdd, this entry point does not reconstruct Model operands. Its NativeCode capability is available only for built-in UInt8/UInt16/UInt32/UInt64 plans.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordSub {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : ExecFloat (Family format (Code plan) plan)

Direct built-in packed-storage subtraction.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordMul {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : ExecFloat (Family format (Code plan) plan)

Direct built-in packed-storage multiplication.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordDiv {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : ExecFloat (Family format (Code plan) plan)

Direct built-in packed-storage division.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordSqrt {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (value : ExecFloat (Family format (Code plan) plan)) : ExecFloat (Family format (Code plan) plan)

Direct built-in packed-storage square root.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordFma {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right addend : ExecFloat (Family format (Code plan) plan)) : ExecFloat (Family format (Code plan) plan)

Direct built-in packed-storage fused multiply-add.

Direct two-limb packed-storage kernels

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbAdd {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))

Two-limb addition that reads and returns .pair storage directly.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbSub {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))

Direct two-limb packed-storage subtraction.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbMul {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))

Direct two-limb packed-storage multiplication.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbDiv {format : Format} (width_le : format.bits ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))

Width-generic quotient-prefix division with direct .pair operand decoding.

This is only a storage adapter: it removes the pair-to-model round trip while retaining the same DirectDyadicQuotient.round kernel used by arbitrary-width Posits.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbSqrt {format : Format} (width_le : format.bits ≤ 128) (value : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))

Direct two-limb packed-storage square root.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbFma {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right addend : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))

Direct two-limb packed-storage fused multiply-add.