On Thu, 17 Oct 2024 15:12:32 GMT, Raffaello Giulietti <rgiulie...@openjdk.org> wrote:
>> @rgiulietti That's correct, although I prefer that the correctness is proved >> by "reducing the size of the problem" rather than "total number of removed >> powers", because it was the logic to prove implicitly the correctness of the >> older implementation, namely by reducing the number of zeros without >> exceeding the largest scale decreasing allowed, and because, at least for >> me, it is less complex to write and understand. > > With the definition remainingZeros = scale - preferredScale, the proof above > could be adapted almost on the fly to the old implementation. > > In any reduction approach, you still need to prove that the reduced problem > is equivalent to the original. This is to say that the running variables (in > code and proof) must somehow be related to the initial values. > > Anyway, very nice contribution! Thanks. Will approve at the beginning of next week to let you add some last minute (not substantial) changes during the next few days. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1804979931
