Correctness of the native binary64 square-root kernel

The restoring two-limb kernel reconstructs its scaled radicand one base-four digit at a time, and its state invariant shows that the final native root is Nat.sqrt with the exact remainder. A checked Newton candidate gives the same state (rootAndRemainderChecked_eq). Finally, the format-level theorem refines the native field packing to Lean's unpacked binary64 model.

Restoring-root invariant

Two-word radicand digits

Restoring-loop refinement

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootAndRemainder_spec (mantissa : UInt64) (shift : ℕ) (hpositive : 0 < shift) (hshift : shift < 128) (hfit : mantissa.toNat <<< shift < 2 ^ 106) : have state := rootAndRemainder mantissa shift; state.root.toNat = (mantissa.toNat <<< shift).sqrt ∧ state.remainder.toNat = mantissa.toNat <<< shift - (mantissa.toNat <<< shift).sqrt * (mantissa.toNat <<< shift).sqrt

When the shifted significand fits in 106 bits, the restoring root returns the integer square root and its remainder.

Binary64 scaling and rounding specification

Checked Newton root

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootAndRemainderChecked_eq (mantissa : UInt64) (shift : ℕ) : rootAndRemainderChecked mantissa shift = rootAndRemainder mantissa shift

On every input, the checked candidate path computes rootAndRemainder.

Native-core refinement

Unpacked binary64 semantic refinement

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrt_eq_generic_of_positive_finite (x : Value) (hexponent : Model.expField x ≠ FloatFormat.binary64.expAllOnesNat) (hnonzero : isZero x = false) (hsign : Model.signBit x = false) : ofUInt64 (sqrtPositiveFinite (expField (toUInt64 x)) (fracField (toUInt64 x))) = ofModel FloatFormat.binary64 (Float.Model.UnpackedFloat.sqrt FloatFormat.binary64.toModel (toModel x))

On every positive finite binary64 value, including subnormals, the native square root agrees with the unpacked model after packing.