(* xor-loop.ec *) prover quorum=2 ["Z3" "Alt-Ergo"]. require import AllCore IntDiv. (* a type mybool with elements tt standing for "true" and ff standing for "false", and an exclusive or operator ^^: *) type mybool = [tt | ff]. 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. (* define even, odd : int -> bool SMT provers know about %%, so smt() can reason about even and odd *) op even (k : int) = k %% 2 = 0. (* %% is mod *) op odd (k : int) = ! even k. module M = { proc f(n : int, (* public *) x : mybool, (* public *) y : mybool) (* private *) : mybool = { (* public *) var i : int; (* not visible to observer *) var b : mybool; (* not visible to observer, but returned *) i <- 0; b <- x; if (0 <= n) { while (i < n) { b <- b ^^ y; i <- i + 1; } if (odd n) { b <- b ^^ y; } } return b; } }. (* four noninterference proofs are below: *) lemma noninter1 : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. qed. lemma noninter1' : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. qed. lemma noninter2 : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. qed. lemma noninter2' : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. qed.