On Fri, 12 Jul 2024 13:43:29 GMT, fabioromano1 <d...@openjdk.org> wrote:
>> 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. (Yes, I proved it to myself in this way.) A similar explanation should be in a comment in the code, not here. The source of truth is the code, not the comments on GitHub ;-) ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/19710#discussion_r1675959960
