(* 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 quorum=2 ["Alt-Ergo" "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.
(* note that ={M1.y} is used as abbreviation for M1.y{1} = M1.y{2} *)
proc.
(* because the programs are the same "in sync", only one copy is
  displayed *)
wp. skip. trivial. 
qed.

lemma lem1' :
  equiv [M1.f ~ M1.f : M1.y{1} = M1.y{2} ==> M1.y{1} = M1.y{2}].
proof.
(* auto tries to use wp, skip and trivial to solve a goal *)
proc; auto.
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.
proc; wp; skip.
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.
  proc; auto.
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.
proc.
if. (* two-sided if *)
trivial.
auto.
auto.
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.
proc; if.
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;
    }
  }
}.

(* just used to explain how while tactic works *)
op P (x : bool * bool) : bool = true.

lemma lem6 :
  equiv [M6.f ~ M6.f :
         ={M6.i, M6.xs} ==>
         ={M6.i, M6.xs} /\
         P (M6.r{1}, M6.r{2})].
         (* this second conjunct isn't needed to show noninterference,
            but it helps explain how the while tactic works *)
proof.
(* seq is now given number of statements to take from left-side,
   followed by number of statements to take from right-side
   (we don't have to use a seq, as while works as long as both
   programs end with a while loop *)
seq 2 2 : (={M6.i, M6.xs}).
auto.
while (={M6.i, M6.xs}).
  (* can't use two-sided if here; try it! *)
if{1}. (* one-sided if-then-else - left *)
if{2}. (* one-sided if-then-else - right *)
auto.
auto.
if{2}.
auto.
auto.
skip.
trivial.
qed.

lemma lem6' :
  equiv [M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs}].
proof.
proc.
(* our program ends with while, so don't need initial seq *)
while (={M6.i}).  (* proof of 1st subgoal doesn't need ={M6.xs} *)
wp.  (* can push this program into the postcondition *)
skip; trivial.
auto.
qed.

lemma lem6'' :
  equiv [M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs}].
proof.
proc; while (={M6.i}); auto.
qed.

module M7 = {
  proc f(xs : int list,  (* public *)
         ys : int list)  (* private *)
         : int *         (* i's value - public *)
           bool = {      (* r's value - private *)
    var i : int;         (* public *)
    var r : bool;        (* private *)
    i <- 0;
    r <- false;
    while (i < 10) {
      if (! (nth 0 xs i = nth 1 ys i)) {
        r <- true;
      }
      i <- i + 1;
    }
    return (i, r);
  }
}.

lemma lem7 :
  equiv [M7.f ~ M7.f : ={xs} ==> res{1}.`1 = res{2}.`1].
proof.
proc; while (={i}); auto.
qed.