On Tue, 15 Oct 2024 09:02:58 GMT, fabioromano1 <d...@openjdk.org> wrote:
>> 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 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.
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1800761892
