On Tue, 15 Oct 2024 08:23:23 GMT, Raffaello Giulietti <rgiulie...@openjdk.org>
wrote:
>> @rgiulietti Or maybe "i.e., 5^(2^i) is larger than the largest power of five
>> that is still removable from intVal", could it be ok?
>
> While I intuitively understand, and I'm convinced of the clever algorithm,
> I'm struggling to find a proof, in particular to formulate a useful invariant
> for the first loop which seamlessly would bind with the second loop and its
> invariant.
> I need to find more time for this.
@rgiulietti Actually, an useful invariant for `remainingZeros` follows directly
from its definition: letting `z = max{n : ((intVal * 2^powsOf2) % 10^n) == 0 &&
n <= scale - preferredScale}`, at the first iteration, it is true that
`remainingZeros >= z`, and the loop condition is `remainingZeros >= 2^i`. So,
if `z < 2^i`, then `intVal % 5^(2^i) != 0` and the "then" branch of the "if" is
executed, otherwise `z >= 2^i` and the "else" branch is executed. In both
branchs, the invariant `remainingZeros >= z` is preserved by the instructions.
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1800746960
