fix(phl): swap with a code path must rebuild the enclosing program

doc/tactics/swap.rst

@@ -37,7 +37,18 @@ Here:
   right program in relational goals. If omitted, the tactic applies to the
   single program under consideration.
 
-- `{codepos1}` denotes a *top-level code position*.
+- `{codepos1}` denotes a code position in the program.
+
+- Any `{codepos1}` or block `[{codepos1}..{codepos1}]` may be prefixed with a
+  *code path*, selecting a nested block in which the swap takes place. Each
+  step of the path is a code position followed by a branch selector: `.`
+  for the then-branch of a conditional or the body of a loop, `?` for the
+  else-branch of a conditional, and `#C.` for the arm of a `match` labelled
+  by the constructor `C`. A single position directly follows the path,
+  while a block is separated from it by `:`. For instance, `2#Some.1`
+  designates the first command of the `Some` arm of the `match` at position
+  `2`, and `1.:[1..2]` the block formed by the first two commands of the
+  then-branch (or loop body) of the command at position `1`.
 
 - A `{codeoffset1}` is either:
 
@@ -64,6 +75,11 @@ The meaning of these forms is as follows:
 In all cases, the swap is only valid when the exchanged fragments are
 independent, so that the transformation preserves the program semantics.
 
+When a code path is given, positions and offsets are interpreted relative
+to the selected block, the destination must lie inside that block, and the
+enclosing command (conditional, loop or `match`) and its other branches are
+left unchanged.
+
 ------------------------------------------------------------------------
 Example (single statement)
 ------------------------------------------------------------------------
@@ -137,6 +153,41 @@ commands with a later, independent command.
     admit.
   qed.
 
+------------------------------------------------------------------------
+Example (swapping inside a branch)
+------------------------------------------------------------------------
+
+The following example uses a code path to swap two commands located in the
+then-branch of a conditional. The conditional itself and its else-branch are
+preserved.
+
+.. ecproof::
+
+  require import AllCore.
+
+  module M = {
+    var x : bool
+    var y : int
+
+    proc branch(b : bool) : unit = {
+      if (b) { x <- true; y <- 2; } else { x <- false; y <- 6; }
+    }
+  }.
+
+  lemma branch_correct : hoare [ M.branch : !b ==> !M.x ].
+  proof.
+    proc.
+
+    (*$*)
+    (* Swap the first command of the then-branch of command 1 with the
+       following command of that branch. The program becomes
+       `if (b) { y <- 2; x <- true; } else { x <- false; y <- 6; }`. *)
+    swap 1.:[1..1] 1.
+
+    (* The conditional is still there. *)
+    admit.
+  qed.
+
 ------------------------------------------------------------------------
 Example (invalid swap)
 ------------------------------------------------------------------------

src/ecMatching.ml

@@ -642,8 +642,7 @@ module Zipper = struct
    *) 
   let zipper_and_split_of_cgap_range (env: env) (path, (start, fin) : codegap_range) (s: stmt) : zipper * _ * nm_codegap_range =
     let (zpr, ((cpath, _), s)) = zipper_of_cgap_r env (path, start) s in
-    let start = normalize_cgap1 env start s in
-    let fin = normalize_cgap1 env fin s in
+    let (start, fin) = normalize_cgap1_range env (start, fin) s in
     let ss = split_by_nmcgap_range (start, fin) s in
     (zpr, ss, (cpath, (start, fin)))
 

src/phl/ecPhlOutline.ml

@@ -73,6 +73,8 @@ let process_outline info tc =
       let mode = if alias then `Alias else `Exact in
       t_outline side range (OV_Proc (mode, f)) tc
   with
+  | EcMatching.Position.InvalidCPos ->
+     tc_error !!tc "Outline: invalid code position"
   | UnificationError (UE_UnificationFailArg x) ->
      tc_error !!tc "Outline: unable to unify arg `%s`." x
   | UnificationError (UE_UnificationFailPv x) ->

src/phl/ecPhlRewrite.ml

@@ -312,7 +312,11 @@ let t_change_stmt
   let mt = odfl metc mt in
 
   let zpr, (_,stmt, epilog), _nmr =
-    EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt in
+    try
+      EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt
+    with EcMatching.Position.InvalidCPos ->
+      tc_error !!tc "invalid code position"
+  in
 
   (* Collect the variables that may be modified by the surrounding context,
      excluding the fragment being replaced. *)

src/phl/ecPhlSwap.ml

@@ -69,16 +69,18 @@ module LowInternal = struct
     (info : swap_kind  )
     (s    : stmt       )
   =
-    let (env, s), (_, (start, fin)) = try 
-      let (cpath, (start, fin)) = info.interval in
-      normalize_cgap_range env (cpath, (start, fin)) s 
+    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 ->
@@ -92,7 +94,8 @@ module LowInternal = struct
       ) s
     with 
     | [hd; s1; s2; tl] -> check_swap pf env (stmt s1) (stmt s2);
-      stmt (List.flatten [hd; s2; s1; tl])
+      EcMatching.Zipper.zip
+        { zpr with z_head = []; z_tail = List.flatten [hd; s2; s1; tl] }
     | _ -> assert false
 end
 

tests/swap-codepath-context.ec

@@ -0,0 +1,63 @@
+(* `swap` with a code path (`1.:[1 .. 1]`: then-branch of instruction 1,
+   `1?:[1 .. 1]`: else-branch, `2.:[1 .. 1]`: body of the loop at 2) must
+   keep the enclosing `if`/`while` and the sibling branch. It used to
+   replace the whole program by the addressed block, so the false goals
+   below (e.g. `M.f(false)` sets `M.x` to 5) were closed by `auto`/`sim`. *)
+require import AllCore.
+
+module M = {
+  var x, y : int
+  proc f(b : bool) : unit = {
+    if (b) { x <- 1; y <- 2; } else { x <- 5; y <- 6; }
+  }
+  proc w() : unit = {
+    x <- 0;
+    while (false) { x <- 1; y <- 2; }
+  }
+  proc g() : unit = { y <- 2; x <- 1; }
+}.
+
+lemma then_branch : hoare [M.f : true ==> M.x = 1].
+proof.
+proc.
+fail (swap 1.:[1 .. 1] 1; auto; done).
+abort.
+
+lemma else_branch : hoare [M.f : true ==> M.x = 5].
+proof.
+proc.
+fail (swap 1?:[1 .. 1] 1; auto; done).
+abort.
+
+lemma while_body : hoare [M.w : true ==> M.x = 1].
+proof.
+proc.
+fail (swap 2.:[1 .. 1] 1; auto; done).
+abort.
+
+lemma equiv_side : equiv [M.f ~ M.g : true ==> ={M.x, M.y}].
+proof.
+proc.
+fail (swap{1} 1.:[1 .. 1] 1; by sim).
+abort.
+
+(* a reversed range is rejected, with or without a path (it used to be
+   accepted as a no-op) *)
+lemma reversed_range : hoare [M.f : true ==> true].
+proof.
+proc.
+fail (swap 1.:[3 .. 1] 1).
+fail (swap 1?:[3 .. 1] -1).
+abort.
+
+(* sanity: a top-level swap still works *)
+lemma toplevel : hoare [M.g : true ==> M.x = 1 /\ M.y = 2].
+proof. proc. fail (swap [3 .. 1] 1). fail (swap [3 .. 1] -1). swap 1 1. auto. qed.
+
+(* the destination must stay inside the addressed block *)
+lemma escape : hoare [M.f : true ==> true].
+proof.
+proc.
+fail (swap 1.:[1 .. 1] 2).
+fail (swap 1?:[2 .. 2] -2).
+abort.

tests/swap-codepath.ec

@@ -0,0 +1,69 @@
+(* `swap` with a code path swaps inside the addressed block only; the
+   enclosing `if`/`while` and the sibling branch stay in the goal, so the
+   untouched branch is what makes the postconditions below hold. *)
+require import AllCore.
+
+module M = {
+  var x, y : int
+  proc f(b : bool) : unit = {
+    if (b) { x <- 1; y <- 2; } else { x <- 5; y <- 6; }
+  }
+  proc w(b : bool) : unit = {
+    x <- 0; y <- 0;
+    while (b) { x <- 1; y <- 2; }
+  }
+}.
+
+module N = {
+  proc f(b : bool) : unit = {
+    if (b) { M.y <- 2; M.x <- 1; } else { M.y <- 6; M.x <- 5; }
+  }
+  proc w(b : bool) : unit = {
+    M.x <- 0; M.y <- 0;
+    while (b) { M.y <- 2; M.x <- 1; }
+  }
+}.
+
+lemma then_branch : hoare [M.f : !b ==> M.x = 5 /\ M.y = 6].
+proof. proc. swap 1.:[1 .. 1] 1. auto. qed.
+
+lemma else_branch : hoare [M.f : b ==> M.x = 1 /\ M.y = 2].
+proof. proc. swap 1?:[1 .. 1] 1. auto. qed.
+
+lemma while_body : hoare [M.w : !b ==> M.x = 0 /\ M.y = 0].
+proof. proc. swap 3.:[1 .. 1] 1. rcondf 3; auto. qed.
+
+lemma then_branch_ph : phoare [M.f : !b ==> M.x = 5 /\ M.y = 6] = 1%r.
+proof. proc. swap 1.:[1 .. 1] 1. auto. qed.
+
+lemma equiv_if : equiv [M.f ~ N.f : ={b} ==> ={M.x, M.y}].
+proof. proc. swap{1} 1.:[1 .. 1] 1. swap{1} 1?:[1 .. 1] 1. sim. qed.
+
+lemma equiv_while : equiv [M.w ~ N.w : ={b} ==> ={M.x, M.y}].
+proof. proc. swap{1} 3.:[1 .. 1] 1. sim. qed.
+
+(* match arm: the path binds the arm's locals *)
+module P = {
+  proc m(o : int option) : unit = {
+    match o with
+    | None   => { M.x <- 5; M.y <- 6; }
+    | Some v => { M.x <- v; M.y <- 2; }
+    end;
+  }
+}.
+
+module Q = {
+  proc m(o : int option) : unit = {
+    match o with
+    | None   => { M.x <- 5; M.y <- 6; }
+    | Some v => { M.y <- 2; M.x <- v; }
+    end;
+  }
+}.
+
+lemma match_arm : equiv [P.m ~ Q.m : ={o} ==> ={M.x, M.y}].
+proof. proc. swap{1} 1#Some.:[1 .. 1] 1. sim. qed.
+
+(* a single position under a path is written without `:` *)
+lemma bare_position : equiv [M.f ~ N.f : ={b} ==> ={M.x, M.y}].
+proof. proc. swap{1} 1.1 1. swap{1} 1?1 1. sim. qed.