Configured OCP MX identities

E8M0 is an exponent-only shared scale, not a scalar floating-point layout. An MX block jointly stores that scale with an array of binary element words. Both families use the common ExecFloat carrier while retaining their complete encodings.

References

• Open Compute Project, OCP Microscaling Formats (MX) Specification, Version 1.0: https://www.opencompute.org/documents/ocp-microscaling-formats-mx-v1-0-spec-final-pdf.
• ONNX, E8M0 technical specification: https://onnx.ai/onnx/technical/float8.html#e8m0.

inductive FloatLib.Floats.ExecFloat.OCP.MX.E8M0.Family : Type

Type-level identity of the OCP E8M0 exponent-only scale encoding.

• format : Family

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.OCP.MX.E8M0.instEncodedFormatFamily : Numerics.EncodedFormat Family

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.OCP.MX.E8M0.instFormatSemanticsFamily : Numerics.FormatSemantics Family

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.OCP.MX.E8M0 : Type

OCP E8M0 exponent-only shared scale on the common executable carrier.

inductive FloatLib.Floats.ExecFloat.OCP.MX.Block.Family (format : Formats.BinaryInterchange.FloatFormat) : Type

Type-level identity of an E8M0-scaled block with one binary element descriptor.

• format {format : Formats.BinaryInterchange.FloatFormat} : Family format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.OCP.MX.Block.instEncodedFormatFamily (format : Formats.BinaryInterchange.FloatFormat) : Numerics.EncodedFormat (Family format)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.OCP.MX.Block.instFormatSemanticsFamily (format : Formats.BinaryInterchange.FloatFormat) : Numerics.FormatSemantics (Family format)

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.OCP.MX.Block (format : Formats.BinaryInterchange.FloatFormat) : Type

Runtime-sized E8M0-scaled block with the selected binary element descriptor.