(* Exercise 2: A Simple Probabilistic Noninterference Exercise *) prover [""]. (* no use of SMT solvers *) require import AllCore Distr. (* a type mybool with elements T standing for "true" and F standing for "false", and an exclusive or operator ^^: *) type mybool = [T | F]. 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: *) axiom xor_T_T : T ^^ T = F. axiom xor_T_F : T ^^ F = T. axiom xor_F_T : F ^^ T = T. axiom xor_F_F : F ^^ F = F. (* lemmas for exclusive or: *) (* false on the right *) lemma xor_F (x : mybool) : x ^^ F = x. proof. case x; [apply xor_T_F | apply xor_F_F]. qed. (* cancelling *) lemma xorK (x : mybool) : x ^^ x = F. proof. case x; [apply xor_T_T | apply xor_F_F]. qed. (* commutativity *) lemma xorC (x y : mybool) : x ^^ y = y ^^ x. case x. case y => //. rewrite xor_T_F xor_F_T //. case y => //. rewrite xor_F_T xor_T_F //. qed. (* associativity *) lemma xorA (x y z : mybool) : (x ^^ y) ^^ z = x ^^ (y ^^ z). proof. case x. case y. rewrite xor_T_T. case z. rewrite xor_F_T xor_T_T xor_T_F //. rewrite xor_F_F xor_T_F xor_T_T //. case z. rewrite xor_T_F xor_T_T xor_F_T xor_T_T //. rewrite xor_T_F xor_T_F xor_F_F xor_T_F //. case y. rewrite xor_F_T. case z. rewrite xor_T_T xor_F_F //. rewrite xor_T_F xor_F_T //. case z. rewrite xor_F_F xor_F_T xor_F_T //. rewrite xor_F_F xor_F_F //. qed. (* a sub-distribution dmybool on mybool - this means that the sum of the weights of T and F in dmybool may be less than 1 *) op dmybool : mybool distr. (* dmybool is a distribution, i.e., the sum of the weights of T and F 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 weight 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 T and F have weight 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 T and F have non-zero weights in dmybool: *) lemma dmybool_fu : is_full dmybool. proof. rewrite /is_full => x. rewrite /support dmybool1E StdOrder.RealOrder.divr_gt0 //. qed. (* consider the following module with two global variables, one that we think of as private and one that we think of as public: *) module M = { var x : mybool (* private *) var y : mybool (* public *) proc f() : unit = { var b : mybool; b <\$ dmybool; y <- y ^^ x ^^ b; } }. (* here is the probabilistic noninterference lemma for M.f: *) lemma noninter_M : equiv[M.f ~ M.f : ={M.y} ==> ={M.y}]. proof. (* BEGIN FILL IN *) (* END FILL IN *) qed.