refactor(pl): weakmem as recheckable per-logic rules

src/phl/README.md

@@ -143,7 +143,7 @@ src/phl/
     transforms/ EcTr<Name>: catalogue entries of the program transformations
     ecPl*.ml    computations shared by the rules of every logic: EcPlFrame,
                 EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform,
-                EcPlMatch, EcPlFun, EcPlCall
+                EcPlMatch, EcPlFun, EcPlCall, EcPlWeakMem
   ecPlRecheck.ml     checker scaffolding
   ecPhl<Tactic>.ml   legacy: thin dispatchers and adapters, not-yet-migrated
                      tactics
@@ -158,6 +158,10 @@ src/phl/
 - The `call` rules (`Ec<Logic>Call`) are logic rules on the call alone;
   `call` is derived (`seq` + rule), except in bdhoare, whose rule keeps its
   composite statement on `c; x <@ f(a)`.
+- The `weakmem` rules (`Ec<Logic>WeakMem`) weaken the memory of a statement
+  judgement by fresh locals it does not mention; the `weakmem` tactic is
+  derived (cut of the weakened hypothesis, closed by the rule and the
+  hypothesis).
 - A rule relating two logics (e.g. the `pr` bridges) lives with the logic of
   its conclusion.
 - A rule concluding a probability statement from a judgement (`byphoare`,

src/phl/REFACTORING.md

@@ -157,7 +157,9 @@ src/phl/
                 fresh program variables), EcPlFun (unfolding a procedure,
                 the oracle conditions of the abstract-procedure rules,
                 the single-call statement of `proc*`), EcPlCall (the
-                result assignment and argument substitution of a call)
+                result assignment and argument substitution of a call),
+                EcPlWeakMem (restricting a memory weakened by fresh local
+                variables)
   ecPlRecheck.ml     checker scaffolding
   ecPhl<Tactic>.ml   legacy: thin dispatchers and adapters, not-yet-migrated
                      tactics
@@ -183,6 +185,11 @@ uniform across logics or relate several judgements:
   `call` is derived (`seq`, then the rule); the bdhoare rule keeps its
   statement on `c; lv <@ f(a)` (implicit seq and framing: the bdhoare
   `seq` rule has extra premises);
+- the `weakmem` rules (`Ec<Logic>WeakMem`; equiv: one side at a time)
+  weaken the memory of a judgement on a statement by fresh local
+  variables it does not mention (the shared computation in
+  `EcPlWeakMem`); the `weakmem` tactic is derived: a cut of the weakened
+  hypothesis, closed by the rule and the hypothesis;
 - a rule relating judgements of two logics (the `pr` bridges, `hoare` from
   `phoare`, …) lives with the logic of its conclusion;
 - a rule concluding a statement on probabilities from a judgement

src/phl/ecPhlCodeTx.ml

@@ -31,7 +31,8 @@ module TTC = EcProofTyping
    logic-agnostic dispatcher [t_transform] below, and no per-logic module.
 
    [weakmem] is not a program transformation (it changes the memory type
-   of the goal and adds an implication): it is not migrated. *)
+   of a hypothesis and adds an implication): it has its own rule in each
+   logic ([Ec<Logic>WeakMem], see [process_weakmem] below). *)
 
 (* -------------------------------------------------------------------- *)
 (* The memory and statement transformed: the program of the goal (hoare,
@@ -180,11 +181,17 @@ let process_set_match (side, cpos, id, pattern) tc =
     tc
 
 (* -------------------------------------------------------------------- *)
+(* [weakmem h (xs : t)]: the hypothesis [h], a judgement on a statement,
+   weakened by the fresh local variables [xs] (in the memory of the given
+   side for equiv, both memories by default), is added as a premise of the
+   goal. Derived in each logic (cut, then the [weakmem] rule of the logic
+   of [h], [Ec<Logic>WeakMem]); the variables are typed first, the logic
+   being then the one of [h]. *)
 let process_weakmem (side, id, params) tc =
   let open EcLocation in
   let hyps = FApi.tc1_hyps tc in
   let env = FApi.tc1_env tc in
-  let _, f =
+  let h, f =
     try LDecl.hyp_by_name (unloc id) hyps
     with LDecl.LdeclError _ ->
       tc_lookup_error !!tc ~loc:id.pl_loc `Local ([], unloc id)
@@ -198,42 +205,28 @@ let process_weakmem (side, id, params) tc =
 
   let decls = List.map process_decl params in
 
-  let bind me =
-    try EcMemory.bindall decls me
-    with EcMemory.DuplicatedMemoryBinding x ->
-      tc_error ~loc:id.pl_loc !!tc "variable %s already declared" x in
-
-  let h =
+  let t =
     match f.f_node with
-    | FhoareS hs ->
-      let _, mt = bind hs.hs_m in
-      f_hoareS mt (hs_pr hs) hs.hs_s (hs_po hs)
-
-    | FeHoareS hs ->
-      let _, mt = bind hs.ehs_m in
-      f_eHoareS mt (ehs_pr hs) hs.ehs_s (ehs_po hs)
-
-    | FbdHoareS hs ->
-      let _, mt = bind hs.bhs_m in
-      f_bdHoareS mt (bhs_pr hs) hs.bhs_s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
-
-    | FequivS es ->
-      let do_side side (ml, mr) =
-        let es_ml, es_mr = if side = `Left then bind ml, mr else ml, bind mr in
-        (es_ml, es_mr)
-      in
-      let ((_, mtl), (_, mtr)) =
-        match side with
-        | None -> do_side `Left (do_side `Right (es.es_ml, es.es_mr))
-        | Some side -> do_side side (es.es_ml, es.es_mr) in
-      f_equivS mtl mtr (es_pr es) es.es_sl es.es_sr (es_po es)
+    | FhoareS _ ->
+      EcHoareWeakMem.t_hoare_weakmem_hyp h { hwm_vars = decls }
+
+    | FeHoareS _ ->
+      EcEHoareWeakMem.t_ehoare_weakmem_hyp h { ehwm_vars = decls }
+
+    | FbdHoareS _ ->
+      EcBdHoareWeakMem.t_bdhoare_weakmem_hyp h { bwm_vars = decls }
+
+    | FequivS _ ->
+      EcEquivWeakMem.t_equiv_weakmem_hyp h side decls
 
     | _ ->
       tc_error ~loc:id.pl_loc !!tc
         "the hypothesis need to be a hoare/phoare/ehoare/equiv on statement"
   in
-  let concl = f_imp h (FApi.tc1_goal tc) in
-  FApi.xmutate1 tc `WeakenMem [concl]
+
+  try t tc
+  with EcMemory.DuplicatedMemoryBinding x ->
+    tc_error ~loc:id.pl_loc !!tc "variable %s already declared" x
 
 (* -------------------------------------------------------------------- *)
 (* [case <- p]: split the tuple assignment at [p]. The checks done before

src/phl/rules/bdhoare/ecBdHoareWeakMem.ml

@@ -0,0 +1,61 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+open EcEnv
+
+open EcCoreGoal
+open EcLowPhlGoal
+open EcPlWeakMem
+
+(* -------------------------------------------------------------------- *)
+(* Parameter of the bdhoare [weakmem] rule: the variables declared in the
+   goal's memory, typed. Nothing to resolve: the same record is the rule
+   argument and the node payload. *)
+type bdhoare_weakmem = {
+  bwm_vars : ovariable list;
+}
+
+type EcCoreGoal.rule += RBdHoareWeakMem of bdhoare_weakmem
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. Its side conditions (the
+   variables are the last ones declared in the memory, fresh in the rest
+   of it, and not used by the judgement) are re-checked by
+   [EcPlWeakMem.restrict], so the checker re-validates them. *)
+let bdhoare_weakmem_subgoals
+    (hyps : LDecl.hyps) (hs : bdHoareS) (n : bdhoare_weakmem)
+=
+  let env  = LDecl.toenv hyps in
+  let used =
+    used env (fst hs.bhs_m) hs.bhs_s [hs.bhs_pr; hs.bhs_po; hs.bhs_bd] in
+  [f_bdHoareS_r { hs with bhs_m = restrict env n.bwm_vars hs.bhs_m used }]
+
+(* -------------------------------------------------------------------- *)
+(* Rule (TCB). *)
+let t_bdhoare_weakmem (r : bdhoare_weakmem) (tc : tcenv1) =
+  let hs = tc1_as_bdhoareS tc in
+  let sg =
+    try  bdhoare_weakmem_subgoals (FApi.tc1_hyps tc) hs r
+    with InvalidWeakening msg -> tc_error !!tc "%s" msg in
+  FApi.xrule1 tc (RBdHoareWeakMem r) sg
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | RBdHoareWeakMem n ->
+         Some (EcPlRecheck.checker_of "bdhoare-weakmem" pf_as_bdhoareS
+                 (fun hyps hs -> bdhoare_weakmem_subgoals hyps hs n))
+     | _ -> None)
+
+(* -------------------------------------------------------------------- *)
+(* Derived (no proof-node): cut the hypothesis [h] weakened by the
+   variables, close the cut judgement by the rule and [h]. Raises
+   [EcMemory.DuplicatedMemoryBinding] (before acting) when a variable is
+   already declared. *)
+let t_bdhoare_weakmem_hyp (h : EcIdent.t) (r : bdhoare_weakmem) (tc : tcenv1) =
+  let hs = destr_bdHoareS (LDecl.hyp_by_id h (FApi.tc1_hyps tc)) in
+  let hs = { hs with bhs_m = EcMemory.bindall r.bwm_vars hs.bhs_m } in
+  FApi.t_first
+    (FApi.t_seq (t_bdhoare_weakmem r) (EcLowGoal.t_apply_hyp h ~args:[] ~sk:0))
+    (EcLowGoal.t_cut (f_bdHoareS_r hs) tc)

src/phl/rules/bdhoare/ecBdHoareWeakMem.mli

@@ -0,0 +1,41 @@
+(* -------------------------------------------------------------------- *)
+open EcAst
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+type bdhoare_weakmem = {
+  bwm_vars : ovariable list;   (* the variables, typed *)
+}
+
+(* [t_bdhoare_weakmem { bwm_vars = xs }] — weakening of the memory:
+
+        phoare [c : P ==> Q] <> b  (memory m)
+     ------------------------------------------  m' = m + xs
+        phoare [c : P ==> Q] <> b  (memory m')
+
+   ([<>] any of [<=], [=], [>=]), where [m + xs] is [m] in which the
+   local program variables [xs] are declared ([EcMemory.bindall]). Side
+   conditions (re-checked by [EcPlWeakMem.restrict], otherwise fails):
+   [xs] are the last variables declared in the memory [m'] of the goal,
+   each fresh in [m], and none of them is read or written by [c] nor
+   occurs in [P], [Q] or [b] (the premise is well-formed in [m]).
+
+   Node: [RBdHoareWeakMem { bwm_vars = xs }]. Checker: "bdhoare-weakmem". *)
+val t_bdhoare_weakmem : bdhoare_weakmem -> backward
+
+(* ==================================================================== *)
+(* Derived tactics                                                      *)
+
+(* [t_bdhoare_weakmem_hyp h { bwm_vars = xs }] — on any goal [G], [h] being
+   the hypothesis [phoare [c : P ==> Q] <> b] (memory [m]), with
+   [H' := phoare [c : P ==> Q] <> b] (memory [m + xs]):
+   1. [EcLowGoal.t_cut] [H'], giving
+        (a) H',
+        (b) H' => G                           — left open;
+   2. [t_bdhoare_weakmem] reduces (a) to [h], closed by [h].
+   Visible goal: (b). Raises [EcMemory.DuplicatedMemoryBinding] (before
+   acting) when a variable of [xs] is already declared in [m]. Emits no
+   node of its own. *)
+val t_bdhoare_weakmem_hyp : EcIdent.t -> bdhoare_weakmem -> backward

src/phl/rules/ecPlWeakMem.ml

@@ -0,0 +1,65 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcAst
+open EcTypes
+open EcEnv
+open EcPV
+
+(* -------------------------------------------------------------------- *)
+(* Weakening of a memory, shared by the [weakmem] rules of every logic: a
+   judgement on a statement that holds in a memory [me] holds in [me]
+   extended with fresh local program variables [xs], which the judgement
+   does not mention. *)
+
+exception InvalidWeakening of string
+
+let invalid fmt = Format.kasprintf (fun msg -> raise (InvalidWeakening msg)) fmt
+
+(* -------------------------------------------------------------------- *)
+(* The memory [me] is rebuilt from the declarations of [me'] that precede
+   [xs] (a memory being built by successive [EcMemory.bindall]), then
+   checked: binding [xs] in it must give back [me'] (which re-checks the
+   freshness of [xs]). *)
+let restrict
+    (env : env) (xs : ovariable list) ((m, mt') : memenv) (used : PV.t)
+=
+  let name, decls' =
+    match EcMemory.for_printing mt' with
+    | None   -> invalid "the memory has no local variables"
+    | Some x -> x in
+
+  let n = List.length decls' - List.length xs in
+  let decls  = List.filteri (fun i _ -> i <  n) decls' in
+  let suffix = List.filteri (fun i _ -> i >= n) decls' in
+
+  if n < 0 || not (List.all2 ov_equal xs suffix) then
+    invalid "the variables are not the last declared ones";
+
+  let mt = EcMemory.empty_local_mt ~witharg:(is_some name) in
+  let mt =
+    try  EcMemory.bindall_mt decls mt
+    with EcMemory.DuplicatedMemoryBinding x ->
+      invalid "variable %s declared twice" x in
+
+  let mt'' =
+    try  EcMemory.bindall_mt xs mt
+    with EcMemory.DuplicatedMemoryBinding x ->
+      invalid "variable %s already declared" x in
+
+  if not (EcMemory.mt_equal mt'' mt') then
+    invalid "the memory is not an extension of a memory by the variables";
+
+  List.iter (fun (x : ovariable) ->
+      x.ov_name |> oiter (fun x ->
+        if PV.mem_pv env (pv_loc x) used then
+          invalid "variable %s is used by the judgement" x))
+    xs;
+
+  (m, mt)
+
+(* -------------------------------------------------------------------- *)
+let used (env : env) (m : memory) (s : stmt) (fs : form list) =
+  List.fold_left
+    (fun pv f -> PV.union pv (PV.fv env m f))
+    (PV.union (s_read env s) (s_write env s))
+    fs

src/phl/rules/ecPlWeakMem.mli

@@ -0,0 +1,25 @@
+(* -------------------------------------------------------------------- *)
+open EcAst
+open EcEnv
+open EcPV
+
+(* -------------------------------------------------------------------- *)
+(* Weakening of a memory, shared by the [weakmem] rules of every logic: a
+   judgement on a statement that holds in a memory [me] holds in [me]
+   extended with fresh local program variables [xs], which the judgement
+   does not mention. *)
+
+exception InvalidWeakening of string
+
+(* [restrict env xs me' used] is the memory [me] such that
+   [me' = EcMemory.bindall xs me] (same memory identifier): [xs] are the
+   last variables declared in [me'], each fresh in [me]. The program
+   variables [used] by the judgement must not include [xs], so that the
+   judgement is well-formed in [me]. Raises [InvalidWeakening]
+   otherwise. *)
+val restrict : env -> ovariable list -> memenv -> PV.t -> memenv
+
+(* [used env m s fs]: the program variables read or written by [s],
+   joined with the program variables of memory [m] in the formulas
+   [fs]. *)
+val used : env -> memory -> stmt -> form list -> PV.t

src/phl/rules/ehoare/ecEHoareWeakMem.ml

@@ -0,0 +1,61 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+open EcEnv
+
+open EcCoreGoal
+open EcLowPhlGoal
+open EcPlWeakMem
+
+(* -------------------------------------------------------------------- *)
+(* Parameter of the ehoare [weakmem] rule: the variables declared in the
+   goal's memory, typed. Nothing to resolve: the same record is the rule
+   argument and the node payload. *)
+type ehoare_weakmem = {
+  ehwm_vars : ovariable list;
+}
+
+type EcCoreGoal.rule += REHoareWeakMem of ehoare_weakmem
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. Its side conditions (the
+   variables are the last ones declared in the memory, fresh in the rest
+   of it, and not used by the judgement) are re-checked by
+   [EcPlWeakMem.restrict], so the checker re-validates them. *)
+let ehoare_weakmem_subgoals
+    (hyps : LDecl.hyps) (hs : eHoareS) (n : ehoare_weakmem)
+=
+  let env  = LDecl.toenv hyps in
+  let used =
+    used env (fst hs.ehs_m) hs.ehs_s [hs.ehs_pr; hs.ehs_po] in
+  [f_eHoareS_r { hs with ehs_m = restrict env n.ehwm_vars hs.ehs_m used }]
+
+(* -------------------------------------------------------------------- *)
+(* Rule (TCB). *)
+let t_ehoare_weakmem (r : ehoare_weakmem) (tc : tcenv1) =
+  let hs = tc1_as_ehoareS tc in
+  let sg =
+    try  ehoare_weakmem_subgoals (FApi.tc1_hyps tc) hs r
+    with InvalidWeakening msg -> tc_error !!tc "%s" msg in
+  FApi.xrule1 tc (REHoareWeakMem r) sg
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | REHoareWeakMem n ->
+         Some (EcPlRecheck.checker_of "ehoare-weakmem" pf_as_ehoareS
+                 (fun hyps hs -> ehoare_weakmem_subgoals hyps hs n))
+     | _ -> None)
+
+(* -------------------------------------------------------------------- *)
+(* Derived (no proof-node): cut the hypothesis [h] weakened by the
+   variables, close the cut judgement by the rule and [h]. Raises
+   [EcMemory.DuplicatedMemoryBinding] (before acting) when a variable is
+   already declared. *)
+let t_ehoare_weakmem_hyp (h : EcIdent.t) (r : ehoare_weakmem) (tc : tcenv1) =
+  let hs = destr_eHoareS (LDecl.hyp_by_id h (FApi.tc1_hyps tc)) in
+  let hs = { hs with ehs_m = EcMemory.bindall r.ehwm_vars hs.ehs_m } in
+  FApi.t_first
+    (FApi.t_seq (t_ehoare_weakmem r) (EcLowGoal.t_apply_hyp h ~args:[] ~sk:0))
+    (EcLowGoal.t_cut (f_eHoareS_r hs) tc)