(* Assignment 2 - EasyCrypt's Hoare Logic (100 points)

   Due Friday, October 16, at 11:59pm on Gradescope

   You may use the smt tactic in this assignment, but you must
   use the form

     smt(lem_1 ... lem_n)

   to limit the SMT solvers to their internal knowledge bases plus the
   supplied lemmas.

   If you use AI to solve a question, you must add a comment
   explaining the process you followed, including a complete
   transcript of your interaction with the AI agent. Whether or not
   you use AI, you must understand your answers, and be able to
   explain them orally. *)

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

require import AllCore IntDiv.

(* Question 1 (25 points) *)

module M = {
  var i : int

  proc f() : unit = {
    if (i < 0) {
      while (i < 0) {
        i <- i + 1;
      }
    }
    else {
      while (0 < i) {
        i <- i - 1;
      }
    }
  }
}.

lemma M_correct :
  hoare [M.f : true ==> M.i = 0].
proof.
(* FILL IN *)
(* END FILL IN *)
qed.

(* Question 2 (25 points) *)

(* smt_opaque doesn't give SMT solvers access to the definition
   of f: *)

op [smt_opaque] f (n : int) : int = if n %% 2 = 0 then 1 else -1.

(* but you can tell the SMT solvers to use this lemma: *)

lemma fS (n : int) :
  f (n + 1) = - f n.
proof. rewrite /f /#. qed.

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

lemma N_correct (k_ : int) :
  hoare [N.f : k = k_ /\ 0 <= k ==> res = f k_].
proof.
(* FILL IN *)
(* END FILL IN *)
qed.

(* Question 3 (50 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. *)

(* size : 'a list -> int returns the number of elements of a
   list. E.g., *)

lemma size_ex : size xs = 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.

(* 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. trivial. qed.

lemma nth_ex2 : nth (-2) ws (-1) = -2.
proof. trivial. qed.

lemma nth_ex3 : nth (-2) ws 5 = -2.
proof. trivial. qed.

(* sorted_nth ys uses nth to test whether ys is sorted in ascending
   order, possibly with duplicates *)

op sorted_nth (ys : int list) : bool =
  forall (i j : int),
  0 <= i < j < size ys =>
  nth (-1) ys i <= nth (-1) ys j.

(* mem_by_nth x ys uses nth to test whether x is a member of ys *)

op mem_by_nth (x : int, ys : int list) : bool =
  exists (i : int),
  0 <= i < size ys /\ nth (-1) ys i = x.

(* this lemma helps us understand why the procedure Find.find, below,
   is correct and terminates *)

lemma window_mid (low high : int) :
  low < high => low <= (low + high) %/ 2 < high.
proof. smt(). qed.

module Find = {
  proc find(x : int, ys : int list) : int = {
    var low, high, mid, y : int;
    low <- 0; high <- size ys - 1;
    while (low < high) {
      mid <- (low + high) %/ 2;
      y <- nth (-1) ys mid;
      if (y < x) {
        low <- mid + 1;
      }
      elif (y = x) {
        low <- mid; high <- mid;
      }
      else {  (* x < y *)
        high <- mid;
        while (false) { }  (* just to limit auto, wp and sp *)
      }
    }
    return low;
  }
}.

(* you can put any auxiliary defintions or lemmas (proved) that you
   need, here: *)

(* FILL IN *)
(* END FILL IN *)

lemma find_correct (x_ : int, ys_ : int list) :
  hoare
  [Find.find :
   x = x_ /\ ys = ys_ /\ sorted_nth ys /\ mem_by_nth x ys ==>
   0 <= res < size ys_ /\ nth (-1) ys_ res = x_].
proof.
(* FILL IN *)
(* END FILL IN *)
qed.