Correctness of two-word square root for normal inputs

The normal path aligns a fracWidth + 1-bit significand in a UInt256, computes a restoring integer square root with fracWidth + 1 base-four digits, and rounds from exact remainder information. sqrtNormal_refines identifies each accepted result with the public format-level square-root specification.

The kernel accepts only eligible layouts with fracWidth ≤ 124 and fracWidth + 1 ≤ bias. The first bound keeps the doubled remainder inside the two-word restoring state, and the second is the hypothesis under which SqrtArithmetic.target_exponent identifies the model's target exponent with the kernel's affine exponent formula. Exceptional, subnormal, and unsupported inputs are left to the operation dispatcher.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.sqrtNormal_refines {fmt : FloatFormat} (h : Eligible fmt) (x result : Model fmt) (hfast : sqrtNormal? x = some result) : result = Spec.sqrt x

Every accepted two-word square root agrees with Model.Spec.sqrt.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.sqrtNormal?_eq_map {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) : sqrtNormal? x = Option.map (ofWords fmt) (sqrtNormalWords? fmt (toWords x))

sqrtNormal? is the ofWords image of sqrtNormalWords? on the operand's storage words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.sqrtNormal?_of_words {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) (words : Numerics.FixedWord.UInt128) (hwords : sqrtNormalWords? fmt (toWords x) = some words) : sqrtNormal? x = some (ofWords fmt words)

An accepted storage-word root is the model-level two-word root.