(* 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; } }. (* two proofs are below: *) lemma noninter : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. proc; simplify. seq 2 2 : (={n, i, b} /\ i{1} = 0). auto. if => //. seq 1 1 : (={n} /\ (even n{1} => ={b}) /\ (odd n{1} => b{1} ^^ y{1} = b{2} ^^ y{2})). while (={n, i} /\ i{1} <= n{1} /\ (even i{1} => ={b}) /\ (odd i{1} => b{1} ^^ y{1} = b{2} ^^ y{2})). auto; progress; smt(xorA xorK). auto; smt(). if => //; auto; smt(). qed. lemma noninter' : equiv[M.f ~ M.f : ={n, x} ==> ={res}]. proof. proc; simplify. seq 2 2 : (={n, x, i, b} /\ i{1} = 0 /\ b{1} = x{1}). auto. if => //. seq 1 1 : (={n, x} /\ (even n{1} => ={b} /\ b{1} = x{1}) /\ (odd n{1} => b{1} = x{1} ^^ y{1} /\ b{2} = x{2} ^^ y{2})). while (={n, x, i} /\ i{1} <= n{1} /\ (even i{1} => ={b} /\ b{1} = x{1}) /\ (odd i{1} => b{1} = x{1} ^^ y{1} /\ b{2} = x{2} ^^ y{2})). auto; progress; smt(xorA xorK xor_ff). auto; progress; smt(). if => //; auto; progress; smt(xorA xorK). qed.