(* ASSIGNMENT 5

   Due on Gradescope by 5pm on Friday, March 19 *)

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

timeout 2.  (* smt timeout in seconds - can increase *)

require import AllCore Distr.

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

type mybool = [tt | ff].

(* because tt is an alias for the value () : unit, you'll sometimes
   see Top.tt in goals for the value tt of mybool *)

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 => //.
by rewrite xor_tt_ff xor_ff_tt.
case y => //.
by rewrite xor_ff_tt xor_tt_ff.
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.

(* a sub-distribution dmybool on mybool - this means that the sum of
   the values of tt and ff in dmybool may be less than 1 *)

op dmybool : mybool distr.

(* dmybool is a distribution, i.e., the sum of the values of tt and ff
   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 value 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 tt and ff have value 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 tt and ff have non-zero values in
   dmybool: *)

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

(* QUESTION 1 (40 Points) *)

module M1 = {
  var x, y : mybool  (* private *)
  var z : mybool     (* public *)

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

lemma lem1 :
  equiv[M1.f ~ M1.f : ={M1.z} ==> ={M1.z}].
proof.
(* BEGIN FILL IN *)

(* END FILL IN *)
qed.

(* QUESTION 2 (60 Points) *)

module M2 = {
  var x, y : mybool  (* private *)
  var z    : mybool  (* public *)

  proc f() : unit = {
    var u, v : mybool;
    if (x = y) {
      u <$ dmybool;
      z <- u ^^ x;
    }
    else {
      u <$ dmybool;
      v <$ dmybool;
      z <- u ^^ v ^^ x ^^ y;
    }
  }
}.

lemma lem2 :
  equiv[M2.f ~ M2.f : ={M2.z} ==> ={M2.z}].
proof.
(* BEGIN FILL IN *)

(* END FILL IN *)
qed.