Following program is rejected by EasyCrypt with that message:
* In [lemmas or axioms]:/ [frag -1.0B])
lemma eq:
forall (M_T <: T),
equiv[ M_T.f ~ Sim(M_T).g : ={glob M_T} ==> ={glob M_T, res}].
[critical] [: line 1 (0) to line 39 (27)] call cannot be used with a lemma referring to `M.f/Sim(M).g': the last statement is a call to `M.f/M_T'.g'
module type T = {
proc f(): bool
}.
module type T' (O : T) = {
proc g(): bool
}.
module Sim (O : T) = {
proc g() = {
var r;
r <@ O.f();
return r;
}
}.
section Bad.
declare module M_T <: T.
module M_T' = Sim(M_T). (* This should fail: M_T' should be required to be marked as local *)
equiv eq: M_T.f ~ M_T'.g: ={glob M_T} ==> ={glob M_T, res}.
proof. by proc *; inline *; sim. qed.
end section Bad.
print eq.
module M = {
var b : bool
proc f() = {
b <- !b;
return b;
}
}.
equiv eq': M.f ~ M_T'.g: ={glob M} ==> ={glob M, res}.
proof. proc *. call (eq M).
Following program is rejected by EasyCrypt with that message: