refactor(pl): skip as recheckable per-logic rules

[strub]

Fourth PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the skip tactic class:

• rules/hoare/ecHoareSkip.ml, rules/ehoare/ecEHoareSkip.ml,
  rules/bdhoare/ecBdHoareSkip.ml, rules/equiv/ecEquivSkip.ml: one
  trusted rule per logic, documented as an inference rule in its .mli,
  emitting a (parameterless) node with a registered checker. The
  rules' side conditions (empty statements; for bdhoare, a = or >=
  comparison) are part of the subgoal builder, so the checker
  re-validates them.
• bdhoare skip keeps its derived form, t_bdhoare_skip_full: the
  bound-changing consequence to = 1%r (temporarily from the
  unmigrated EcPhlConseq), then the rule.
• EcPhlSkip is reduced to the logic-agnostic dispatcher (interface
  unchanged); the no-op FApi.t_low0 wrappers are dropped.

Behaviour is preserved; the only change is that the bdhoare rule,
applied directly to a <= goal, now explains why it fails instead of
raising an empty error message.

A new test, tests/skip.ec, exercises the four logics (including a
bound other than 1 and the failing cases). The stdlib and the unit
tests pass under EC_RECHECK=1 with no RecheckFailure; each checker,
when deliberately broken, is caught only under EC_RECHECK (stdlib:
hoare 27 files, bdhoare 33, equiv 34; ehoare, unused in the stdlib,
on tests/skip.ec).