RFR: 8315066: Add unsigned bounds and known bits to TypeInt/Long [v48]

[Emanuel Peter]

On Wed, 30 Apr 2025 15:50:10 GMT, Quan Anh Mai <qamai at openjdk.org> wrote:

>> @merykitty 
>> Hmm, I'm a little nervous about the case where `there does not exist one such number`. Because all your proof does is basically assume that there is such a `r`, and then shows that we compute it correctly.
>> 
>> But such proofs do not give us the guarantee that if there is no such `r`, that the computation indeed overflows, i.e. produces a number smaller than `lo`. That would be required for the correctness, no?
>> 
>> So I guess the proof / examples with overflow should happen further down, I'm just mentioning it up here because it is here that you say there can be an overflow. Hope that makes sense 🙈
>
> Thanks for the clarification, I have added a section for this case.
> 
> The fundamental logic here is that if there exists a result `r`, then the algorithm will find it. The opposite is also true, if the algorithm finds a satisfying `r`, then of course there exists one. This makes the negation of those statements also equivalent, the algorithm does not find a satisfying result if and only if there is no such value.

Right, I think the missing part was that then the result is smaller than `lo`, which depends on that the result still satisfies bits... you now wrote a section about that, so that's better now :)

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

PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r2069910446