From d5a770933b58f6bdf4965d57ad5c08b51d7660ba Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 6 Nov 2026 14:49:00 +0100
Subject: [PATCH] fix(env): keep calls to applied parameters in partial
 applications

Fixes #1175.

When a functor is partially applied, `Mod.unsuspend` keeps the oracle
calls whose target is one of the remaining parameters. It compared the
full target of the call with the parameter, so a call such as
`S(M).kg`, whose target is `S(M)` and not `S`, was dropped even when
`S` is a remaining parameter.

The partial application then looked as if it made no call at all. In
the example of the issue, the following module is accepted at `Adv`,
whose `run` may call nothing:

    module (B (D : T) : Adv) (S : Sch) = {
      proc run() : unit = { S(M).kg(); }
    }.

and so is the instantiation of `A <: Adv {-St}` by `B(M)`, which is
enough to prove `false`.

The filter now compares the functor of the target, as `get_oi_calls`
already does when it computes the calls of a module. `ModTy.sig_of_mt`
uses the same filter and is changed in the same way.
---
 src/ecEnv.ml                      |  4 +--
 tests/partial-app-oracle-calls.ec | 46 +++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 2 deletions(-)
 create mode 100644 tests/partial-app-oracle-calls.ec

diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index f287afbba..bfc7215fa 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -1997,7 +1997,7 @@ module Mod = struct
         let me_oinfos =
           let keep = List.map (EcPath.mident -| fst) me_params in
           let keep = Sm.of_list keep in
-          Msym.map (OI.filter (fun f -> Sm.mem (f.x_top) keep)) me.me_oinfos in
+          Msym.map (OI.filter (fun f -> Sm.mem (m_functor f.x_top) keep)) me.me_oinfos in
 
         { me with me_params; me_oinfos; }
     in
@@ -2258,7 +2258,7 @@ module ModTy = struct
 
     let keep = List.map (EcPath.mident -| fst) params in
     let keep = Sm.of_list keep in
-    let ois = Msym.map (OI.filter (fun f -> Sm.mem (f.x_top) keep)) ois in
+    let ois = Msym.map (OI.filter (fun f -> Sm.mem (m_functor f.x_top) keep)) ois in
 
     { mis_params = params;
       mis_body   = items;
diff --git a/tests/partial-app-oracle-calls.ec b/tests/partial-app-oracle-calls.ec
new file mode 100644
index 000000000..dcacbc129
--- /dev/null
+++ b/tests/partial-app-oracle-calls.ec
@@ -0,0 +1,46 @@
+(* Regression for #1175: partially applying a functor must keep the
+   calls to its remaining parameters, including calls to an applied
+   parameter such as `S(M).kg`. Dropping them let `B (D : T) (S : Sch)`
+   be cast to (or instantiate) an adversary type forbidding those calls. *)
+require import AllCore.
+
+module type T   = { }.
+module type Sch (X : T) = { proc kg() : unit }.
+module type Adv (S : Sch) = { proc run() : unit }.
+
+module M : T = { }.
+
+module St (X : T) = {
+  var c : int
+  proc kg() : unit = { c <- c + 1; }
+}.
+
+(* Without a leading parameter: rejected. *)
+fail module (B' : Adv) (S : Sch) = {
+  proc run() : unit = { S(M).kg(); }
+}.
+
+(* With a leading parameter: must be rejected as well. *)
+fail module (B (D : T) : Adv) (S : Sch) = {
+  proc run() : unit = { S(M).kg(); }
+}.
+
+(* A leading parameter alone does not make the cast fail. *)
+module (C (D : T) : Adv) (S : Sch) = {
+  proc run() : unit = { }
+}.
+
+(* Without the cast, `B(M)` must not instantiate an `Adv`. *)
+module B (D : T) (S : Sch) = {
+  proc run() : unit = { S(M).kg(); }
+}.
+
+lemma frame (A <: Adv {-St}) n :
+  hoare [A(St).run : St.c = n ==> St.c = n].
+proof. by proc (St.c = n). qed.
+
+lemma ok : hoare [C(M, St).run : St.c = 0 ==> St.c = 0].
+proof. exact (frame (C(M)) 0). qed.
+
+lemma bad : hoare [B(M, St).run : St.c = 0 ==> St.c = 0].
+proof. fail exact (frame (B(M)) 0). abort.