(* mod3.ec *) prover ["Z3"]. require import AllCore IntDiv. module M = { var x : int (* private *) var y : int (* public *) proc f() : unit = { if (M.x %% 3 = 0) { (* %% is integer mod *) M.y <- M.y + 3; } elif (M.x %% 3 = 1) { M.y <- M.y + 2; } else { M.y <- M.y + 1; } M.y <- M.y + (M.x %% 3); } }. lemma noninter : equiv[M.f ~ M.f : ={M.y} ==> ={M.y}]. proof. (* NOTE: in this proof, you may ONLY use wp or auto on goals when BOTH programs consist of ASSIGNMENTS, ONLY this is to make you learn about the one-sided if tactics, if{1} and if{2}, and to learn when to use them instead of the ordinary if tactic *) (* fill in *) qed.