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, and 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, and they do not affect how stored non-finite element words decode.

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 the (overflow := ...) option, .saturate or .native, of Numerics.OverflowMode. The default is SAT, as recommended in §6.3. FP4, FP6, and INT8 always saturate. Their scalar NaN conversion maps to zero, while block conversion 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.

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 the element has one, and zero for the finite-only 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, and the E5M2 midpoint 61440 overflows.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.quantize (profile : Profile) (value : Numerics.NumericalValue Numerics.SignedRat) (overflow : Numerics.OverflowMode := Numerics.OverflowMode.saturate) : Element profile

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

overflow := .saturate (the default) is the SAT conversion mode of §5.3.1 and .native the OVF mode, which only FP8 elements distinguish: other profiles saturate under both.

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

Numerical element contract, with the 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. An all-zero block gets 2^0, an exponent below -127 clamps to -127, and one above 127 gives the NaN scale, so only finite E8M0 exponents reach rational scaling in the element kernel.

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

Quantize a finite vector at the given scale, or produce the canonical NaN block.

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

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

def FloatLib.Floats.Formats.OCP.MX.Standard.Quantizes (profile : Profile) (overflow : Numerics.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) (input : Vector (Numerics.NumericalValue Numerics.SignedRat) 32) (overflow : Numerics.OverflowMode := Numerics.OverflowMode.saturate) : 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.