From d1b2b50c6d71a0d1c6209d02e407639e057aaf79 Mon Sep 17 00:00:00 2001
From: Xingyu Xie <namasikanam@gmail.com>
Date: Fri, 28 Aug 2026 14:56:05 +0200
Subject: [PATCH] fix(sim): eqobs_in must not assume abstract call preserves
 glob A for distinct oracles

`f_eqobs_in` (FBabs case, ecPhlEqobs.ml) unconditionally added `={glob A}` to
the invariant inferred for an abstract call `A(O_l) ~ A(O_r)` (`Mpv2.add_glob
top top eqi`), asserting the call preserves the adversary's globals without
checking the oracle pair. With two distinct oracles where the right one writes
a global belonging to `glob A`, `={glob A}` is not actually preserved, so `sim`
inferred a false

    equiv[ A(O1).main ~ A(O2).main : ={glob A} ==> ={res} ]

(turned into a proof of `false` via byequiv). This is the eqobs_in analogue of
the equivF_abs oracle-footprint bug.

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.

Regression: tests/eqobs-abs-oracle-glob.ec (the `proc*; sim` proof must fail).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 src/phl/ecPhlEqobs.ml          | 18 ++++++++++++++++++
 tests/eqobs-abs-oracle-glob.ec | 25 +++++++++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 tests/eqobs-abs-oracle-glob.ec

diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml
index ed2122ab9..519e94416 100644
--- a/src/phl/ecPhlEqobs.ml
+++ b/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 ->
diff --git a/tests/eqobs-abs-oracle-glob.ec b/tests/eqobs-abs-oracle-glob.ec
new file mode 100644
index 000000000..dcfb9a631
--- /dev/null
+++ b/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.