On Tue, 29 Jul 2025 11:05:43 GMT, Raffaello Giulietti <rgiulie...@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
