Correctness of packed field access

The packed-field laws describe how Model.ofFields decodes. The results are uniform in the format and isolate the bit-layout reasoning needed by rounding, status-flag, and interval proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_eq_true_iff_signMaskNat_le {fmt : FloatFormat} (x : Model fmt) : x.signBit = true ↔ fmt.signMaskNat ≤ x.toNatBits

The sign bit is set exactly for storage words in the upper half of the format's code space.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_eq_false_iff_toNatBits_lt_signMaskNat {fmt : FloatFormat} (x : Model fmt) : x.signBit = false ↔ x.toNatBits < fmt.signMaskNat

The sign bit is clear exactly for storage words in the lower half of the format's code space.

Field classification

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponent : exponent < 2 ^ fmt.expWidth) (hfraction : fraction < 2 ^ fmt.fracWidth) : (ofFields fmt sign exponent fraction).isZero = match fmt.encoding with | FloatFormat.Encoding.finiteUnsignedZero => !sign && exponent == 0 && fraction == 0 | FloatFormat.Encoding.ieee => exponent == 0 && fraction == 0 | FloatFormat.Encoding.finiteMaxNaN => exponent == 0 && fraction == 0 | FloatFormat.Encoding.finite => exponent == 0 && fraction == 0

Classification of an in-range explicit field tuple as zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponent : exponent < 2 ^ fmt.expWidth) (hfraction : fraction < 2 ^ fmt.fracWidth) : (ofFields fmt sign exponent fraction).isFinite = match fmt.encoding with | FloatFormat.Encoding.ieee => exponent != fmt.expAllOnesNat | FloatFormat.Encoding.finiteMaxNaN => !(exponent == fmt.expAllOnesNat && fraction == fmt.fracMaskNat) | FloatFormat.Encoding.finiteUnsignedZero => !(sign && exponent == 0 && fraction == 0) | FloatFormat.Encoding.finite => true

Classification of an in-range explicit field tuple as finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofFields_ieee (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (exponent fraction : ℕ) (hexponent : exponent < fmt.expAllOnesNat) : (ofFields fmt sign exponent fraction).isFinite = true

An IEEE field tuple is finite whenever its exponent is not the reserved all-ones pattern.

ofFields truncates the supplied fraction to the descriptor width, so this specialization needs no separate fraction bound.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_maxFinite (fmt : FloatFormat) (sign : Bool) : (maxFinite fmt sign).isFinite = true

The maximum-magnitude finite encoding is finite for either sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_posMaxFinite (fmt : FloatFormat) : (posMaxFinite fmt).isFinite = true

The largest positive finite encoding is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofFields_normal_of_le_maxFinite (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponentPos : exponent ≠ 0) (hexponent : exponent < 2 ^ fmt.expWidth) (hfraction : fraction < 2 ^ fmt.fracWidth) (hmax : exponent < fmt.maxFiniteExpField ∨ exponent = fmt.maxFiniteExpField ∧ fraction ≤ fmt.maxFiniteFracField) : (ofFields fmt sign exponent fraction).isFinite = true

A normal field pair at or below the descriptor's greatest finite field pair is finite.

Finite field decoding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_ofFields_of_isFinite (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponent : exponent < 2 ^ fmt.expWidth) (hfraction : fraction < 2 ^ fmt.fracWidth) (hfinite : (ofFields fmt sign exponent fraction).isFinite = true) : (ofFields fmt sign exponent fraction).toDyadic? = if exponent = 0 then if fraction = 0 then some { negative := sign, significand := 0, exponent := 0 } else some { negative := sign, significand := fraction, exponent := fmt.minSubnormalExponent } else some { negative := sign, significand := pow2 fmt.fracWidth + fraction, exponent := Int.ofNat exponent - Int.ofNat fmt.exponentBias - Int.ofNat fmt.fracWidth }

Decode in-range fields known to denote a finite value.

The exact exponent uses the bias declared by the complete format descriptor. This includes all-ones exponent fields when the selected non-IEEE encoding treats them as finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_ofFields_subnormal (fmt : FloatFormat) (sign : Bool) (fraction : ℕ) (hfractionPos : fraction ≠ 0) (hfraction : fraction < 2 ^ fmt.fracWidth) : (ofFields fmt sign 0 fraction).toDyadic? = some { negative := sign, significand := fraction, exponent := fmt.minSubnormalExponent }

An in-range nonzero fraction at biased exponent zero decodes as a subnormal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_ofFields_normal (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponentPos : exponent ≠ 0) (hexponent : exponent < fmt.expAllOnesNat) (hfraction : fraction < 2 ^ fmt.fracWidth) : (ofFields fmt sign exponent fraction).toDyadic? = some { negative := sign, significand := pow2 fmt.fracWidth + fraction, exponent := Int.ofNat exponent - Int.ofNat fmt.exponentBias - Int.ofNat fmt.fracWidth }

In-range nonexceptional fields with nonzero biased exponent decode as a normal value.

Closed-form real semantics

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofFields_subnormal (fmt : FloatFormat) (sign : Bool) (fraction : ℕ) (hfractionPos : fraction ≠ 0) (hfraction : fraction < 2 ^ fmt.fracWidth) : (ofFields fmt sign 0 fraction).toReal = (if sign = true then -1 else 1) * ↑fraction * Flocq.bpow Numerics.binaryRadix fmt.minSubnormalExponent

Closed-form real value of an explicitly packed subnormal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofFields_normal (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponentPos : exponent ≠ 0) (hexponent : exponent < fmt.expAllOnesNat) (hfraction : fraction < 2 ^ fmt.fracWidth) : (ofFields fmt sign exponent fraction).toReal = (if sign = true then -1 else 1) * ↑(pow2 fmt.fracWidth + fraction) * Flocq.bpow Numerics.binaryRadix (Int.ofNat exponent - Int.ofNat fmt.exponentBias - Int.ofNat fmt.fracWidth)

Closed-form real value of explicitly packed normal fields.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofFields_normal_of_isFinite (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponentPos : exponent ≠ 0) (hexponent : exponent < 2 ^ fmt.expWidth) (hfraction : fraction < 2 ^ fmt.fracWidth) (hfinite : (ofFields fmt sign exponent fraction).isFinite = true) : (ofFields fmt sign exponent fraction).toReal = (if sign = true then -1 else 1) * ↑(pow2 fmt.fracWidth + fraction) * Flocq.bpow Numerics.binaryRadix (Int.ofNat exponent - Int.ofNat fmt.exponentBias - Int.ofNat fmt.fracWidth)

Closed-form real value of finite normal fields, including all-ones exponent fields when the selected encoding treats them as finite.