Declared operators can indirectly leak into modules

[oskgo]

The section mechanism allows defining abstract operators, types and modules (maybe more?) that act as though they were defined inside the section but become parameters of their dependees inside the section when concluding the section. This only works properly when EasyCrypt supports making the dependees parametric, but some things like modules cannot currently be parameterized by operators and types.

Because of these issues with modules in sections EasyCrypt tries to prevent usage of declared operators and types in modules. The current checks do not take into account transitive usages.

Example:

theory Thy.
section.

declare type _T.
type T = _T.
declare op _f: T.
op f: T = _f.

module M = {proc main() = {return f;}}.

end section.
end Thy.
print Thy.

On a side note, it seems to me like sections are a leaky abstraction in a language like EasyCrypt where not everything can be made parametric in terms of everything else.

[oskgo]

A fix should also take into account clones like the following:

theory TO.

type _T.
type T = _T.
op _f: T.
op f: T = _f.

module M = {proc main() = {return f;}}.

end TO.

theory Thy.
section.

declare type _T.
type T = _T.
declare op _f: T.

clone include TO with
type _T <- _T,
type T <- T,
op _f <- _f.

end section.
end Thy.

print Thy.

The current logic handles clones just fine in the non-transitive case, but I could see this needing special care when handling transitive dependencies.