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

[Quan Anh Mai]

On Wed, 30 Apr 2025 15:08:14 GMT, Emanuel Peter <epeter at openjdk.org> wrote:

>> What do you mean? It is the doc for `adjust_lo`, of course it needs to be here, I think it is logical to say what the function does before saying how it does it. For that purpose I think it is very clear already and an example is not needed.
>
> @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.

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

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