Conversion into P3109 formats

P3109 destinations use Rat as their canonical exact scalar domain. This lets integers, exact dyadics, configured binary floats, configured posits, and other rationally decoded sources use the ordinary convert, cast, and destination-driven mixed-operation APIs without first passing through a host float.

The conversion context is ProjectionPolicy itself, so the P3109 rounding and saturation modes live in one policy type. Every policy produces a P3109 datum, so conversion returns success for finite, infinite, and exceptional observations. Changes to an input infinity or exceptional observation are reported through mappedSpecial, and endpoint clamping through saturated.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.decodeRat {format : Formats.P3109.Format} (value : P3109 format) : Numerics.NumericalValue ℚ

Decode a P3109 value in the common exact-rational scalar domain.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.exceedsFiniteRange (format : Formats.P3109.Format) (exact : ℚ) : Bool

Whether an exact rational lies strictly outside the closed interval [minFinite, maxFinite].

This is a property of the exact input alone. It is not the overflow indicator: an input slightly above maxFinite that rounds back to maxFinite satisfies this predicate but does not overflow.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.roundedExceedsFiniteRange (format : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (exact : ℚ) : Bool

Whether the precision-rounded value of an exact rational lies strictly outside [minFinite, maxFinite].

Rounding is roundFiniteRatToPrecision in the requested mode, before any saturation. This is the after-rounding range condition of P3109 §4.7.3: an input that rounds to maxFinite is in range even when its exact magnitude exceeds maxFinite. Because the endpoints lie on the precision grid, no rounding mode moves an in-range input past them, so this condition is stronger than exceedsFiniteRange. The theorem roundedExceedsFiniteRange_implies_exceedsFiniteRange in Conversion.Range proves this implication for every mode and every supplied stochastic word.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.belowMinPositive (format : Formats.P3109.Format) (exact : ℚ) : Bool

Whether a nonzero exact magnitude is strictly smaller than the least positive finite P3109 datum.

The comparison is sign-independent and scales by binary position before cross multiplication, so large exponent ranges do not create an enormous temporary rational. This threshold is the least positive datum (the smallest subnormal when the descriptor has subnormals), not the least normal datum used by IEEE 754 tininess.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.isFiniteEndpoint (format : Formats.P3109.Format) : Numerics.NumericalValue Numerics.Dyadic → Bool

Whether a projected datum is one of the descriptor's finite endpoints.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.mappedSpecial : Numerics.NumericalValue ℚ → Numerics.NumericalValue Numerics.Dyadic → Bool

Whether projection deliberately changed a source special-value class or infinity sign.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.finiteInexact (exact : ℚ) : Numerics.NumericalValue Numerics.Dyadic → Bool

Whether projection changes the exact rational input or produces a nonfinite datum.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.status (format : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) : ConversionStatus

Conversion indicators for one completed P3109 projection.

The report defines no status flags, so these are FloatLib's conversion indicators:

• overflow is roundedExceedsFiniteRange: the value rounded to the descriptor's precision in the requested mode lies outside [minFinite, maxFinite]. It does not depend on the saturation mode, and an input that rounds to an endpoint does not overflow (Section 4.7.3, NOTE 1).
• underflow is belowMinPositive: a nonzero exact input strictly smaller in magnitude than the least positive datum. A subnormal-range input that is at least the least positive datum does not raise it, so this is narrower than IEEE 754 tininess.
• saturated is raised only when saturation changed the rounding result and the delivered datum is a finite endpoint.
• invalid is raised for a signaling NaN source, as for binary destinations.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.Conversion.run {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) : ConversionOutcome (P3109 format)

Quantize one complete exact-rational observation according to its P3109 projection policy.

def FloatLib.Floats.ExecFloat.P3109.Conversion.spec {format : Formats.P3109.Format} : Numerics.Quantization.Spec Formats.P3109.ProjectionPolicy (Numerics.NumericalValue ℚ) (ConversionOutcome (P3109 format))

Conversion contract: the outcome has run's word and status, and the word denotes the round-then-saturate datum.

SameDatum compares finite values numerically and identifies NaN payloads, so the word equality is stated as well.

@[instance_reducible, instance 2000]

instance FloatLib.Floats.ExecFloat.P3109.Conversion.exactDecoder {format : Formats.P3109.Format} : ExactDecoder (P3109 format) ℚ

P3109 values decode into the common exact-rational scalar domain.

The raised priority overrides the carrier's generic codebook decoder, whose finite domain is Dyadic, so importing the generic codebook API with P3109 still leaves one source domain for ordinary scalar conversion.