refactor(pl): swap as program transformations

src/ecMatching.ml

@@ -583,33 +583,51 @@ module Zipper = struct
 
   let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; }
 
-  let zipper_step_into_block
+  (* Step into the block selected by a normalized step: nothing is
+     resolved. *)
+  let zipper_step_into_nm_block
     (env        : EcEnv.env)
-    ((cp1, sub) : codepos_step)
+    ((cp1, sub) : nm_codepos_step)
     (s          : stmt)
     (zpr        : ipath)
-  : (ipath * stmt) * nm_codepos_step * env
+  : (ipath * stmt) * env
   =
-    let (s1, i, s2) = find_by_cpos1 env cp1 s in
-    let zpr, step, env =
-      match i.i_node, sub with
-      | Swhile (e, sw), `Cond true ->
-          (ZWhile (e, ((s1, s2), zpr)), sw), `Cond true, env
+    let (s1, i, s2) = find_by_nmcpos1 cp1 s in
+    match i.i_node, sub with
+    | Swhile (e, sw), `Cond true ->
+        (ZWhile (e, ((s1, s2), zpr)), sw), env
 
-      | Sif (e, ifs1, ifs2), `Cond true ->
-          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), `Cond true, env
+    | Sif (e, ifs1, ifs2), `Cond true ->
+        (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), env
 
-      | Sif (e, ifs1, ifs2), `Cond false ->
-          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env
+    | Sif (e, ifs1, ifs2), `Cond false ->
+        (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), env
 
-      | Smatch (e, bs), _ ->
-          let ix = select_match_arm (fun () -> raise InvalidCPos) env e sub in
-          let prebr, (locals, body), postbr = List.pivot_at ix bs in
-          let env = EcEnv.Var.bind_locals locals env in
-          (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env
+    | Smatch (e, bs), `Match ix ->
+        let prebr, (locals, body), postbr =
+          try  List.pivot_at ix bs
+          with (Invalid_argument _ | Not_found) -> raise InvalidCPos in
+        let env = EcEnv.Var.bind_locals locals env in
+        (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), env
 
-      | _ -> raise InvalidCPos
-    in zpr, ((List.length s1), step), env
+    | _ -> raise InvalidCPos
+
+  let zipper_step_into_block
+    (env        : EcEnv.env)
+    ((cp1, sub) : codepos_step)
+    (s          : stmt)
+    (zpr        : ipath)
+  : (ipath * stmt) * nm_codepos_step * env
+  =
+    let (_, i, _), cp1 = find_and_normalize_cpos1 env cp1 s in
+    let sub =
+      match i.i_node, sub with
+      | Smatch (e, _), _ ->
+          `Match (select_match_arm (fun () -> raise InvalidCPos) env e sub)
+      | _, `Cond b -> `Cond b
+      | _ -> raise InvalidCPos in
+    let zs, env = zipper_step_into_nm_block env (cp1, sub) s zpr in
+    zs, (cp1, sub), env
 
   let pre_zipper_of_codepos_path (env : EcEnv.env) (cpath: codepos_path) (s: stmt) =
     List.fold_left_map
@@ -634,6 +652,17 @@ module Zipper = struct
 
   let zipper_of_cgap (env : EcEnv.env) (cp : codegap) (s : stmt) =
     fst (zipper_of_cgap_r env cp s)
+
+  (* Normalized counterpart of [zipper_of_cgap]: nothing is resolved. *)
+  let zipper_of_nm_cgap (env : EcEnv.env) ((cpath, nm) : nm_codegap) (s : stmt) =
+    let (zpr, s), env =
+      List.fold_left
+        (fun ((zpr, s), env) step -> zipper_step_into_nm_block env step s zpr)
+        ((ZTop, s), env) cpath in
+    check_nm_cgap1 nm s;
+    let s1, s2 = split_at_nmcgap1 nm s in
+    zipper ~env (List.rev s1) s2 zpr
+
   (* 
    * Returns:
    *  - A zipper pointing to the start of the range

src/ecMatching.mli

@@ -263,6 +263,13 @@ module Zipper : sig
   val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * (nm_codepos * stmt)
   val zipper_of_cpos : env -> codepos -> stmt -> zipper
 
+  (* Return the zipper for the stmt [stmt] at the normalized code gap
+   * [nm_codegap], the environment binding the locals of the enclosing
+   * [match] arms. Pure: nothing is resolved. Raise [InvalidCPos] if
+   * [nm_codegap] is not valid for [stmt].
+   *)
+  val zipper_of_nm_cgap : env -> nm_codegap -> stmt -> zipper
+
   (* Return the zipper for the stmt [stmt] from the start of the code position
    * range [codepos_range]. It also returns a code position relative to
    * the zipper that represents the final position in the range.

src/phl/README.md

@@ -83,7 +83,7 @@ Run the test suite with `EC_RECHECK=1` to exercise every migrated checker.
 ## Program transformations
 
 Tactics that replace the program by an equivalent one and keep the judgement
-(rndsem, rcond, and later inline, swap, …) go through **one** trusted
+(rndsem, rcond, swap, and later inline, …) go through **one** trusted
 transformation rule per logic, `t_<logic>_transform` (`Ec<Logic>Transform`;
 equiv: one side at a time), parameterized by an entry of a catalogue:
 
@@ -106,10 +106,11 @@ equiv: one side at a time), parameterized by an entry of a catalogue:
   subgoals up to conversion (programs up to alpha-equivalence).
 
 Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`),
-`rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`) and `match-push`
-(`EcTrMatchPush`), the last two pushing the continuation of a leading
-conditional / `match` into its branches. The `if` and `match` tactics are
-push + rule on the conditional alone (`Ec<Logic>If`, `Ec<Logic>Match`).
+`rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`), `match-push`
+(`EcTrMatchPush`) and `swap` (`EcTrSwap`). `if-push` / `match-push` push
+the continuation of a leading conditional / `match` into its branches: the
+`if` and `match` tactics are push + rule on the conditional alone
+(`Ec<Logic>If`, `Ec<Logic>Match`).
 Further entries come with the tactics that use them. The framed form of
 `match C k` changes the precondition: it stays a separate trusted rule of
 each logic, `t_<logic>_rmatch_framed` (`Ec<Logic>RMatch`). See

src/phl/REFACTORING.md

@@ -382,16 +382,21 @@ Current catalogue:
   the single instruction `match e with C xs => { b; c } ...`; no
   obligation. The pattern variables are local identifiers bound in the
   branch only: the binders of a branch are renamed apart when they occur
-  free in `c`, so that `c` is not captured.
+  free in `c`, so that `c` is not captured;
+- `swap` (`EcTrSwap`, moving the block `[s..f)` of the possibly nested block
+  at a resolved path to a gap `t` outside it; the independence of the
+  exchanged statements and the absence of `raise` are checked by the entry;
+  no obligation, same memory), used by `swap` (and `interleave`, a sequence
+  of swaps) in every logic.
 
 The decisions of a conditional or a match are computed by `EcPlRCond`.
 The `if` and `match` tactics are push + rule on the conditional alone: they
 push the continuation into the branches (when there is one) through the
 transformation rule (on each side, for the two-sided equiv forms), then
 apply the `if` / `match` rule of their logic (`Ec<Logic>If`,
 `Ec<Logic>Match`), stated on the conditional alone. Further entries come
-with the tactics that use them: swap, inline, kill/alias/cfold/set and
-proc rewrite.
+with the tactics that use them: inline, kill/alias/cfold/set and proc
+rewrite.
 
 Exception: the framed form of `match C k` (used when the variables of the
 discriminant `e` are neither read nor written by the prefix, and the

src/phl/ecPhlSwap.ml

@@ -4,8 +4,6 @@ open EcParsetree
 open EcLocation
 open EcAst
 open EcModules
-open EcFol
-open EcPV
 open EcMatching.Position
 open EcCoreGoal
 open EcLowGoal
@@ -17,133 +15,60 @@ type swap_kind = {
 }
 
 (* -------------------------------------------------------------------- *)
-module LowInternal = struct
-  (* [exn] holds when the goal observes exceptions (a hoare goal whose
-     postcondition constrains some exception, see
-     [EcLowPhlGoal.hs_observes_exn]). Swapping two independent blocks
-     preserves the final state of the runs that terminate normally, but
-     not the state in which an exception is raised: if one of the blocks
-     raises, the other one has run (or not) before. Hence:
-     - blocks that contain a [raise] are never swapped;
-     - when the goal observes exceptions, blocks that may raise (through
-       a procedure call, see [EcLowPhlGoal.s_may_raise]) are not swapped
-       either. Otherwise, raising is as good as not terminating, which
-       the swap preserves. *)
-  let check_swap
-      (pf : proofenv) ~(exn : bool) (env : EcEnv.env) (s1 : stmt) (s2 : stmt)
-  =
-    let is_contains_raise =
-      let exception HasRaise in
-
-      let rec i_contains_raise (i : instr) =
-        match i.i_node with
-        | Sraise _ -> raise HasRaise
-        | _ -> EcModules.i_iter i_contains_raise i in
-
-      fun (s : stmt) ->
-        try
-          List.iter i_contains_raise s.s_node;
-          false
-        with HasRaise -> true in
-
-    if List.exists is_contains_raise [s1; s2] then
-      tc_error pf "cannot swap blocks that contain exceptions";
-
-    if exn && List.exists (EcLowPhlGoal.s_may_raise env) [s1; s2] then
-      tc_error pf
-        "cannot swap blocks that may raise an exception \
-         (through a procedure call) when the postcondition \
-         constrains exceptions";
-
-    let m1,m2 = s_write env s1, s_write env s2 in
-    let r1,r2 = s_read  env s1, s_read  env s2 in
-    (* FIXME: this is not sufficient *)
-    let m2r1 = PV.interdep env m2 r1 in
-    let m1m2 = PV.interdep env m1 m2 in
-    let m1r2 = PV.interdep env m1 r2 in
-
-    let error mode d =
-      tc_error_lazy pf (fun fmt ->
-        Format.fprintf fmt
-          "the two statements are not independent, %t"
-          (fun fmt ->
-            let (s1, s2) =
-              match mode with
-              | `RW -> "reads" , "written"
-              | `WR -> "writes", "read"
-              | `WW -> "writes", "written"
-            in
-              Format.fprintf fmt
-                "the first statement %s %a which is %s by the second"
-                s1 (PV.pp env) d s2))
-    in
-      if not (PV.is_empty m2r1) then error `RW m2r1;
-      if not (PV.is_empty m1m2) then error `WW m1m2;
-      if not (PV.is_empty m1r2) then error `WR m1r2
-
-
-  let swap_stmt
-    (pf   : proofenv   )
-   ~(exn  : bool       )
-    (env  : EcEnv.env  )
-    (info : swap_kind  )
-    (s    : stmt       )
-  =
-    let zpr, _, (_, (start, fin)) = try
-      EcMatching.Zipper.zipper_and_split_of_cgap_range env info.interval s
-    with InvalidCPos ->
-      tc_error_lazy pf (fun fmt ->
-        let ppe = EcPrinting.PPEnv.ofenv env in
-        Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codegap_range ppe) info.interval
-      )
-    in
-
-    let env = odfl env zpr.z_env in
-    let s = stmt (List.rev_append zpr.z_head zpr.z_tail) in
-
-    let target = try
-      resolve_gap_offset env (start, fin) info.offset s
-    with InvalidCPos ->
-      tc_error pf "invalid offset for swap"
-    in
-
-    match split_by_nmcgaps
-      (if target <= start
-      then [target; start; fin]
-      else [start; fin; target]
-      ) s
-    with 
-    | [hd; s1; s2; tl] -> check_swap pf ~exn env (stmt s1) (stmt s2);
-      EcMatching.Zipper.zip
-        { zpr with z_head = []; z_tail = List.flatten [hd; s2; s1; tl] }
-    | _ -> assert false
-end
-
-(* -------------------------------------------------------------------- *)
-let t_swap_r (side : oside) (info : swap_kind) (tc : tcenv1) =
-  let env = FApi.tc1_env tc in
-  let _, stmt = EcLowPhlGoal.tc1_get_stmt side tc in
-  let exn =
-    match (FApi.tc1_goal tc).f_node with
-    | FhoareS hs -> EcLowPhlGoal.hs_observes_exn (hs_po hs)
-    | _ -> false in
-  let stmt = LowInternal.swap_stmt !!tc ~exn env info stmt in
-  FApi.xmutate1 tc `Swap [EcLowPhlGoal.hl_set_stmt side (FApi.tc1_goal tc) stmt]
+(* [swap] is derived in every logic: the positions are resolved here
+   (failing as before the migration when they are invalid), then the
+   [swap] program transformation ([EcTrSwap], which checks the
+   independence of the exchanged statements) is applied through the
+   transformation rule of the logic. The derived tactic is the same in
+   every logic, hence a single dispatcher on the goal kind. *)
+let resolve_swap (pf : proofenv) (env : EcEnv.env) (info : swap_kind) (s : stmt) =
+  let zpr, _, (path, (start, fin)) = try
+    EcMatching.Zipper.zipper_and_split_of_cgap_range env info.interval s
+  with InvalidCPos ->
+    tc_error_lazy pf (fun fmt ->
+      let ppe = EcPrinting.PPEnv.ofenv env in
+      Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codegap_range ppe) info.interval
+    )
+  in
+
+  let env = odfl env zpr.z_env in
+  let s = stmt (List.rev_append zpr.z_head zpr.z_tail) in
+
+  let target = try
+    resolve_gap_offset env (start, fin) info.offset s
+  with InvalidCPos ->
+    tc_error pf "invalid offset for swap"
+  in
+
+  EcTrSwap.TrSwap { trsw_range = (path, (start, fin)); trsw_target = target; }
 
 (* -------------------------------------------------------------------- *)
-let t_swap = FApi.t_low2 "swap" t_swap_r
+let t_swap (side : oside) (info : swap_kind) (tc : tcenv1) =
+  let _, s = EcLowPhlGoal.tc1_get_stmt side tc in
+  let tr = resolve_swap !!tc (FApi.tc1_env tc) info s in
+  match side, (FApi.tc1_goal tc).f_node with
+  | None, FhoareS _ ->
+      EcHoareTransform.t_hoare_transform { htr_tr = tr } tc
+  | None, FeHoareS _ ->
+      EcEHoareTransform.t_ehoare_transform { ehtr_tr = tr } tc
+  | None, FbdHoareS _ ->
+      EcBdHoareTransform.t_bdhoare_transform { btr_tr = tr } tc
+  | Some side, FequivS _ ->
+      EcEquivTransform.t_equiv_transform { etr_side = side; etr_tr = tr } tc
+  | _ -> assert false
 
 (* -------------------------------------------------------------------- *)
 let rec process_swap1 (info : (oside * pswap_kind) located) (tc : tcenv1) =
   let side, pos = info.pl_desc in
   let concl = FApi.tc1_goal tc in
 
-  if is_equivS concl && Option.is_none side then
+  match side, concl.f_node with
+  | None, FequivS _ ->
     FApi.t_seq
       (process_swap1 { info with pl_desc = (Some `Left , pos)})
       (process_swap1 { info with pl_desc = (Some `Right, pos)})
       tc
-  else
+  | _ ->
     let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
     let env = EcEnv.Memory.push_active_ss me (FApi.tc1_env tc) in
 

src/phl/rules/bdhoare/ecBdHoareTransform.ml

@@ -32,6 +32,7 @@ let bdhoare_transform_subgoals
     trc_env  = env;
     trc_me   = bhs.bhs_m;
     trc_post = lazy (EcPV.PV.fv env m (bhs_po bhs).inv);
+    trc_exn  = false;
   } in
   let r = apply ctxt n.btr_tr bhs.bhs_s in
   let obligation = function

src/phl/rules/ecPlTransform.ml

@@ -21,6 +21,7 @@ type tr_ctxt = {
   trc_env  : env;
   trc_me   : memenv;
   trc_post : EcPV.PV.t Lazy.t;
+  trc_exn  : bool;
 }
 
 type tr_result = {

src/phl/rules/ecPlTransform.mli

@@ -33,7 +33,8 @@ open EcEnv
    (deciding a [match], its unframed form), [EcTrIfPush] and
    [EcTrMatchPush] (pushing the continuation of a leading conditional /
    [match] into its branches; the [if] and [match] tactics are push + rule
-   on the conditional alone). Entries live in [rules/transforms/], as
+   on the conditional alone), [EcTrSwap] (moving a block of a possibly
+   nested block). Entries live in [rules/transforms/], as
    [EcTr<Name>]. The framed form of [match C k] changes the precondition:
    it is not a transformation, but a separate rule of each logic
    ([Ec<Logic>RMatch]). *)
@@ -65,6 +66,12 @@ type tr_ctxt = {
   trc_post : EcPV.PV.t Lazy.t;     (* program variables of [trc_me] read
                                       by the postcondition (for hoare,
                                       including the exceptional ones) *)
+  trc_exn  : bool;                 (* the judgement observes exceptions:
+                                      a hoare postcondition constraining
+                                      some exception
+                                      ([EcLowPhlGoal.hs_observes_exn]);
+                                      otherwise, raising is as good as
+                                      not terminating *)
 }
 
 (* The result of an entry: the (possibly extended) memory, the

src/phl/rules/ehoare/ecEHoareTransform.ml

@@ -33,6 +33,7 @@ let ehoare_transform_subgoals
     trc_env  = env;
     trc_me   = hs.ehs_m;
     trc_post = lazy (EcPV.PV.fv env m (ehs_po hs).inv);
+    trc_exn  = false;
   } in
   let r = apply ctxt n.ehtr_tr hs.ehs_s in
   let pre () =

src/phl/rules/equiv/ecEquivTransform.ml

@@ -40,6 +40,7 @@ let equiv_transform_subgoals
     trc_env  = env;
     trc_me   = me;
     trc_post = lazy (EcPV.PV.fv env m (es_po es).inv);
+    trc_exn  = false;
   } in
   let r = apply ctxt n.etr_tr s in
   let ts_inv_lower_side2 =