refactor(pl): codetx as program transformations

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the codetx tactic class (kill,
alias, set, set-match, cfold, case <- and simplify if) onto the
transformation rule of each logic:

• rules/transforms/ecTr{Kill,Alias,Set,SetMatch,CFold,AsgnCase,
  SimplifyIf}.ml: seven catalogue entries, with resolved parameters
  (normalized, possibly nested, code positions; typed expressions; the
  matched subterm and its occurrences for set-match). Each entry
  re-checks its side conditions (kill: the killed code writes nothing
  read by the code that may run after it, loops included, as computed by
  EcPV.zpr_pv, or by the postcondition; set-match: the
  selected occurrences are alpha-equivalent to the named subterm; the
  tuple split: the assigned variables are not read by the expression;
  ...) with today's messages, so the checker re-validates them.
• rules/ecPlTransform.ml: a new obligation kind, OLossless ks (the
  statement ks is lossless), stated by each of the four transformation
  rules as phoare [ks : true ==> true] = 1 in the memory of the
  transformed program: the premise kill has always stated.
• kill reads the postcondition through the context of the rule, which
  for hoare includes the exceptional postconditions (as on main since
  the corresponding fix).
• EcMatching.Zipper.zipper_of_nm_cpos: the zipper at a normalized code
  position, without environment.
• EcPhlCodeTx is reduced to derived tactics and a logic-agnostic
  dispatcher onto the transformation rule of the goal's logic; its
  interface is unchanged, the no-op FApi.t_low* wrappers are dropped,
  and it no longer uses EcLowPhlGoal.t_code_transform (still used by
  EcPhlLoopTx). weakmem changes the memory type of the goal: it is not
  a program transformation and is left unchanged.

Behaviour is otherwise preserved: on the new test, the goals after
every step and the error messages of every failing invocation are
identical to those of the unmodified build. Anomalies (assertion
failures) raised by case <- on ill-formed input are kept, their
reported source location aside.

A new test, tests/codetx.ec, exercises every entry in every logic
(hoare, ehoare, phoare, both equiv sides), at top-level and nested
positions, the error paths, and the kill of a variable read by an
exceptional postcondition (rejected); tests/kill-exn.ec and
tests/kill-loop.ec pass unchanged. The stdlib, the unit tests and the examples pass
under EC_RECHECK=1 with no RecheckFailure. The transformation checkers,
when deliberately broken on the entries of this class, are caught only
under EC_RECHECK: on the new test, on the stdlib (bdhoare-transform 1,
equiv-transform 2), the other unit tests (hoare-transform 2) and the
examples (hoare-transform 1, bdhoare-transform 1); ehoare-transform only
by the new test.