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