Canonical representations in Lean's floating-point model

The bridge uses the conventional IEEE interpretation of the exponent and fraction widths. Packing an unpacked value need not preserve an arbitrary mantissa and exponent, but unpacking packed bits always gives a representable value. Repacking those values preserves every bit except the sign and payload of a noncanonical NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pack_unpack_eq (spec : Float.Model.Format) (bits : BitVec spec.numBits) : Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.unpack spec bits) = if Float.Model.UnpackedFloat.unpackExponent bits = -1#spec.exponentBits ∧ Float.Model.UnpackedFloat.unpackMantissa bits ≠ 0#spec.mantissaBitsWithoutImplicit then Float.Model.UnpackedFloat.packedNaN spec else bits

Repacking a bit pattern changes only NaN encodings. This statement is independent of any fixed exponent or fraction width.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pack_unpack_of_valid (spec : Float.Model.Format) (bits : BitVec spec.numBits) (hvalid : spec.Valid bits) : Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.unpack spec bits) = bits

A valid packed value is recovered exactly after unpacking and repacking.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_pack_notANumber (spec : Float.Model.Format) : Float.Model.UnpackedFloat.unpack spec (Float.Model.UnpackedFloat.pack spec Float.Model.UnpackedFloat.notANumber) = Float.Model.UnpackedFloat.notANumber

The canonical NaN payload unpacks to the model's single NaN value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_pack_unpack (spec : Float.Model.Format) (bits : BitVec spec.numBits) : Float.Model.UnpackedFloat.unpack spec (Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.unpack spec bits)) = Float.Model.UnpackedFloat.unpack spec bits

Unpacking forgets precisely the information discarded by NaN canonicalization.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalizeModel_eq_self_iff {fmt : FloatFormat} (value : Model fmt) : value.canonicalizeModel = value ↔ value.IsModelCanonical

Canonicalization fixes precisely the bit patterns admitted by Lean's packed model.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalizeModel_eq_self {fmt : FloatFormat} (value : Model fmt) (h : value.IsModelCanonical) : value.canonicalizeModel = value

Canonical packed words round-trip exactly through the unpacked model.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalizeModel_idempotent {fmt : FloatFormat} (value : Model fmt) : value.canonicalizeModel.canonicalizeModel = value.canonicalizeModel

A second canonicalization leaves the result unchanged.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalizeModel_ofModel (fmt : FloatFormat) (value : Float.Model.UnpackedFloat) : (ofModel fmt value).canonicalizeModel = ofModel fmt value

Values packed from the unpacked model are already canonical.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_canonicalizeModel {fmt : FloatFormat} (value : Model fmt) : value.canonicalizeModel.toModel = value.toModel

Canonicalization preserves the entire unpacked value, including the sign of zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_eq_iff_canonicalizeModel_eq {fmt : FloatFormat} (left right : Model fmt) : left.toModel = right.toModel ↔ left.canonicalizeModel = right.canonicalizeModel

Equality after unpacking is exactly equality of canonical packed representations. Operation refinement proofs may therefore use either form of the representation relation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.eq_of_toModel_eq {fmt : FloatFormat} {left right : Model fmt} (hleft : left.IsModelCanonical) (hright : right.IsModelCanonical) (h : left.toModel = right.toModel) : left = right

The unpacked interpretation is injective on canonical packed representations.