Correctness of checked square roots #
An accepted candidate is the floor square root with its exact remainder (checkRoot?_spec,
acceptRootWide?_spec), and rootAndRemainder and Internal.rootAndRemainder equal the
restoring loop on every input.
theorem
FloatLib.Numerics.FixedWord.CheckedSquareRoot.checkRoot?_spec
{radicand : UInt128}
{guess : UInt64}
{state : RestoringRootState UInt64}
(h : checkRoot? radicand guess = some state)
:
An accepted candidate is the floor square root, with the exact remainder.
theorem
FloatLib.Numerics.FixedWord.CheckedSquareRoot.rootAndRemainder_eq
(radicand : UInt256)
(steps : ℕ)
:
rootAndRemainder equals the restoring loop on every input.
theorem
FloatLib.Numerics.FixedWord.CheckedSquareRoot.acceptRootWide?_spec
{radicand : UInt256}
{guess : UInt128}
{state : RestoringRootState UInt128}
(h : acceptRootWide? radicand guess = some state)
:
An accepted four-word candidate is the floor square root, with the exact remainder.
theorem
FloatLib.Numerics.FixedWord.CheckedSquareRoot.Internal.rootAndRemainder_eq
(radicand : UInt256)
(steps : ℕ)
:
Internal.rootAndRemainder equals the two-word checked path, hence the loop, on every
input.