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

src/phl/ecPhlEqobs.ml

@@ -341,6 +341,24 @@ and f_eqobs_in fl fr sim eqO =
             PV.check_depend env fvr topr
           with TcError _ -> raise EqObsInError
         end;
+        (* Adding [={glob top}] below asserts the abstract call preserves the
+           adversary's globals. That is sound only if, for every oracle pair,
+           either the two oracles are the SAME procedure (same code => mirrored
+           writes to [glob top]) or neither oracle modifies [glob top]. With
+           distinct oracles where one writes a global in [glob top], the
+           equality is NOT preserved and must not be assumed (otherwise a false
+           [equiv[ A(O1) ~ A(O2) : ={glob A} ==> ={res} ]] is inferred). *)
+        let restr_of adv =
+          { mr_empty with ur_neg = (Sx.empty, Sm.singleton adv) } in
+        let oracle_ok o_l o_r =
+          EcPath.x_equal o_l o_r ||
+          (try
+             EcTyping.check_mem_restr_fun env o_l (restr_of topl);
+             EcTyping.check_mem_restr_fun env o_r (restr_of topr);
+             true
+           with _ -> false) in
+        if not (List.for_all2 oracle_ok (OI.allowed oil) (OI.allowed oir)) then
+          raise EqObsInError;
         sim, (Mpv2.add_glob env top top eqi)
 
       | FBdef funl, FBdef funr ->

tests/eqobs-abs-oracle-glob.ec

@@ -0,0 +1,25 @@
+(* Regression for the eqobs_in / `sim` abstract-oracle glob drop.
+
+   `f_eqobs_in` (FBabs case, ecPhlEqobs.ml) unconditionally added `={glob A}`
+   to the inferred invariant of an abstract call, asserting the call preserves
+   the adversary's globals without checking the oracle pair. Here the right
+   oracle O2 writes the concrete global Shared.g (which unrestricted `A` may
+   touch, so Shared.g in glob A) while the left oracle O1 does not, so
+   `={glob A}` is NOT preserved and this equiv must not be provable by `sim`.
+   Before the fix `proc*; sim` closed it (a proof of `false` followed). *)
+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.
+
+lemma bad : equiv[ A(O1).main ~ A(O2).main : ={glob A} ==> ={res} ].
+proof.
+fail (by proc*; sim).
+abort.
+end section.