Exact destination quantization for concrete OCP MX blocks

The default conversion implements the recommended algorithm of OCP MX 1.0 §6.3: select the largest input binade, subtract the element's largest power-of-two exponent, and quantize each scaled input with nearest-even rounding and saturation. The all-zero block uses scale 2^0. An exponent below -127 is clamped to -127; one above 127 produces a NaN block. Non-finite input lanes also produce a NaN block. These choices resolve cases for which §6.3 does not prescribe a scale. They are distinct from decoding existing non-finite element words.

Nearest rounding is relative to the selected scale, not to all possible block encodings. For example, a constant E4M3 block with value 15/8 selects scale 2^-8 and saturates to 7/4, even though the input is representable using another scale.

Element rounding searches at most 256 words with exact rational comparisons. This bounded reference kernel covers floating and two's-complement elements through the same numerical contract. Its cost depends on the size of the exact input rationals, not on an unbounded shift derived from an exponent field. Signed floating zeros are retained.

FP8's required SAT and OVF element-conversion modes (§5.3.1, Table 3) are explicit. The block default is SAT as recommended in §6.3. FP4, FP6, and INT8 always saturate. Their scalar NaN conversion maps to zero; block conversion instead records a NaN scale.

Reference: OCP, Microscaling Formats (MX) Specification, version 1.0, September 2023, §§5.3 and 6.3, https://www.opencompute.org/documents/ocp-microscaling-formats-mx-v1-0-spec-final-pdf.

inductive FloatLib.Floats.Formats.OCP.MX.Standard.OverflowMode : Type

FP8 element overflow choice. Other concrete element encodings use finite saturation.

• saturate : OverflowMode
• overflow : OverflowMode

@[instance_reducible]

instance FloatLib.Floats.Formats.OCP.MX.Standard.instDecidableEqOverflowMode : DecidableEq OverflowMode

def FloatLib.Floats.Formats.OCP.MX.Standard.instReprOverflowMode.repr : OverflowMode → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.OCP.MX.Standard.instReprOverflowMode : Repr OverflowMode

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.candidates (profile : Profile) : List (Element profile × ℚ)

All finite element words paired with their exact rational values.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.roundingKey {profile : Profile} (input : Numerics.SignedRat) (candidate : Element profile × ℚ) : Lex (ℚ × ℕ)

Nearest-even ordering key: distance first, then even least-significant bit, then zero sign. The last component only resolves duplicate numerical encodings such as the two floating zeros.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.Quantizes {profile : Profile} (input : Numerics.SignedRat) (word : Element profile) : Prop

Finite nearest-even conversion minimizes absolute error; ties favor an even low bit and then the input's zero sign. This relation is independent of how candidates are enumerated.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.quantizeFinite (profile : Profile) (input : Numerics.SignedRat) : Element profile

Saturating nearest-even element rounding, using only exact rational comparisons.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.endpoint (profile : Profile) (negative : Bool) : Element profile

Signed finite endpoint, including the permitted -2 endpoint of this INT8 profile.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.nan (profile : Profile) : Element profile

Canonical scalar NaN when supported; zero for the finite-only scalar encodings.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.overflow (profile : Profile) (negative : Bool) : Element profile

Scalar FP8 OVF result, or the finite endpoint for a finite-only element encoding.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.roundsOut (profile : Profile) (input : ℚ) : Bool

FP8 overflow after nearest-even rounding. The E4M3 midpoint 464 rounds to the even finite 448; the E5M2 midpoint 61440 rounds to overflow.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.quantize (profile : Profile) (mode : OverflowMode) : Numerics.NumericalValue Numerics.SignedRat → Element profile

Convert a scalar observation to an element, before applying any shared block scale.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.QuantizesWith {profile : Profile} (mode : OverflowMode) (input : Numerics.SignedRat) (word : Element profile) : Prop

Numerical element contract with an explicit FP8 after-rounding overflow alternative.

def FloatLib.Floats.Formats.OCP.MX.Standard.maxMagnitude (input : Vector Numerics.SignedRat 32) : ℚ

Largest absolute finite input, computed before any element rounding.

def FloatLib.Floats.Formats.OCP.MX.Standard.requestedExponent (profile : Profile) (input : Vector Numerics.SignedRat 32) : ℤ

Recommended shared exponent before handling the finite E8M0 range.

def FloatLib.Floats.Formats.OCP.MX.Standard.selectScale (profile : Profile) (input : Vector Numerics.SignedRat 32) : E8M0

Recommended max-binade scale, with explicit zero, underflow, and overflow policies. Only finite E8M0 exponents reach rational scaling in the element kernel.

def FloatLib.Floats.Formats.OCP.MX.Standard.quantizeAt (profile : Profile) (mode : OverflowMode) (scale : E8M0) (input : Vector Numerics.SignedRat 32) : Block profile

Quantize an already finite vector at an explicit scale, or produce a canonical NaN block.

def FloatLib.Floats.Formats.OCP.MX.Standard.quantizeFinite (profile : Profile) (mode : OverflowMode) (input : Vector Numerics.SignedRat 32) : Block profile

Recommended scale selection followed by one rounding of each exact scaled lane.

def FloatLib.Floats.Formats.OCP.MX.Standard.Quantizes (profile : Profile) (mode : OverflowMode) (input : Vector Numerics.SignedRat 32) (block : Block profile) : Prop

Destination contract: use the chosen shared scale and round each normalized lane according to the numerical element contract, or propagate an unrepresentable scale as NaN.

def FloatLib.Floats.Formats.OCP.MX.Standard.quantize (profile : Profile) (mode : OverflowMode) (input : Vector (Numerics.NumericalValue Numerics.SignedRat) 32) : Block profile

Convert a vector of scalar observations. Any non-finite lane produces a NaN shared scale. Finite neighbors are preserved when decoding a stored block, but not during this scale selection.