On Fri, 12 Jul 2024 13:06:35 GMT, Raffaello Giulietti <rgiulie...@openjdk.org> wrote:
>> fabioromano1 has updated the pull request incrementally with one additional >> commit since the last revision: >> >> Added comment on normalization in MutableBigInteger.sqrtRemZimmermann() > > src/java.base/share/classes/java/math/MutableBigInteger.java line 1941: > >> 1939: >> 1940: // Initial estimate is the square root of the unsigned >> long value. >> 1941: long s = (long) Math.sqrt(x > 0 ? x : x + 0x1p64); > > As a matter of simplification, the above cases can be collapsed to just this > one. I don't think there's a real need to optimize for 0, [1, 4), `int`. > > Also, there should be a proof that the code below is correct, as there are > many roundings involved. > > Suggestion: > > long s = (long) Math.sqrt(x >= 0 ? x : x + 0x1p64); The proof has been made simply by exaustive experiment: for every long value `s` in [0, 2^32) such that `x == s * s`, it is true that `s == (long) Math.sqrt(x >= 0 ? x : x + 0x1p64)`. This can be verified directly by a Java program. It means that Math.sqrt() returns the correct value for every perfect square, and so the value returned by Math.sqrt() for whatever long value in the range [0, 2^64) is either correct, or rounded up by one if the value is too high and too close to a perfect square. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/19710#discussion_r1675951166
