Summary
Applying a fine-grained module update to a submodule whose body references the
enclosing module's global variables produces a module that (a) contains
references to a global the new module never declares, (b) whose intended
semantics is silently changed, and (c) is nevertheless accepted and fully usable
by the program logics — hoare judgments about it can be stated and proved, with
assignments stepping through the phantom variable.
Observed on 761aaf2 (2026-07-01).
Reproduction
require import AllCore.
module P = {
var g : int
module O = {
proc f() : int = { g <- g + 1; return g; }
}
}.
module Q = P.O with {
proc f [ 1 + { P.g <- P.g + 2; } ]
}.
print Q.
This outputs:
module Q = {
proc f() : int = {
Q.g <- Q.g + 1; (* <- re-rooted parent global: Q declares no `g' *)
P.g <- P.g + 2;
return Q.g;
}
}.
This causes the following problems:
1. Dangling reference. Q.g cannot be named in any formula:
hoare[ Q.f : Q.g = 0 ==> Q.g = 1 ] fails with
unknown variable or constant: `Q.g'.
2.Silently changed semantics. The base P.O.f increments P.g, so a
faithful patch would take P.g from 0 to 3. Instead the increment lands on
the phantom, and the following proves:
lemma semantics_changed : hoare[ Q.f : P.g = 0 ==> P.g = 2 ].
proof. by proc; auto. qed.
3. The phantom is steppable. proc/auto/wp happily walk through the
assignment to Q.g — the logics assign meaning to a program referencing
undeclared state. This is why I'd class it as (at least adjacent to) a
soundness issue rather than a usability wart.
Summary
Applying a fine-grained module update to a submodule whose body references the
enclosing module's global variables produces a module that (a) contains
references to a global the new module never declares, (b) whose intended
semantics is silently changed, and (c) is nevertheless accepted and fully usable
by the program logics — hoare judgments about it can be stated and proved, with
assignments stepping through the phantom variable.
Observed on 761aaf2 (2026-07-01).
Reproduction