Native one-word finite fused multiply-add

The native FMA path serves conventional IEEE formats with at most 29 fraction bits (Eligible), which include binary16, bfloat16, and the eight-bit formats. It is the word-tier counterpart of the IEEE branch of FiniteKernel.Internal.fmaComponents. The exact product of the two significands and the addend significand are placed at unsigned scales in the product rounder's coordinate and passed to the same signed-magnitude helpers as one-word addition, with scale offset 0. With at most 2 * fracWidth + 2 ≤ 60 bits in the product, every aligned sum and every sticky magnitude fits in UInt64. Refinement proofs are in Fma.Proof.

It returns none for exceptional operands, a zero product, a wide alignment that the sticky path declines, results below the normal threshold before rounding, and overflow after rounding. The dispatcher then tries the native-storage component kernel, which returns the addend of a zero product as it is.

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.Eligible (fmt : FloatFormat) : Prop

Capacity contract of the one-word FMA kernel.

A significand has at most fracWidth + 1 bits, so the exact product of two significands is below 2 ^ 60, and the exponent bound keeps every product-coordinate scale below 2 ^ 33.

@[instance_reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.instDecidableEligible (fmt : FloatFormat) : Decidable (Eligible fmt)

FMA eligibility is decided from the descriptor fields. As for NativeSmallWord.StorageEligible, the conditional form is inlined and simplifies for a closed format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.productShiftLimit (fmt : FloatFormat) : UInt64

Largest shift of the exact product above the addend that stays exact: the product has at most 2 * fracWidth + 2 bits, so shifting it left by 61 - 2 * fracWidth keeps it below 2 ^ 63.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.fmaFields? (fmt : FloatFormat) (productSign : Bool) (product productScale : UInt64) (addendSign : Bool) (addend addendScale : UInt64) : Option (Model fmt)

Round product * 2 ^ productScale + addend * 2 ^ addendScale once, in product coordinates.

The signs belong to the product and the addend. A zero addend rounds the product alone. Otherwise the operand at the larger scale is shifted left onto the smaller one when the shift is exact (shiftLimit for the addend, productShiftLimit for the product), and larger gaps go through the sticky alignment of roundJammed?. A zero product returns none.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.fmaFinite? {fmt : FloatFormat} (x y z : Model fmt) : Option (Model fmt)

One-word finite fused multiply-add on the operands' storage words.

The three operands are decoded with the shared one-word field extractors, and an exceptional operand returns none. The product scale is the sum of the compact finite scales of x and y, and alignOffset fmt moves the addend's compact scale into product coordinates. Fma.Proof proves every accepted result equal to FiniteKernel.fma? x y z.