On Tue, 29 Jul 2025 12:25:21 GMT, fabioromano1 <d...@openjdk.org> wrote:
>> @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? > >> 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. >> ``` > > And this should follow by the fact that `bl - (sh - ex) = bl - (bl - P - ex) > = P + ex`, since `ex ≥ 0`. 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. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/24898#discussion_r2239769849
