Posit format descriptors

A posit format has one sign bit and a tapered payload whose regime length depends on the encoded value. The Posit Standard (2022) fixes the maximum exponent field at two bits, so a standard format is selected only by its total width.

The descriptor is static in the Lean type. It therefore supports arbitrary widths without storing the width in every runtime value.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Sections 2--4, https://posithub.org/docs/posit_standard-2.pdf.
• John L. Gustafson, Standard Posit Arithmetic, Supercomputing Frontiers and Innovations 9(1), 2022, https://doi.org/10.14529/jsfi220102.

structure FloatLib.Floats.Formats.Posit.Format : Type

A validated, statically configured Posit Standard encoding.

• bits : ℕ

  Total encoded width, including the sign bit.

• bits_ge_two : 2 ≤ self.bits

  The Posit Standard requires at least two total bits.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.instReprFormat : Repr Format

def FloatLib.Floats.Formats.Posit.instReprFormat.repr : Format → ℕ → Std.Format

@[inline]

def FloatLib.Floats.Formats.Posit.Format.payloadBits (format : Format) : ℕ

Number of encoded bits below the sign bit.

@[inline]

def FloatLib.Floats.Formats.Posit.Format.signIndex (format : Format) : ℕ

Index of the sign bit in least-significant-bit numbering.

@[inline]

def FloatLib.Floats.Formats.Posit.Format.signMaskNat (format : Format) : ℕ

Natural-number bit mask containing only the sign bit.

@[inline]

def FloatLib.Floats.Formats.Posit.Format.oneCodeNat (format : Format) : ℕ

Unsigned encoding of the exact posit value one.

@[inline]

def FloatLib.Floats.Formats.Posit.Format.modulus (format : Format) : ℕ

Modulus of the exact-width unsigned encoding.

@[inline]

def FloatLib.Floats.Formats.Posit.Format.exponentBits (_format : Format) : ℕ

Maximum number of exponent bits available after the regime terminator.

@[inline]

def FloatLib.Floats.Formats.Posit.Format.regimeExponentStep (_format : Format) : ℕ

Binary exponent contributed by one unit of regime value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Format.regimeExponentStep_eq_two_pow_exponentBits (format : Format) : format.regimeExponentStep = 2 ^ format.exponentBits

One regime unit contributes 2 ^ exponentBits to the decoded binary exponent.

@[inline]

def FloatLib.Floats.Formats.Posit.Format.nextPrecision (format : Format) : Format

The same standardized posit family at one additional bit of precision.

Section 4.1 of the standard defines an n-bit rounding boundary using an (n + 1)-bit posit, so this descriptor transformation is part of the exact rounding definition rather than an implementation convenience.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Format.nextPrecision_payloadBits (format : Format) : format.nextPrecision.payloadBits = format.payloadBits + 1

Adding one encoded bit adds exactly one bit to the tapered payload.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Format.nextPrecision_signMaskNat (format : Format) : format.nextPrecision.signMaskNat = 2 * format.signMaskNat

Adding one encoded bit shifts the sign mask left by one place.

theorem FloatLib.Floats.Formats.Posit.Format.payloadBits_pos (format : Format) : 0 < format.payloadBits

Every valid posit has at least one payload bit.

theorem FloatLib.Floats.Formats.Posit.Format.signMaskNat_pos (format : Format) : 0 < format.signMaskNat

The unique sign-bit mask is nonzero.

theorem FloatLib.Floats.Formats.Posit.Format.one_lt_signMaskNat (format : Format) : 1 < format.signMaskNat

At least the codes zero and one lie below the sign-bit boundary.

theorem FloatLib.Floats.Formats.Posit.Format.oneCodeNat_pos (format : Format) : 0 < format.oneCodeNat

The exact-one encoding is nonzero.

theorem FloatLib.Floats.Formats.Posit.Format.oneCodeNat_lt_signMaskNat (format : Format) : format.oneCodeNat < format.signMaskNat

The exact-one encoding lies in the positive finite half of the word space.

theorem FloatLib.Floats.Formats.Posit.Format.signMaskNat_lt_modulus (format : Format) : format.signMaskNat < format.modulus

The sign bit is strictly below the exact-width modulus.

theorem FloatLib.Floats.Formats.Posit.Format.modulus_eq_two_mul_signMaskNat (format : Format) : format.modulus = 2 * format.signMaskNat

The complete unsigned modulus is twice the mask containing the sign bit.

def FloatLib.Floats.Formats.Posit.Format.ofBits (bits : ℕ) (bits_ge_two : 2 ≤ bits := by decide) : Format

Construct a Posit Standard descriptor from its total encoded width.