Restoring square-root refinement

The restoring loop returns the floor square root and square remainder of its input. The invariant relates the consumed radicand prefix to the partial root at each shift-and-subtract step. This direct refinement proof lets callers use the kernel without a runtime certificate check, provided the scaled radicand fits the fixed-word bound.

Restoring-loop invariant

Four-word radicand reconstruction

Restoring-loop refinement

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootAndRemainder_spec (radicand : UInt256) (steps : ℕ) (hlower : 64 ≤ steps) (hupper : steps ≤ 125) (hfit : radicand.toNat < 2 ^ (2 * steps)) : have state := rootAndRemainder radicand steps; state.root.toNat = radicand.toNat.sqrt ∧ state.remainder.toNat = radicand.toNat - radicand.toNat.sqrt * radicand.toNat.sqrt

The restoring kernel with steps digits returns the exact floor root and square remainder for every radicand below 2^(2 * steps), for any digit count between 64 and 125.

The upper bound keeps the remainder doubled twice inside the two-word state; the two-word square-root kernels use fracWidth + 1 digits.

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.roundRoot_toNat (radicand : UInt256) (steps : ℕ) (hlower : 64 ≤ steps) (hupper : steps ≤ 125) (hfit : radicand.toNat < 2 ^ (2 * steps)) : (roundRoot (rootAndRemainder radicand steps)).toNat = have root := radicand.toNat.sqrt; have remainder := radicand.toNat - root * root; if remainder ≤ root then root else root + 1

Native nearest-root rounding agrees with the mathematical remainder boundary.