Model square root of a normalized positive value

The binary32, binary64 and binary128 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)

Rounding a normalized square-root core result back to packed fields.

The input is the positive finite value m * 2 ^ inputExponent. The root exponent is q - bias, and shift scales the significand so that the integer root of m <<< shift has exactly fracWidth + 1 bits. Under these conditions the model square root is the packed encoding of the remainder-rounded root, with a carry into the exponent field when rounding reaches 2 ^ (fracWidth + 1).