[documentation]: tactic swap

Author: strub

doc/tactics/swap.rst

@@ -0,0 +1,170 @@
+========================================================================
+Tactic: `swap`
+========================================================================
+
+The `swap` tactic applies to program-logic goals by rewriting the program
+into a semantically equivalent form where two consecutive, independent
+program fragments are exchanged.
+
+In a nutshell, `swap` permutes commands when doing so does not change the
+program’s behavior (typically because the swapped fragments do not
+interfere, e.g., they write to disjoint variables and neither reads what the
+other writes).
+
+Applying `swap` replaces the current goal by the same goal, but with the
+selected commands swapped in the program. This is useful to expose a more
+convenient program structure, for example to align programs in relational
+proofs or to bring related statements closer together.
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+Syntax
+------------------------------------------------------------------------
+
+The `swap` tactic comes in several forms:
+
+.. admonition:: Syntax
+
+  - `swap {side}? {codepos1}`
+  - `swap {side}? {codepos1} {codeoffset1}`
+  - `swap {side}? [{codepos1}..{codepos1}] {codeoffset1}``
+
+Here:
+
+- `{side}` is optional and is either `1` or `2`. It selects the left or
+  right program in relational goals. If omitted, the tactic applies to the
+  single program under consideration.
+
+- `{codepos1}` denotes a *top-level code position*.
+
+- A `{codeoffset1}` is either:
+
+  - a signed integer (`n` or `-n`), denoting a relative position, or
+  - an absolute code position written `@ {codepos1}`.
+
+The meaning of these forms is as follows:
+
+- `swap {side}? {codepos1}`
+
+  swaps the two adjacent commands starting at the top-level position
+  `{codepos1}`.
+
+- `swap {side}? {codepos1} {codeoffset1}`
+
+  swaps the command at top-level position `{codepos1}` with the command
+  at the position designated by `{codeoffset1}`.
+
+- `swap {side}? [{codepos1}..{codepos1}] {codeoffset1}`
+
+  swaps a whole sequence of commands delimited by `[{codepos1}..{codepos1}]`
+  with the commands starting at the position designated by `{codeoffset1}`.
+
+In all cases, the swap is only valid when the exchanged fragments are
+independent, so that the transformation preserves the program semantics.
+
+------------------------------------------------------------------------
+Example (single statement)
+------------------------------------------------------------------------
+
+The following example swaps two adjacent assignments that do not interfere.
+The returned result is unchanged, but the rewritten program may be more
+convenient for subsequent proof steps.
+
+.. ecproof::
+
+  require import AllCore.
+
+  module M = {
+    proc reorder(x : int) : int = {
+      var a, b : int;
+      a <- x + 1;
+      b <- x + 2;
+      return a + b;
+    }
+  }.
+
+  lemma reorder_correct (n : int) :
+    hoare [ M.reorder : x = n ==> res = (n + 1) + (n + 2) ].
+  proof.
+    proc.
+
+    (*$*) (* Swap the command at position 1 with the next command (offset +1). *)
+    swap 1 1.
+
+    (* The goal is the same, but with the program rewritten. *)
+    admit.
+  qed.
+
+------------------------------------------------------------------------
+Example (swapping a block)
+------------------------------------------------------------------------
+
+The following example illustrates the block form
+`swap [{codepos1}..{codepos1}] {codeoffset1}`.  We swap a block of two
+commands with a later, independent command.
+
+.. ecproof::
+
+  require import AllCore.
+
+  module M = {
+    proc swap_block(x : int) : int = {
+      var a, b, c : int;
+
+      a <- x + 1;      (* 1 *)
+      b <- x + 2;      (* 2 *)
+      c <- x + 3;      (* 3 *)
+      a <- a + 10;     (* 4 *)
+
+      return a + b + c;
+    }
+  }.
+
+  lemma swap_block_correct (n : int) :
+    hoare [ M.swap_block : x = n ==> res = (n + 1 + 10) + (n + 2) + (n + 3) ].
+  proof.
+    proc.
+    (*$*)
+    (* Swap the block [2..3] (b <- x+2; c <- x+3) with the following command
+       a <- a + 10. These fragments are independent since:
+       - the block assigns b and c, and
+       - the command updates a using only a. *)
+    swap [2..3] 1.
+
+    (* The goal is the same, but with the program rewritten. *)
+    admit.
+  qed.
+
+------------------------------------------------------------------------
+Example (invalid swap)
+------------------------------------------------------------------------
+
+The following example shows a swap attempt that fails because the two
+commands are not independent: the second command reads the value written by
+the first one.
+
+.. ecproof::
+
+  require import AllCore.
+
+  module M = {
+    proc bad_swap(x : int) : int = {
+      var a, b : int;
+      a <- x + 1;   (* 1 *)
+      b <- a + 2;   (* 2 *)
+      return b;
+    }
+  }.
+
+  lemma bad_swap_demo (n : int) :
+    hoare [ M.bad_swap : x = n ==> res = n + 3 ].
+  proof.
+    proc.
+
+    (*$*)(* This swap is invalid: b depends on a. *)
+    fail swap 1 1.
+
+    admit.
+  qed.