Descriptor-indexed binary-interchange proof model

Model fmt is the bit-exact specification carrier for the binary-interchange family. Statically declared formats use FloatLib.Floats.ExecFloat F, whose runtime representation is selected by EncodedFormat F.

This model stores BitVec fmt.bitWidth so descriptor-generic specifications and refinement proofs can quantify over a runtime-selected layout. Concrete format packages bridge their direct runtime codes to this model at the proof boundary.

References

• IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, Sections 3.4 and 6.2, https://doi.org/10.1109/IEEESTD.2019.8766229.

structure FloatLib.Floats.Formats.BinaryInterchange.Model (fmt : FloatFormat) : Type

Descriptor-indexed bit-level proof model for format fmt.

The carrier is BitVec fmt.bitWidth, and every stored bit is part of the format.

• bits : fmt.ExecWord

  Raw binary storage pattern.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instDecidableEqModel {fmt✝ : FloatFormat} : DecidableEq (Model fmt✝)

def FloatLib.Floats.Formats.BinaryInterchange.instDecidableEqModel.decEq {fmt✝ : FloatFormat} (x✝ x✝¹ : Model fmt✝) : Decidable (x✝ = x✝¹)

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ofBits {fmt : FloatFormat} (b : fmt.ExecWord) : Model fmt

Wrap a storage word as a Model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ofNatBits {fmt : FloatFormat} (n : ℕ) : Model fmt

Wrap a Nat pattern, reduced to the format's exact bit width.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.toBits {fmt : FloatFormat} (x : Model fmt) : fmt.ExecWord

Extract the raw storage word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.toNatBits {fmt : FloatFormat} (x : Model fmt) : ℕ

Return the encoded bit pattern as a natural number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toNatBits_lt_two_pow {fmt : FloatFormat} (x : Model fmt) : x.toNatBits < 2 ^ fmt.bitWidth

Every encoded word lies below the radix determined by its stored width.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ofUInt32 {fmt : FloatFormat} (b : UInt32) : Model fmt

Wrap a UInt32 pattern, truncating it when the destination has fewer than 32 bits.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofNatBits_toNatBits {fmt : FloatFormat} (x : Model fmt) : ofNatBits x.toNatBits = x

Re-encoding the exact natural-number bit pattern preserves a binary value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toNatBits_ofNatBits_of_lt {fmt : FloatFormat} (bits : ℕ) (hbits : bits < 2 ^ fmt.bitWidth) : (ofNatBits bits).toNatBits = bits

An in-range natural-number pattern is not changed by fixed-width encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toBits_ofBits {fmt : FloatFormat} (b : fmt.ExecWord) : (ofBits b).toBits = b

Wrapping a storage word and reading it back is the identity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofBits_toBits {fmt : FloatFormat} (x : Model fmt) : ofBits x.toBits = x

Rewrapping the storage word of a value is the identity.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instInhabited {fmt : FloatFormat} : Inhabited (Model fmt)

Field extraction and classification

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.signBit {fmt : FloatFormat} (x : Model fmt) : Bool

Whether the sign bit is set.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_eq_msb {fmt : FloatFormat} (x : Model fmt) : x.signBit = BitVec.msb x.bits

The executable sign test is the most significant bit of the storage word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.expField {fmt : FloatFormat} (x : Model fmt) : ℕ

The biased exponent field as a natural number.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.fracField {fmt : FloatFormat} (x : Model fmt) : ℕ

The low fracWidth bits of the fraction field.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isNaN {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x has an IEEE NaN bit pattern.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isQNaN {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x has an IEEE quiet-NaN bit pattern.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isSNaN {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x has an IEEE signaling-NaN bit pattern.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isInf {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x has an IEEE infinity bit pattern.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isZero {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x has an IEEE signed-zero bit pattern.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isFinite {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x has an IEEE finite bit pattern.

Policy-aware classification

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x is one of the NaN encodings selected by its complete format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isQNaN {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x is a quiet NaN.

The non-IEEE policies represented by FloatFormat.Encoding do not distinguish signaling from quiet NaNs, so every NaN in those formats is classified as quiet.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isSNaN {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x is a signaling NaN. Only the IEEE encoding has signaling NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isSNaN_eq_false_of_isNaN_eq_false {fmt : FloatFormat} (x : Model fmt) (hx : x.isNaN = false) : x.isSNaN = false

A value that is not a NaN cannot be a signaling NaN.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isInf {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x is an infinity. Only the IEEE encoding contains infinities.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isZero {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x denotes zero under its complete format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x denotes a finite value under its complete format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isSubnormal {fmt : FloatFormat} (x : Model fmt) : Bool

Whether x is a finite subnormal under its complete format.

Encoding and constants

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.mkBits (fmt : FloatFormat) (sign : Bool) (exp frac : ℕ) : fmt.ExecWord

Pack a sign, biased exponent, and fraction into one exact-width storage word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ofFields (fmt : FloatFormat) (sign : Bool) (exp frac : ℕ) : Model fmt

Construct a value from its sign, exponent, and fraction fields.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.posZero (fmt : FloatFormat) : Model fmt

Positive zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.negZero (fmt : FloatFormat) : Model fmt

The negative-zero bit pattern, which denotes NaN in FNUZ formats.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.posOne (fmt : FloatFormat) : Model fmt

Positive one.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.negOne (fmt : FloatFormat) : Model fmt

Negative one.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.posInf (fmt : FloatFormat) : Model fmt

The positive-infinity IEEE bit pattern. Use infinity? for policy-aware construction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.negInf (fmt : FloatFormat) : Model fmt

The negative-infinity IEEE bit pattern. Use infinity? for policy-aware construction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.maxFinite (fmt : FloatFormat) (sign : Bool) : Model fmt

Finite value of greatest magnitude with the requested sign.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.posMaxFinite (fmt : FloatFormat) : Model fmt

Largest finite positive value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.negMaxFinite (fmt : FloatFormat) : Model fmt

Finite value with the largest negative magnitude.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalNaN (fmt : FloatFormat) : Model fmt

The canonical IEEE quiet-NaN bit pattern. Use canonicalNaN? for other encodings.

Policy-aware constants

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.zero (fmt : FloatFormat) (sign : Bool) : Model fmt

Signed zero, canonicalizing negative zero when the format has only one zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.infinity? (fmt : FloatFormat) (sign : Bool) : Option (Model fmt)

Signed infinity when the format supports it.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalNaN? (fmt : FloatFormat) : Option (Model fmt)

A canonical NaN when the format has a NaN encoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.invalidResult (fmt : FloatFormat) : Model fmt

Total result for an invalid operation in the complete format descriptor.

Formats with a NaN encoding use their canonical NaN. A format whose every bit pattern is numeric uses positive zero because it has no exceptional result to encode.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.infinityOrMaxFinite (fmt : FloatFormat) (sign : Bool) : Model fmt

Signed infinity when the format supports it, otherwise the same-sign largest finite value.

This constructs a range boundary for saturation and interval endpoints. Nonsaturating conversion, arithmetic, and exact reductions use nativeOverflow, which may return NaN when the format reserves an exceptional encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.zero_eq_signedZero_of_isIEEE (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) : zero fmt sign = if sign = true then negZero fmt else posZero fmt

Conventional IEEE policy zero is the usual signed zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.invalidResult_eq_canonicalNaN_of_isIEEE (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : invalidResult fmt = canonicalNaN fmt

Conventional IEEE invalid operations return the canonical NaN.

NaN propagation

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.quietNaN {fmt : FloatFormat} (x : Model fmt) : Model fmt

Set the quiet bit of a NaN, leaving non-NaN values unchanged.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.payloadOfNaNField (signaling : Bool) (field : ℕ) (encoding : FloatFormat.Encoding := FloatFormat.Encoding.ieee) : ℕ

The IEEE 754 §9.7 payload of a binary NaN fraction field: the field without its quiet bit.

The quiet bit is the most significant fraction bit. It is therefore the highest set bit of a quiet NaN's field and clear in a signaling NaN's field, so the payload is recovered without knowing the fraction width. A zero field has payload zero. Non-IEEE encodings have no diagnostic payload bits, so their payload is zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.nanPayload {fmt : FloatFormat} (x : Model fmt) : ℕ

Diagnostic payload of a binary NaN, excluding its quiet bit.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.propagatedNaN (fmt : FloatFormat) (negative : Bool) (payload : ℕ) : Model fmt

A quiet NaN of fmt carrying a source NaN's sign and payload, following IEEE 754-2019 §6.2.3.

IEEE encodings keep the sign, set the quiet bit, and keep the payload when it fits below the quiet bit. A payload that does not fit is replaced by zero, the canonical payload. The maximum-NaN encoding keeps only the sign, FNUZ has a single NaN, and a fully finite encoding returns invalidResult fmt, positive zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN1 {fmt : FloatFormat} (x : Model fmt) : Option (Model fmt)

Return x quieted when it is a NaN.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN2 {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Select signaling NaNs before quiet NaNs, breaking ties from left to right.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN3 {fmt : FloatFormat} (x y z : Model fmt) : Option (Model fmt)

Ternary NaN selection used by fused multiply-add.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.withNaNSelection {fmt : FloatFormat} (selected : Option (Model fmt)) (otherwise : selected = none → Model fmt) : Model fmt

Return a selected NaN, or continue with evidence that NaN selection produced no result.

The continuation proof is erased. Operations use it to rule out impossible ordinary branches without duplicating selection logic.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.withNaNSelection_of_none {fmt : FloatFormat} (selected : Option (Model fmt)) (otherwise : selected = none → Model fmt) (hselected : selected = none) : withNaNSelection selected otherwise = otherwise hselected

A failed NaN selection enters the ordinary operation.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.withNaNSelection_of_some {fmt : FloatFormat} (selected : Option (Model fmt)) (otherwise : selected = none → Model fmt) (nan : Model fmt) (hselected : selected = some nan) : withNaNSelection selected otherwise = nan

A successful NaN selection returns the selected NaN.

Sign and adjacency

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.toggleSign {fmt : FloatFormat} (x : Model fmt) : Model fmt

Flip only the stored sign bit, without interpreting the format's encoding policy.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_toggleSign {fmt : FloatFormat} (x : Model fmt) : x.toggleSign.fracField = x.fracField

Toggling the stored sign bit preserves the fraction field.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_toggleSign {fmt : FloatFormat} (x : Model fmt) : x.toggleSign.expField = x.expField

Toggling the stored sign bit preserves the exponent field.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_toggleSign {fmt : FloatFormat} (x : Model fmt) : x.toggleSign.signBit = !x.signBit

Toggling the stored sign bit complements the decoded sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toggleSign_toggleSign {fmt : FloatFormat} (x : Model fmt) : x.toggleSign.toggleSign = x

Toggling the stored sign bit twice restores the original word.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isNaN_toggleSign {fmt : FloatFormat} (x : Model fmt) : isNaN x.toggleSign = isNaN x

Toggling the stored sign bit preserves IEEE NaN classification.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isInf_toggleSign {fmt : FloatFormat} (x : Model fmt) : isInf x.toggleSign = isInf x

Toggling the stored sign bit preserves IEEE infinity classification.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isZero_toggleSign {fmt : FloatFormat} (x : Model fmt) : isZero x.toggleSign = isZero x

Toggling the stored sign bit preserves IEEE zero classification.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isFinite_toggleSign {fmt : FloatFormat} (x : Model fmt) : isFinite x.toggleSign = isFinite x

Toggling the stored sign bit preserves IEEE finiteness.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.neg {fmt : FloatFormat} (x : Model fmt) : Model fmt

Negate an encoded value according to its format.

Formats with signed zero use the flat sign-bit operation. An unsigned-zero format preserves its single zero and reserved NaN encodings instead of exchanging them.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_eq_toggleSign_of_supportsSignedZero {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.supportsSignedZero = true) : x.neg = x.toggleSign

Formats with signed zero implement negation as a flat stored-sign toggle.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_eq_self_of_not_supportsSignedZero_of_isNaN {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.supportsSignedZero = false) (hx : x.isNaN = true) : x.neg = x

An unsigned-zero format preserves a NaN under negation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_eq_self_of_not_supportsSignedZero_of_isZero {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.supportsSignedZero = false) (hx : x.isZero = true) : x.neg = x

An unsigned-zero format preserves its single zero under negation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_eq_toggleSign_of_isNaN_eq_false_of_isZero_eq_false {fmt : FloatFormat} (x : Model fmt) (hnan : x.isNaN = false) (hzero : x.isZero = false) : x.neg = x.toggleSign

A value that is neither NaN nor zero is negated by the raw stored-sign toggle.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_neg {fmt : FloatFormat} (x : Model fmt) : x.neg.fracField = x.fracField

Negation preserves the fraction field of every encoded value, including NaNs.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_neg {fmt : FloatFormat} (x : Model fmt) : x.neg.expField = x.expField

Negation preserves the exponent field of every encoded value, including infinities and NaNs.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_neg {fmt : FloatFormat} (x : Model fmt) : x.neg.signBit = if fmt.supportsSignedZero = true then !x.signBit else if (x.isNaN || x.isZero) = true then x.signBit else !x.signBit

Negation toggles the sign unless an unsigned-zero format preserves zero or NaN.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isNaN_neg {fmt : FloatFormat} (x : Model fmt) : isNaN x.neg = isNaN x

Negation preserves IEEE NaN classification.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isInf_neg {fmt : FloatFormat} (x : Model fmt) : isInf x.neg = isInf x

Negation preserves IEEE infinity classification.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isZero_neg {fmt : FloatFormat} (x : Model fmt) : isZero x.neg = isZero x

Negation preserves IEEE zero classification.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.IEEE.isFinite_neg {fmt : FloatFormat} (x : Model fmt) : isFinite x.neg = isFinite x

Negation preserves IEEE finiteness.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.copySign {fmt : FloatFormat} (magnitude signSource : Model fmt) : Model fmt

Copy the numerical sign of signSource onto magnitude.

For formats with signed zero, this is the usual quiet sign-bit operation. An unsigned-zero format uses its sign-bit word as the NaN encoding, so zero and NaN are preserved instead of being changed into one another. Every other finite value receives the requested stored sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.copySign_eq_self_of_signBit_eq {fmt : FloatFormat} (magnitude signSource : Model fmt) (hsign : magnitude.signBit = signSource.signBit) : magnitude.copySign signSource = magnitude

Copying an already equal sign leaves the complete encoded word unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.copySign_eq_self_of_not_supportsSignedZero_of_isZero {fmt : FloatFormat} (magnitude signSource : Model fmt) (hfmt : fmt.supportsSignedZero = false) (hzero : magnitude.isZero = true) : magnitude.copySign signSource = magnitude

An unsigned-zero format preserves its zero when a sign is copied onto it.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.copySign_eq_self_of_not_supportsSignedZero_of_isNaN {fmt : FloatFormat} (magnitude signSource : Model fmt) (hfmt : fmt.supportsSignedZero = false) (hnan : magnitude.isNaN = true) : magnitude.copySign signSource = magnitude

An unsigned-zero format preserves its reserved NaN word when a sign is copied onto it.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.abs {fmt : FloatFormat} (x : Model fmt) : Model fmt

Absolute value under the complete format policy.

This clears an ordinary stored sign. In an unsigned-zero encoding it leaves the unique zero and reserved NaN word intact, avoiding the raw-bit alias between those two encodings.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.posMinSubnormal (fmt : FloatFormat) : Model fmt

The smallest positive subnormal encoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.negMinSubnormal (fmt : FloatFormat) : Model fmt

The negative subnormal of smallest magnitude.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.nextUp {fmt : FloatFormat} (x : Model fmt) : Model fmt

The next representable value strictly greater than x, the kernel of Model.nextUp x.

A quiet NaN and the positive endpoint are fixed. A signaling NaN becomes the corresponding quiet NaN, and the invalid signal IEEE 754-2019 §5.3.1 owes to a signaling operand is reported by Model.nextUp x (status := true) in Operations.Runtime. Formats without infinity saturate at their largest finite value. In an unsigned-zero encoding, the word immediately below the negative minimum subnormal is reserved for NaN, so that transition goes directly to the format's unique zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.nextDown {fmt : FloatFormat} (x : Model fmt) : Model fmt

The next representable value strictly less than x, the kernel of Model.nextDown x.

A quiet NaN and the negative endpoint are fixed. A signaling NaN becomes the corresponding quiet NaN, and the invalid signal it owes is reported by Model.nextDown x (status := true) in Operations.Runtime. Formats without infinity saturate at their most negative finite value.