(* Assignment 3 - Noninterference and EasyCrypt's Relational Hoare
   Logic (100 points)

   Due Friday, October 30, 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.

(* Question 1 (45 points) *)

module M = {
  var x : int  (* private *)
  var y : int  (* public *)
  var z : int  (* public *)

  proc f() : unit = {
    if (y < z) {
      while (y < z) {
        x <- x + y;
        y <- y + 1;
      }
    }
    elif (y = z) { }
    else {
      while (z < y) {
        x <- x + y;
        y <- y - 1;
      }
    }
  }
}.

lemma M_noninter :
  equiv [M.f ~ M.f : ={M.y, M.z} ==> ={M.y, M.z}].
proof.
(* FILL IN *)
(* END FILL IN *)
qed.

(* Question 2 (55 points) *)

module N = {
  var x : int  (* private *)
  var y : int  (* public *)
  var z : int  (* public *)

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

lemma N_noninter :
  equiv [N.f ~ N.f : ={N.y, N.z} ==> ={N.y, N.z}].
proof.
(* FILL IN *)
(* END FILL IN *)
qed.