refactor(pl): rcond and rmatch as program transformations

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the rcond / rmatch tactic
class (rcondt, rcondf, match C k) onto the transformation rule of each
logic:

• rules/transforms/ecTrRCond.ml, ecTrRMatch.ml: two catalogue entries,
  with resolved parameters. rcond (instruction index, branch) decides
  the if / while at that index, with the obligation
  OPrefixPost (hd, b) (resp. !b). rmatch (instruction index,
  constructor index) decides the match, the arguments of the
  constructor being assigned to fresh program variables
  (ys <- oget (get_as_C e)), with the obligation
  OPrefixPost (hd, exists xs, e = C xs): the unframed form of
  match C k.
• rules/ecPlRCond.ml: the decisions shared by the entries, the framed
  rules and the tactics (the instruction at a resolved index, the
  rmatch decomposition and framing condition, and the tactic-side
  resolution with today's error messages).
• rules/{hoare,ehoare,bdhoare,equiv}/ecRMatch.ml: the framed
  form of match C k (used when the variables of e are neither read
  nor written by the prefix, and the judgement is hoare, ehoare or
  phoare <=, or the prefix is empty) adds e = C ys to the
  precondition: it is not a program transformation, so it stays a
  separate trusted rule per logic, t_<logic>_rmatch_framed, kept
  over the whole statement (implicit seq) pending a later discussion.
  Its node records the resolved indices, its pure builder re-checks
  every side condition (a match, a valid constructor, e independent
  of the prefix, the per-logic termination condition), and its
  checker is "-rmatch-framed". The .mli states it as an
  inference rule and why it is only sound under that condition.
• The tactics are derived in every logic (EcRCond,
  EcRMatch): resolve the position and the constructor, check
  what they always checked, then apply t_<logic>_transform with the
  entry (equiv: on the given side), or the framed rule when today's
  condition selects the framed form. The t_low* wrappers are gone.
• EcPhlRCond is reduced to the dispatchers and positional adapters;
  its interface is unchanged, so if, match and unroll for keep
  using it (if now goes through the transformation rule, match
  through the framed rule).
• REFACTORING.md, README.md, EcPlTransform: the catalogue now lists
  rcond and rmatch, and names the framed-match rule.

Behaviour is preserved: on every rcond / match step of the new test
and of tests/rmatch-frame.ec, tests/rmatch-ehoare.ec and
tests/single_match.ec, the goals printed by the reference and new
builds are identical, and so is every error message, except for one
alpha-renaming: the prefix obligation of the unframed equiv
match C {i} k (non-empty prefix) is now stated as the transformation
rule states it for rcond, quantifying over &m (was the name of the
other memory, e.g. &2) with the hoare memory &hr (was &1). The
premises keep their order (obligation first).

A new test, tests/rcond.ec, exercises rcondt / rcondf on if and while
in every logic (both equiv sides, hoare exceptions kept), framed and
unframed match C k (hoare, ehoare, phoare <=, phoare = forcing
the unframed form, equiv with a non-empty prefix, empty prefix framed),
the plain match, and the error paths; it passes with the reference
build too. The stdlib (128 files), the unit tests (124) and the
examples (49) pass under EC_RECHECK=1 with no RecheckFailure. Each
checker, when deliberately broken, is caught only under EC_RECHECK:
on the new test, and on the stdlib through rcond / if for
hoare-transform (8 files), bdhoare-transform (13) and equiv-transform
(21). ehoare-transform and the four rmatch-framed checkers are not
used by the stdlib; they are caught on the unit tests (2 files for
ehoare-transform and ehoare-rmatch-framed, 3 for the hoare, bdhoare
and equiv rmatch-framed checkers).