Lean floating-point model bridge

Model fmt retains the raw interchange bits, including noncanonical NaN payloads. Lean's Float.Model.UnpackedFloat interprets those bits using the conventional IEEE bias and exceptional encodings for their field widths. This module connects the two without selecting binary32 or any other fixed format. Custom descriptor biases and encoding policies require separate semantic agreement theorems.

The bridge is width preserving: FloatFormat.toModel has exactly fmt.bitWidth packed bits, so no padding, truncation, or host Float conversion occurs. Packing a model value canonicalizes NaNs, as Lean's model requires; unpacking arbitrary Model bits remains total.

References

• Init.Data.Float.Model, Lean 4's logical floating-point model.
• IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019. https://doi.org/10.1109/IEEESTD.2019.8766229

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.modelSign (negative : Bool) : Float.Model.UnpackedFloat.Sign

Translate the executable sign bit to Lean's logical floating-point sign.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.modelSignBit : Float.Model.UnpackedFloat.Sign → Bool

Translate Lean's logical floating-point sign back to an executable sign bit.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.modelSign_false : modelSign false = Float.Model.UnpackedFloat.Sign.positive

Translating a clear executable sign bit produces Lean's positive sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.modelSign_true : modelSign true = Float.Model.UnpackedFloat.Sign.negative

Translating a set executable sign bit produces Lean's negative sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.modelSignBit_negative : modelSignBit Float.Model.UnpackedFloat.Sign.negative = true

Lean's negative logical sign translates to a set executable sign bit.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.modelSignBit_positive : modelSignBit Float.Model.UnpackedFloat.Sign.positive = false

Lean's positive logical sign translates to a clear executable sign bit.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.modelSignBit_modelSign (negative : Bool) : modelSignBit (modelSign negative) = negative

Translating an executable sign bit to the logical model and back is the identity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.toModelBits {fmt : FloatFormat} (x : Model fmt) : BitVec fmt.toModel.numBits

View executable bits at the exactly equal width expected by Lean's model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ofModelBits {fmt : FloatFormat} (bits : BitVec fmt.toModel.numBits) : Model fmt

Wrap packed Lean-model bits as an executable value of the corresponding format.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModelBits_ofModelBits {fmt : FloatFormat} (bits : BitVec fmt.toModel.numBits) : (ofModelBits bits).toModelBits = bits

Wrapping Lean-model bits and viewing them again preserves every bit.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofModelBits_toModelBits {fmt : FloatFormat} (x : Model fmt) : ofModelBits x.toModelBits = x

Viewing an executable value as Lean-model bits and wrapping them again is the identity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.packComponents_unpackComponents (spec : Float.Model.Format) (bits : BitVec spec.numBits) : Float.Model.UnpackedFloat.packComponents spec (Float.Model.UnpackedFloat.Sign.ofBitVec (Float.Model.UnpackedFloat.unpackSign bits)) (Float.Model.UnpackedFloat.unpackExponent bits) (Float.Model.UnpackedFloat.unpackMantissa bits) = bits

Splitting and recombining Lean-model components preserves the packed bit vector.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModelBits_ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) : (ofFields fmt sign exponent fraction).toModelBits = Float.Model.UnpackedFloat.packComponents fmt.toModel (modelSign sign) (BitVec.ofNat fmt.expWidth exponent) (BitVec.ofNat fmt.fracWidth fraction)

Packing explicit fields agrees with Lean's sign/exponent/fraction concatenation. Inputs are reduced to their declared field widths by the corresponding BitVec.ofNat.

Agreement of packed fields

These lemmas are the representation boundary for the generic bridge. They show that the manual field extractors used by the executable kernel and the extractors used by Lean's logical model read the same raw bit vector. Arithmetic refinement proofs can therefore work with one decoded sign, exponent, and mantissa rather than repeat bit-layout arguments for each format.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpackSign_packComponents (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (exponent : BitVec spec.exponentBits) (mantissa : BitVec spec.mantissaBitsWithoutImplicit) : Float.Model.UnpackedFloat.unpackSign (Float.Model.UnpackedFloat.packComponents spec sign exponent mantissa) = sign.toBitVec

Packing and then extracting the one-bit sign field returns the original model sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpackMantissa_toNat {fmt : FloatFormat} (x : Model fmt) : (Float.Model.UnpackedFloat.unpackMantissa x.toModelBits).toNat = x.fracField

Lean's model and the executable decoder extract the same fraction field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_lt_pow2 {fmt : FloatFormat} (x : Model fmt) : x.fracField < 2 ^ fmt.fracWidth

The decoded fraction field fits in exactly the number of bits declared by its format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toNat_neg_one_exponentBits (fmt : FloatFormat) : (-1#fmt.toModel.exponentBits).toNat = fmt.expAllOnesNat

The all-ones exponent word of Lean's model is the executable all-ones exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpackExponent_toNat {fmt : FloatFormat} (x : Model fmt) : (Float.Model.UnpackedFloat.unpackExponent x.toModelBits).toNat = x.expField

Lean's model and the executable decoder extract the same biased exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_lt_pow2 {fmt : FloatFormat} (x : Model fmt) : x.expField < 2 ^ fmt.expWidth

The decoded biased exponent fits in exactly the number of bits declared by its format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_interior_bounds {fmt : FloatFormat} (x : Model fmt) (hnonzero : x.expField ≠ 0) (hnotAllOnes : x.expField ≠ fmt.expAllOnesNat) : 0 < x.expField ∧ x.expField < fmt.expAllOnesNat

An exponent field that is neither endpoint lies strictly inside the encoded range.

Native normal-number kernels use this fact after checking zero and the all-ones pattern. Keeping the arithmetic here avoids repeating width-specific proofs for binary64, binary128, and future fixed-width backends.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpackSign_eq_ofBool_msb {fmt : FloatFormat} (x : Model fmt) : Float.Model.UnpackedFloat.unpackSign x.toModelBits = BitVec.ofBool (BitVec.msb x.bits)

Lean's one-bit sign field is exactly the most significant executable bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.modelSignBit_ofBitVec_unpackSign {fmt : FloatFormat} (x : Model fmt) : modelSignBit (Float.Model.UnpackedFloat.Sign.ofBitVec (Float.Model.UnpackedFloat.unpackSign x.toModelBits)) = x.signBit

Lean's unpacked sign and the executable Boolean sign agree.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) : (ofFields fmt sign exponent fraction).fracField = fraction % 2 ^ fmt.fracWidth

Packing explicit fields retains the low fracWidth bits of the fraction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) : (ofFields fmt sign exponent fraction).expField = exponent % 2 ^ fmt.expWidth

Packing explicit fields retains the low expWidth bits of the biased exponent.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) : (ofFields fmt sign exponent fraction).signBit = sign

Packing explicit fields preserves the requested sign bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFields_signBit_expField_fracField {fmt : FloatFormat} (x : Model fmt) : ofFields fmt x.signBit x.expField x.fracField = x

Repacking the fields extracted from a Model reconstructs its exact bit pattern.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFields_false_zero_zero (fmt : FloatFormat) : ofFields fmt false 0 0 = posZero fmt

Packing three zero fields produces positive zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFields_true_zero_zero (fmt : FloatFormat) : ofFields fmt true 0 0 = negZero fmt

Packing only the sign bit produces the IEEE negative-zero bit pattern.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_ofFields_of_lt (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hfraction : fraction < 2 ^ fmt.fracWidth) : (ofFields fmt sign exponent fraction).fracField = fraction

An in-range fraction is recovered exactly after field packing.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_ofFields_of_lt (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) (hexponent : exponent < 2 ^ fmt.expWidth) : (ofFields fmt sign exponent fraction).expField = exponent

An in-range biased exponent is recovered exactly after field packing.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.toModel {fmt : FloatFormat} (x : Model fmt) : Float.Model.UnpackedFloat

Interpret an arbitrary bit pattern using Lean's width-parameterized IEEE model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ofModel (fmt : FloatFormat) (x : Float.Model.UnpackedFloat) : Model fmt

Encode a Lean logical value at fmt's field widths; NaNs use Lean's canonical payload.

def FloatLib.Floats.Formats.BinaryInterchange.Model.IsModelCanonical {fmt : FloatFormat} (x : Model fmt) : Prop

Whether the bits satisfy Lean's canonical-NaN invariant for packed model values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isModelCanonical_ofModel (fmt : FloatFormat) (x : Float.Model.UnpackedFloat) : (ofModel fmt x).IsModelCanonical

Every value produced by model packing satisfies the model's canonical-NaN invariant.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalizeModel {fmt : FloatFormat} (x : Model fmt) : Model fmt

Repacking through Lean's model canonicalizes bit patterns it interprets as IEEE NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isModelCanonical_canonicalizeModel {fmt : FloatFormat} (x : Model fmt) : x.canonicalizeModel.IsModelCanonical

Canonicalizing through Lean's model always establishes its packed-value invariant.