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