Executable configured OCP MX operations

E8M0 exposes checked scale decoding and construction. MX blocks expose their joint storage and a checked decoder that rejects non-finite element words and, for nonempty blocks, NaN scales.

These wrappers allow any array length and binary element descriptor. A successful block decode returns the exact dyadic value of every element after applying the shared scale. An empty block decodes to an empty array without inspecting its scale.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.ofCode (code : Formats.OCP.MX.E8M0) : E8M0

Wrap a complete E8M0 code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.toCode (value : E8M0) : Formats.OCP.MX.E8M0

Recover the complete E8M0 code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.ofNatBits (bits : ℕ) : E8M0

Construct an E8M0 value from its complete byte pattern.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.toNatBits (value : E8M0) : ℕ

Read the complete E8M0 byte pattern.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.isNaN (value : E8M0) : Bool

Whether the value is the unique E8M0 NaN code.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.exponent? (value : E8M0) : Option ℤ

Decode the unbiased power-of-two exponent, or none for NaN.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.toDyadic? (value : E8M0) : Option Numerics.Dyadic

Decode the exact positive dyadic scale, or none for NaN.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.ofExponent? (exponent : ℤ) : Option E8M0

Construct an E8M0 scale when the requested exponent is representable.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.ofExponentSaturating (exponent : ℤ) : E8M0

Construct an E8M0 scale after explicitly clamping its exponent.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.E8M0.scaleDyadic? (scale : E8M0) (value : Numerics.Dyadic) : Option Numerics.Dyadic

Apply a finite E8M0 scale to an exact dyadic value.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.Block.ofCode {format : Formats.BinaryInterchange.FloatFormat} (code : Formats.OCP.MX.BlockCode format) : Block format

Wrap a complete MX block code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.Block.toCode {format : Formats.BinaryInterchange.FloatFormat} (value : Block format) : Formats.OCP.MX.BlockCode format

Recover the complete MX block code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.Block.ofComponents {format : Formats.BinaryInterchange.FloatFormat} (scale : E8M0) (values : Array (Formats.BinaryInterchange.Model format)) : Block format

Construct a joint block from one configured E8M0 scale and its element words.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.Block.ofElements {F : Type u} [Formats.BinaryInterchange.StaticByte.Family F] (scale : E8M0) (values : Array (ExecFloat F)) : Block (Formats.BinaryInterchange.StaticByte.Family.format F)

Construct a block from nominal static-byte elements.

The element family determines the block descriptor. Conversion to the proof model happens only at this storage boundary, so application code can keep using the ordinary executable low-bit type.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.Block.scale {format : Formats.BinaryInterchange.FloatFormat} (value : Block format) : E8M0

Configured E8M0 scale stored by the block.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.Block.values {format : Formats.BinaryInterchange.FloatFormat} (value : Block format) : Array (Formats.BinaryInterchange.Model format)

Binary-interchange element words stored by the block.

@[inline]

def FloatLib.Floats.ExecFloat.OCP.MX.Block.decode? {format : Formats.BinaryInterchange.FloatFormat} (value : Block format) : Option (Array Numerics.Dyadic)

Decode each scaled element; an empty block succeeds without inspecting the scale.