(* ASSIGNMENT 2 Due on Gradescope by 5pm on Friday, February 19 *) require import AllCore. (* NOTE: in the following Hoare Logic proofs, you may *not* use the tactics `auto` or `sp`, which we haven't covered in Lab or the slides yet. You *may* use `smt`. *) (* Any uses of the `smt` tactic in your proof must be solvable by *both* Alt-Ergo and Z3: *) prover quorum=2 ["Alt-Ergo" "Z3"]. (* QUESTION 1 (* 20 Points *) *) module Swap = { var x, y : int proc f() : unit = { var z : int; z <- x; x <- y; y <- z; } }. lemma swapping (_x _y : int) : hoare [Swap.f : Swap.x = _x /\ Swap.y = _y ==> Swap.x = _y /\ Swap.y = _x]. proof. (* BEGIN FILL IN *) proc. wp. skip. trivial. (* END FILL IN *) qed. lemma swapping' (_x _y : int) : hoare [Swap.f : Swap.x = _x /\ Swap.y = _y ==> Swap.x = _y /\ Swap.y = _x]. proof. (* BEGIN FILL IN *) proc; wp; skip; trivial. (* END FILL IN *) qed. (* QUESTION 2 (40 Points) *) module M = { var x, y, z : int proc f() : unit = { if (x < y) { z <- x - y; if (x <= y) { while (false) { } } } else { z <- y - x - 1; } } }. lemma M1 : hoare [M.f : true ==> M.z < 0]. proof. (* BEGIN FILL IN *) proc. if. seq 1 : (M.z < 0). wp; skip; smt(). if. while (true). skip; trivial. skip; trivial. skip; trivial. wp; skip; smt(). (* END FILL IN *) qed. lemma M1' : hoare [M.f : true ==> M.z < 0]. proof. (* BEGIN FILL IN *) proc. if. seq 1 : (M.z < 0). wp; skip; smt(). if. while (true); skip; trivial. skip; trivial. wp; skip; smt(). (* END FILL IN *) qed. lemma M2 : hoare [M.f : true ==> (M.x < M.y => M.z = M.x - M.y) /\ (M.y <= M.x => M.z + 1 = M.y - M.x)]. proof. (* BEGIN FILL IN *) proc. if. seq 1 : (M.x < M.y /\ M.z = M.x - M.y). wp; skip; trivial. if. while (true). skip; trivial. skip; smt(). skip; smt(). wp; skip; trivial. (* END FILL IN *) qed. (* QUESTION 3 (40 Points) *) require import List. (* This introduces a new type constructor, 'a list, which means that for any type t, t list is the type of finite lists of elements of type t. Lists are written [x1; x2; ...; xn]. E.g., *) op xs = [1; 3; 5; 7]. (* is the value of type int list consisting of the first four odd natural numbers. If x has type 'a and ys has type 'a list, then x :: ys is the value of type 'a list whose first element (head) is x, and whose remaining elements (its tail) are those of ys. (We pronounce :: "cons", for "construct".) E.g., *) op zs = 1 :: [3; 5; 7]. lemma eq_xs_zs : xs = zs. proof. by rewrite /xs /zs. qed. (* size : 'a list -> int returns the number of elements of a list. E.g., *) lemma size_ex : size zs = 4. proof. smt(). qed. (* If we have lists xs and ys of type 'a list, then xs ++ ys is the concatenation of xs and ys, i.e., the list consisting of the elements of xs followed by the elements of ys. E.g., *) op ws = xs ++ [9]. lemma ws_lem : ws = [1; 3; 5; 7; 9]. proof. smt(). qed. (* rcons : 'a list -> 'a -> 'a list ("reverse cons") takes xs : 'a list and y : 'a and returns xs ++ [y]. rcons is defined recursively, and you can see how this is done by doing print rcons. *) lemma rcons_ex : rcons ws 11 = ws ++ [11]. proof. (* search rcons (++). *) by rewrite -cats1. qed. (* nth : 'a -> 'a list -> int -> 'a takes def : 'a, xs : 'a list, and i : int, and returns (+) the ith element of xs (counting from 0), if 0 <= i < size xs; (+) the default element, def, if i < 0 \/ size xs <= i E.g., *) lemma nth_ex1 : nth (-2) ws 3 = 7. proof. smt(). qed. lemma nth_ex2 : nth (-2) ws (-1) = -2. proof. smt(). qed. lemma nth_ex3 : nth (-2) ws 5 = -2. proof. smt(). qed. (* take : 'a list -> int -> 'a list takes in a list xs and an integer n, and returns the list consisting of the first n elements of xs (it returns [] if n is negative, and returns xs if more then size xs elements are requested). E.g., *) lemma take_ex1 : take 3 ws = [1; 3; 5]. proof. by rewrite /ws /xs. qed. lemma take_ex2 : take (-1) ws = []. proof. trivial. qed. lemma take_ex3 : take 6 ws = [1; 3; 5; 7; 9]. proof. by rewrite /ws /xs. qed. (* drop : 'a list -> int -> 'a list takes in a list xs and an integer n, and returns the list consisting of what's left over if we remove the first n elements of xs (it returns [] if more than size xs elements are dropped, and returns xs if n is negative). E.g., *) lemma drop_ex1 : drop 3 ws = [7; 9]. proof. by rewrite /ws /xs. qed. lemma drop_ex2 : drop (-1) ws = ws. proof. trivial. qed. lemma drop_ex3 : drop 6 ws = []. proof. by rewrite /ws /xs. qed. (* rev : 'a list -> 'a list reverses a list. E.g., *) lemma rev_ex : rev ws = [9; 7; 5; 3; 1]. proof. by rewrite /ws /xs. qed. (* You can search for combinations of (::), (++), size, rcons, nth, take, drop and rev to find numerous useful lemmas, which you can tell smt to try to use or you can use directly via apply or rewrite. *) module Rev = { proc f(xs : int list) : int list = { var i : int; var ys : int list; i <- 0; ys <- []; while (i < size xs) { ys <- nth 0 xs i :: ys; i <- i + 1; } return ys; } }. lemma Rev_rev (_xs : int list) : hoare [Rev.f : xs = _xs ==> res = rev _xs]. proof. (* BEGIN FILL IN *) proc. seq 2 : (xs = _xs /\ i = 0 /\ ys = []). wp; skip; trivial. while (0 <= i /\ i <= size xs /\ ys = rev (take i xs)). wp; skip; progress. smt(). smt(). smt(take_nth rev_rcons). skip; progress. smt(size_ge0). smt(take0 rev_nil). smt(take_size). (* END FILL IN *) qed. lemma Rev_rev' (_xs : int list) : hoare [Rev.f : xs = _xs ==> res = rev _xs]. proof. (* BEGIN FILL IN *) proc. while (0 <= i /\ i <= size xs /\ ys = rev (take i xs)). wp; skip; progress. smt(). smt(). smt(take_nth rev_rcons). wp; skip; progress. smt(size_ge0). smt(take0 rev_nil). smt(take_size). (* END FILL IN *) qed.