Correctness of native finite decoding for one-word formats

The executable decoder and arithmetic entry points live in Finite.Runtime. Their extracted sign, significand, and stored exponent agree with the format-generic decoder. Addition, fused multiply-add, and positive square root then reuse the corresponding component kernels.

Keeping the bridge here avoids coupling every operation to storage masks and field shifts. Runtime imports remain small, and later refinements reason about exact dyadics rather than raw words.

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 names the compiled addComponentsImpl; addComponentsImpl_eq identifies it with the exact addComponents used by 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 equals the generic compact finite kernel.

The runtime names the compiled fmaComponentsImpl; fmaComponentsImpl_eq identifies it with the exact fmaComponents used by FiniteKernel.fma?.

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.