(* noninterference results using EasyCrypt's Relational Hoare Logic
   (RHL)

  actually, we're using pRHL, which stands for "probabilistic
  Relational Hoare Logic"; but we're ignoring the probabilistic
  aspects for now *)

require import AllCore IntDiv.

prover ["Z3"].

module M1 = {
  var x : int (* private *)
  var y : int (* public *)
  proc f() : unit = {
    x <- y;
  }
}.

(* RHL quadruples are written using equiv[...] *)

lemma lem1 :
  equiv[M1.f ~ M1.f : M1.y{1} = M1.y{2} ==> M1.y{1} = M1.y{2}].
proof.

qed.

module M2 = {
  var x : int (* private *)
  var y : int (* public *)
  proc f() : unit = {
    y <- x;
  }
}.

lemma lem2 :
  equiv[M2.f ~ M2.f : ={M2.y} ==> ={M2.y}].
proof.

abort.  (* abort this proof *)

module M3 = {
  var x : int (* private *)
  var y : int (* public *)
  proc f() : unit = {
    y <- x;
    y <- 5;
  }
}.

lemma lem3 :
  equiv[M3.f ~ M3.f : ={M3.y} ==> ={M3.y}].
proof.

qed.

module M4 = {
  var x : int (* private *)
  var y : int (* public *)
  proc f() : unit = {
    if (y %% 3 = 0) {
      x <- 0;
    }
    else {
      x <- 1;
    }
  }
}.

lemma lem4 :
  equiv[M4.f ~ M4.f : ={M4.y} ==> ={M4.y}].
proof.

qed.

module M5 = {
  var x : int (* private *)
  var y : int (* public *)
  proc f() : unit = {
    if (x %% 3 = 0) {
      y <- 0;
    }
    else {
      y <- 1;
    }
  }
}.

lemma lem5 :
  equiv[M5.f ~ M5.f : ={M5.y} ==> ={M5.y}].
proof.

abort.

require import List.

(* 'a list is the type of finite lists of type 'a
   ('a is a type variable - may stand for any type)

   these operators are polymorphic:

   size : 'a list -> int
   nth  : 'a -> 'a list -> int -> 'a
   
   nth def ys i means:
     return the ith element of ys (counting from 0),
       if 0 <= i < size ys;
     return def,
       otherwise *)

module M6 = {
  var i : int       (* public *)
  var xs : int list (* public *)
  var ys : int list (* private *)
  var r : bool      (* private *)

  proc f() : unit = {
    i <- 0;
    r <- false;
    while (i < 10) {
      if (! (nth 0 xs i = nth 1 ys i)) {
        r <- true;
      }
      i <- i + 1;
    }
  }
}.

lemma lem6 :
  equiv[M6.f ~ M6.f :
        ={M6.i, M6.xs} ==> ={M6.i, M6.xs}].
proof.

qed.

lemma lem6' :
  equiv[M6.f ~ M6.f :
        ={M6.i, M6.xs} ==> ={M6.i, M6.xs} /\ M6.i{1} = 10].
(* changed the postcondition to illustrate the while tactic better *)
proof.

qed.