Concrete OCP MX block representations

Profile lists the six concrete element encodings in Table 1 of the OCP Microscaling Formats (MX) Specification, version 1.0, September 2023. Block stores exactly 32 elements and an E8M0 scale. The existing arbitrary-length MX.BlockCode remains a separate raw interchange API.

INT8 uses two's complement with six fractional bits (§5.3.4). This profile uses the permitted asymmetric range, including code 0x80, which denotes -2. It does not reinterpret the bytes as sign-magnitude integers. Physical placement of the scale and element words is unspecified by the standard and by this structure.

Decoding follows §5.1: a NaN scale poisons every lane; otherwise element infinities and NaNs survive unchanged. For finite products beyond binary32's range, this implementation retains the exact rational product, one of the implementation choices left open by that section.

Reference: https://www.opencompute.org/documents/ocp-microscaling-formats-mx-v1-0-spec-final-pdf.

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

The six concrete element encodings specified by OCP MX 1.0, Table 1.

• e5m2 : Profile
• e4m3 : Profile
• e3m2 : Profile
• e2m3 : Profile
• e2m1 : Profile
• int8 : Profile

@[instance_reducible]

instance FloatLib.Floats.Formats.OCP.MX.Standard.instDecidableEqProfile : DecidableEq Profile

@[instance_reducible]

instance FloatLib.Floats.Formats.OCP.MX.Standard.instReprProfile : Repr Profile

def FloatLib.Floats.Formats.OCP.MX.Standard.instReprProfile.repr : Profile → ℕ → Std.Format

def FloatLib.Floats.Formats.OCP.MX.Standard.Profile.width : Profile → ℕ

Number of stored bits per element.

def FloatLib.Floats.Formats.OCP.MX.Standard.Profile.floatFormat? : Profile → Option BinaryInterchange.FloatFormat

Binary descriptor for floating elements; INT8 is a fixed-point two's-complement encoding.

def FloatLib.Floats.Formats.OCP.MX.Standard.Profile.maxPowerExponent : Profile → ℤ

Exponent of the largest positive power of two representable by an element (§6.3).

@[reducible, inline]

abbrev FloatLib.Floats.Formats.OCP.MX.Standard.Element (profile : Profile) : Type

A complete element word, whose width is enforced by its profile.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.decodeFloat {fmt : BinaryInterchange.FloatFormat} (word : BinaryInterchange.Model fmt) : Numerics.NumericalValue Numerics.SignedRat

Decode a binary floating element, retaining signed zero, infinity, and canonical NaN.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.decode {profile : Profile} (word : Element profile) : Numerics.NumericalValue Numerics.SignedRat

Exact scalar observation before applying the block scale.

def FloatLib.Floats.Formats.OCP.MX.Standard.Element.toRat? {profile : Profile} (word : Element profile) : Option ℚ

Finite rational interpretation, forgetting only the sign of zero.

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

The stored sign bit, including the sign of floating zero.

structure FloatLib.Floats.Formats.OCP.MX.Standard.Block (profile : Profile) : Type

OCP MX 1.0 concrete blocks have one scale and exactly 32 elements of one profile.

• scale : E8M0

  Shared eight-bit E8M0 scale; every byte, including NaN, is an admissible encoding.

• values : Vector (Element profile) 32

  Element count and storage width are part of the type.

def FloatLib.Floats.Formats.OCP.MX.Standard.instDecidableEqBlock.decEq {profile✝ : Profile} (x✝ x✝¹ : Block profile✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.OCP.MX.Standard.instDecidableEqBlock {profile✝ : Profile} : DecidableEq (Block profile✝)

def FloatLib.Floats.Formats.OCP.MX.Standard.instReprBlock.repr {profile✝ : Profile} : Block profile✝ → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.OCP.MX.Standard.instReprBlock {profile✝ : Profile} : Repr (Block profile✝)

def FloatLib.Floats.Formats.OCP.MX.Standard.scaleFinite (exponent : ℤ) (value : Numerics.SignedRat) : Numerics.SignedRat

Exact multiplication by a positive binary scale, preserving a finite zero's sign.

def FloatLib.Floats.Formats.OCP.MX.Standard.Block.ofArray? {profile : Profile} (scale : E8M0) (values : Array (Element profile)) : Option (Block profile)

Accept an array exactly when it has the standard lane count.

def FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeLane {profile : Profile} (block : Block profile) (lane : Fin 32) : Numerics.NumericalValue Numerics.SignedRat

Decode one lane according to the shared-scale and per-element rules of §5.1.

def FloatLib.Floats.Formats.OCP.MX.Standard.Block.decode {profile : Profile} (block : Block profile) : Vector (Numerics.NumericalValue Numerics.SignedRat) 32

Complete lane-wise observation; exceptional elements do not erase their finite neighbors.

def FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeFinite {profile : Profile} (block : Block profile) : Numerics.NumericalValue (Vector Numerics.SignedRat 32)

Whole-block finite observation for generic conversion. A block with any non-finite lane is reported as NaN here; decode retains each lane's individual classification and sign.

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

Canonical block NaN. Element bits are immaterial when the shared scale is NaN.