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

[Quan Anh Mai]

On Thu, 30 Jan 2025 13:23:10 GMT, Emanuel Peter <epeter at openjdk.org> wrote:

>> Quan Anh Mai has updated the pull request incrementally with one additional commit since the last revision:
>> 
>>   include
>
> src/hotspot/share/opto/rangeinference.cpp line 148:
> 
>> 146:   Trivially, lo < v since lo[i] < v[i] and lo[x] == v[x] for x < i.
>> 147: 
>> 148:   As established above, the first (i + 1) bits of v satisfy bits.
> 
> When reading through here, I'm getting a sense of overwhealm with all the defined variables and statements we have proven already. It could be very helpful if you give statements a number / name, so that we can refer back to them.
> 
> That way, I never need to fully cache the whole proof in my head, I can just combine the steps and check if they are correct.
> 
> That is what I have extensively done in proofs of `AlignmentSolver::solve`, which also got a little long...

I have break the steps further and number the lemmas as you suggested, hope it is more manageable now.

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

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