 Doubling-loop ceiling logarithm

For positive $x$, start at $i=0,y=1$ and repeatedly increment $i$ and double $y$ while $y<x$. In exact integer arithmetic, the loop invariant $y=2^i$ together with $i=0$ or $2^{i-1}<x$ yields $i=\lceil {\log }_{2}x\rceil$ at exit. For fixed-width arithmetic, this proof requires every useful doubling to be representable. A signed 32-bit doubling variable becomes negative at $2^{31}$ and then zero, so the loop need not terminate for inputs above $2^{30}$. Widening the variable to a signed 64-bit type repairs the algorithm for positive 32-bit inputs.