OCP FP8 E4M3FN

OCP E4M3FN has a nominal format identity and a direct UInt8 runtime carrier. For addition, subtraction, multiplication, division, and square root, balanced and throughput planning select exhaustive byte tables; latency planning selects the arithmetic kernels. Fused multiply-add uses the proved generic single-rounding kernel because an eight-bit ternary table would contain 16,777,216 entries.

The binary-interchange descriptor specifies the format and its kernels. It is not stored in FloatLib.Floats.ExecFloat E4M3FN.

Reference

• Open Compute Project, 8-bit Floating Point Specification, revision 1.0, E4M3, https://www.opencompute.org/documents/ocp-8-bit-floating-point-specification-ofp8-revision-1-0-2023-12-01-pdf-1.

inductive FloatLib.Floats.Formats.OCP.FP8.E4M3FN : Type

OCP E4M3 finite-number FP8 with direct byte storage.

theorem FloatLib.Floats.Formats.OCP.FP8.e4m3fn_width_le_eight : BinaryInterchange.FloatFormat.e4m3fn.bitWidth ≤ 8

The E4M3FN encoding fits in its direct byte carrier.

def FloatLib.Floats.Formats.OCP.FP8.e4m3fnAddTable : ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fn e4m3fn_width_le_eight) BinaryInterchange.Model.Spec.add

Certified direct-byte E4M3FN addition table.

def FloatLib.Floats.Formats.OCP.FP8.e4m3fnSubTable : ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fn e4m3fn_width_le_eight) BinaryInterchange.Model.Spec.sub

Certified direct-byte E4M3FN subtraction table.

def FloatLib.Floats.Formats.OCP.FP8.e4m3fnMulTable : ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fn e4m3fn_width_le_eight) BinaryInterchange.Model.Spec.mul

Certified direct-byte E4M3FN multiplication table.

def FloatLib.Floats.Formats.OCP.FP8.e4m3fnDivTable : ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fn e4m3fn_width_le_eight) BinaryInterchange.Model.Spec.div

Certified direct-byte E4M3FN division table.

def FloatLib.Floats.Formats.OCP.FP8.e4m3fnSqrtTable : ExecFloat.Backend.TinyTable.CertifiedUnary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fn e4m3fn_width_le_eight) BinaryInterchange.Model.Spec.sqrt

Certified direct-byte E4M3FN square-root table.

@[instance_reducible, always_inline]

instance FloatLib.Floats.Formats.OCP.FP8.instFamilyE4M3FN : BinaryInterchange.StaticByte.Family E4M3FN

Package the five dense byte tables with the proved arithmetic FMA baseline. The tables total roughly 257 KiB; retaining the single-rounding model kernel avoids a separate 16 MiB FMA table.

@[instance_reducible]

instance FloatLib.Floats.Formats.OCP.FP8.instFamilyInfoE4M3FN : BinaryInterchange.StaticByte.FamilyInfo E4M3FN

@[instance_reducible, always_inline]

instance FloatLib.Floats.Formats.OCP.FP8.instTablePlanE4M3FN : BinaryInterchange.StaticByte.Plans.TablePlan E4M3FN

@[instance_reducible, always_inline]

instance FloatLib.Floats.Formats.OCP.FP8.instFmaE4M3FN [planning : ExecFloat.Backend.PolicyFor E4M3FN] : ExecFloat.Fma E4M3FN

@[inline]

def FloatLib.Floats.Formats.OCP.FP8.E4M3FN.ofNatBits (bits : ℕ) : ExecFloat E4M3FN

Construct OCP E4M3FN from a natural bit pattern, reduced to eight bits.

@[inline]

def FloatLib.Floats.Formats.OCP.FP8.E4M3FN.toUInt8 (value : ExecFloat E4M3FN) : UInt8

Read the complete OCP E4M3FN encoding byte.