(* 3-expon.ec *) (* definition and proof of correctness of exponentiation *) prover ["Z3"]. require import AllCore IntExtra. (* do: ^ is exponentiation print (^). op (^) : int -> int -> int. *) (* do: search (^). lemma pow0 : forall (x : int), x ^ 0 = 1. lemma powS : forall (p x : int), 0 <= p => x ^ (p + 1) = x * x ^ p. *) module M = { proc exp(n : int, k : int) : int = { var i : int; var r : int; i <- 0; r <- 1; while (i < k) { r <- r * n; i <- i + 1; } return r; } }. lemma correct (n_ k_ : int) : hoare[M.exp : n = n_ /\ k = k_ /\ 0 <= k ==> res = n_ ^ k_]. proof. proc. simplify. while (k = k_ /\ n = n_ /\ 0 <= i <= k_ /\ r = n_ ^ i). wp; skip; progress. smt(). smt(). smt(powS). wp; skip; progress. smt(pow0). smt(). qed.