(* xor-loop.ec *)

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

require import AllCore IntDiv.

(* a type mybool with elements tt standing for "true" and ff standing
   for "false", and an exclusive or operator ^^: *)

type mybool = [tt | ff].

op (^^) : mybool -> mybool -> mybool.

(* we can write x ^^ y instead of (^^) x y

   ^^ is left associatve, so x ^^ y ^^ z means (x ^^ y) ^^ z *)

(* axioms defining exclusive or (nosmt means these axioms aren't
   available to the SMT provers): *)

axiom nosmt xor_tt_tt : tt ^^ tt = ff.
axiom nosmt xor_tt_ff : tt ^^ ff = tt.
axiom nosmt xor_ff_tt : ff ^^ tt = tt.
axiom nosmt xor_ff_ff : ff ^^ ff = ff.

(* lemmas for exclusive or: *)

(* false on the right *)
lemma xor_ff (x : mybool) : x ^^ ff = x.
proof.
case x.
apply xor_tt_ff.
apply xor_ff_ff.
qed.

(* cancelling *)
lemma xorK (x : mybool) : x ^^ x = ff.
proof.
case x.
apply xor_tt_tt.
apply xor_ff_ff.
qed.

(* commutativity *)
lemma xorC (x y : mybool) : x ^^ y = y ^^ x.
    case x.
    case y.
    trivial.
    rewrite xor_ff_tt.
    apply xor_tt_ff.
    case y.
    rewrite xor_tt_ff.
    apply xor_ff_tt.
    trivial.
qed.
    

(* associativity *)
lemma xorA (x y z : mybool) : (x ^^ y) ^^ z = x ^^ (y ^^ z).
proof.
case x.
case y.
rewrite xor_tt_tt.
case z.
by rewrite xor_ff_tt xor_tt_tt xor_tt_ff.
by rewrite xor_ff_ff xor_tt_ff xor_tt_tt.
case z.
by rewrite xor_tt_ff xor_tt_tt xor_ff_tt xor_tt_tt.
by rewrite xor_tt_ff xor_tt_ff xor_ff_ff xor_tt_ff.
case y.
rewrite xor_ff_tt.
case z.
by rewrite xor_tt_tt xor_ff_ff.
by rewrite xor_tt_ff xor_ff_tt.
case z.
by rewrite xor_ff_ff xor_ff_tt xor_ff_tt.
by rewrite xor_ff_ff xor_ff_ff.
qed.

(* define even, odd : int -> bool

   SMT provers know about %%, so smt() can reason about even and
   odd *)

op even (k : int) = k %% 2 = 0.  (* %% is mod *)
op odd  (k : int) = ! even k.

module M = {
  proc f(n : int,      (* public *)       
         x : mybool,   (* public *)
         y : mybool)   (* private *)
         : mybool = {  (* public *)
    var i : int;       (* not visible to observer *)
    var b : mybool;    (* not visible to observer, but returned *)
    i <- 0;
    b <- x;
    if (0 <= n) {
      while (i < n) {
        b <- b ^^ y;
        i <- i + 1;
      }
      if (odd n) {
        b <- b ^^ y;
      }
    }
    return b;
  }
}.


(* three versions each of two different approaches to proving
   noninterference for M.f are below *)

lemma noninter1 :
  equiv[M.f ~ M.f : ={n, x} ==> ={res}].  
proof.
proc => /=.
seq 2 2 : (={n, i, b} /\ i{1} = 0); [auto | idtac].
if => //.
seq 1 1 :
  (={n} /\
   (even n{1} => ={b}) /\
   (odd n{1} => b{1} ^^ y{1} = b{2} ^^ y{2})).
while
  (={n, i} /\ i{1} <= n{1} /\
   (even i{1} => ={b}) /\
   (odd i{1} => b{1} ^^ y{1} = b{2} ^^ y{2})).
auto; smt(xorA xorK).
auto; smt().
auto; smt().
qed.

lemma noninter1' :
  equiv[M.f ~ M.f : ={n, x} ==> ={res}].  
proof.
proc => /=.
seq 2 2 : (={n, i, b} /\ i{1} = 0); [auto | idtac].
if => //.
wp.
while
  (={n, i} /\ i{1} <= n{1} /\
   (even i{1} => ={b}) /\
   (odd i{1} => b{1} ^^ y{1} = b{2} ^^ y{2})).
auto; smt(xorA xorK xor_ff).
auto; smt().
qed.

lemma noninter1'' :
  equiv[M.f ~ M.f : ={n, x} ==> ={res}].  
proof.
proc => /=.
sp.
if => //.
wp.
while
  (={n, i} /\ i{1} <= n{1} /\
   (even i{1} => ={b}) /\
   (odd i{1} => b{1} ^^ y{1} = b{2} ^^ y{2})).
auto; smt(xorA xorK xor_ff).
auto; smt().
qed.

lemma noninter2 :
  equiv[M.f ~ M.f : ={n, x} ==> ={res}].  
proof.
proc => /=.
seq 2 2 : (={n, i, b} /\ i{1} = 0 /\ b{1} = x{1}); [auto | idtac].
if => //.
seq 1 1 :
  (={n} /\
   if even n{1}
   then ={b} /\ b{1} = x{1}
   else b{1} = x{1} ^^ y{1} /\ b{2} = x{1} ^^ y{2}).
while
  (={n, i} /\ i{1} <= n{1} /\
   (if even i{1}
    then ={b} /\ b{1} = x{1}
    else b{1} = x{1} ^^ y{1} /\ b{2} = x{1} ^^ y{2})).
auto; smt(xorA xorK xor_ff).
auto; smt().
auto; smt(xorA xorK).
qed.

lemma noninter2' :
  equiv[M.f ~ M.f : ={n, x} ==> ={res}].  
proof.
proc => /=.
seq 2 2 : (={n, i, b} /\ i{1} = 0 /\ b{1} = x{1}); [auto | idtac].
if => //.
wp.
while
  (={n, i} /\ i{1} <= n{1} /\
   (if even i{1}
    then ={b} /\ b{1} = x{1}
    else b{1} = x{1} ^^ y{1} /\ b{2} = x{1} ^^ y{2})).
auto; smt(xorA xorK xor_ff).
auto; smt(xorA xorK).
qed.

lemma noninter2'' :
  equiv[M.f ~ M.f : ={n, x} ==> ={res}].  
proof.
proc => /=.
sp.
if => //.
wp.
while
  (={n, i} /\ i{1} <= n{1} /\
   (if even i{1}
    then ={b} /\ b{1} = x{1}
    else b{1} = x{1} ^^ y{1} /\ b{2} = x{1} ^^ y{2})).
auto; smt(xorA xorK xor_ff).
auto; progress; smt(xorA xorK).
qed.