(* Ancient Egyptian multiplication

   Multiply two integers a and b using only addition, multiplication by 2,
   and division by 2. You may assume b to be nonnegative.

   Note: library int.ComputerDivision (already imported) provide functions
   "div" and "mod".

   Questions:

   1. Prove soundness of function multiplication.

   2. Prove its termination.

*)

module Multiplication

  use import int.Int
  use import int.ComputerDivision
  use import ref.Ref

  let multiplication (a b: int) : int
    requires { true }
    ensures  { true }
  = let x = ref a in
    let y = ref b in
    let z = ref 0 in
    while !y <> 0 do
      invariant { true }
      if mod !y 2 = 1 then z := !z + !x;
      x := 2 * !x;
      y := div !y 2
    done;
    !z

end

(* Note: this is exactly the same algorithm as exponentiation by squarring
   with power/*/1 being replaced by */+/0.
*)