I was looking in V. Shoup's book 'A Computational Introduction to Number Theory and Algebra' (freely available here). The exercise is as follows:
As I'm not very familiar with proving correctness of algorithms, I got stuck quite quickly on (a). As this is quite a simple algorithm, perhaps a common method such as using a loop invariant or induction could work here, but I do not see how the specific argument would go.
As for subquestion (b), my initial thought was that one could expand $(m+2^i)^2$ to $m^2+2^{i+1}m+2^{2i}$, and pre-compute $m^2$ before the loop. The rest of the terms are all bit shifts, and can be done efficiently. Since addition can be done in $O(\text{len}(n))$, each loop iteration takes time $O(\text{len}(n))$. Would you say this is a correct answer?
Thanks in advance!
Best Answer
Firstly note that $m \mapsto m^2$ is a monotonically increasing function for $m > 0$. This mean that $m^2 = n$ has the only positive solution, and that $m \ge m_i$ if and only if $m_i^2 \le n$.
A rigorous proof can be based on mathematical induction. Let $m_k = 2^k$ and $m_i = m_{i + 1} + [(m_{i + 1} + 2^i)^2 \le n] \cdot 2^i$ for $i = k - 1, k - 2, \ldots, 0$. Here I use Iverson's notation $[P] = \begin{cases} 1, & \text{if } P;\\ 0, & \text{otherwise.}\end{cases}$ Such $m_i$ corresponds to the value of $m$ after $(k - i)$th iteration of the cycle. Let's prove that $m_i^2 \le n < (m_i + 2^i)^2$.
The base case is $i = k$. Indeed, if $\mathrm{len}(n) = \lfloor\log_2 n\rfloor + 1$, then $$2^{\mathrm{len}(n) - 1} \le n < 2^{\mathrm{len}(n)}.$$ Since $k = \lfloor(\mathrm{len}(n) - 1) / 2\rfloor$ and $m_k = 2^k$, then $$m_k^2 = 2^{2k} = 2^{2\lfloor(\mathrm{len}(n) - 1) / 2\rfloor} \le 2^{2 \cdot (\mathrm{len}(n) - 1) / 2} = 2^{\mathrm{len}(n) - 1} \le n.$$ Since $k$ is semi-integer and therefore $k \ge (\mathrm{len}(n) - 1) / 2 - 1/2$, then $$(m_k + 2^k)^2 = (2^k + 2^k)^2 = 2^{2 \cdot (k + 1/2 + 1/2)} \ge 2^{2 \cdot ((\mathrm{len}(n) - 1) / 2 + 1/2)} = 2^{\mathrm{len}(n)} > n.$$
Suppose that $m_{j + 1}^2 \le n < (m_{j + 1} + 2^{j + 1})^2$. Now there are two cases. If $(m_{j + 1} + 2^j)^2 > n$ then $m_j = m_{j + 1}$ and $$m_j^2 = m_{j + 1}^2 \le n < (m_{j + 1} + 2^j)^2 = (m_j + 2^j)^2.$$ Otherwise $m_j = m_{j + 1} + 2^j$ and $$m_j^2 = (m_{j + 1} + 2^j)^2 \le n < (m_{j + 1} + 2^{j + 1})^2 = (m_{j + 1} + 2^j + 2^j)^2 = (m_j + 2^j)^2.$$
So $m_0^2 \le n < (m_0 + 1)^2$, i. e., $m_0 = \lfloor \sqrt{n} \rfloor$. And $m_0$ is the final value of $m$ in the provided algorithm, so the algorithm is correct.
Your reasoning about running time optimization is correct.