On Tue, 29 Jul 2025 13:03:59 GMT, Raffaello Giulietti <rgiulie...@openjdk.org> wrote:
>>> 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. @rgiulietti Are there other points that are still not clear? ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/24898#discussion_r2239834907
