(* xor-loop.ec *) prover ["Z3"]. 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 => //. 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. (* 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 = { (* n: public x: public y: private return value: public *) proc f(n : int, x : mybool, y : mybool) : mybool = { var i : int; (* not visible to observer/adversary *) var b : mybool; (* not visible to observer/adversary *) i <- 0; b <- x; if (0 <= n) { while (i < n) { b <- b ^^ y; i <- i + 1; } if (odd n) { b <- b ^^ y; } } return b; } }. lemma noninter : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. (* fill in *) qed.