refactor(pl): codetx as program transformations

src/ecMatching.ml

@@ -650,6 +650,33 @@ module Zipper = struct
   let zipper_of_cpos (env : EcEnv.env) (cp : codepos) (s : stmt) =
     fst (zipper_of_cpos_r env cp s)
 
+  let zipper_of_nm_cpos ((cpath, cp1) : nm_codepos) (s : stmt) =
+    let step (zpr, s) ((k, br) : nm_codepos_step) =
+      let (s1, i, s2) = find_by_nmcpos1 k s in
+      match i.i_node, br with
+      | Swhile (e, sw), `Cond true ->
+          (ZWhile (e, ((s1, s2), zpr)), sw)
+
+      | Sif (e, ifs1, ifs2), `Cond true ->
+          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1)
+
+      | Sif (e, ifs1, ifs2), `Cond false ->
+          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2)
+
+      | Smatch (e, bs), `Match ix ->
+          let prebr, (locals, body), postbr =
+            try  List.pivot_at ix bs
+            with Invalid_argument _ | Not_found -> raise InvalidCPos in
+          (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body)
+
+      | _ -> raise InvalidCPos
+    in
+
+    let zpr, s = List.fold_left step (ZTop, s) cpath in
+    check_nm_cgap1 cp1 s;
+    let s1, s2 = split_at_nmcgap1 cp1 s in
+    zipper (List.rev s1) s2 zpr
+
   let zipper_of_cgap (env : EcEnv.env) (cp : codegap) (s : stmt) =
     fst (zipper_of_cgap_r env cp s)
 

src/ecMatching.mli

@@ -270,6 +270,14 @@ module Zipper : sig
    *)
   val zipper_of_nm_cgap : env -> nm_codegap -> stmt -> zipper
 
+  (* Return the zipper for the stmt [stmt] at the normalized code position
+   * [nm_codepos] (as returned by [zipper_of_cpos_r]): the cursor is before
+   * the designated instruction, or at the end of its block. Needs no
+   * environment ([z_env] is unset). Raise [InvalidCPos] if [nm_codepos] is
+   * not valid for [stmt].
+   *)
+  val zipper_of_nm_cpos : nm_codepos -> 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

@@ -99,15 +99,18 @@ equiv: one side at a time), parameterized by an entry of a catalogue:
   function, which may extend the memory with fresh program variables.
 - The obligations are abstract (a small closed set: so far, "every
   terminating run of the prefix `hd` from the precondition satisfies
-  `cond`"); each logic's rule states them as its own premises (see its
-  `.mli`).
+  `cond`" and "the statement `ks` is lossless"); each logic's rule states
+  them as its own premises (see its `.mli`).
 - The node records the transformation and its parameters; the checker
   ("<logic>-transform") re-runs it on the goal's program and compares the
   subgoals up to conversion (programs up to alpha-equivalence).
 
 Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`),
 `rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`), `match-push`
-(`EcTrMatchPush`), `swap` (`EcTrSwap`) and `inline` (`EcTrInline`). `if-push` / `match-push` push
+(`EcTrMatchPush`), `swap` (`EcTrSwap`), `inline` (`EcTrInline`), `kill`
+(`EcTrKill`), `alias` (`EcTrAlias`), `set` (`EcTrSet`), `set-match`
+(`EcTrSetMatch`), `cfold` (`EcTrCFold`), `asgn-case` (`EcTrAsgnCase`) and
+`simplify-if` (`EcTrSimplifyIf`). `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`).

src/phl/REFACTORING.md

@@ -342,18 +342,24 @@ parameterized by an entry of a **catalogue** of transformations:
   Entries live in `rules/transforms/`, one module `EcTr<Name>` each.
 - **The obligations** are **abstract** and form a small closed set; each
   logic's rule states them as premises of its own (first, in order, then the
-  transformed judgement — same pre/post, possibly extended memory). The only
-  kind so far is `OPrefixPost (hd, cond)`: every terminating run of the prefix
-  `hd` from the precondition ends in a state satisfying `cond`. Per logic:
-  - hoare: `hoare [hd : P ==> cond | E]` (the goal's exceptional
-    postconditions kept);
-  - ehoare: `hoare [hd : P_bool ==> cond]`, the precondition having the form
-    ``P_bool `|` f``;
-  - bdhoare: `hoare [hd : P ==> cond]`;
-  - equiv (transformation of side `i`): `forall &j, hoare [hd : P ==> cond]`,
-    the relation read on side `i` with the other memory quantified.
-
-  These are the premises `rcondt` / `rcondf` have always stated.
+  transformed judgement — same pre/post, possibly extended memory). The
+  kinds so far:
+  - `OPrefixPost (hd, cond)`: every terminating run of the prefix `hd` from
+    the precondition ends in a state satisfying `cond`. Per logic:
+    - hoare: `hoare [hd : P ==> cond | E]` (the goal's exceptional
+      postconditions kept);
+    - ehoare: `hoare [hd : P_bool ==> cond]`, the precondition having the
+      form ``P_bool `|` f``;
+    - bdhoare: `hoare [hd : P ==> cond]`;
+    - equiv (transformation of side `i`): `forall &j, hoare [hd : P ==>
+      cond]`, the relation read on side `i` with the other memory
+      quantified.
+
+    These are the premises `rcondt` / `rcondf` have always stated.
+  - `OLossless ks`: the statement `ks` terminates with probability 1 from
+    every state; in every logic `phoare [ks : true ==> true] = 1`, in the
+    memory of the transformed program (the premise `kill` has always
+    stated).
 - **The rules** `t_<logic>_transform` (`rules/<logic>/Ec<Logic>Transform`;
   equiv: one side at a time, the other program and memory unchanged) record
   `(transformation, resolved parameters)` (and the side) in their node. The
@@ -394,15 +400,35 @@ Current catalogue:
   parameters and locals renamed to fresh program variables added to the
   memory, result assigned (component-wise through fresh variables for a
   tuple pattern without `tuple`); no obligation), used by `inline` in every
-  logic.
+  logic;
+- `kill` (`EcTrKill`): removes the `n` instructions `ks` at a (possibly
+  nested) position, provided that what they write is read neither by the
+  code that may run after them (in their block and the enclosing ones, and
+  the guard and whole body of each enclosing loop) nor by the postcondition
+  (for hoare, including the exceptional ones); obligation `OLossless ks`;
+- `alias` (`EcTrAlias`): `lv <- e` / `lv <$ d` / `lv <@ f(a)` becomes
+  `x' <- e; lv <- x'` (resp. `<$`, `<@`), `x'` a fresh program variable;
+  no obligation;
+- `set` (`EcTrSet`): inserts `x' <- e` at a position, `x'` fresh; no
+  obligation;
+- `set-match` (`EcTrSetMatch`): names the subterm `t` matched in the
+  expression of an instruction, `x' <- t; i(e[occ := x'])`, the selected
+  occurrences being alpha-equivalent to `t`; no obligation;
+- `cfold` (`EcTrCFold`): propagates an assignment to local variables into
+  the following instructions as long as valid (eager or not), and
+  materializes it afterwards; no obligation;
+- `asgn-case` (`EcTrAsgnCase`): splits a tuple assignment into one
+  assignment per variable (`case <-`); no obligation;
+- `simplify-if` (`EcTrSimplifyIf`): turns a conditional whose branches are
+  assignments into a single assignment (`simplify if`); no obligation.
 
 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: kill/alias/cfold/set and proc rewrite.
+with the tactics that use them: the loop transformations 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