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

[Quan Anh Mai]

On Fri, 2 May 2025 07:30:33 GMT, Emanuel Peter <epeter at openjdk.org> wrote:

>> src/hotspot/share/opto/type.hpp line 708:
>> 
>>> 706:  *   I.e. x <= y in the signed domain iff x <= y in the unsigned domain
>>> 707:  *
>>> 708:  *   Then, we have:
>> 
>> The two `Then` are confusing me a little. The assumption is only the first sentence, not `x <= y iff juint(x) <= juint(y)`, right?
>> 
>> Hmm, ah you have an additional Lemma 3.1 here. But it is a little unclear where that starts and ends. Maybe that can be fixed with some indentation?
>
> Or you just cram in the Lemma 3.1 before you start the proof of Lemma 3. That would probably be cleanest.

That's a good idea, I lifted lemma 3.1 to number 3 and make the old lemma 3 lemma 4.

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

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