Packing finite values in Lean's float model

Lean's Float.Model.UnpackedFloat.pack assumes that finite inputs have already been normalized for the selected format. This module proves exact round trips for representable normal and subnormal values in Lean's width-parameterized IEEE model. Agreement with the descriptor's real decoder requires fmt.isIEEE = true.

Numerical rounding is handled separately by the rounding semantics.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.noOverflow_of_isFinite_ofModel_finite (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (hm : mantissa ≠ 0) (hfin : (ofModel fmt (Float.Model.UnpackedFloat.finite sign mantissa exponent ⋯)).isFinite = true) : (exponent + ↑fmt.toModel.exponentBias + ↑fmt.toModel.mantissaBitsWithoutImplicit).toNat + 1 < 2 ^ fmt.toModel.exponentBits

If packing a finite logical value produces a finite executable value, the biased exponent did not reach the all-ones encoding. This observable side condition keeps overflow handling out of arithmetic refinement proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_pack_finite_normal (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (hm : mantissa ≠ 0) (hbits : mantissa.log2 + 1 = spec.mantissaBits) (hbiasedNonneg : 0 ≤ exponent + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit) (hbiasedPos : 0 < exponent + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit) (hnoOverflow : (exponent + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit).toNat + 1 < 2 ^ spec.exponentBits) : Float.Model.UnpackedFloat.unpack spec (Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.finite sign mantissa exponent ⋯)) = Float.Model.UnpackedFloat.finite sign mantissa exponent ⋯

Packing and unpacking a representable normal value preserves the unpacked value exactly.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_finite_normal (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (hm : mantissa ≠ 0) (hbits : mantissa.log2 + 1 = fmt.toModel.mantissaBits) (hbiasedNonneg : 0 ≤ exponent + ↑fmt.toModel.exponentBias + ↑fmt.toModel.mantissaBitsWithoutImplicit) (hbiasedPos : 0 < exponent + ↑fmt.toModel.exponentBias + ↑fmt.toModel.mantissaBitsWithoutImplicit) (hnoOverflow : (exponent + ↑fmt.toModel.exponentBias + ↑fmt.toModel.mantissaBitsWithoutImplicit).toNat + 1 < 2 ^ fmt.toModel.exponentBits) : (ofModel fmt (Float.Model.UnpackedFloat.finite sign mantissa exponent ⋯)).toReal = (if modelSignBit sign = true then -1 else 1) * ↑mantissa * Flocq.bpow Numerics.binaryRadix exponent

Packing a representable normal model value preserves its exact real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_pack_finite_subnormal (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (hm : mantissa ≠ 0) (hfit : mantissa < 2 ^ fmt.fracWidth) : Float.Model.UnpackedFloat.unpack fmt.toModel (Float.Model.UnpackedFloat.pack fmt.toModel (Float.Model.UnpackedFloat.finite sign mantissa fmt.ieeeMinSubnormalExponent ⋯)) = Float.Model.UnpackedFloat.finite sign mantissa fmt.ieeeMinSubnormalExponent ⋯

Packing and unpacking a nonzero subnormal preserves its sign, mantissa, and exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_pack_finite_at_minSubnormal (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (hm : mantissa ≠ 0) (hfit : mantissa ≤ 2 ^ fmt.fracWidth) : Float.Model.UnpackedFloat.unpack fmt.toModel (Float.Model.UnpackedFloat.pack fmt.toModel (Float.Model.UnpackedFloat.finite sign mantissa fmt.ieeeMinSubnormalExponent ⋯)) = Float.Model.UnpackedFloat.finite sign mantissa fmt.ieeeMinSubnormalExponent ⋯

Packing and unpacking any nonzero value on the minimum-exponent grid is exact up to and including the smallest normal value. The endpoint 2^p changes encoding class, but not its unpacked logical value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_finite_subnormal (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (hm : mantissa ≠ 0) (hfit : mantissa < 2 ^ fmt.fracWidth) : (ofModel fmt (Float.Model.UnpackedFloat.finite sign mantissa fmt.ieeeMinSubnormalExponent ⋯)).toReal = (if modelSignBit sign = true then -1 else 1) * ↑mantissa * Flocq.bpow Numerics.binaryRadix fmt.ieeeMinSubnormalExponent

Packing a representable nonzero subnormal preserves its exact real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_finite_at_minSubnormal (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (hm : mantissa ≠ 0) (hfit : mantissa ≤ 2 ^ fmt.fracWidth) : (ofModel fmt (Float.Model.UnpackedFloat.finite sign mantissa fmt.ieeeMinSubnormalExponent ⋯)).toReal = (if modelSignBit sign = true then -1 else 1) * ↑mantissa * Flocq.bpow Numerics.binaryRadix fmt.ieeeMinSubnormalExponent

Every nonzero value on the minimum-exponent grid up to the smallest normal value keeps its exact real value when packed.