(* prob-noninter.ec *) (* three probabilistic interference examples *) prover quorum=2 ["Alt-Ergo" "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 => //. 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 *) 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 example *) module M1 = { var x : mybool (* private *) var y : mybool (* public *) proc f() : unit = { var b : mybool; b <\$ dmybool; y <- x ^^ b; } }. lemma lem1 : equiv[M1.f ~ M1.f : ={M1.y} ==> ={M1.y}]. 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). by apply H. smt(xorA xorC xorK xor_ff). qed. (* second example *) module M2 = { var x : mybool (* private *) var y : mybool (* public *) proc f() : unit = { var b : mybool; if (x = tt) { b <\$ dmybool; if (b = tt) { y <- y ^^ tt; } } else { b <- ff; } y <- y ^^ b; } }. lemma lem2 : equiv[M2.f ~ M2.f : ={M2.y} ==> ={M2.y}]. proof. proc. wp. if{1}. if{2}. seq 1 1 : (={M2.y, b}). rnd. auto. auto. seq 1 0 : (={M2.y}). rnd{1}. skip; smt(dmybool_ll). auto; progress. smt(xorA xorK). smt(). if{2}. seq 0 1 : (={M2.y}). rnd{2}. skip; smt(dmybool_ll). auto; progress. smt(xorA xorK). smt(). auto. qed. lemma lem2' : equiv[M2.f ~ M2.f : ={M2.y} ==> ={M2.y}]. proof. proc. if{1}; if{2}; wp. (* first case *) auto. (* second case *) auto; progress. smt(dmybool_ll). smt(xorA xorK). smt(). (* third case *) auto; progress. smt(dmybool_ll). smt(xorA xorK). smt(). (* fourth case *) auto. qed. (* third example *) module M3 = { 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 lem3 : equiv[M3.f ~ M3.f : ={M3.y} ==> ={M3.y}]. proof. proc. if{1}; if{2}; wp. (* first case *) auto. (* second case *) rnd (fun z => M3.y{2} ^^ z). skip; progress. smt(xorA xorC xorK xor_ff). smt(dmybool1E). smt(dmybool_fu). by apply H0. (* third case *) rnd (fun z => M3.y{1} ^^ z). skip; progress. smt(xorA xorC xorK xor_ff). smt(dmybool1E). smt(dmybool_fu). by apply H0. (* fourth case *) auto. qed.