Derived binary interchange format properties #
FloatFormat stores the choices that vary between binary interchange families:
exponent and fraction widths, bias, and exceptional-value encoding. This module derives the
capabilities, masks, and exponent bounds used everywhere else.
Keeping these formulas descriptor-driven is what makes FP8 variants, binary16/32/64/128, custom biases, and finite-only encodings instances of one development. Format-specific kernels may specialize the results, but they do not redefine the layout semantics.
Conventional IEEE exponent bias 2^(expWidth-1) - 1.
This layout-derived quantity can differ from fmt.exponentBias for a custom or FNUZ descriptor.
The FloatFormat invariant guarantees expWidth ≥ 2.
Instances For
The layout-derived conventional bias is positive for every binary descriptor.
The exponent field range in terms of the conventional bias: 2 ^ expWidth = 2 * bias + 2.
The conventional bias always fits in the exponent field that defines it.
Whether this format contains signed infinities.
Instances For
Whether this format reserves at least one NaN pattern.
Instances For
Whether zero has distinct positive and negative encodings.
Instances For
Whether the descriptor has the conventional IEEE bias and exceptional-value encoding.
Custom widths can satisfy this predicate as well as the named IEEE 754 layouts.
Instances For
Every descriptor constructed by ieee is recognized as conventionally IEEE encoded.
Characterization of descriptors represented exactly by Lean's IEEE logical model.
An IEEE descriptor uses the IEEE exceptional-value encoding.
An IEEE descriptor uses the conventional layout-derived exponent bias.
A conventional IEEE descriptor necessarily uses the infinity-bearing encoding policy.
Every IEEE descriptor represents positive and negative zero separately.
Smallest unbiased normal exponent under the format's declared bias.
Instances For
Dyadic exponent of the least positive subnormal under the format's declared bias.
Instances For
Dyadic scale constants #
Two families of exponent bounds coexist. The policy-aware family (minNormalExponent,
minSubnormalExponent, maxNormalExponent, normalMantissaExpOffset, subnormalAlignExp) is
derived from the declared fmt.exponentBias and fmt.encoding and is the one executable
semantics use. The ieee-prefixed family below is derived from the layout alone through the
conventional bias fmt.bias and matches Lean's logical IEEE model; it agrees with the
policy-aware family when fmt.isIEEE, as the *_eq_ieee theorems state. Custom biases and
finite-only encodings can change these bounds.
Dyadic exponent of the least positive subnormal in the conventional IEEE reading of the layout
(binary32: -149). For policy-aware semantics use minSubnormalExponent, which is based on
fmt.exponentBias rather than the layout-derived fmt.bias.
Instances For
Offset from the biased exponent field to the dyadic exponent of an integer normal significand:
a normal word with biased exponent e and fraction f denotes
(2^fracWidth + f) * 2^(e - normalMantissaExpOffset) (binary32: 150).
Instances For
Largest unbiased normal exponent in the conventional IEEE reading of the layout
(binary32: 127). For policy-aware semantics use maxNormalExponent; the two differ for
finite-only encodings, whose all-ones exponent field is finite, and for custom biases.
Instances For
Smallest unbiased normal exponent in the conventional IEEE reading of the layout
(binary32: -126). For policy-aware semantics use minNormalExponent.
Instances For
For an IEEE descriptor, the policy-aware lower normal exponent is the conventional bound.
For an IEEE descriptor, the policy-aware subnormal quantum is the conventional bound.
Shift that aligns a subnormal fraction field with its dyadic exponent under the declared bias
(binary32: 149).
Instances For
Layout-derived counterpart of normalMantissaExpOffset, using the conventional bias fmt.bias.
Instances For
Layout-derived counterpart of subnormalAlignExp, using the conventional bias fmt.bias.
Instances For
Layout formulas #
The sign occupies the top bit, followed by the exponent and then the low fraction field.
Sign bit index (binary32: 31).
Instances For
All-ones exponent field alone (binary32: 255).
Instances For
The all-ones exponent field is twice the conventional layout-derived bias plus one.
Every supported descriptor has exponent fields zero, one, and the all-ones pattern.
A valid exponent field has a nonzero all-ones pattern.
Fraction mask in low bits (binary32: 2^23 - 1).
Instances For
A valid fraction field has a nonzero low-bit mask.
Largest encoded exponent that belongs to a finite value.
Instances For
Largest fraction at maxFiniteExpField that remains finite.
Instances For
The largest finite exponent field is nonzero.
The largest finite exponent field fits in the stored exponent width.
The largest finite fraction field fits in the stored fraction width.
Largest unbiased exponent occurring among finite normal values.
Instances For
For an IEEE descriptor, the policy-aware upper exponent is the conventional IEEE bound.
Exponent mask shifted into place (binary32: 0x7F800000).
Instances For
Sign-bit mask (binary32: 2^31).
Instances For
Quiet-NaN bit (binary32: 2^22).