(* 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.
(* this is one of the goal forms involving Pr[...] that the ambient
   logic tactic byequiv can handle - and equality of Pr[...] for
   a pair of procedures *)
byequiv (_ : true ==> ={res}).
apply M_N_equiv.
trivial.  (* precondition established *)
trivial.  (* postcondition implies iff on events *)
qed.

(* a more succint proof: *)

lemma M_N_true' &m :
  Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.
byequiv => //.  (* byequiv can often infer the needed lemma *)
apply M_N_equiv.
qed.

(* a still more succint proof: *)

lemma M_N_true'' &m :
  Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.
(* we can tell byequiv which lemma to use *)
by byequiv M_N_equiv.
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.
by byequiv M_N_equiv.
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.
(* we can use the ambient logic tactic byphoare to reduce this
   equality to a pHL (probabilistic Hoare Logic) judgement and
   two ambient logic goals *)
byphoare (_ : true ==> res).
(* note that in contrast to Hoare logic goals, the judgement includes
   a bound *)
proc.
(* rnd takes a predicate as argument (hint: try using pred0 (the
   predicate that doesn't like anything), to help figure out
   what predicate you need; predT is the predicate that likes
   everything) *)
rnd (pred1 true).
skip; progress.
(* x / y is an abbreviation for x * inv y, and the
   1%r has been simplified away *)
smt(dbool1E).
smt().
smt().
trivial.  (* precondition is established *)
trivial.  (* simplification of iff between postcondition and
             event *)
qed.

(* here is a more succinct proof: *)

lemma M_true' &m :
  Pr[M.f() @ &m : res] = 1%r / 2%r.
proof.
byphoare => //.
proc.
rnd (pred1 true).
auto; smt(dbool1E).
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.
by rewrite -(M_N_true &m) (M_true &m).
qed.

(* or we can prove N_true directly: *)

lemma N_true' &m :
  Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.
byphoare => //.
proc.
seq 1 :         (* seq has a more complex, optional form *)
  b1            (* intermediate condition (IC) *)
  (1%r / 2%r)   (* (a) *)
  (1%r / 2%r)   (* (b) *)
  (1%r / 2%r)   (* (c) *)
  (1%r / 2%r).  (* (d) *)
(* Hoare judgment with postcondition true - has to do with yet
   another optional argument to seq that we're not using *)
auto.
(* proof that if we start in memory satisfying precondition, the
   probability that IC will hold after running 1st statement is (a) *)
rnd (pred1 true).
skip; progress.
smt(dbool1E).
smt().
smt().
(* proof that if we start in memory satisfying IC, the probability
   that postcondition will hold after running 2nd statement is (b) *)
rnd (pred1 false).
skip; progress.
smt(dbool1E).
smt().
smt().
smt().
(* proof that if we start in memory satisfying precondition, the
   probability that !IC will hold after running 1st statement is (c) *)
rnd (pred1 false).
skip; progress.
smt(dbool1E).
smt().
smt().
(* proof that if we start in memory satisfying !IC, the probability
   that postcondition will hold after running 2nd statement is (d) *)
rnd (pred1 true).
skip; progress.
smt(dbool1E).
smt().
smt().
smt().
(* probability agreement: proof that
   (a) * (b) + (c) * (d) = 1%r / 2%r,
   but EasyCrypt has simplified it *)
trivial.
qed.