Binary conversion of zeros and NaNs

The zero theorem includes all status flags. The NaN field theorems establish the stored sign, all-ones exponent and quiet-bit-plus-payload fraction independently of any destination width.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryOverflow_zero (fmt : BinaryInterchange.FloatFormat) (mode : RoundingMode) (s : Bool) : binaryOverflow fmt mode s 0 = false

Zero magnitude cannot overflow in any rounding direction.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_zero (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) (q : ℤ) : toBinary fmt hfmt mode (Datum.finite s 0 q) = { value := BinaryInterchange.Model.zero fmt s, status := { } }

Every decimal zero cohort converts to the source-signed binary zero with clear status.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNaN_signBit (fmt : BinaryInterchange.FloatFormat) (s : Bool) (payload : ℕ) : (binaryNaN fmt s payload).signBit = s

NaN conversion preserves the sign bit for every destination width.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNaN_expField (fmt : BinaryInterchange.FloatFormat) (s : Bool) (payload : ℕ) : (binaryNaN fmt s payload).expField = fmt.expAllOnesNat

The encoded NaN exponent is all ones.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNaN_fracField (fmt : BinaryInterchange.FloatFormat) (s : Bool) (payload : ℕ) : (binaryNaN fmt s payload).fracField = 2 ^ (fmt.fracWidth - 1) + if payload < 2 ^ (fmt.fracWidth - 1) then payload else 0

The quiet bit is set and the remaining fraction bits contain the selected payload.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNaN_isNaN (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) (payload : ℕ) : (binaryNaN fmt s payload).isNaN = true

The binary NaN constructed by conversion is classified as NaN on IEEE destinations.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNaN_quiet_bit (fmt : BinaryInterchange.FloatFormat) (s : Bool) (payload : ℕ) : (binaryNaN fmt s payload).fracField / 2 ^ (fmt.fracWidth - 1) = 1

The highest fraction bit is one, so the constructed NaN is quiet.