(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 Fast exponentiation} *)

use int.Int
use int.ComputerDivision

let rec function power (x:int) (n:int) : int
   requires { n >= 0 }
   variant { n }
= if n = 0 then 1 else x * power x (n-1)

(** a few helper lemmas *)

let rec lemma power_mult (x y n:int)
  requires { n >= 0 }
  variant { n }
  ensures { power (x*y) n = power x n * power y n }
= if n > 0 then power_mult x y (n-1)

let rec lemma power_even (x:int) (n:int)
  requires { n >= 0 /\ mod n 2 = 0 }
  variant { n }
  ensures { power x n = (power (x * x) (div n 2)) }
= if n > 1 then
    begin
      power_even x (n-2);
      (* we learn power x (n-2) = power (x*x) (div (n-2) 2) *)
      assert { power x n = x * x * power x (n-2) };
      assert { div (n-2) 2 = div n 2 - 1 };
    end

let lemma power_odd (x:int) (n:int)
  requires { n >= 0 /\ mod n 2 = 1 }
  ensures {  power x n = x * (power (x * x) (div n 2)) }
= power_even x (n-1)


(** fast exponentiation *)
let power_x_n (x:int) (n:int) : int
  requires { n >= 0 }
  ensures { result = power x n }
  diverges
  =
   let ref r = 1 in
   let ref p = x in
   let ref e = n in
   while e > 0 do
     invariant { 0 <= e }
     invariant { r * power p e = power x n }
     if mod e 2 = 1 then r <- r * p;
     p <- p * p;
     e <- div e 2
   done;
   r