(* phoare.ec *)

(* I haven't written slides for pHL, the probabilistic Hoare logic,
   which is used for proving probabilistic facts about individual
   procedures.

   Many of its tactics are similar to those of the Hoare logic, so
   reading those slides is useful. But below are examples of a
   few exceptions. *)

require import AllCore.
require import Bool.

(* x ^^ y is actually an abbreviation for x = !y (do print (^^) to see
   this); consequently, an assumption of the form x ^^ y can be used
   by the rewrite tactic *)

require import Distr.
require import DBool.

(* let's see how we can directly prove that N.f() (compare with
   rnd.ec) returns true exactly half the time *)

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

(* working backward is easiest: *)

lemma N &m :
  Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.
byphoare => //.
proc.
(* because the last statement is a random assignment, we can use the
   rnd tactic to push it into the postcondition. to figure out the
   argument to pred1, consider that for the postcondition to be true,
   b2 will have to be the negation of b1 *)
rnd (pred1 (!b1)).
(* now note that the bound is [=] 1%r; consequently, the argument
   of the next application of rnd can be predT *)
rnd predT.
skip; progress.
by rewrite dbool_ll.
by rewrite dbool1E.
by rewrite /pred1 in H4; rewrite H4.
by rewrite /pred1 H4.
qed.

(* but we can also work forward: *)

lemma N' &m :
  Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.
byphoare => //.
proc.
(* we need to use the pHL version of seq *)
seq 1 :
  b1            (* intermediate condition (IC) *)
  (1%r / 2%r)   (* probability that IC holds after first choice
                   from precondition *)
  (1%r / 2%r)   (* probability that postcondition holds after
                   second choice from IC *)
  (1%r / 2%r)   (* probability that !IC holds after first choice
                   from precondition *)
  (1%r / 2%r).  (* probability that postcondition holds after
                   second choice from !IC *)
auto.
rnd (pred1 true).
skip; progress.
by rewrite dbool1E.
rewrite /pred1 in H1; rewrite H1.
by rewrite /pred1 H1.
rnd (pred1 false).
skip; progress.
by rewrite dbool1E.
by rewrite /pred1 in H2; rewrite H2 H.
rewrite H xorC xor_true in H2.
by rewrite /pred1 H2.
rnd (pred1 false).
skip; progress.
by rewrite dbool1E.
by rewrite /pred1 in H1; rewrite H1.
by rewrite /pred1 H1.
rnd (pred1 true).
skip; progress.
by rewrite dbool1E.
rewrite /pred1 in H2.
by rewrite H2 H.
rewrite H xorC in H2.
by rewrite /pred1 H2.
(* this goal was simplified by EasyCrypt, but it originally
   asserted that
   
  (1%r / 2%r) * (1%r / 2%r) + (1%r / 2%r) (1%r / 2%r) = 1%r / 2%r

   i.e., that the sum of the probability that we end up with
   the postcondition holding after IC holding, and the probability
   that we end up with the postcondition holding after IC not holding,
   is equal to 1%r / 2%r *)
trivial.
qed.

module L = {
  proc f(x : int, y : int) : int = {
    var z : int;
    if (x <= y) {
      z <- y - x;
    }
    else {
      z <- x - y;
    }
    z <- z * 2;
    return z;
  }
}.

lemma L1 :
  phoare[L.f : true ==> 0 <= res] = 1%r.
proof.
proc.
(* as usual, the if tactic can only be used when the first
   statement is an if-then-else (conditional) *)
if.
wp.
skip.
smt().
auto.  (* auto combines wp, skip and trivial *)
smt().
qed.

lemma L2 :
  phoare[L.f : true ==> 0 <= res] = 1%r.
proof.
proc.
(* like with the Hoare logic, wp can push nested conditionals of
   ordinary assignments into the postcondition *)
wp.
skip.
smt().
qed.

lemma L3 :
  phoare[L.f : true ==> 0 <= res] = 1%r.
proof.
proc; auto; smt().
qed.