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

[strub]

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

• rules/ecPlWp.ml: the weakest-precondition computation (wp, and ewp
  for ehoare), shared by the wp rules of every logic and moved out of
  EcPhlWp unchanged (minus an always-absent optional argument).
• rules/hoare/ecHoareWp.ml, rules/ehoare/ecEHoareWp.ml,
  rules/equiv/ecEquivWp.ml: a trusted rule stated on the suffix only,
  hoare [c2 : wp(c2, Q | E) ==> Q | E] (resp. ehoare with ewp, and
  two-sided equiv), with no premise. Its side conditions (the
  statement is entirely wp-able, the precondition is its wp up to
  conversion) are re-checked by the subgoal builder, which takes the
  goal's hyps; the node records only uselet.
• The surface wp (with or without positions) is now derived in these
  three logics: seq (EcHoareSeq / EcEHoareSeq / EcEquivSeq) at the
  resolved split index with R = wp(c2, Q), then the wp rule closes the
  suffix premise. The split is thus no longer implicit.
• rules/bdhoare/ecBdHoareWp.ml: the bdhoare rule keeps the implicit
  seq (phoare [c1 : P ==> wp(c2, Q)] ~ d proves
  phoare [c1; c2 : P ==> Q] ~ d), documented as such in its .mli: a
  derived composition through the bdhoare seq rule cannot reproduce
  its single premise. The node records the resolved split index.
• EcPhlWp is reduced to the logic-agnostic dispatchers (interface
  unchanged); the per-logic modules own the elaboration of positions.

Behaviour is preserved: same visible goals and same error messages
(checked goal by goal and error by error against the unmodified build
on the new test).

A new test, tests/wp.ec, exercises the four logics with and without
positions, exceptions, 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 22 files, bdhoare 24, equiv 29; ehoare, unused in the stdlib,
on tests/wp.ec). The examples using wp also pass under EC_RECHECK=1.