Model square root of a normalized positive value

The binary32, binary64, one-word, two-word, and wide-limb square-root kernels compute the same recipe: shift the significand so that its integer square root has exactly fracWidth + 1 bits, take the integer root, round it by comparing the remainder with the root, and pack the result with a possible carry into the exponent field. This module proves once, for every IEEE format, that the recipe agrees with Float.Model.UnpackedFloat.sqrt on the proof model.

Each kernel proves that its word arithmetic computes this recipe, that the scaled radicand and encoded exponent satisfy the stated bounds, and that its scaling constants satisfy htarget and hshift. Backends.SqrtArithmetic supplies the shared affine exponent identities.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofModel_sqrt_finite_positive_eq_ofFields (fmt : FloatFormat) (m shift q : ℕ) (inputExponent : ℤ) (hm : 0 < m) (hshiftLower : 2 * fmt.fracWidth ≤ m.log2 + shift) (hshiftUpper : m.log2 + 1 + shift ≤ 2 * fmt.fracWidth + 2) (hq : 1 ≤ q) (hqCarry : q + 1 ≤ 2 * fmt.bias) (htarget : min (inputExponent.ediv 2) (fmt.toModel.targetExponent ((Float.Model.totalExponent m inputExponent + 1).ediv 2)) = Int.ofNat q - Int.ofNat fmt.bias - ↑fmt.fracWidth) (hshift : (inputExponent - 2 * (Int.ofNat q - Int.ofNat fmt.bias - ↑fmt.fracWidth)).toNat = shift) : have root := (m <<< shift).sqrt; have remainder := m <<< shift - root * root; have rounded := if remainder ≤ root then root else root + 1; ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m inputExponent hm)) = ofFields fmt false (q + if rounded = pow2 (fmt.fracWidth + 1) then 1 else 0) ((if rounded = pow2 (fmt.fracWidth + 1) then pow2 fmt.fracWidth else rounded) - pow2 fmt.fracWidth)

The model square root of a positive finite m * 2 ^ inputExponent is the packed, rounded integer root.

The root's biased exponent before a rounding carry is q, and shift scales the significand so that the integer root of m <<< shift has exactly fracWidth + 1 bits. Rounding compares the remainder with the root, and a rounded root of 2 ^ (fracWidth + 1) carries into the exponent field.