On Fri, 11 Oct 2024 19:45:23 GMT, fabioromano1 <d...@openjdk.org> wrote:
> This doesn't say much about `maxPowsOf5`, though. You are not using `intVal`
> but 2^`bitLength` > `intVal` in the computation of `maxPowsOf5`. So maybe the
> property you are looking for is `maxPowsOf5` - 1 <= log5(intVal) <
> `maxPowsOf5` || `maxPowsOf5` <= log5(intVal) < `maxPowsOf5` + 1
To clarify as much as possible, the weakest property that `maxPowsOf5` must
satisfy is:
`maxPowsOf5 >= max{integer n : intVal % 5^n == 0}`.
Clearly, it is true that `max{integer n : 5^n <= intVal} >= max{integer n :
intVal % 5^n == 0}`;
and since `floor(log5(intVal)) == max{integer n : 5^n <= intVal}`,
it follows that `maxPowsOf5 >= floor(log5(intVal)) ==> maxPowsOf5 >=
max{integer n : intVal % 5^n == 0}.`
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1797381043
