Binary-interchange conversion runtime

Every binary-interchange family uses the same representation-independent conversion policy. A concrete carrier supplies only a pack function from its Model format, so configured machine-word formats and nominal static-byte formats share one exact quantizer.

The exact domain is SignedRat, so the sign of a zero input reaches the destination. Finite values are rounded once by Model.Policy.roundRat, with the sign bit taken from the signed rational and the magnitude from its value. Infinity and exceptional observations have their own policies because finite-only formats cannot preserve every IEEE value class. Status flags are computed from exact rational comparisons, never through a host floating-point value.

specWith pack preserves the complete executable outcome and adds an independent nearest-value predicate for nearest-even/native-overflow/gradual-underflow conversion to conventional IEEE descriptors. Its proof uses the descriptor's real rounding semantics. The nearest-value clause applies when the delivered model has a finite rational denotation. Overflow, tie selection, signed zero, status, and the other policies are covered by the complete executable-outcome clause.

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

Policy for an infinity presented to a binary-interchange destination.

• preserve : InfinityPolicy

  Preserve infinity when the destination encoding supports it, and otherwise reject the cast.

• saturate : InfinityPolicy

  Clamp infinity to the finite destination value of greatest magnitude with the same sign.

• reject : InfinityPolicy

  Reject infinity even when the destination could represent it.

@[instance_reducible]

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

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

@[instance_reducible]

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

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

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

• propagateNaN : ExceptionalPolicy

  Propagate a source NaN as Model.propagatedNaN does in Model.cast. IEEE destinations keep the sign, set the quiet bit, and preserve a payload that fits, otherwise using payload zero. Other encodings follow their own NaN rule. Other exceptional observations become the destination's canonical NaN. This is the default.

• canonicalNaN : ExceptionalPolicy

  Produce the destination's canonical NaN for every exceptional observation.

• reject : ExceptionalPolicy

  Reject every exceptional observation.

@[instance_reducible]

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

@[instance_reducible]

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

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

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

Complete context for conversion into a binary-interchange destination.

• quantization : Numerics.QuantizationPolicy

  Finite rounding, overflow, and underflow behavior.

• entropy : ℕ

  Entropy consumed only by stochastic finite rounding.

• infinity : InfinityPolicy

  Treatment of source infinity.

• exceptional : ExceptionalPolicy

  Treatment of source exceptional values.

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

@[instance_reducible]

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

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

@[instance_reducible]

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

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

Canonical binary conversion context.

Finite values use nearest-even/native-overflow/gradual-underflow behavior. Infinities and exceptional values keep their value class when the destination encoding supports that class, and otherwise conversion fails. An IEEE destination quiets a NaN, keeps its sign and any payload that fits, and replaces an oversized payload with zero. Maximum-NaN encodings keep only the sign, while FNUZ has a single NaN. A signaling NaN raises invalid.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.Context.withRounding (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : Context

Canonical conversion context with finite rounding direction mode.

This is the context a conversion's (mode := ...) option selects for a binary destination. Native overflow, gradual underflow, infinity preservation, and NaN propagation keep their default behavior. Use a record update when any of those policies must also change, or when the finite rounding is stochastic.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.addExact (context : Context) (left right : Numerics.SignedRat) : Numerics.SignedRat

Exact addition with the destination's cancellation-sign rule, before rounding.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.subExact (context : Context) (left right : Numerics.SignedRat) : Numerics.SignedRat

Exact subtraction applies the same cancellation rule to the negated right operand.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.roundedSignificandStatus (format : Formats.BinaryInterchange.FloatFormat) (rounding : Numerics.RoundingMode) (entropy : ℕ) (sign : Bool) (numerator denominator : ℕ) : Bool × Bool

Overflow and tininess of the exact magnitude numerator / denominator from its significand rounded under rounding with an unbounded exponent range, as a pair (overflow, tiny).

The denominator must be nonzero, as it is for every Rat. A zero numerator gives (false, false): an exact zero neither overflows nor underflows. Otherwise the significand is the quotient scaled to fracWidth + 1 significant bits and rounded by Policy.roundQuot, with sign and entropy for the directions and stochastic rounding that need them. It overflows above the largest finite significand of the top binade. Below the normal range it is tiny unless rounding carries it up to the smallest normal value. finiteStatus uses this calculation for rounding modes without an IEEERoundingMode direction.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.finiteStatus {format : Formats.BinaryInterchange.FloatFormat} (context : Context) (exact : ℚ) (rounded : Formats.BinaryInterchange.Model format) : ConversionStatus

Status derived from exact rational binary rounding.

Overflow and tininess use the precision-rounded value with an unbounded exponent range. Merely exceeding the largest finite value does not signal overflow when rounding brings the value back into range. Rounding modes with an IEEERoundingMode direction use the exact classifiers rationalRoundingOverflows and rationalIsTinyAfterRoundingScaled. Stochastic policies use roundedSignificandStatus, with their own integer rounding rule and the supplied entropy, at the same precision boundary.

rounded must be the value that Policy.roundRat delivers for exact under context, as in quantizeFiniteWith. The flags read it, and the direction classifiers count a delivered zero or subnormal as tiny, so a status computed for an unrelated pair has no meaning.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.quantizeFiniteWith {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) (exact : Numerics.SignedRat) : ConversionOutcome Destination

Round one finite signed rational and pack the resulting binary model into a destination carrier.

The sign bit of the result comes from exact.negative, so a negative zero rounds to the destination's negative zero when the encoding has one. pack is the only representation-specific argument. It is applied after exact rounding, so changing storage or an execution backend cannot change numerical meaning.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.quantizeExceptionalWith {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) (exceptional : Numerics.ExceptionalValue) : ConversionOutcome Destination

Apply the exceptional-value policy and pack a destination NaN.

A signaling NaN raises invalid under either NaN-producing policy (IEEE 754-2019 §7.2). Under propagateNaN a source NaN becomes Model.propagatedNaN format negative payload, with the payload supplied by the source decoder without encoding markers. Binary decoders use Model.nanPayload, so this is the NaN that Model.cast delivers across unequal descriptors. It stays in the NaN class, so mappedSpecial is clear. NaR, reserved, and undefined observations, and every observation under canonicalNaN, become the canonical NaN with mappedSpecial. A destination without a NaN encoding rejects the conversion.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.quantizeInfinityWith {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) (negative : Bool) : ConversionOutcome Destination

Apply the infinity policy and pack the selected binary model value.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.runWith {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) : Numerics.NumericalValue Numerics.SignedRat → ConversionOutcome Destination

Reference conversion shared by every carrier for the same binary descriptor.

def FloatLib.Floats.ExecFloat.Binary.Conversion.NearestFinite {format : Formats.BinaryInterchange.FloatFormat} (exact : ℚ) (rounded : Formats.BinaryInterchange.Model format) : Prop

A finite rounded denotation is no farther from the input than any finite destination value.

def FloatLib.Floats.ExecFloat.Binary.Conversion.specWith {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) : Numerics.Quantization.Spec Context (Numerics.NumericalValue Numerics.SignedRat) (ConversionOutcome Destination)

Complete conversion outcome, together with an independent nearest-value clause for IEEE defaults.

The rational predicate is runtime-free: its proof uses real rounding only in Conversion.Proof. Complete outcome equality also preserves overflow, tie selection, zero signs, all status fields, and every nondefault policy. A nonfinite result has no nearest finite denotation.