Executable word-specialized square-root dispatch

Executable square-root kernels and their format dispatcher live here. Correctness theorems are in SqrtWord.Proof, so runtime-only clients do not load the native refinement proofs.

Binary32 and binary64 use their native paths, other one-word IEEE formats use the shared word kernel, and every remaining format uses the general implementation. All of these implement one square-root specification.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.generic {fmt : FloatFormat} (x : Model fmt) : Model fmt

Width-generic compiled square root.

The outer cases handle NaN payloads, infinities, signed zeros and negative inputs. Positive finite nonzero values use the compact decoder and checked model square root. Their classification proof makes the finite decoder total, so this path needs no fallback.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.smallWord {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) : Model fmt

One-word square root with native finite-field decoding.

The outer cases match SqrtBackend.generic. Only the positive finite kernel changes: it becomes the one-word root of NativeSmallWordSqrt where the format allows it. Eligibility and classification evidence are erased, so compiled code keeps the native field kernel without an impossible fallback.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.word {fmt : FloatFormat} (x : Model fmt) : Model fmt

Word-specialized compiled implementation of sqrt.

Binary32 uses the checked UInt32/UInt64 backend. Binary64 uses the two-limb restoring kernel. Other eligible one-word IEEE formats use native storage decoding and, when the radicand fits one word, the one-word root. Remaining formats use SqrtBackend.generic. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.