(* fast-expon.ec *) (* definition and proof of correctness of fast exponentiation *) prover ["Z3"]. (* only use listed provers *) require import AllCore IntDiv. (* search (^). lemma pow0 (x : int) : x ^ 0 = 1. lemma pow1 (n : int) : n ^ 1 = n. lemma powS (p x : int) : 0 <= p => x ^ (p + 1) = x * x ^ p. lemma pow_mul : (z p1 p2 : int) : 0 <= p1 => 0 <= p2 => z ^ p1 ^ p2 = z ^ (p1 * p2). *) lemma pow2 (n : int) : n ^ 2 = n * n. proof. smt(pow1 powS). qed. (* define even, odd : int -> bool *) op even (k : int) = k %% 2 = 0. (* %% is mod *) op odd (k : int) = ! even k. lemma even_eq (k : int) : even k => k = 2 * (k %/ 2). (* %/ is integer division *) proof. smt(). qed. lemma odd_eq (k : int) : odd k => k = 2 * ((k - 1) %/ 2) + 1. proof. smt(). qed. lemma fastdiv_even (n k : int) : 1 < k => even k => n ^ k = (n * n) ^ (k %/ 2). proof. move => gt1_k even_k. rewrite {1}(even_eq k) // -pow_mul //. rewrite divz_ge0 // /#. by rewrite pow2. qed. lemma fastdiv_odd (n k : int) : 1 < k => odd k => n ^ k = (n * n) ^ ((k - 1) %/ 2) * n. proof. move => gt1_k odd_k. rewrite {1}(odd_eq k) 1:/# //. rewrite powS 1:/#. rewrite -pow_mul // 1:/# pow2. by rewrite mulzC. qed. module M = { proc f(n : int, k : int) : int = { var n' : int; var k' : int; var r : int; n' <- n; k' <- k; r <- 1; if (0 < k') { while (1 < k') { if (even k') { n' <- n' * n'; k' <- k' %/ 2; } else { r <- n' * r; n' <- n' * n'; k' <- (k' - 1) %/ 2; } } r <- n' * r; } return r; } }. lemma correct (n_ k_ : int) : hoare[M.f : n = n_ /\ k = k_ /\ 0 <= k ==> res = n_ ^ k_]. proof. proc; simplify. seq 3 : (n' = n_ /\ k' = k_ /\ r = 1 /\ 0 <= k'). wp; skip; trivial. if. wp. while (0 < k' /\ n' ^ k' * r = n_ ^ k_). if. wp; skip; progress. smt(). smt(fastdiv_even). wp; skip; progress. smt(). smt(fastdiv_odd). skip; progress. smt(pow1). skip; progress. smt(pow0). qed.