fix(equiv): equivF_abs must check the glob-A oracle footprint on both oracles

src/phl/ecPhlFun.ml

@@ -205,8 +205,7 @@ module FunAbsLow = struct
       let use =
         try
           check_oracle_use pf env topl o_l;
-          if   EcPath.x_equal o_l o_r
-          then check_oracle_use pf env topl o_r;
+          check_oracle_use pf env topr o_r;
           false
         with _ -> true
       in
@@ -330,8 +329,7 @@ module UpToLow = struct
 
     let ospec o_l o_r =
       check_oracle_use pf env topl o_l;
-      if   EcPath.x_equal o_l o_r
-      then check_oracle_use pf env topl o_r;
+      check_oracle_use pf env topr o_r;
 
       let fo_l = EcEnv.Fun.by_xpath o_l env in
       let fo_r = EcEnv.Fun.by_xpath o_r env in

tests/equivf-abs-oracle-glob.ec

@@ -0,0 +1,31 @@
+(* Regression for the equivF_abs oracle-footprint asymmetry.
+
+   `equiv ... proc` for an abstract adversary must require that BOTH oracles
+   leave `glob A` unchanged, not only the left one. Here the right oracle O2
+   writes the concrete global Shared.g (which an unrestricted `A` may touch, so
+   Shared.g in glob A) while the left oracle O1 does not, so the `={glob A}`
+   invariant is not preserved by the oracle pair and this equiv is not provable.
+
+   Before the fix `check_oracle_use` was run on the right oracle only when
+   o_l = o_r, so the distinct-oracle case silently dropped the obligation and
+   the proof below closed (and could be turned into a proof of `false`). With
+   the fix the O2 `={glob A}` obligation remains, so the closing `by` must
+   fail. *)
+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 (true) => //; proc; auto).
+abort.
+end section.

theories/query_counting/Counter.eca

@@ -35,7 +35,7 @@ module Counter(S : System) = {
 
 section.
   declare module S <: System { -Counter }.
-  declare module D <: Distinguisher { -S }.
+  declare module D <: Distinguisher { -S, -Counter }.
 
 
   lemma ind_counting (E : (glob S) -> bool) &m: