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; 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✝¹)

def FloatLib.Floats.Formats.BinaryInterchange.instReprModel.repr {fmt✝ : FloatFormat} : Model fmt✝ → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instReprModel {fmt✝ : FloatFormat} : Repr (Model fmt✝)

@[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; it 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.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. Keeping this dependent boundary beside the NaN selectors lets operations 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 still 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.nextUp {fmt : FloatFormat} (x : Model fmt) : Model fmt

The next representable value strictly greater than x.

A quiet NaN and the positive endpoint are fixed. A signaling NaN becomes the corresponding quiet NaN; since this value-only operation carries no status, the invalid signal IEEE 754-2019 §5.3.1 owes to a signaling operand is reported by nextUpWithStatus 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.nextDown {fmt : FloatFormat} (x : Model fmt) : Model fmt

The next representable value strictly less than x.

A quiet NaN and the negative endpoint are fixed. A signaling NaN becomes the corresponding quiet NaN; the invalid signal it owes is reported by nextDownWithStatus in Operations.Runtime. Formats without infinity saturate at their most negative finite value.