Definition A.2.1. Pre and Post Values.
Given a variable \(x\text{,}\) the pre value of \(x\text{,}\) denoted \(\grave x\text{,}\) is the value before an iteration of a loop. The post value, denoted \(\acute x\text{,}\) is the value after the iteration.
Definition A.2.3. Invariant Relation.
Given an algorithm’s inputs and a set of variables that are used in the algorithm, an invariant relation is a set of one or more equations that are true prior to entering a loop and remain true in every iteration of the loop.
We claim that the invariant relation in the fast algorithm is \(b t^k = a^m (mod\,n)\text{.}\) We will prove that this is indeed true below.
Theorem A.2.5. The Invariant Relation Theorem.
Given a loop within an algorithm, if \(R\) is a relation with the properties
R is true before entering the loop
the truth of R is maintained in any iteration of the loop
the condition for exiting the loop will always be reached in a finite number of iterations.
then R will be true upon exiting the loop.
The condition that the loop ends in a finite number of iterations lets us apply mathematical induction with the induction variable being the number of iterations. We leave the details to the reader.
We can verify the correctness of the fast exponentiation algorithm using the Invariant Relation Theorem. First we note that prior to entering the loop, \(b t^k = 1 a^m = a^m (mod\,n)\text{.}\) Assuming the relation is true at the start of any iteration, that is \(\grave{b} \grave{t}^{\grave k} = a^m (mod\,n)\text{,}\) then
\begin{equation*}
\begin{split}
\acute{b} \acute{t}^{\acute{k}} & \equiv (\grave{b} \grave{t}^{\grave{k}\,mod\,2})(\grave t^2)^{ \grave k//2}(mod\,n)\\
& \equiv\grave{b} \grave{t}^{2(\grave{k}//2) +\grave{k}\,mod\,2 }(mod\,n) \\
& \equiv \grave{b} \grave{t}^{\grave{k}}(mod\,n)\\
& \equiv a^m (mod\,n)
\end{split}
\end{equation*}
Finally, the value of \(k\) will decrease to zero in a finite number of steps because the number of binary digits of \(k\) decreases by one with each iteration. At the end of the loop,
\begin{equation*}
b = b t^0 = b t^k \equiv a^m(mod\,n)
\end{equation*}
which verifies the correctness of the algorithm.