Configured posit conversion runtime

Every configured posit uses Rat as its executable exact domain. Finite conversion follows the Posit Standard (2022) directly: interior values use the appended-bit boundary, nonzero values below minPos select signed minPos, and values above maxPos select signed maxPos.

The default context maps infinity and exceptional observations to the unique NaR. For IEEE infinities and NaNs this follows §6.5 of the Posit Standard (2022); both IEEE signed zeros become posit zero. Callers may explicitly reject infinity or exceptional observations, or saturate infinity to signed maxPos.

The mathematical conversion relation is declared in Conversion.Proof, where the real rounding specification and its rational bridge are available without adding them to runtime imports.

References

• Posit Standard (2022), §6.5.

inductive FloatLib.Floats.ExecFloat.Posit.Conversion.InfinityPolicy : Type

Policy for source infinity presented to a posit destination.

• reject : InfinityPolicy

  Reject infinity because the posit scalar domain has no infinite point.

• toNaR : InfinityPolicy

  Map infinity to the unique posit NaR.

• saturate : InfinityPolicy

  Clamp infinity to signed maxPos.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Posit.Conversion.instDecidableEqInfinityPolicy : DecidableEq InfinityPolicy

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Posit.Conversion.instReprInfinityPolicy : Repr InfinityPolicy

def FloatLib.Floats.ExecFloat.Posit.Conversion.instReprInfinityPolicy.repr : InfinityPolicy → ℕ → Std.Format

inductive FloatLib.Floats.ExecFloat.Posit.Conversion.ExceptionalPolicy : Type

Policy for NaN, NaR, reserved, or undefined observations.

• reject : ExceptionalPolicy

  Reject the observation.

• toNaR : ExceptionalPolicy

  Map the observation to the unique posit NaR.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Posit.Conversion.instDecidableEqExceptionalPolicy : DecidableEq ExceptionalPolicy

def FloatLib.Floats.ExecFloat.Posit.Conversion.instReprExceptionalPolicy.repr : ExceptionalPolicy → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Posit.Conversion.instReprExceptionalPolicy : Repr ExceptionalPolicy

structure FloatLib.Floats.ExecFloat.Posit.Conversion.Context : Type

Posit conversion policies, defaulting to the Posit Standard (2022) special-value mapping.

• infinity : InfinityPolicy

  Source infinity maps to NaR by default, as required by §6.5.

• exceptional : ExceptionalPolicy

  Source exceptional observations map to NaR by default, including IEEE NaNs (§6.5).

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Posit.Conversion.instDecidableEqContext : DecidableEq Context

def FloatLib.Floats.ExecFloat.Posit.Conversion.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

def FloatLib.Floats.ExecFloat.Posit.Conversion.instReprContext.repr : Context → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Posit.Conversion.instReprContext : Repr Context

def FloatLib.Floats.ExecFloat.Posit.Conversion.Context.default : Context

Map source infinity and exceptional observations to NaR (Posit Standard (2022), §6.5).

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Conversion.maxPositiveRat (format : Formats.Posit.Format) : ℚ

Exact magnitude of the largest positive finite posit.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Conversion.finiteStatus {format : Formats.Posit.Format} (exact : ℚ) (rounded : Formats.Posit.Model format) : ConversionStatus

Conversion status computed by exact rational comparison with the posit endpoints.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Conversion.quantizeFinite {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (exact : ℚ) : ConversionOutcome (ExecFloat (Formats.Posit.Configured.Family format code plan))

Quantize a finite rational by the exact arbitrary-width posit reference rounder.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Conversion.quantizeInfinity {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (context : Context) (negative : Bool) : ConversionOutcome (ExecFloat (Formats.Posit.Configured.Family format code plan))

Explicitly handle source infinity.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Conversion.quantizeExceptional {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (context : Context) (exceptional : Numerics.ExceptionalValue) : ConversionOutcome (ExecFloat (Formats.Posit.Configured.Family format code plan))

Explicitly handle a source exceptional observation.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Conversion.run {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (context : Context) : Numerics.NumericalValue ℚ → ConversionOutcome (ExecFloat (Formats.Posit.Configured.Family format code plan))

Reference conversion for every exact-rational observation.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Posit.Conversion.exactDecoder {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : ExactDecoder (ExecFloat (Formats.Posit.Configured.Family format code plan)) ℚ

Configured posit decoding selects the exact-rational conversion domain.