P3109 formats

P3109 descriptors have four parameters from the interim report: bit width, precision, signedness, and finite or extended domain. Every valid descriptor produces an exact-width codebook and an ExecFloat carrier.

This module covers representation and exact decoding. The arithmetic and projection modules supply operations and rounding policies.

The finite magnitude formula agrees with ordinary binary scientific notation after fields have been extracted. Classification does not: P3109 unsigned formats omit the sign bit, while signed formats use the midpoint code for their single NaN and mirror finite magnitudes across the upper half of the code space. P3109 also admits field widths excluded by BinaryInterchange.FloatFormat, so it needs its own field classification.

Reference

• IEEE Working Group P3109, Interim Report on Arithmetic Formats for Machine Learning, version 4.0.3 (1 September 2026), Sections 3.1 and 4.7.2, repository revision 34f5964, https://github.com/P3109/Public/tree/34f5964d9bb2382b2665d15467fc3517b990b308. tests/oracles/format-standards.sh compares decoding with the published value tables.

inductive FloatLib.Floats.Formats.P3109.Signedness : Type

Whether a P3109 format represents negative finite values.

• signed : Signedness
• unsigned : Signedness

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instDecidableEqSignedness : DecidableEq Signedness

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instReprSignedness : Repr Signedness

def FloatLib.Floats.Formats.P3109.instReprSignedness.repr : Signedness → ℕ → Std.Format

inductive FloatLib.Floats.Formats.P3109.Domain : Type

Whether a P3109 format represents infinities as well as finite values and NaN.

• finite : Domain
• extended : Domain

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instDecidableEqDomain : DecidableEq Domain

def FloatLib.Floats.Formats.P3109.instReprDomain.repr : Domain → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instReprDomain : Repr Domain

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

A validated descriptor for the complete four-parameter P3109 format family.

One value of this structure selects a profile; there is no separate Lean type or decoder for each bit width. The proof fields rule out precisely the invalid (K, P, signedness) combinations from the report before any value can be constructed.

• bitWidth : ℕ

  Total number of encoded bits (K in the report).

• precision : ℕ

  Significand precision including the implicit leading bit (P in the report).

• signedness : Signedness

  Signed or unsigned datum set.

• domain : Domain

  Finite or extended datum set.

• bitWidth_gt_two : 2 < self.bitWidth

  P3109 requires more than two encoded bits.

• precision_pos : 0 < self.precision

  P3109 requires positive precision.

• precision_bound : match self.signedness with | Signedness.signed => self.precision < self.bitWidth | Signedness.unsigned => self.precision ≤ self.bitWidth

  Signed formats require P < K; unsigned formats allow P = K.

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

@[instance_reducible]

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

@[inline]

def FloatLib.Floats.Formats.P3109.Format.trailingBits (format : Format) : ℕ

Number of explicitly stored trailing significand bits.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.exponentBits (format : Format) : ℕ

Width of the biased exponent field.

Unsigned formats gain the bit that a signed format uses to divide positive and negative codes.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.exponentBias (format : Format) : ℕ

P3109 exponent bias, derived from the exponent-field width.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.minimumNormalExponent (format : Format) : ℤ

Smallest leading exponent used by a normal finite value.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.minimumQuantumExponent (format : Format) : ℤ

Quantum exponent of the smallest positive finite value.

@[inline]

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

Number of code points in the format.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.signBoundary (format : Format) : ℕ

First code in the negative half of a signed format.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.nanBits (format : Format) : ℕ

Code point assigned to the format's single NaN.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.positiveInfinityBits (format : Format) : ℕ

Code point assigned to positive infinity when the domain is extended.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.negativeInfinityBits (format : Format) : ℕ

Code point assigned to negative infinity in a signed extended format.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.signed (bitWidth precision : ℕ) (domain : Domain) (bitWidth_gt_two : 2 < bitWidth := by decide) (precision_pos : 0 < precision := by decide) (precision_lt_bitWidth : precision < bitWidth := by decide) : Format

Construct a signed P3109 descriptor.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.unsigned (bitWidth precision : ℕ) (domain : Domain) (bitWidth_gt_two : 2 < bitWidth := by decide) (precision_pos : 0 < precision := by decide) (precision_le_bitWidth : precision ≤ bitWidth := by decide) : Format

Construct an unsigned P3109 descriptor.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.ofParameters? (bitWidth precision : ℕ) (signedness : Signedness) (domain : Domain) : Option Format

Validate parameters supplied at runtime and construct the corresponding P3109 descriptor.

Use signed or unsigned when the parameters are fixed in Lean code and their constraints can be discharged at elaboration time. This checked constructor is for parsers, generated format matrices, and other callers whose parameters are ordinary runtime values.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite (format : Format) (bits : ℕ) : Numerics.Dyadic

Exact positive finite value decoded from one in-range magnitude.

Informally, row zero is subnormal and uses the stored trailing bits directly. Every other row prepends the implicit leading bit and subtracts the descriptor's exponent bias. Exceptional-code classification and negative mirroring happen in decodeNat, outside this shared mathematical formula.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.decodeNat (format : Format) (bits : ℕ) : Numerics.NumericalValue Numerics.Dyadic

Decode an in-range natural-number code point according to P3109 Section 4.7.2.

Callers with arbitrary natural numbers should first construct a BitVec format.bitWidth; the public decode and ExecFloat.P3109.ofNatBits functions do this automatically.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.decode (format : Format) (code : BitVec format.bitWidth) : Numerics.NumericalValue Numerics.Dyadic

Exact P3109 denotation of one width-bounded code point.

def FloatLib.Floats.Formats.P3109.Format.codebook (format : Format) : Codebook format.bitWidth Numerics.Dyadic

Complete codebook induced by a P3109 descriptor.

def FloatLib.Floats.Formats.P3109.Format.numericalSystem (format : Format) : Numerics.NumericalSystem

P3109 as a family-independent exact numerical system.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.P3109 (format : Formats.P3109.Format) : Type

Executable exact-width carrier for any valid P3109 descriptor.

Generic exact-expression operations can use this type as a destination through its conversion capability. The representation layer does not install a separate arithmetic interface.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.zero {format : Formats.P3109.Format} : P3109 format

Construct P3109's unique zero without exposing its stored word.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.nan {format : Formats.P3109.Format} : P3109 format

Construct P3109's sole NaN without exposing its descriptor-dependent code point.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.positiveInfinity {format : Formats.P3109.Format} (_extended : format.domain = Formats.P3109.Domain.extended := by decide) : P3109 format

Construct positive infinity when the descriptor has an extended domain.

Using this function with a statically finite-only descriptor fails during elaboration.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.negativeInfinity {format : Formats.P3109.Format} (_signed : format.signedness = Formats.P3109.Signedness.signed := by decide) (_extended : format.domain = Formats.P3109.Domain.extended := by decide) : P3109 format

Construct negative infinity when the descriptor is both signed and extended.

Using this function with an unsigned or finite-only descriptor fails during elaboration.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.ofFiniteFields? {format : Formats.P3109.Format} (negative : Bool) (biasedExponent trailing : ℕ) : Option (P3109 format)

Construct a finite P3109 value from named representation fields.

biasedExponent and trailing are checked against the descriptor widths. The constructor also rejects a negative request for an unsigned format and every field combination reserved for NaN or infinity. It is the structured alternative to ofNatBits when an application already has decoded P3109 fields; it does not perform numerical rounding.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.ofNatBits {format : Formats.P3109.Format} (bits : ℕ) : P3109 format

Construct a P3109 value from the low K bits of a serialized word.

Prefer the named semantic constructors or ofFiniteFields? in ordinary code.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.toNatBits {format : Formats.P3109.Format} (value : P3109 format) : ℕ

Read a P3109 value as its natural-number code point.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.decode {format : Formats.P3109.Format} (value : P3109 format) : Numerics.NumericalValue Numerics.Dyadic

Decode a P3109 value to its exact finite, infinity, or NaN semantics.