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