On Tue, 15 Oct 2024 09:11:40 GMT, Raffaello Giulietti <rgiulie...@openjdk.org>
wrote:
>> @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 branches, the invariant `remainingZeros >= z` is
>> preserved by the instructions.
>
> Yes, I considered that as well.
> Not sure, however, if this is sufficient to prove that intVal has been indeed
> divided by 5^z after the 2nd loop is terminated.
Anyway, if you find a nice proof please add it to the comments. The algorithm
is quite sophisticated, so it needs one.
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1800765293
