(* simp-expon.ec *)

(* definition and proof of simple exponentiation *)

(* smt tactic only succeeds if both Alt-Ergo and Z3 solve the goal: *)

prover quorum=2 ["Alt-Ergo" "Z3"].

require import AllCore.

(*
search (^).  (* integer exponentiation *)

lemma expr0 (x : int) : x ^ 0 = 1.
lemma expr1 (x : int) : x ^ 1 = x.
lemma exprS (x i : int) :
  0 <= i => x ^ (i + 1) = x * x ^ i.
lemma expr2 (x : int) : x ^ 2 = x * x.
lemma exprM (x m n : int) : x ^ (m * n) = x ^ m ^ n.
*)

module M = {
  var i, k, r, n : int

  proc f() : unit = {
    i <- 0;
    r <- 1;
    while (i < k) {
      r <- r * n;
      i <- i + 1;
    }
  }
}.

lemma correct_M :
  hoare [M.f : 0 <= M.k ==> M.r = M.n ^ M.k].
proof.

qed.

module N = {
  proc f(n : int, k : int) : int = {
    var i, r : int;
    i <- 0;
    r <- 1;
    while (i < k) {
      r <- r * n;
      i <- i + 1;
    }
    return r;
  }
}.

lemma correct_N (n_ k_ : int) :
  hoare [N.f : n = n_ /\ k = k_ /\ 0 <= k ==> res = n_ ^ k_].
proof.

qed.

lemma correct'_N (n_ k_ : int) :
  hoare [N.f : n = n_ /\ k = k_ /\ 0 <= k ==> res = n_ ^ k_].
proof.

qed.