Field packing for directed dyadic rounding

Directed rounding first chooses a point on the representable dyadic grid and then packs that point into exponent and fraction fields. This module proves that the normal and subnormal packing formulas preserve the chosen exact value.

The field-width bounds prevent truncation during packing. Normal packing also requires a finiteness hypothesis, since some encoding policies reserve patterns within those widths for exceptional values.

Field-packing semantics

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofFields_normalized (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hlow : pow2 fmt.fracWidth ≤ mantissa) (hhigh : mantissa < pow2 (fmt.fracWidth + 1)) (hmin : fmt.minNormalExponent ≤ exponent) (hmax : exponent ≤ fmt.maxNormalExponent) (hfinite : (ofFields fmt false (exponent + Int.ofNat fmt.exponentBias).toNat (mantissa - pow2 fmt.fracWidth)).isFinite = true) : (ofFields fmt false (exponent + Int.ofNat fmt.exponentBias).toNat (mantissa - pow2 fmt.fracWidth)).toReal = ↑mantissa * bpow (exponent - Int.ofNat fmt.fracWidth)

Packing a normalized mantissa at an in-range exponent preserves its exact value when the packed word is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundSubnormalDown (fmt : FloatFormat) (mantissa : ℕ) (hhigh : mantissa < pow2 fmt.fracWidth) : (if mantissa = 0 then zero fmt false else ofFields fmt false 0 mantissa).toReal = ↑mantissa * bpow fmt.minSubnormalExponent

The downward zero-or-subnormal branch denotes its mantissa on the subnormal grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.encodedExponent_minNormal_eq_one (fmt : FloatFormat) : (fmt.minNormalExponent + Int.ofNat fmt.exponentBias).toNat = 1

The minimum normal exponent encodes as biased exponent field one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundSubnormalUp (fmt : FloatFormat) (mantissa : ℕ) (hzero : mantissa ≠ 0) (hhigh : mantissa ≤ pow2 fmt.fracWidth) : (if mantissa = 0 then posMinSubnormal fmt else if pow2 fmt.fracWidth ≤ mantissa then ofFields fmt false 1 0 else ofFields fmt false 0 mantissa).toReal = ↑mantissa * bpow fmt.minSubnormalExponent

The upward subnormal branch, including its smallest-normal boundary, preserves its grid value.