On Tue, 29 Jul 2025 13:26:41 GMT, fabioromano1 <d...@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
