(* Exercise 2: A Simple Probabilistic Noninterference Exercise *)

prover [""].  (* no use of SMT solvers *)

require import AllCore Distr.

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

type mybool = [T | F].

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: *)

axiom xor_T_T : T ^^ T = F.
axiom xor_T_F : T ^^ F = T.
axiom xor_F_T : F ^^ T = T.
axiom xor_F_F : F ^^ F = F.

(* lemmas for exclusive or: *)

(* false on the right *)
lemma xor_F (x : mybool) : x ^^ F = x.
proof.
case x; [apply xor_T_F | apply xor_F_F].
qed.

(* cancelling *)
lemma xorK (x : mybool) : x ^^ x = F.
proof.
case x; [apply xor_T_T | apply xor_F_F].
qed.

(* commutativity *)
lemma xorC (x y : mybool) : x ^^ y = y ^^ x.
case x.
case y => //.
rewrite xor_T_F xor_F_T //.
case y => //.
rewrite xor_F_T xor_T_F //.
qed.

(* associativity *)
lemma xorA (x y z : mybool) : (x ^^ y) ^^ z = x ^^ (y ^^ z).
proof.
case x.
case y.
rewrite xor_T_T.
case z.
rewrite xor_F_T xor_T_T xor_T_F //.
rewrite xor_F_F xor_T_F xor_T_T //.
case z.
rewrite xor_T_F xor_T_T xor_F_T xor_T_T //.
rewrite xor_T_F xor_T_F xor_F_F xor_T_F //.
case y.
rewrite xor_F_T.
case z.
rewrite xor_T_T xor_F_F //.
rewrite xor_T_F xor_F_T //.
case z.
rewrite xor_F_F xor_F_T xor_F_T //.
rewrite xor_F_F xor_F_F //.
qed.

(* a sub-distribution dmybool on mybool - this means that the sum of
   the weights of T and F in dmybool may be less than 1 *)

op dmybool : mybool distr.

(* dmybool is a distribution, i.e., the sum of the weights of T and F
   in dmybool is 1%r *)

axiom dmybool_ll : is_lossless dmybool.

(* if d is a sub-distribution on type 'a, and E is an event
   (predicate) on 'a (E : 'a -> bool), then mu d E is the probability
   that choosing a value from d will satisfy E

   if d is a sub-distribution on type 'a, and x : 'a, then mu1 d x is
   the probablity that choosing a value from d will result in x, i.e.,
   is the weight of x in d

   mu1 is defined by: mu1 d x = mu d (pred1 x), where pred1 x is the
   predicate that returns true iff its argument is x *)

(* both T and F have weight one-half in dmybool: *)

axiom dmybool1E (b : mybool) :
  mu1 dmybool b = 1%r / 2%r.

(* then we can prove that dmybool is full, i.e., that its support is
   all of mybool, i.e., that both T and F have non-zero weights in
   dmybool: *)

lemma dmybool_fu : is_full dmybool.
proof.
rewrite /is_full => x.
rewrite /support dmybool1E StdOrder.RealOrder.divr_gt0 //.
qed.

(* consider the following module with two global variables, one that
   we think of as private and one that we think of as public: *)

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

  proc f() : unit = {
    var b : mybool;
    b <$ dmybool;
    y <- y ^^ x ^^ b;
  }
}.

(* here is the probabilistic noninterference lemma for M.f: *)

lemma noninter_M :
  equiv[M.f ~ M.f : ={M.y} ==> ={M.y}].
proof.
(* BEGIN FILL IN *)
proc.
wp.
rnd (fun z => M.x{1} ^^ M.x{2} ^^ z).
skip; progress.
by rewrite -(xorA (M.x{1} ^^ M.x{2})) xorK xorC xor_F.
by rewrite 2!dmybool1E.
rewrite dmybool_fu.
by rewrite -(xorA (M.x{1} ^^ M.x{2})) xorK xorC xor_F.
rewrite 2!(xorA M.y{2}).
have -> // :
  M.x{2} ^^ (M.x{1} ^^ M.x{2} ^^ bL) = M.x{1} ^^ bL.
  by rewrite -(xorA M.x{2}) (xorC M.x{2}) (xorA M.x{1}) xorK xor_F.
(* END FILL IN *)
qed.