[namasikanam]

sim or outline (via f_eqobs_in) infers a false equivalence between two abstract-function calls
A(O1).main ~ A(O2).main when the two oracles differ and one of them writes a global that
belongs to glob A. This yields a proof of false with no axioms/admits/clones.

Proof of false

require import AllCore.
module Shared = { var g : int }.
module type O = { proc f() : unit }.
module type Adv (M : O) = { proc main() : int }.
module O1 : O = { proc f() : unit = { } }.
module O2 : O = { proc f() : unit = { Shared.g <- Shared.g + 1; } }.

section.
declare module A <: Adv.
(* Accepted, but FALSE: O2 writes Shared.g, which is in glob A. *)
lemma bad : equiv[ A(O1).main ~ A(O2).main : ={glob A} ==> ={res} ].
proof. proc*. sim. qed.
end section.

module C (M : O) = { proc main() : int = { M.f(); return Shared.g; } }.
module GL = { proc run() : int = { var r; Shared.g <- 5; r <@ C(O1).main(); return r; } }.
module GR = { proc run() : int = { var r; Shared.g <- 5; r <@ C(O2).main(); return r; } }.

lemma eqrun : equiv[ GL.run ~ GR.run : true ==> ={res} ].
proof. proc. call (bad C). auto. qed.

lemma contradiction &m : false.
proof.
have h1 : Pr[GL.run() @ &m : res = 5] = 1%r by byphoare => //; proc; inline*; auto.
have h0 : Pr[GR.run() @ &m : res = 5] = 0%r by byphoare => //; hoare; proc; inline*; auto.
have heq : Pr[GL.run() @ &m : res = 5] = Pr[GR.run() @ &m : res = 5] by byequiv eqrun => //.
smt().
qed.

Instantiating A with C (which returns Shared.g) and running from Shared.g = 5, the left
side returns 5 and the right returns 6, so the results genuinely differ; the false equiv
equates their probabilities, giving 1 = 0.