Peasant multiplication

Show total correctness of function peasant_mult, by providing a loop invariant and a variant for the while loop.

use int.Int
use int.ComputerDivision

let peasant_mult (a b: int) : int
  requires { b >= 0 }
  ensures  { result = a * b }
= let ref p = a in
  let ref q = b in
  let ref r = 0 in
  while q > 0 do
    invariant { q >= 0 }
    invariant { p * q + r = a * b }
    variant   { q }
    if mod q 2 = 1 then r <- r + p;
    p <- p + p;
    q <- div q 2
  done;
  return r