(* 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.

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

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.

qed.

lemma L2 :
  phoare[L.f : true ==> 0 <= res] = 1%r.
proof.

qed.

lemma L3 :
  phoare[L.f : true ==> 0 <= res] = 1%r.
proof.

qed.