Native finite decoding for one-word formats

A flat UInt64 field decoder serves every conventional IEEE format covered by NativeSmallWord.StorageEligible. The executable operations have refinements in Finite.Proof.

@[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 retain the exact compact component representation 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.

The body names FiniteKernel.addComponentsImpl rather than the exact-dyadic addComponents. The two are proved equal in Kernel.Proof, but a runtime module cannot import that proof, so naming the compiled kernel here is what 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.

As for addFinite?, the body names FiniteKernel.fmaComponentsImpl, the compiled twin of the exact fmaComponents, because the equality between them is proved in a module this runtime cannot import.

@[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 proofs state the exact contract of the unchecked field kernel and are erased by compilation. The implementation keeps the one-word decoder and enters the same descriptor-generic square-root kernel used by the arbitrary-width path.