(* rnd-phl.ec *) (* an extension of the example rnd.ec, illustrating how more complex EasyCrypt's probabilistic Hoare logic (pHL) proofs may be done search for "NEW" for extension *) (* 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. (* 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 => //. rewrite xor_tt_ff xor_ff_tt //. case y => //. 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. rewrite xor_ff_tt xor_tt_tt xor_tt_ff //. rewrite xor_ff_ff xor_tt_ff xor_tt_tt //. case z. rewrite xor_tt_ff xor_tt_tt xor_ff_tt xor_tt_tt //. rewrite xor_tt_ff xor_tt_ff xor_ff_ff xor_tt_ff //. case y. rewrite xor_ff_tt. case z. rewrite xor_tt_tt xor_ff_ff //. rewrite xor_tt_ff xor_ff_tt //. case z. rewrite xor_ff_ff xor_ff_tt xor_ff_tt //. 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 *) 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. rewrite xorA xorK xor_ff //. rewrite 2!dmybool1E //. rewrite dmybool_fu. rewrite xorA xorK xor_ff //. rewrite xorC xorA 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 => //. apply 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 *) rewrite 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. rewrite -(M_N_tt &m) (M_tt &m) //. qed. (************************************ NEW ************************************) (* but suppose we wanted to prove N_tt directly, using pHL? *) lemma N_tt' &m : Pr[N.f() @ &m : res = tt] = 1%r / 2%r. proof. qed. (* multi-argument seq works similarly when the bound is <= *)