Correctness of native finite decoding for one-word formats

The decoder of Finite.Runtime extracts the same sign, significand and stored exponent as the format-generic decoder. Addition, fused multiply-add and positive square root then reuse the corresponding component kernels.

With this bridge in one place, no operation proof deals with storage masks and field shifts. Runtime imports stay small, and the later refinements reason about exact dyadics.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.decode_eq {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) : decode? x = FiniteKernel.decode? x

Native one-word decoding equals the width-generic compact decoder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.addFinite_eq {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x y : Model fmt) : addFinite? x y = FiniteKernel.add? x y

Native-storage finite addition equals the generic compact finite kernel.

The runtime calls the compiled Internal.addComponents, and Internal.addComponents_eq identifies it with the exact addComponents behind FiniteKernel.add?.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.fmaFinite_eq {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x y z : Model fmt) : fmaFinite? x y z = FiniteKernel.fma? x y z

Native-storage finite FMA, including the exact zero-product exit, equals the generic kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.sqrtPositive_eq {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) : sqrtPositive? x = FiniteSqrt.sqrtPositive? x

Native-storage positive square root equals the generic compact finite kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFinite.sqrtPositive_eq_runtime {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) (hfinite : x.isFinite = true) (hnonzero : x.isZero = false) (hpositive : x.signBit = false) : sqrtPositive heligible x hfinite hnonzero hpositive = FiniteSqrt.sqrtPositiveRuntime x hfinite hnonzero hpositive

The unchecked one-word positive square-root kernel agrees with the proof-guided generic kernel.