RFR: 8077587: BigInteger Roots [v52]

[Raffaello Giulietti]

On Tue, 29 Jul 2025 11:03:24 GMT, Raffaello Giulietti <rgiulietti at openjdk.org> wrote:

>> fabioromano1 has updated the pull request incrementally with one additional commit since the last revision:
>> 
>>   Zimmermann suggestion
>
> src/java.base/share/classes/java/math/MutableBigInteger.java line 2002:
> 
>> 2000:             // Try to shift as many bits as possible
>> 2001:             // without losing precision in double's representation.
>> 2002:             if (bitLength - (sh - shExcess) <= Double.MAX_EXPONENT) {
> 
> Here's an example of what I mean by "documenting the details"
> Suggestion:
> 
>             if (bitLength - (sh - shExcess) <= Double.MAX_EXPONENT) {
>                 /*
>                  * Let x = this, P = Double.PRECISION, ME = Double.MAX_EXPONENT,
>                  * bl = bitLength, ex = shExcess, sh' = sh - ex
>                  *
>                  * We have
>                  *      bl - (sh - ex) ≤ ME  ⇔  bl - (bl - P - ex) ≤ ME  ⇔  ex ≤ ME - P
>                  * hence, recalling x < 2^bl
>                  *      x 2^(-sh') = x 2^(ex-sh) = x 2^(-bl+ex+P) = x 2^(-bl) 2^(ex+P)
>                  *          < 2^(ex+P) ≤ 2^ME < Double.MAX_VALUE
>                  * Thus, x 2^(-sh') is in the range of finite doubles.
>                  * All the more so, this holds for ⌊x / 2^sh'⌋ ≤ x 2^(-sh'),
>                  * which is what is computed below.
>                  */
> 
> Without this, the reader has to reconstruct this "proof", which is arguably harder than just verifying its correctness.
> 
> OTOH, the statement "Adjust shift to a multiple of n" in the comment below is rather evident, and IMO does not need further explanations (but "mileage may vary" depending on the reader).

The proof might help replacing the `if` condition bl - (sh - ex) ≤ ME with ex ≤ ME - P.

-------------

PR Review Comment: https://git.openjdk.org/jdk/pull/24898#discussion_r2239415806