RFR: 8077587: BigInteger Roots [v52]

[fabioromano1]

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

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

@rgiulietti Yes, but why that complication, it is not more natural to prove it in the following way?

recalling x < 2^bl:
x / 2^sh' = x / 2^(sh-ex) ≤ 2^bl / 2^(sh-ex) = 2^(bl - (sh-ex)) ≤ 2^ME < Double.MAX_VALUE
``` 
relying on the fact that `bl - (sh-ex)` is the length of the shifted value?

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

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