(* 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. 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 *) 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 *) 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: *) 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. 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. qed.