refactor(pl): rnd and rndsem as recheckable per-logic rules

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the rnd / rndsem tactic
class; the trusted rnd rules no longer seq implicitly where seq can
do it:

• rules/{hoare,ehoare}/ecRnd.ml: an axiom on the single sampling
  x <$ d, whose precondition is its weakest precondition (checked up
  to alpha-conversion by the rule and its checker). The surface rnd
  is derived: the migrated seq rule before the sampling, with that
  weakest precondition as intermediate assertion, then the axiom.
• rules/equiv/ecEquivRnd.ml: the same for equiv, with two axioms: the
  two-sided one, recording the bijection instantiated at the sampled
  types (well-typedness re-checked), and the one-sided one, on
  x <$ d ~ skip. The surface forms (seq + axiom, then the existing
  simplification of the remaining relation via conseq, and rnd : k k'
  through rndsem) are derived.
• rules/bdhoare/ecBdHoareRnd.ml: kept over c; x <$ d, documented as
  such: its premises are judgements on c (a hoare one for <=)
  that the bdhoare seq rule cannot reproduce, and it relies on c not
  writing the bound when it does not generalize it. The node records
  the event and bounds instantiated at the sampled type; the derived
  t_bdhoare_rnd_full tries to close the non-negativity premise.
• rules/{hoare,bdhoare,equiv}/ecRndSem.ml, with the shared
  semantic sampling in rules/ecPlRndSem.ml: rndsem is a trusted
  program transformation rewriting the suffix c[k..] in place; it
  keeps the prefix, which seq cannot express without an intermediate
  assertion.
• EcPhlRnd is reduced to the logic-agnostic dispatchers and the legacy
  adapters (interface unchanged); the no-op FApi.t_low* wrappers are
  dropped.

Behaviour is preserved: on the new test, the transcripts of the
reference and new builds (all goals printed after each command,
including every error message) are identical.

A new test, tests/rnd.ec, exercises every logic and form, including
the bdhoare non-negativity premise and the error paths. The stdlib and
the unit tests, and the 24 examples using rnd / rndsem, pass under
EC_RECHECK=1 with no RecheckFailure; each of
the eight checkers, when deliberately broken, is caught only under
EC_RECHECK, on the new test and, where the rule is used there, on the
stdlib (files: hoare-rnd 15, bdhoare-rnd 21, equiv-rnd 25,
equiv-rnd-onesided 13, equiv-rndsem 4; ehoare-rnd, hoare-rndsem and
bdhoare-rndsem are not used by the stdlib).