(* noninterference results using EasyCrypt's Relational Hoare Logic (RHL) actually, we're using pRHL, which stands for "probabilistic Relational Hoare Logic"; but we're ignoring the probabilistic aspects for now *) require import AllCore IntDiv. prover ["Z3"]. module M1 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { x <- y; } }. (* RHL quadruples are written using equiv[...] *) lemma lem1 : equiv[M1.f ~ M1.f : M1.y{1} = M1.y{2} ==> M1.y{1} = M1.y{2}]. proof. (* note that ={M1.y} is used as abbreviation for M1.y{1} = M1.y{2} *) proc. (* because the programs are the same "in sync", only one copy is displayed *) wp; skip; trivial. qed. module M2 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { y <- x; } }. lemma lem2 : equiv[M2.f ~ M2.f : ={M2.y} ==> ={M2.y}]. proof. proc. wp; skip. abort. (* abort this proof *) module M3 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { y <- x; y <- 5; } }. lemma lem3 : equiv[M3.f ~ M3.f : ={M3.y} ==> ={M3.y}]. proof. proc. wp; skip; trivial. qed. module M4 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { if (y %% 3 = 0) { x <- 0; } else { x <- 1; } } }. lemma lem4 : equiv[M4.f ~ M4.f : ={M4.y} ==> ={M4.y}]. proof. proc. if. (* two-sided if *) trivial. auto. (* automates wp;skip;trivial *) auto. qed. module M5 = { var x : int (* private *) var y : int (* public *) proc f() : unit = { if (x %% 3 = 0) { y <- 0; } else { y <- 1; } } }. lemma lem5 : equiv[M5.f ~ M5.f : ={M5.y} ==> ={M5.y}]. proof. proc. wp; skip; progress. abort. require import List. (* 'a list is the type of finite lists of type 'a ('a is a type variable - may stand for any type) these operators are polymorphic: size : 'a list -> int nth : 'a -> 'a list -> int -> 'a nth def ys i means: return the ith element of ys (counting from 0), if 0 <= i < size ys; return def, otherwise *) module M6 = { var i : int (* public *) var xs : int list (* public *) var ys : int list (* private *) var r : bool (* private *) proc f() : unit = { i <- 0; r <- false; while (i < 10) { if (! (nth 0 xs i = nth 1 ys i)) { r <- true; } i <- i + 1; } } }. lemma lem6 : equiv[M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs}]. proof. proc. (* seq is now given number of statements to take from left-side, followed by number of statements to take from right-side *) seq 2 2 : (={M6.i, M6.xs}). auto. while (={M6.i, M6.xs}). (* can't use two-sided if here; try it! *) if{1}. (* one-sided if-then-else - left *) if{2}. (* one-sided if-then-else - right *) auto. auto. if{2}. auto. auto. auto. qed. lemma lem6' : equiv[M6.f ~ M6.f : ={M6.i, M6.xs} ==> ={M6.i, M6.xs} /\ M6.i{1} = 10]. (* changed the postcondition to illustrate the while tactic better *) proof. proc. (* we don't have to do initial seq, as while operates on last statements *) while (={M6.i, M6.xs} /\ M6.i{1} <= 10). (* wp can also push if-then-else-s involving assignments into postcondition; so we can use auto *) auto; smt(). auto; smt(). qed.