fix(typing): sound module updates on sub-module and applied-functor bases

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

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) =

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

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 =

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.