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

   Due Tuesday, February 27, at 11:59pm on Gradescope *)

require import AllCore.

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

(* QUESTION 1 (33 points)

   Prove the lemma M_noninter showing noninterference of the procedure
   `M.f`, using only the tactics

     `proc`, `seq`, `auto`, `if{1}` and `if{2}`,

   with the additional restriction that

     `auto` may only be used when both programs consist *entirely*
     of assignments

   Structure your proof so each tactic application is on a single
   line, and you don't use the tactic combinator `;`. It must be
   possible to step through your proof and check that each application
   of `auto` meets the above restriction. *)

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

  proc f() : unit = {
    y <- 1;
    z <- 0;
    if (x = 0) {
      z <- 1;
    }
    if (z = 0) {
      y <- 1;
    }
  }
}. 

lemma M_noninter :
  equiv [M.f ~ M.f : ={M.y} ==> ={M.y}].
proof.
(* BEGIN FILL IN *)
proc.
seq 2 2 : (M.y{1} = 1 /\ M.y{2} = 1).
auto.
seq 1 1 : (M.y{1} = 1 /\ M.y{2} = 1).
if{1}.
if{2}.
auto.
auto.
if{2}.
auto.
auto.
if{1}.
if{2}.
auto.
auto.
if{2}.
auto.
auto.
(* END FILL IN *)
qed.

(* QUESTION 2 (34 points)

   Prove the lemma N_noninter showing noninterference of the procedure
   N.f. *)

module N = {
  var x : int   (* private *)
  var y : int   (* private *)
  var i : int   (* public *)
  var b : bool  (* public *)

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

lemma N_noninter :
  equiv [N.f ~ N.f : ={N.i, N.b} ==> ={N.i, N.b}].
proof.
(* BEGIN FILL IN *)
proc; wp; sp.
if{1}; if{2};
  while (={N.i} /\ 0 <= N.y{1} /\ 0 <= N.y{2}); auto; smt().
(* END FILL IN *)
qed.

(* QUESTION 3 (33 points)

   Prove the lemma L_noninter, which expresses the noninterference of
   the procedure `N.f` using Hoare logic, in a style suggested in
   the last lecture on Relational Hoare Logic.

   In the module L, we have made two copies of the variables of
   module N, and the procedure L.f has two copies of the code
   of N.f, each operating on its own copy of the variables.

   Assuming L.f terminates for all memories (it does), the executions
   of the two copies proceed independently, and the lemma faithfully
   expresses noninterference. *)

module L = {
  (* variables of first copy *)
  var x  : int   (* private *)
  var y  : int   (* private *)
  var i  : int   (* public *)
  var b  : bool  (* public *)

  (* variables of second copy *)
  var x' : int   (* private *)
  var y' : int   (* private *)
  var i' : int   (* public *)
  var b' : bool  (* public *)

  proc f() : unit = {
    (* code of first copy *)
    y <- 0;
    if (x < 0) {
      while (0 < i) { 
        y <- y + 1;
        i <- i - 1;
      }
    }
    else {
      while (0 < i) {
        y <- y + 2;
        i <- i - 1;
      }
    }
    b <- 0 <= y;

    (* code of second copy *)
    y' <- 0;
    if (x' < 0) {
      while (0 < i') { 
        y' <- y' + 1;
        i' <- i' - 1;
      }
    }
    else {
      while (0 < i') {
        y' <- y' + 2;
        i' <- i' - 1;
      }
    }
    b' <- 0 <= y';
  }
}.

lemma L_noninter :
  hoare [L.f : L.i = L.i' /\ L.b = L.b' ==> L.i = L.i' /\ L.b = L.b'].
proof.
(* BEGIN FILL IN *)
proc.
(* handle first copy *)
seq 3 : (L.b /\ (L.i = L.i' /\ L.i < 0 \/ L.i = 0 /\ 0 <= L.i')).
wp; sp.
if;
  while (0 <= L.y /\ (L.i = L.i' /\ L.i < 0 \/ 0 <= L.i <= L.i'));
  auto; smt().
(* handle second copy *)
wp; sp.
if;
  while (0 <= L.y' /\ (L.i = L.i' /\ L.i < 0 \/ L.i = 0 /\ 0 <= L.i'));
  auto; smt().
(* END FILL IN *)
qed.