(* rnd.ec example involving pHL (probabilistic Hoare logic) as well as pRHL (probabilistic Relational Hoare Logic) *) prover quorum=2 ["Alt-Ergo" "Z3"]. (* Distr has definitions and lemmas about sub-distributions *) require import AllCore Distr. (* a type mybool with elements tt standing for "true" and ff standing for "false", and an exclusive or operator ^^: *) type mybool = [tt | ff]. (* because tt is an alias for the value () : unit, you'll sometimes see Top.tt in goals for the value tt of mybool *) op (^^) : mybool -> mybool -> mybool. (* we can write x ^^ y instead of (^^) x y ^^ is left associatve, so x ^^ y ^^ z means (x ^^ y) ^^ z *) (* axioms defining exclusive or (nosmt means these axioms aren't available to the SMT provers): *) axiom nosmt xor_tt_tt : tt ^^ tt = ff. axiom nosmt xor_tt_ff : tt ^^ ff = tt. axiom nosmt xor_ff_tt : ff ^^ tt = tt. axiom nosmt xor_ff_ff : ff ^^ ff = ff. lemma not_ff (x : mybool) : x <> ff <=> x = tt. proof. by case x. qed. lemma not_tt (x : mybool) : x <> tt <=> x = ff. proof. by rewrite -not_ff. qed. (* lemmas for exclusive or: *) (* false on the right *) lemma xor_ff (x : mybool) : x ^^ ff = x. proof. case x; [apply xor_tt_ff | apply xor_ff_ff]. qed. (* cancelling *) lemma xorK (x : mybool) : x ^^ x = ff. proof. case x; [apply xor_tt_tt | apply xor_ff_ff]. qed. (* commutativity *) lemma xorC (x y : mybool) : x ^^ y = y ^^ x. case x. case y => //. by rewrite xor_tt_ff xor_ff_tt. case y => //. by rewrite xor_ff_tt xor_tt_ff. qed. (* associativity *) lemma xorA (x y z : mybool) : (x ^^ y) ^^ z = x ^^ (y ^^ z). proof. case x. case y. rewrite xor_tt_tt. case z. by rewrite xor_ff_tt xor_tt_tt xor_tt_ff. by rewrite xor_ff_ff xor_tt_ff xor_tt_tt. case z. by rewrite xor_tt_ff xor_tt_tt xor_ff_tt xor_tt_tt. by rewrite xor_tt_ff xor_tt_ff xor_ff_ff xor_tt_ff. case y. rewrite xor_ff_tt. case z. by rewrite xor_tt_tt xor_ff_ff. by rewrite xor_tt_ff xor_ff_tt. case z. by rewrite xor_ff_ff xor_ff_tt xor_ff_tt. by rewrite xor_ff_ff xor_ff_ff. qed. (* a sub-distribution dmybool on mybool - this means that the sum of the values of tt and ff in dmybool may be less than 1 *) op dmybool : mybool distr. (* dmybool is a distribution, i.e., the sum of the values of tt and ff in dmybool is 1%r this is expressed as weight dmybool = 1%r, i.e., is_lossless dmybool *) axiom dmybool_ll : is_lossless dmybool. (* if d is a sub-distribution on type 'a, and E is an event (predicate) on 'a (E : 'a -> bool), then mu d E is the probability that choosing a value from d will satisfy E if d is a sub-distribution on type 'a, and x : 'a, then mu1 d x is the probablity that choosing a value from d will result in x, i.e., is the value of x in d mu1 is defined by: mu1 d x = mu d (pred1 x), where pred1 x is the predicate that returns true iff its argument is x *) (* both tt and ff have value one-half in dmybool: *) axiom dmybool1E (b : mybool) : mu1 dmybool b = 1%r / 2%r. (* then we can prove that dmybool is full, i.e., that its support is all of mybool, i.e., that both tt and ff have non-zero values in dmybool: *) lemma dmybool_fu : is_full dmybool. proof. rewrite /is_full => x. rewrite /support dmybool1E StdOrder.RealOrder.divr_gt0 //. qed. (* now we have two modules, each with a procedure f: *) module M = { proc f() : mybool = { var b : mybool; b <$ dmybool; return b; } }. module N = { proc f() : mybool = { var b1, b2 : mybool; b1 <$ dmybool; b2 <$ dmybool; return b1 ^^ b2; } }. (* we prove a pRHL judgement relating M.f and N.f: *) lemma M_N_equiv : equiv[M.f ~ N.f : true ==> ={res}]. proof. proc. seq 0 1 : true. rnd{2}; auto; progress. apply dmybool_ll. rnd (fun x => x ^^ b1{2}). skip; progress. smt(xorA xorK xor_ff). smt(dmybool1E). smt(dmybool_fu). smt(xorA xorK xor_ff). smt(xorA xorC xorK xor_ff). qed. (* now we can use M_N_equiv twice: *) lemma M_N_tt &m : Pr[M.f() @ &m : res = tt] = Pr[N.f() @ &m : res = tt]. proof. (* we can use byequiv to reduce this equality of Pr[...] expressions to a pRHL judgement *) byequiv => //. by apply M_N_equiv. qed. lemma M_N_ff &m : Pr[M.f() @ &m : res = ff] = Pr[N.f() @ &m : res = ff]. proof. (* we can tell byequiv which lemma to use *) by byequiv M_N_equiv. qed. lemma M_tt &m : Pr[M.f() @ &m : res = tt] = 1%r / 2%r. proof. (* we can use byphoare to reduce this equality to a pHL (probabilistic Hoare Logic) judgement: *) byphoare => //. proc. (* rnd takes a predicate as argument: *) rnd (pred1 tt). skip; progress. (* x / y is an abbreviation for x * inv y *) smt(dmybool1E). trivial. qed. (* now we can combine M_N_tt and M_tt to get: *) lemma N_tt &m : Pr[N.f() @ &m : res = tt] = 1%r / 2%r. proof. by rewrite -(M_N_tt &m) (M_tt &m). qed. (* or we can prove N_tt directly: *) lemma N_tt' &m : Pr[N.f() @ &m : res = tt] = 1%r / 2%r. (* see what has to be changed if we say, instead, Pr[N.f() @ &m : res = tt] <= 1%r / 2%r. *) proof. byphoare => //. proc. seq 1 : (* seq has a more complex, optional form *) (b1 = tt) (* 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 tt). skip; progress. smt(dmybool1E). trivial. (* proof that if we start in memory satisfying IC, the probability that postcondition will hold after running 2nd statement is (b) *) rnd (pred1 ff). skip; progress. smt(dmybool1E). smt(xorK xor_ff). (* clearing unneeded assumptions can help smt focus *) clear H H0; smt(xorK xor_ff). (* proof that if we start in memory satisfying precondition, the probability that !IC will hold after running 1st statement is (c) *) rnd (pred1 ff). skip; progress. smt(dmybool1E). smt(). clear H H0; smt(not_tt). (* proof that if we start in memory satisfying !IC, the probability that postcondition will hold after running 2nd statement is (d) *) rnd (pred1 tt). skip; progress. smt(dmybool1E). smt(not_tt xorC xor_ff). clear H0 H1; smt(not_tt xorC xor_ff). (* probability agreement: proof that (a) * (b) + (c) * (d) = 1%r / 2%r *) trivial. qed.