On Sun, 13 Oct 2024 16:34:09 GMT, Raffaello Giulietti <rgiulie...@openjdk.org> wrote:
>>> What's really crucial for _correctness_ is to ensure maxPowsOf5 >= k. >> >> Yes, I meant that the only way we know to ensure that condition is to ensure >> `m <= maxPowsOf5`... >> >>> Perhaps leave m <= maxPowsOf5 <= m + 1 and maxPowsOf5 >= k and drop the >>> note "and is never off by more than 1 from the theoretical m" >> >> I would put `maxPowsOf5 <= m + 2` instead, because `maxPowsOf5 <= m + 1` is >> not obvious to prove mathematically... > > It can be proven by considering > > - the inequality | b * LOG_5_OF_2 - b log5(2) | < 2^(-21) > - the properties of round() (to an integer) > - log5(2) < 1/2 > > The last one is crucial for the upper bound to be m + 1 rather than m + 2. > > Feel free to use m + 2, though. I understood that it follows from the fact that `log5(2^(n+1)) - log5(2^n) == [log5(2^n) + log5(2)] - log5(2^n)`, but I think it's superfluous having to explain it in the comments just to prove `maxPowsOf5 <= m + 1`, while it is more clear to understand why `maxPowsOf5 <= m + 2` is true. Anyway, thanks for the insight. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1798459950
