Rework Int.Pow() and Int.ModPow() using by method

[DavePearce]

In a similar way to what was done for the Int.FromBytes() function, it would make sense to implement the Int.Pow() and Int.ModPow() methods using by method to avoid expensive recursion.

[DavePearce]

This turns out to be quite a challenge, and after investing a fair amount of time I did not figure it out! Here is my method code (without the necessary invariants):

function Pow(n:nat, k:nat) : (r:nat)
// Following needed for some proofs
ensures n > 0 ==> r > 0 
{
     if k == 0 then 1
     else if k == 1 then n
     else
         var p := k / 2;
         var np := Pow(n,p);
         if p*2 == k then np * np
         else
             np * np * n
} by method {
     r := 1;
     var i : nat := k;
     var m : nat := n;
     //
     while i > 0
     {
         if i%2 == 1 {
             r := r * m;
         }
         m := m * m;
         i := i / 2;
     }
    }

One way to view what this does is to consider the bit representation of a number. For example: 5 = 0b101. Then we have:

   Pow(n,0b101)
 == 
   Pow(n,0b100) * Pow(n,0b001)

Which is n^5 == n^4 * n

What I've struggled with is figuring out the correct loop invariant for r. Based on the description seems like we have r == Pow(n, k%j) where j is the loop iteration.