RFR: 8077587: BigInteger Roots [v52]

[Raffaello Giulietti]

On Tue, 29 Jul 2025 13:26:41 GMT, fabioromano1 <duke at openjdk.org> wrote:

>> My point is that this should be done, not the exact form it takes. Mine or yours are both better than nothing.
>> 
>> Another point I wanted to make is that the `if` condition bl - (sh - ex) ≤ ME can be replaced with the simpler ex ≤ ME - P, whose right-hand side is a compile time constant.
>> 
>>> And this should follow by the fact that bl - (sh - ex) =  bl - (bl - P - ex) = P + ex, since ex ≥ 0.
>> 
>> To show that ⌊x / 2^sh'⌋ has at least P bits of precision, I think you need to make use of x ≥ 2^(bl-1).
>> 
>> Anyway, I hope I made my point clear: it is better to write proofs rather than relying on readers to reverse-engineer them from the code. Surely, there's no need to be pedantic in every single detail.
>
> @rgiulietti Are there other points that are still not clear?

Well, that was the easy case!
(BTW, the condition shExcess != 0 on L.2025 is always true, as shExcess > Double.MAX_EXPONENT - Double.PRECISION there.)

There should be similar reasoning for the `else` part on L.2020.

And, more importantly so, for the more obscure parts (for a 1st time reader, not for the author ;-) ) starting at L.2034. This is the code that took most of my time.

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

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