Binary interchange format definitions

FloatFormat completely describes a binary storage format: its sign/exponent/fraction layout, exponent bias, and exceptional-value encoding. There is no global precision ceiling. IEEE, finite-only, and FNUZ formats are values of the same structure, and so is a custom format, which pairs one of the four exceptional-value encodings with a validated exponent bias.

Lean's generic Float.Model.Format represents the IEEE interpretation of a layout. The toModel conversion below therefore exposes that logical view only for the layout fields; the policy-aware executable semantics use exponentBias and encoding directly.

References:

• IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, https://doi.org/10.1109/IEEESTD.2019.8766229.

inductive FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding : Type

Assignment of exceptional values within a sign/exponent/fraction binary format.

• ieee : Encoding

  All-ones exponent: zero fraction is infinity, nonzero fraction is NaN.

• finiteMaxNaN : Encoding

  No infinity; the all-ones exponent and all-ones fraction pattern is NaN.

• finiteUnsignedZero : Encoding

  No infinity or negative zero; the negative-zero bit pattern is the sole NaN.

• finite : Encoding

  Every nonzero bit pattern is finite; both signs of zero remain representable.

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.instReprEncoding.repr : Encoding → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.instReprEncoding : Repr Encoding

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.beq : Encoding → Encoding → Bool

Executable equality of encodings by case split.

The explicit inlined test lets the compiler reduce comparisons of known constructors. The DecidableEq instance uses this test so descriptor eligibility checks can specialize with it.

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.beq_eq_true_iff (left right : Encoding) : left.beq right = true ↔ left = right

Encoding.beq decides propositional equality of encodings.

@[instance_reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.instDecidableEqEncoding : DecidableEq Encoding

Equality of encodings is decidable; the instance is inlined so literal comparisons fold.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.maxFiniteExponent (encoding : Encoding) (expWidth : Nat) : Nat

Largest encoded exponent that is finite at fraction zero.

structure FloatLib.Floats.Formats.BinaryInterchange.FloatFormat : Type

Complete binary storage, exponent-bias, and exceptional-value format descriptor.

• expWidth : Nat

  Width of the biased exponent field.

• expWidth_ge_two : 2 ≤ self.expWidth

  At least two exponent bits are needed to separate zero/subnormal encodings, finite normal exponents, and the all-ones infinity/NaN class.

• fracWidth : Nat

  Width of the fraction (significand without the implicit integer bit).

• fracWidth_pos : 0 < self.fracWidth

  An interchange format has at least one explicit fraction bit.

• exponentBias : Nat

  Bias subtracted from every nonzero encoded exponent.

• encoding : Encoding

  Interpretation of infinity, NaN, and zero bit patterns.

• exponentBias_pos : 0 < self.exponentBias

  A positive bias makes exponentBias the normal encoding of one.

• exponentBias_le_maxFinite : self.exponentBias ≤ self.encoding.maxFiniteExponent self.expWidth

  The normal encoding of one is finite and fits in the exponent field.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instDecidableEqFloatFormat : DecidableEq FloatFormat

def FloatLib.Floats.Formats.BinaryInterchange.instDecidableEqFloatFormat.decEq (x✝ x✝¹ : FloatFormat) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instReprFloatFormat : Repr FloatFormat

def FloatLib.Floats.Formats.BinaryInterchange.instReprFloatFormat.repr : FloatFormat → Nat → Std.Format

Format construction

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeBias (expWidth : Nat) : Nat

The conventional IEEE exponent bias determined by the exponent width.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.defaultBias (encoding : Encoding) (expWidth : Nat) : Nat

Default exponent bias for a configured encoding.

IEEE, finite-max-NaN, and signed-zero finite formats use the conventional IEEE bias. The finite-unsigned-zero encoding shifts the bias by one, matching its reuse of negative zero as NaN. Callers can still supply any other validated bias through FloatFormat.custom.

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeBias_pos (expWidth : Nat) (h : 2 ≤ expWidth) : 0 < ieeeBias expWidth

The conventional IEEE bias is positive when the exponent field has at least two bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeBias_le_maxFiniteExponent (expWidth : Nat) (h : 2 ≤ expWidth) : ieeeBias expWidth ≤ Encoding.ieee.maxFiniteExponent expWidth

The conventional IEEE bias fits below the largest finite IEEE exponent encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeBias_le_finiteMaxExponent (expWidth : Nat) (h : 2 ≤ expWidth) : ieeeBias expWidth ≤ Encoding.finite.maxFiniteExponent expWidth

The conventional IEEE bias fits below the largest finite-only exponent encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.finiteUnsignedBias_le_maxFiniteExponent (expWidth : Nat) (h : 2 ≤ expWidth) : ieeeBias expWidth + 1 ≤ Encoding.finiteUnsignedZero.maxFiniteExponent expWidth

The shifted FNUZ bias fits below the largest finite exponent encoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.custom (expWidth fracWidth exponentBias : Nat) (encoding : Encoding) (expWidth_ge_two : 2 ≤ expWidth := by decide) (fracWidth_pos : 0 < fracWidth := by decide) (exponentBias_pos : 0 < exponentBias := by decide) (exponentBias_le_maxFinite : exponentBias ≤ encoding.maxFiniteExponent expWidth := by decide) : FloatFormat

Construct a validated custom binary format.

For literal widths and biases, Lean discharges the four side conditions with by decide.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieee (expWidth fracWidth : Nat) (expWidth_ge_two : 2 ≤ expWidth := by decide) (fracWidth_pos : 0 < fracWidth := by decide) : FloatFormat

Give an arbitrary layout its ordinary IEEE bias and exceptional-value interpretation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.finiteMaxNaN (expWidth fracWidth : Nat) (expWidth_ge_two : 2 ≤ expWidth := by decide) (fracWidth_pos : 0 < fracWidth := by decide) : FloatFormat

OCP E4M3-style format with no infinity and one maximum-magnitude NaN per sign.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.finiteUnsignedZero (expWidth fracWidth : Nat) (expWidth_ge_two : 2 ≤ expWidth := by decide) (fracWidth_pos : 0 < fracWidth := by decide) : FloatFormat

FNUZ format with bias one above the IEEE bias and negative zero reused as NaN.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.finite (expWidth fracWidth : Nat) (expWidth_ge_two : 2 ≤ expWidth := by decide) (fracWidth_pos : 0 < fracWidth := by decide) : FloatFormat

Finite-only binary format in which no bit pattern denotes infinity or NaN.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.bitWidth (fmt : FloatFormat) : Nat

Total storage width: sign + exponent + fraction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.toModel (fmt : FloatFormat) : Float.Model.Format

The corresponding format used by Lean's logical floating-point model.

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.exponentBias_lt_two_pow (fmt : FloatFormat) : fmt.exponentBias < 2 ^ fmt.expWidth

The declared exponent bias fits in the stored exponent field.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ofModel (fmt : Float.Model.Format) (h : 2 ≤ fmt.exponentBits) : FloatFormat

Recover an executable IEEE format descriptor from Lean's logical format descriptor.

Both descriptors require at least two exponent bits; fmt.he supplies the explicit width proof. The conversion assigns the conventional IEEE bias and exceptional-value interpretation.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.toModel_ofModel (fmt : Float.Model.Format) (h : 2 ≤ fmt.exponentBits) : (ofModel fmt h).toModel = fmt

Converting a Lean logical format to an executable descriptor and back is exact.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ofModel_toModel (fmt : FloatFormat) : ofModel fmt.toModel ⋯ = ieee fmt.expWidth fmt.fracWidth ⋯ ⋯

Converting through Lean's logical model retains the widths and produces the corresponding conventional IEEE descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.toModel_numBits (fmt : FloatFormat) : fmt.toModel.numBits = fmt.bitWidth

Lean's logical model and the executable descriptor assign the same total storage width.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ExecWord (fmt : FloatFormat) : Type

Raw storage has precisely the width prescribed by the format.