RFR: 8341470: BigDecimal.stripTrailingZeros() optimization [v44]

[fabioromano1]

On Tue, 15 Oct 2024 09:18:59 GMT, fabioromano1 <duke at openjdk.org> wrote:

>> Anyway, if you find a nice proof please add it to the comments. The algorithm is quite sophisticated, so it needs one.
>
> I would say yes... The invariant `i == max{n : 5^(2^n) <= 5^remainingZeros}` should be a sufficient condition to affirm it, indeed the 2nd loop ends when `remainingZeros == 0`, so `remainingZeros >= z` implies `z == 0`...

> 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.

New comments just added should be sufficient to prove it.

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

PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1800837070