Skip to content

fix(env): keep calls to applied parameters in partial applications - #1229

Open
strub wants to merge 1 commit into
mainfrom
fix-unsuspend-oinfos
Open

strub wants to merge 1 commit into
mainfrom
fix-unsuspend-oinfos

Conversation

@strub

@strub strub commented Nov 6, 2026

Copy link
Copy Markdown
Member

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.

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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Unsound: a module can call its parameter S even though its module type forbids it

1 participant