fix(sim): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

[namasikanam]

Summary

sim (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. It is the
eqobs_in analogue of the equivF_abs glob-A oracle-footprint bug fixed in #1099, but in a
separate file and tactic (ecPhlEqobs.ml / sim, not ecPhlFun.ml / proc), so #1099
does not cover it.

Proof of false on current main

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.

Root cause

In f_eqobs_in's FBabs case, the inferred invariant unconditionally gets ={glob top} added
(Mpv2.add_glob env top top eqi), asserting the abstract call preserves the adversary's globals
— without checking the oracle pair ((* TODO check that inv contain only global *)). With
distinct oracles where the right one writes a global in glob A, that equality is not actually
preserved.

Fix

Only add ={glob top} when, for every oracle pair, the two oracles are the same procedure
(same code ⇒ mirrored writes to glob top) or neither modifies glob top; otherwise the
simulation cannot be inferred and eqobs_in falls back to requiring a user-supplied
specification. The common identical-oracle case is unaffected.

Validation

• Witness above: accepted on main, rejected after the fix.
• Full stdlib (128/128) + examples + unit: clean (no legitimate sim proof regresses).
• Regression test tests/eqobs-abs-oracle-glob.ec.