Native finite decoding for one-word formats

A flat UInt64 field decoder serves every conventional IEEE format covered by NativeSmallWord.StorageEligible. Finite.Proof has their refinements.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.finiteMantissa (fmt : FloatFormat) (exponent fraction : UInt64) : UInt64

Decode the finite significand, including the implicit bit for normal values.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.decode? {fmt : FloatFormat} (x : Model fmt) : Option FiniteKernel.Components

Decode a finite value through native storage fields.

An all-ones exponent returns none. Zeros, subnormals and normals decode to the compact components used by FiniteKernel.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.addFinite? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Native-storage finite addition through the compiled unsigned-scale component kernel.

Its body calls FiniteKernel.Internal.addComponents, which Kernel.Proof proves equal to the exact-dyadic addComponents. A runtime module cannot import that proof, so calling the compiled kernel by name keeps the exact-dyadic body out of generated code.

@[inline]

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

Native-storage finite FMA through the compiled unsigned-scale component kernel.

If either multiplicand is zero and the addend is nonzero, the addend is already the exact result. Returning its stored word avoids normalization and rounding. Zero addends keep the kernel's signed-zero rule.

As in addFinite?, the body calls the compiled twin FiniteKernel.Internal.fmaComponents.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.sqrtPositive? {fmt : FloatFormat} (x : Model fmt) : Option (Model fmt)

Native-storage positive square root using the shared compact finite kernel.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.sqrtPositive {fmt : FloatFormat} (_heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) (_hfinite : x.isFinite = true) (_hnonzero : x.isZero = false) (_hpositive : x.signBit = false) : Model fmt

Native-storage square root for an input already proved positive, finite, and nonzero.

The proof arguments state the contract of the unchecked field kernel and are erased by compilation. Its body uses the one-word decoder and the descriptor-generic square-root kernel of the arbitrary-width path.