(* prob-noninter.ec *) (* two probabilistic interference problems *) prover ["Z3"]. 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. (* first problem *) module M1 = { var x : mybool (* private *) var y : mybool (* public *) proc f() : unit = { var b : mybool; b <$ dmybool; y <- x ^^ b; } }. lemma noninter_M1 : equiv[M1.f ~ M1.f : ={M1.y} ==> ={M1.y}]. (* in the following proof, all uses of smt must explicitly list which lemmas they use, i.e., be of the form smt(...) *) proof. proc. wp. rnd (fun z => M1.x{1} ^^ M1.x{2} ^^ z). skip; progress. smt(xorA xorC xorK xor_ff). smt(dmybool1E). smt(dmybool_fu). smt(xorA xorC xorK xor_ff). smt(xorA xorC xorK xor_ff). qed. (* second problem *) module M2 = { var x : mybool (* private *) var y : mybool (* public *) proc f() : unit = { var b : mybool; if (x = tt) { y <$ dmybool; } else { b <$ dmybool; y <- y ^^ b; } } }. lemma noninter_M2 : equiv[M2.f ~ M2.f : ={M2.y} ==> ={M2.y}]. (* in the following proof, all uses of smt must explicitly list which lemmas they use, i.e., be of the form smt(...) *) proof. proc. if{1}. if{2}. rnd; skip; trivial. wp. rnd (fun z => M2.y{1} ^^ z). skip; progress. smt(xorA xorC xorK xor_ff). smt(dmybool1E). smt(dmybool_fu). smt(xorA xorC xorK xor_ff). if{2}. wp. rnd (fun z => M2.y{1} ^^ z). skip; progress. smt(xorA xorC xorK xor_ff). smt(dmybool1E). smt(dmybool_fu). smt(xorA xorC xorK xor_ff). wp; rnd; skip; trivial. qed.