refactor(pl): looptx as program transformations

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the loop transformations
(fission, fusion, unroll, splitwhile) onto the transformation
rule of each logic:

• rules/transforms/ecTrFission.ml, ecTrFusion.ml, ecTrUnroll.ml,
  ecTrSplitWhile.ml: four catalogue entries, with resolved parameters
  (a normalized, possibly nested, code position; the prelude length and
  the body offsets; the typed condition of splitwhile). Each one is a
  pure function of the statement that re-checks all its side conditions
  (a loop at the position, the prelude and the offsets, the side
  conditions of fission / fusion as on main: read / write independence,
  deterministic and loop-, call- and raise-free prelude and epilog,
  raise-free body parts, without calls that may raise when the
  judgement observes exceptions; the equality of the preludes, epilogs
  and conditions of fusion), raising today's messages. No obligation,
  the memory is unchanged.
• EcMatching.Position.cpos_of_nm_cpos: the code position denoting a
  normalized one, so that the entries rebuild their zipper from the
  recorded position without any lookup.
• The tactics are derived, in every logic where they exist (hoare,
  ehoare, phoare, equiv on either side): resolve the position, then
  apply t_<logic>_transform with the entry. They are uniform across
  logics, so EcPhlLoopTx holds a single dispatcher on the goal kind
  (no per-logic module that would only hold a one-line call). The
  no-op t_low* wrappers are gone; unroll for stays derived (rcond,
  wp, seq, conseq, cfold). The interface of EcPhlLoopTx is unchanged.
• EcLowPhlGoal.t_code_transform (and its helpers t_fold, t_zip
  and their types) had no user left: removed.

Behaviour is preserved: on every step of the new test, the goals and
the error messages printed by the reference and new builds are
identical.

tests/fission-fusion-soundness.ec passes unchanged. A new test,
tests/looptx.ec, exercises each transformation in every
logic (both equiv sides, the transformed program checked against its
expected form with sim), at nested positions (then / else branches,
match branch, loop body), unroll for, and every error path; it passes
with the reference build too. The stdlib (128 files), the unit tests
(126) and the examples (49) pass under EC_RECHECK=1 with no
RecheckFailure. Each transformation checker, when deliberately broken
for the loop entries only, is caught only under EC_RECHECK: on the new
test, and, for equiv-transform, on the stdlib (3 files) and the
examples (4); hoare-, ehoare- and bdhoare-transform are reached by the
loop transformations only in the new test.