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; configured machine-word formats and nominal static-byte formats therefore 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 use separate explicit 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 retain 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; 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.

• canonicalNaN : ExceptionalPolicy

  Produce the destination's canonical NaN when one exists.

• 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 explicit 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.

@[instance_reducible]

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

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

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 retain their value class when the destination encoding supports that class; otherwise conversion fails explicitly.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Conversion.Context.withRounding (rounding : Numerics.RoundingMode) : Context

Canonical conversion context with one caller-selected finite rounding direction.

Native overflow, gradual underflow, infinity preservation, and canonical-NaN mapping retain their default behavior. Use a record update when any of those policies must also change.

@[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.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. Nearest-away and stochastic policies use their own integer rounding rule, including the supplied entropy, at the same precision boundary.

@[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 deliberately 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 supported canonical NaN.

@[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 additionally preserves overflow, tie selection, zero signs, all status fields, and every nondefault policy. A nonfinite result has no nearest finite denotation.