On Thu, 17 Oct 2024 15:17:38 GMT, Raffaello Giulietti <rgiulie...@openjdk.org> wrote:
>> 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. > 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. Yes, although in the proof by "reducing the size of the problem" this should be evident by induction... ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1804983630
