(* phl-prhl.ec *)

(* using pHL, pRHL and the ambient logic in conjuction

   many of the tactics of pHL work similarly to those of
   Hoare logic *)

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

(* Distr has definitions and lemmas about sub-distributions, DBool has
   the distribution {0,1} on bool that assigns both true and false
   weight 1%r / 2%r, StdOrder has lemmas about orderings (<, <=),
   including a sub-theory RealOrder which has lemmas about the
   orderings on real

   The name of {0,1} : bool distr is misleading, in that the booleans
   are actually true and false (and {1,0} or even {0, 1} are invalid)
   *)

require import AllCore Distr DBool StdOrder.
import RealOrder.

(* For our first example, we have two modules, each with a procedure
   f

   M.f returns a random boolean; N.f returns the exclusive or of two
   random booleans *)

module M = {
  proc f() : bool = {
    var b : bool;
    b <$ {0,1};
    return b;
  }
}.

module N = {
  proc f() : bool = {
    var b1, b2 : bool;
    b1 <$ {0,1};
    b2 <$ {0,1};
    return b1 ^ b2;  (* exclusive or *)
  }
}.

(* we prove a pRHL judgement relating M.f and N.f

   EasyCrypt is able to automatically prove all the needed
   properites of {0,1}

   this proof is similar to ones we've seen in the slides
   on pRHL, and so we'll express it succinct form *)

lemma M_N_equiv :
  equiv [M.f ~ N.f : true ==> ={res}].
proof.
proc.
seq 0 1 : true.
rnd{2}.
auto.
rnd (fun x => x ^ b1{2}).
auto; smt().
qed.

(* now we can use M_N_equiv twice

   first we prove that M.f and N.f are equally likely to return true,
   no matter what initial memory &m they are started in (M and N lack
   global variables, so the behavior on any initial memory is the
   same) *)

lemma M_N_true &m :
  Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.

qed.

(* a more succint proof: *)

lemma M_N_true' &m :
  Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.

qed.

(* a still more succint proof: *)

lemma M_N_true'' &m :
  Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.

qed.

(* next we prove that M.f and N.f are equally likely to return
   false *)

lemma M_N_false &m :
  Pr[M.f() @ &m : !res] = Pr[N.f() @ &m : !res].
proof.

qed.

(* next we use pHL to prove M.f returns true exactly half the
   time *)

lemma M_true &m :
  Pr[M.f() @ &m : res] = 1%r / 2%r.
proof.

qed.

(* here is a more succinct proof: *)

lemma M_true' &m :
  Pr[M.f() @ &m : res] = 1%r / 2%r.
proof.

qed.

(* now we can combine M_N_true and M_true to get: *)

lemma N_true &m :
  Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.

qed.

(* or we can prove N_true directly: *)

lemma N_true' &m :
  Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.

qed.