RFR: 8077587: BigInteger Roots [v52]

[Raffaello Giulietti]

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

>> 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.

To the above, we can also add

                 * 
                 * Noting that x ≥ 2^(bl-1) and ex ≥ 0, similarly to the above we further get
                 *      x 2^(-sh') ≥ 2^(ex+P-1) ≥ 2^(P-1)
                 * which shows that ⌊x / 2^sh'⌋ has at least P bits of precision.

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

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