From 2cd9b21d7ebf550451d2671d56f559bbe2e9ff07 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Thu, 23 Jul 2026 19:59:12 +0100 Subject: [PATCH] fix(typing): sound module updates on sub-module and applied-functor bases `module M' = B with {...}` re-rooted references using only the TOP path of the base mpath, appending the reference's arguments to the destination's. Consequences: - a sub-module base P.O had every P-rooted reference re-rooted onto M': the enclosing module's state (P.g -> M'.g) and even the sub-module's own state (P.O.x -> M'.O.x) became dangling globals, silently changing the program's semantics while remaining fully usable by the program logics; - a functor base F(A) whose body contains self-calls crashed the elaborator (assertion failure in EcEnv.Fun.by_xpath): the self-call F(A).h, unsuspended at A, was rewritten to M'(A).h with M' not a functor. The substitution entry now records the full base expression (top path, arguments, inner path) and rewrites a reference iff it lies at or below the base's inner path AND its arguments extend the base's (references to program variables carry no arguments); the remainders are transplanted onto the destination. Non-matching references (an enclosing module's state, sibling sub-modules, other applications) denote state that is not copied along with the base's items, and are left untouched. This makes updates of sub-modules (P.O), applied functors (F(A)), and sub-modules of applied functors (F(A).O) all well-defined: the base's items are copied, everything else is shared, and the application is baked into the copy. Behavior for plain top-level bases and for section-exit alias inlining is unchanged (empty argument and inner-path components). Also: reject abstract-module bases with a proper error instead of an assertion, and add regression tests covering every base shape. --- src/ecSection.ml | 3 +- src/ecSubst.ml | 118 ++++++++++++++++++---- src/ecSubst.mli | 6 +- src/ecTyping.ml | 15 ++- tests/module-update-bases.ec | 183 +++++++++++++++++++++++++++++++++++ 5 files changed, 301 insertions(+), 24 deletions(-) create mode 100644 tests/module-update-bases.ec diff --git a/src/ecSection.ml b/src/ecSection.ml index fd3db896b..600a4507a 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1072,7 +1072,8 @@ let generalize_module to_gen prefix me = with Inline -> let to_gen = { to_gen with tg_subst = EcSubst.add_moddef - ~src:(EcPath.pqname prefix me.tme_expr.me_name) + ~src:(EcPath.mpath_crt + (EcPath.pqname prefix me.tme_expr.me_name) [] None) ~dst:mp to_gen.tg_subst } in to_gen, None end diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 6dbf75ad4..1cbf0d5a6 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -24,6 +24,29 @@ exception SubstNameClash of subst_name_clash exception InconsistentSubst (* -------------------------------------------------------------------- *) +(* A module-definition substitution: references to a source module + expression are re-rooted onto a destination module. The source is a + concrete module expression [P(a1..an).q] (possibly applied, possibly + a sub-module), recorded as its top-level path [P] (the map key), its + arguments [sm_args] and its inner path [sm_sub]. A reference + [`Concrete (P, sub)] applied at [args] is rewritten iff: + + - [sub] lies at or below [sm_sub] (trivially true when [sm_sub] is + [None]); and + - [args] is empty (references to program variables carry no + arguments) or extends [sm_args]. + + The remainders (the inner path below [sm_sub], the arguments beyond + [sm_args]) are transplanted onto the destination. References that do + not match (an enclosing module's state, sibling sub-modules, other + applications) denote state that is not copied along with the source's + items, and are left untouched. See [subst_mpath]. *) +type sub_moddef = { + sm_args : EcPath.mpath list; + sm_sub : EcPath.path option; + sm_dst : EcPath.mpath; +} + type subst = { sb_module : EcPath.mpath Mid.t; sb_path : EcPath.path Mp.t; @@ -33,7 +56,7 @@ type subst = { sb_fmem : EcIdent.t Mid.t; sb_tydef : (EcIdent.t list * ty) Mp.t; sb_def : (EcIdent.t list * [`Op of expr | `Pred of form]) Mp.t; - sb_moddef : EcPath.mpath Mp.t; (* Only top-level modules *) + sb_moddef : sub_moddef Mp.t; (* keyed by the source's TOP-LEVEL path *) } (* -------------------------------------------------------------------- *) @@ -74,28 +97,74 @@ let rec _subst_path (s : EcPath.path Mp.t) (p : EcPath.path) = let subst_path (s : subst) (p : EcPath.path) = _subst_path s.sb_path p (* -------------------------------------------------------------------- *) +(* Try to match a reference [`Concrete (p, sub)] at (substituted) + arguments [args] against a module-definition entry for [p]. On a + match, return the rewritten mpath; otherwise return [None] and let + the caller fall through to the ordinary path substitution. *) +let _moddef_apply (md : sub_moddef) (args : EcPath.mpath list) + (sub : EcPath.path option) : EcPath.mpath option = + (* Sub component: the reference must lie at or below the source's + inner path; the remainder survives below the destination. *) + let sub_rem = + match md.sm_sub with + | None -> Some sub + | Some q -> + match sub with + | None -> None + | Some sp -> + omap + (List.fold_left (fun acc x -> Some (EcPath.pqoname acc x)) None) + (EcPath.remprefix ~prefix:q ~path:sp) + in + + (* Args component: program-variable references carry no arguments; + other self-references are applied at the source's arguments, + possibly further applied. The excess arguments survive after the + destination's own. ([sm_args] is compared as recorded: the callers + build single-purpose substitutions, so the reference's arguments + cannot have been rewritten by other entries.) *) + let args_rem = + if List.is_empty args then + Some [] + else if List.length args < List.length md.sm_args then + None + else + let pre, rest = List.takedrop (List.length md.sm_args) args in + if List.for_all2 EcPath.m_equal pre md.sm_args then Some rest else None + in + + match sub_rem, args_rem with + | Some sub_rem, Some args_rem -> + let (d_p, d_sub, d_args) = + match md.sm_dst with + | { m_top = `Concrete (d_p, d_sub); m_args = d_args } -> + (d_p, d_sub, d_args) + | _ -> assert false in + let cat_sub = + match d_sub with + | None -> sub_rem + | Some d_sub -> Some (EcPath.poappend d_sub sub_rem) in + Some (EcPath.mpath_crt d_p (d_args @ args_rem) cat_sub) + + | _, _ -> None + let subst_mpath (s : subst) (mp : EcPath.mpath) = let rec doit s (mp : EcPath.mpath) = let args = List.map (doit s) mp.m_args in match mp.m_top with - | `Concrete (p, sub) when Mp.mem p s.sb_moddef -> begin - let s_p, s_sub, s_args = - match Mp.find p s.sb_moddef with - | { m_top = `Concrete (s_p, s_sub); m_args } -> (s_p, s_sub, m_args) - | _ -> assert false in - - let cat_sub = - match s_sub with - | None -> sub - | Some s_sub -> Some (EcPath.poappend s_sub sub) in - - EcPath.mpath_crt s_p (s_args @ mp.m_args) cat_sub + | `Concrete (p, sub) -> begin + let rewritten = + obind + (fun md -> _moddef_apply md args sub) + (Mp.find_opt p s.sb_moddef) + in + match rewritten with + | Some mp -> mp + | None -> + let p = _subst_path s.sb_path p in + EcPath.mpath_crt p args sub end - | `Concrete (p, sub) -> - let p = _subst_path s.sb_path p in - EcPath.mpath_crt p args sub - | `Local id -> match Mid.find_opt id s.sb_module with | None -> EcPath.mpath_abs id args @@ -284,10 +353,19 @@ let add_pddef (s : subst) p (ids, f) = assert (Mp.find_opt p s.sb_def = None); { s with sb_def = Mp.add p (ids, `Pred f) s.sb_def } -let add_moddef (s : subst) ~(src : EcPath.path) ~(dst : EcPath.mpath) = - assert (Mp.find_opt src s.sb_moddef = None); +(* [src] is a concrete module expression (possibly applied, possibly a + sub-module); references to it (and to its sub-modules) get re-rooted + onto [dst]. See the [sub_moddef] documentation above. *) +let add_moddef (s : subst) ~(src : EcPath.mpath) ~(dst : EcPath.mpath) = + let (p, sub) = + match src.m_top with + | `Concrete (p, sub) -> (p, sub) + | `Local _ -> assert false in + assert (Mp.find_opt p s.sb_moddef = None); assert (EcPath.is_concrete dst); - { s with sb_moddef = Mp.add src dst s.sb_moddef } + { s with sb_moddef = + Mp.add p { sm_args = src.m_args; sm_sub = sub; sm_dst = dst; } + s.sb_moddef } (* -------------------------------------------------------------------- *) let subst_flocal (s : subst) (f : form) = diff --git a/src/ecSubst.mli b/src/ecSubst.mli index 64ae60cf0..79118a3e2 100644 --- a/src/ecSubst.mli +++ b/src/ecSubst.mli @@ -28,7 +28,11 @@ val add_path : subst -> src:path -> dst:path -> subst val add_tydef : subst -> path -> (EcIdent.t list * ty) -> subst val add_opdef : subst -> path -> (EcIdent.t list * expr) -> subst val add_pddef : subst -> path -> (EcIdent.t list * form) -> subst -val add_moddef : subst -> src:path -> dst:mpath -> subst (* Only concrete modules *) +(* Re-root references to the concrete module expression [src] (possibly + applied, possibly a sub-module) onto [dst]. References to an + enclosing module's state, to sibling sub-modules, and to other + applications of the same functor are left untouched. *) +val add_moddef : subst -> src:mpath -> dst:mpath -> subst val add_memory : subst -> EcIdent.t -> EcIdent.t -> subst val add_flocal : subst -> EcIdent.t -> form -> subst diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 1be5f098c..313fff050 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -2185,6 +2185,11 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = if not (List.is_empty sig_.miss_params) then tyerror loc env (InvalidModUpdate MUE_Functor); + (* Prohibit abstract-module updates (a declared module, or a + sub-module of one) *) + if not (EcPath.is_concrete mp) then + tyerror loc env (InvalidModUpdate MUE_AbstractModule); + (* Construct the set of new module variables *) let items = List.concat_map @@ -2201,8 +2206,14 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = let delete_vars = List.map (fun v -> v.pl_desc) delete_vars in let me, _ = EcEnv.Mod.by_mpath mp env in - let p = match mp.m_top with | `Concrete (p, _) -> p | _ -> assert false in - let subst = EcSubst.add_moddef EcSubst.empty ~src:p ~dst:(EcEnv.mroot env) in + (* Re-root references to the base module expression [mp] (its own + state and procedures, sub-modules included, self-references + unsuspended at the base's arguments) onto the module being + defined, whose items are copies of the base's. References to + anything else (an enclosing module's state, sibling sub-modules, + other modules) denote state that is shared with the base, not + copied, and are left untouched. *) + let subst = EcSubst.add_moddef EcSubst.empty ~src:mp ~dst:(EcEnv.mroot env) in let me = EcSubst.subst_module subst me in let update_fun env fn plocals pupdates pupdate_res = diff --git a/tests/module-update-bases.ec b/tests/module-update-bases.ec new file mode 100644 index 000000000..e6c4af08d --- /dev/null +++ b/tests/module-update-bases.ec @@ -0,0 +1,183 @@ +(* ------------------------------------------------------------------------ + Fine-grained module definitions (`module M' = M with {...}`) on bases + beyond a plain top-level module: + + - applied functors: F(A0) with {...} + - re-parameterized functors: (B:T) = F(B) with {...} + - sub-modules: P.O with {...} + - sub-modules of applied functors: F(A0).O with {...} + + Semantics under test: the update copies the base's ITEMS (variables, + procedures, nested sub-modules), re-rooting exactly the references to + those copied items. References to anything else -- an enclosing + module's state, sibling sub-modules, other modules -- denote state that + is NOT copied and stays SHARED with the base. Functor applications + are baked into the copy. + + Regressions covered: + - functor bases whose bodies contain self-calls used to crash the + elaborator (the self-reference is unsuspended at the application's + arguments, which the re-rooting failed to absorb); + - sub-module bases used to re-root references to the enclosing + module's state -- and even to the sub-module's own state -- onto + paths of the new module that do not exist (dangling globals). + ------------------------------------------------------------------------ *) +require import AllCore. + +module type T = { proc run() : int }. + +module A0 : T = { proc run() : int = { return 7; } }. + +(* ====================================================================== + Functor bases with a self-call (`f` calls its sibling `h`). + ====================================================================== *) +module F (B : T) = { + var g : int + proc h() : int = { var r; r <@ B.run(); g <- g + r; return g; } + proc f() : int = { var r; r <@ h(); return r; } +}. + +(* -- applied at a concrete module: the application is baked in --------- *) +module QC = F(A0) with { proc f [ 1 + ^ { g <- 1; } ] }. + +(* QC.g is a fresh copy of F.g; the self-call resolves to QC.h; F's own + state is not touched by running the copy. *) +lemma QC_f : hoare[ QC.f : QC.g = 0 /\ F.g = 5 + ==> QC.g = 8 /\ F.g = 5 /\ res = 8 ]. +proof. by proc; inline *; auto. qed. + +(* -- re-parameterized: same, at a functor parameter -------------------- *) +module QP (B : T) = F(B) with { proc f [ 1 + ^ { g <- 1; } ] }. + +lemma QP_f : hoare[ QP(A0).f : QP.g = 0 ==> QP.g = 8 /\ res = 8 ]. +proof. by proc; inline *; auto. qed. + +(* ====================================================================== + Sub-module bases. + ====================================================================== *) + +(* -- the enclosing module's state is shared, not copied ---------------- *) +module P = { + var g : int + module O = { + proc f() : int = { g <- g + 1; return g; } + } +}. + +(* Inside the patch, the enclosing module's variables are written + qualified (`P.g`): the patch is typed in the new module's scope. *) +module QO = P.O with { proc f [ 1 + { P.g <- P.g + 2; } ] }. + +lemma QO_f : hoare[ QO.f : P.g = 0 ==> P.g = 3 /\ res = 3 ]. +proof. by proc; auto. qed. + +(* the base is unchanged *) +lemma PO_f : hoare[ P.O.f : P.g = 0 ==> P.g = 1 /\ res = 1 ]. +proof. by proc; auto. qed. + +(* -- the sub-module's own state is copied ------------------------------ *) +module P2 = { + module O = { + var x : int + proc f() : int = { x <- x + 1; return x; } + } +}. + +module QX = P2.O with { proc f [ 1 + { x <- x + 2; } ] }. + +lemma QX_f : hoare[ QX.f : QX.x = 0 /\ P2.O.x = 5 + ==> QX.x = 3 /\ P2.O.x = 5 /\ res = 3 ]. +proof. by proc; auto. qed. + +(* -- self-calls inside the sub-module re-root to the copy -------------- *) +module P3 = { + module O = { + var n : int + proc get() : int = { n <- n + 1; return n; } + proc sample() : unit = { var d; d <@ get(); } + } +}. + +module QS = P3.O with { proc sample [ var e : int 1 + { e <@ get(); } ] }. + +lemma QS_sample : hoare[ QS.sample : QS.n = 0 /\ P3.O.n = 5 + ==> QS.n = 2 /\ P3.O.n = 5 ]. +proof. by proc; inline *; auto. qed. + +(* -- nested sub-modules are copied along ------------------------------- *) +module P4 = { + module O = { + module M = { + var y : int + proc bump() : unit = { y <- y + 1; } + } + proc f() : int = { M.bump(); return M.y; } + } +}. + +module QN = P4.O with { proc f [ 1 + ^ { M.y <- 5; } ] }. + +lemma QN_f : hoare[ QN.f : P4.O.M.y = 0 + ==> QN.M.y = 6 /\ P4.O.M.y = 0 /\ res = 6 ]. +proof. by proc; inline *; auto. qed. + +(* ====================================================================== + Sub-module of an applied functor: the functor's enclosing state is + shared (it is application-independent), the sub-module's state is + copied, and the application is baked in. + ====================================================================== *) +module G (B : T) = { + var g : int + module O = { + var x : int + proc f() : int = { var r; r <@ B.run(); g <- g + r; x <- x + 1; return x; } + } +}. + +module QD = G(A0).O with { proc f [ 1 + ^ { x <- x + 2; } ] }. + +lemma QD_f : hoare[ QD.f : QD.x = 0 /\ G.g = 0 /\ G.O.x = 5 + ==> QD.x = 3 /\ G.g = 7 /\ G.O.x = 5 /\ res = 3 ]. +proof. by proc; inline *; auto. qed. + +(* -- and the re-parameterized variant of the same ----------------------- *) +module QE (B : T) = G(B).O with { proc f [ 1 + ^ { x <- x + 2; } ] }. + +lemma QE_f : hoare[ QE(A0).f : QE.x = 0 /\ G.g = 0 + ==> QE.x = 3 /\ G.g = 7 /\ res = 3 ]. +proof. by proc; inline *; auto. qed. + +(* ====================================================================== + Multi-parameter functors: the argument prefix has length > 1. + ====================================================================== *) +module A1 : T = { proc run() : int = { return 11; } }. + +module H (B1 : T) (B2 : T) = { + var g : int + proc h() : int = { + var r1, r2; + r1 <@ B1.run(); + r2 <@ B2.run(); + g <- g + r1 + r2; + return g; + } + proc f() : int = { var r; r <@ h(); return r; } +}. + +module QM = H(A0, A1) with { proc f [ 1 + ^ { g <- 1; } ] }. + +lemma QM_f : hoare[ QM.f : QM.g = 0 /\ H.g = 5 + ==> QM.g = 19 /\ H.g = 5 /\ res = 19 ]. +proof. by proc; inline *; auto. qed. + +(* ====================================================================== + Abstract bases are rejected with a proper error (not an anomaly). + ====================================================================== *) +section. + +declare module X <: T. + +expect fail "cannot update an abstract module" +local module QA = X with { proc run [ 1 - ] }. + +end section.