diff --git a/doc/language/code-positions.rst b/doc/language/code-positions.rst new file mode 100644 index 000000000..f03267ecf --- /dev/null +++ b/doc/language/code-positions.rst @@ -0,0 +1,58 @@ +:orphan: + +.. remove the :orphan: marker above once this page is referenced from a + language-reference toctree. + +======================================================================== +Code positions +======================================================================== + +A *code position* designates an instruction (or a gap between +instructions) inside a procedure body. One common language of code +positions is shared by the program tactics that take a position +argument — `swap`, `wp`, `sp`, `alias`, `kill`, `outline`, +`proc change`, ... — and by fine-grained module definitions +(:doc:`module-update`). + +------------------------------------------------------------------------ +Base positions +------------------------------------------------------------------------ + +- a plain integer `n` — the `n`-th instruction of the block (1-based); +- an anchor `^if`, `^while`, `^match`, `^x<-` (assignment to `x`), + `^x<$` (sampling into `x`), `^x<@` (call assigned to `x`), or the + left-value-less forms `^<-`, `^<$`, `^<@` — the first matching + instruction; a specific occurrence is selected with `{n}`, e.g. + `^<@{2}` for the second call; +- an offset `{anchor} &+ n` / `{anchor} &- n` relative to an anchor. + +------------------------------------------------------------------------ +Nested positions +------------------------------------------------------------------------ + +A position may descend into the branches of structured instructions, +written as a path of positions and *branch selectors*: after a +position, `.` enters the body of a `while` or the true branch of an +`if`, `?` enters the false branch of an `if`, and `#C.` enters the +branch of a `match` for constructor `C`. + +- `^while.2` is the second instruction of the loop body; +- `^if?1` is the first instruction of the else branch; +- `^match#Some.^if.1` is the first instruction of the true branch of + the `if` inside the `Some` branch of the `match`. + +.. warning:: + + A `.` followed by whitespace ends the sentence. Nested positions and + match-branch selectors must therefore be written **without spaces** + around the dot: `^while.^s<-`, `#Some.]` (with the closing bracket + abutting the selector), never `^while. ^s<-`. + +------------------------------------------------------------------------ +Ranges +------------------------------------------------------------------------ + +Contexts that operate on a block of instructions accept ranges of +positions: `[{codepos} .. {codepos}]` selects an inclusive span, and +`[{codepos} +> n]` selects the instruction at `{codepos}` and the `n` +following ones. diff --git a/doc/language/module-update.rst b/doc/language/module-update.rst new file mode 100644 index 000000000..06b0c84d9 --- /dev/null +++ b/doc/language/module-update.rst @@ -0,0 +1,402 @@ +:orphan: + +.. remove the :orphan: marker above once this page is referenced from a + language-reference toctree. + +======================================================================== +Fine-grained module definitions: `module ... = ... with` +======================================================================== + +A module can be defined *incrementally*, as a patch over an existing +module: the new module copies the base module and applies a set of +declarative updates — adding or removing global variables, and editing +procedure bodies at designated code positions. + +.. code-block:: easycrypt + + module M' = M with { + var c : int (* add a module variable *) + proc f [ ^x<- + { c <- c + 1; } ] (* patch the body of a proc *) + }. + +This is the natural way to define instrumented variants of a scheme +(ghost counters, bad-event flags) and hybrid games that differ from the +previous game by a small, local change: the definition *is* the diff, +the unchanged code cannot drift out of sync with the base module, and +relational proofs between the base and the derived module close cheaply +(`sim`) on all unmodified procedures. + +For a complete worked example of a game-hop proof structured this way, +see `examples/br93.ec` in the EasyCrypt distribution, where each hybrid +is defined as an update of the previous one. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Syntax +------------------------------------------------------------------------ + +.. admonition:: Syntax + + .. code-block:: easycrypt + + module M' = M with { + - var x1, ..., xn (* remove variables *) + var y1 : ty1 ... (* add variables *) + proc f [ {var-decl}* {update}+ ] res ~ e (* patch procedures *) + ... + }. + + The three groups must appear in this order: variable removals (at most + one `- var` clause), variable additions, procedure updates. Each + procedure update consists of optional *local* variable declarations, + followed by one or more body updates, followed by an optional rewrite + `res ~ e` of the returned expression. + +Each body update is a *code position* (or a range of positions) +followed by an update action. The actions come in two families. + +**Statement updates** insert, replace or delete instructions: + +- `{codepos} + { s }` — insert the statement `s` **after** the + instruction at `{codepos}`; +- `{codepos} + ^ { s }` — insert `s` **before** it; +- `{codepos} ~ { s }` — **replace** it by `s`; +- `{codepos} -` — **delete** it. + +Replacement and deletion also accept a range `[{codepos} .. +{codepos}]` (inclusive) or `[{codepos} +> n]` (the instruction at +`{codepos}` and the `n` following ones), acting on the whole selected +block. + +**Condition updates** edit the control structure around the designated +instruction: + +- `{codepos} + e` — keep the instruction at `{codepos}` and wrap the + **rest of the block after it** in `if e { ... }`; +- `{codepos} + ^ e` — wrap the instruction itself **and** the rest of + the block in `if e { ... }`; +- `{codepos} ~ e` — replace the guard of the `if`, the `while`, or the + scrutinee of the `match` at `{codepos}` by `e` (the branches are kept + unchanged); +- `{codepos} - {branch}` — collapse the conditional at `{codepos}` to + one of its branches: `.` selects the true branch of an `if`, `?` its + false branch, and `#C.` the branch of a `match` for constructor `C` + (the constructor's pattern variables become fresh local variables, + bound by projecting the scrutinee). + +------------------------------------------------------------------------ +Code positions +------------------------------------------------------------------------ + +Code positions use the same language as program tactics such as `swap` +or `wp` — plain indices, anchors (`^x<-`, `^<@{2}`, `^while`), offsets, +and nested positions descending into branches (`^while.^s<-`, +`^match#Some.^if.1`). See :doc:`code-positions` for the full syntax, +including the whitespace pitfalls around `.`. + +When a procedure update contains several body updates, they are applied +from the last to the first. List them **in program order** (positions +increasing down the body): every position is then interpreted relative +to the original procedure body. + +------------------------------------------------------------------------ +Semantics +------------------------------------------------------------------------ + +The derived module elaborates to an ordinary structure: procedures and +variables that are not mentioned are copied over verbatim, so they are +definitionally identical to the base module's and relational goals +between the two close by `sim` or `proc; auto`. + +Two points deserve attention: + +- **The derived module owns fresh copies of the base's items — and only + of those.** What is copied is exactly the base module expression's + own items: its variables, its procedures, its nested sub-modules. + References to those items are re-rooted to the new module: if `M` has + a variable `x`, then `M'.x` is a *distinct* global, and a relational + invariant linking the two games is written `M.x{1} = M'.x{2}` (or + `={x}(M, M')`). Everything else stays **shared**: references to + other modules (a joint random oracle), and — when the base is a + sub-module — references to the *enclosing* module's state (see + `Updating sub-modules and functors`_ below). + +- **Updates are checked in the derived module's scope.** Inserted code + may mention the procedure's parameters and locals, the new local + variables declared in the update, the (new and copied) module + variables and procedures — unqualified — and any other module's + global variables. When the base is a sub-module, the enclosing + module's variables must be written *qualified* (`P.g`), as they are + not part of the derived module's own scope. A `res ~ e` rewrite must + preserve the return type. + +------------------------------------------------------------------------ +Restrictions +------------------------------------------------------------------------ + +- The base expression must be a **concrete, fully applied** module. A + functor cannot be updated directly; instead, re-bind its parameters + in the header of the new module: + + .. code-block:: easycrypt + + module F2 (B : T) = F(B) with { ... }. + +- Abstract (declared) modules cannot be updated. + +- Only procedures of the base module's signature can be patched; new + procedures cannot be added, and procedure signatures cannot change. + A procedure defined by alias (`proc f = M.g`) is resolved to its + concrete body before patching. + +- Variable removal (`- var`) happens **before** the procedure updates + are processed: the updates cannot mention the removed variables — not + even in anchors, so use numeric positions to delete their uses — and + it is the user's responsibility to patch out every use (a dangling + reference is reported when the derived module is checked). + +------------------------------------------------------------------------ +Updating sub-modules and functors +------------------------------------------------------------------------ + +The base of an update may also be a **sub-module** (`P.O`), an +**applied functor** (`F(A)`), or a sub-module of an applied functor +(`F(A).O`). The copy/share rule of the previous section decides the +semantics in every case: + +- **Sub-module base.** `module Q = P.O with { ... }` copies `O`'s + items — `Q` gets fresh copies of `O`'s variables and nested + sub-modules, and `O`'s internal (self-) references follow the copy. + References to the *enclosing* module's state (`P.g`) are **shared**: + `Q` reads and writes the same `P.g` as `P.O` does. This is the + natural shape for instrumenting one oracle of a larger construction + in place. + +- **Applied-functor base.** `module Q = F(A) with { ... }` bakes the + application into the copy: parameter references are already resolved + to `A`, self-references (including calls between the functor's own + procedures) land on `Q`, and `Q`'s state is fresh. Note the + difference with an *alias* `module G = F(A)`: the alias shares `F`'s + state (in EasyCrypt, a functor's state is common to all its + applications), whereas the update produces an independent copy. + +- **Sub-module of an applied functor.** `module Q = F(A).O with + { ... }` combines the two: `O`'s state is copied, the enclosing + functor's state `F.g` — which is application-independent — stays + shared, and the application at `A` is baked in. + +.. ecproof:: + + require import AllCore. + + module type T = { proc run() : int }. + + module A0 : T = { proc run() : int = { return 7; } }. + + module F (B : T) = { + var g : int (* enclosing state: SHARED *) + module O = { + var x : int (* sub-module state: COPIED *) + proc f() : int = { + var r; + r <@ B.run(); + g <- g + r; + x <- x + 1; + return x; + } + } + }. + + module Q = F(A0).O with { + proc f [ 1 + ^ { x <- x + 2; } ] (* x is Q's own copy; + F.g would need qualification *) + }. + + lemma Q_f : hoare[ Q.f : Q.x = 0 /\ F.g = 0 /\ F.O.x = 5 + ==> Q.x = 3 /\ F.g = 7 /\ F.O.x = 5 ]. + proof. + (*$*) proc. + by inline *; auto. + qed. + +------------------------------------------------------------------------ +Example: instrumenting a scheme with ghost state +------------------------------------------------------------------------ + +The derived module `Mc` adds a ghost counter `c`, initialised in +`init` and incremented on every call to `f`. The base procedures are +otherwise unchanged: the equivalence between `M.f` and `Mc.f` — with +the two `x` copies related explicitly — closes by `auto`. + +.. ecproof:: + + require import AllCore. + + module M = { + var x : int + + proc init() : unit = { + x <- 0; + } + + proc f(y : int) : int = { + var a : int; + a <- y + 1; + x <- x + a; + return a; + } + }. + + module Mc = M with { + var c : int + proc init [ ^x<- + { c <- 0; } ] (* insert after the write *) + proc f [ 1 + ^ { c <- c + 1; } ] (* insert before instr 1 *) + }. + + (* `+` inserted after the anchor: init runs x <- 0; c <- 0. *) + lemma Mc_init : hoare[ Mc.init : true ==> Mc.x = 0 /\ Mc.c = 0 ]. + proof. + (*$*) proc. + by auto. + qed. + + (* Mc.x is a FRESH global, distinct from M.x: relate them explicitly. *) + equiv M_Mc_f : M.f ~ Mc.f : + ={arg} /\ M.x{1} = Mc.x{2} ==> ={res} /\ M.x{1} = Mc.x{2}. + proof. by proc; auto. qed. + +------------------------------------------------------------------------ +Example: replacing an instruction and the result +------------------------------------------------------------------------ + +A statement replacement (`~ { ... }`) combined with a rewrite of the +returned expression (`res ~ ...`). + +.. ecproof:: + + require import AllCore. + + module M = { + proc f(y : int) : int = { + var a : int; + a <- y + 1; + return a; + } + }. + + module M2 = M with { + proc f [ ^a<- ~ { a <- y + 2; } ] res ~ (a - 1) + }. + + lemma M2_f (v : int) : hoare[ M2.f : y = v ==> res = v + 1 ]. + proof. + (*$*) proc. + by auto. + qed. + +------------------------------------------------------------------------ +Example: editing a loop +------------------------------------------------------------------------ + +Nested code positions reach inside a loop body (`^while.^s<-`), and a +condition update (`~ e`) changes the guard while keeping the body. + +.. ecproof:: + + require import AllCore. + + module M = { + proc g(n : int) : int = { + var i, s : int; + i <- 0; + s <- 0; + while (i < n) { + s <- s + i; + i <- i + 1; + } + return s; + } + }. + + (* double the summand, inside the loop body *) + module Mbody = M with { + proc g [ ^while.^s<- ~ { s <- s + 2 * i; } ] + }. + + (* one more iteration, same body *) + module Mguard = M with { + proc g [ ^while ~ (i < n + 1) ] + }. + + equiv M_Mbody_g : M.g ~ Mbody.g : ={arg} ==> res{2} = 2 * res{1}. + proof. + (*$*) proc. + while (={i, n} /\ s{2} = 2 * s{1}); by auto => /#. + qed. + +------------------------------------------------------------------------ +Example: collapsing a match to one branch +------------------------------------------------------------------------ + +`- #C.` specialises a `match` to its `C` branch; the pattern variables +are introduced as local variables bound by projecting the scrutinee. + +.. ecproof:: + + require import AllCore. + + module M = { + proc h(o : int option) : int = { + var r : int; + r <- 0; + match o with + | None => { r <- 1; } + | Some v => { r <- v; } + end; + return r; + } + }. + + module Msome = M with { + proc h [ ^match - #Some.] + }. + + lemma Msome_h (w : int) : hoare[ Msome.h : o = Some w ==> res = w ]. + proof. + (*$*) proc. + by auto. + qed. + +------------------------------------------------------------------------ +Example: updating a functor +------------------------------------------------------------------------ + +Functors are updated by re-binding their parameters and patching the +applied body. + +.. ecproof:: + + require import AllCore. + + module type T = { proc run() : unit }. + + module F (B : T) = { + var k : int + proc go() : int = { + k <- 0; + B.run(); + return k; + } + }. + + module F2 (B : T) = F(B) with { + proc go [ ^ <@ + { k <- k + 1; } ] + }. + + lemma F2_go (B <: T{-F2}) : hoare[ F2(B).go : true ==> F2.k = 1 ]. + proof. + (*$*) proc. + by wp; call (: true); auto. + qed. 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.