Shared arithmetic for fixed-width square-root refinements

The binary32, binary64, and binary128 square-root kernels use the same affine exponent calculation with different format constants. This module records that calculation once so each backend proof only supplies its descriptor-specific constants.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.roundedMantissa_of_sqrtRemainder (root remainder : ℕ) : have accuracy := if remainder = 0 then Float.Model.UnpackedFloat.Accuracy.exact else Float.Model.UnpackedFloat.Accuracy.inexact (if remainder ≤ root then Ordering.lt else Ordering.gt); (Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy root accuracy).roundedMantissa = if remainder ≤ root then root else root + 1

The unpacked-model accuracy used by integer square root rounds up exactly when the square remainder is larger than the lower root.

For n = root² + remainder, comparison with (root + 1/2)² reduces to comparing the integer remainder with root: remainder ≤ root is below the midpoint, while the next integer remainder is above it. Thus an integer radicand cannot produce a square-root midpoint tie.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.half_sub_eq (position inputShift outputOffset outputBias : ℕ) (hbalance : inputShift + outputOffset = 2 * outputBias) : (Int.ofNat position - Int.ofNat inputShift).ediv 2 = Int.ofNat ((position + outputOffset) / 2) - Int.ofNat outputBias

Move an even affine offset through Euclidean division by two.

The balance equation says that inputShift and outputOffset describe the same exponent origin on opposite sides of the radix point.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.sum_half_sub_eq (leading scale inputShift outputOffset outputBias : ℕ) (hinput : 2 ≤ inputShift) (hbalance : inputShift - 2 + outputOffset = 2 * outputBias) : (Int.ofNat leading + 1 + (Int.ofNat scale - Int.ofNat inputShift) + 1).ediv 2 = Int.ofNat ((leading + scale + outputOffset) / 2) - Int.ofNat outputBias

Normalize the total-exponent numerator used by square-root target-exponent calculations.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.sum_natCast_ediv_two (left right offset : ℕ) : (Int.ofNat left + Int.ofNat right + Int.ofNat offset).ediv 2 = Int.ofNat ((left + right + offset) / 2)

Cast a natural affine numerator before or after division by two.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.target_exponent (leading scale inputShift outputOffset outputBias fractionBits : ℕ) (hleading : leading ≤ fractionBits) (hinput : 2 ≤ inputShift) (hbias : 1 ≤ outputBias) (hnormal : outputBias + fractionBits ≤ inputShift + outputOffset / 2) (hbalance : inputShift + outputOffset = 2 * outputBias) : (Int.ofNat scale - Int.ofNat inputShift).ediv 2 ⊓ (((Int.ofNat leading + 1 + (Int.ofNat scale - Int.ofNat inputShift) + 1).ediv 2 - Int.ofNat (fractionBits + 1)) ⊔ -Int.ofNat inputShift) = (Int.ofNat leading + Int.ofNat scale + Int.ofNat outputOffset).ediv 2 - Int.ofNat outputBias - Int.ofNat fractionBits

Normalize the target exponent selected for a square-root result.

The hypotheses express the format-independent relationships among the encoded exponent origin, the result bias, and the fraction width. In particular, the affine offset must leave enough room for the normalized result significand, and the input leading bit must lie within that significand.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.shift_amount (leading scale inputShift outputOffset outputBias fractionBits : ℕ) (hleading : leading ≤ fractionBits) (hbalance : inputShift + outputOffset = 2 * outputBias) : have position := leading + scale; have rootExponent := Int.ofNat ((position + outputOffset) / 2) - Int.ofNat outputBias; (Int.ofNat scale - Int.ofNat inputShift - 2 * (rootExponent - Int.ofNat fractionBits)).toNat = (position + outputOffset) % 2 + 2 * fractionBits - leading

Compute the nonnegative integer shift required to align a square-root radicand.

After the exponent origins cancel, only the parity of the affine position remains. The result is therefore twice the destination fraction width, minus the input's leading-bit position, plus one when the affine position is odd.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.shift_amount_of_even_offset (leading scale inputShift outputOffset outputBias fractionBits : ℕ) (hleading : leading ≤ fractionBits) (hbalance : inputShift + outputOffset = 2 * outputBias) (hoffset : outputOffset % 2 = 0) : have position := leading + scale; have rootExponent := Int.ofNat ((position + outputOffset) / 2) - Int.ofNat outputBias; (Int.ofNat scale - Int.ofNat inputShift - 2 * (rootExponent - Int.ofNat fractionBits)).toNat = if position % 2 = 0 then 2 * fractionBits - leading else 2 * fractionBits + 1 - leading

Express the square-root shift directly in terms of the input position when the affine offset is even.

theorem FloatLib.Floats.ExecFloat.Backends.SqrtArithmetic.shift_amount_of_odd_offset (leading scale inputShift outputOffset outputBias fractionBits : ℕ) (hleading : leading ≤ fractionBits) (hbalance : inputShift + outputOffset = 2 * outputBias) (hoffset : outputOffset % 2 = 1) : have position := leading + scale; have rootExponent := Int.ofNat ((position + outputOffset) / 2) - Int.ofNat outputBias; (Int.ofNat scale - Int.ofNat inputShift - 2 * (rootExponent - Int.ofNat fractionBits)).toNat = if position % 2 = 0 then 2 * fractionBits + 1 - leading else 2 * fractionBits - leading

Express the square-root shift directly in terms of the input position when the affine offset is odd.