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

[strub]

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

• rules/ecPlSp.ml: the strongest-postcondition calculus, moved
  unchanged out of EcPhlSp, shared by the rules of every logic.

• rules/hoare/ecHoareSp.ml, rules/equiv/ecEquivSp.ml: trusted rules
  stated on the sp-able statement(s) only,

  hoare [c : P ==> sp(c, P)]
  

  and

  equiv [c ~ c' : P ==> sp(c, c', P)]
  

  each with a parameterless node and a registered checker; the side
  conditions (sp-able statements, postcondition convertible to their sp)
  are part of the subgoal builder. The surface sp is now derived: the
  migrated seq rule at the end of the longest sp-able prefix
  (two-sided for equiv), with sp as intermediate assertion, its first
  premise closed by the sp rule. The visible goal is unchanged.

• rules/bdhoare/ecBdHoareSp.ml: the bdhoare rule keeps its implicit
  seq, i.e. it is still stated on c1; c2, with the resolved split
  index in its node and a registered checker. Deriving it from the
  bdhoare seq rule would need closing extra premises (a bound for the
  prefix, the arithmetic and non-modification premises) with
  best-effort tactics and a further trusted rule; this is documented
  as such in its .mli. Its side condition (the bound is not written by
  the prefix) is re-checked by the builder.

• EcPhlSp is reduced to the logic-agnostic dispatchers (interface
  unchanged); the no-op FApi.t_low1 wrapper is dropped. ehoare goals
  are still not supported.

Behaviour is preserved: goals and error messages are identical, as
checked against an unmodified build on 38 sp invocations (all logics,
positions, failing cases).

A new test, tests/sp.ec, exercises the three logics, positions,
exceptional postconditions and the error paths. The stdlib and the unit
tests pass under EC_RECHECK=1 with no RecheckFailure; each of the three
checkers, when deliberately broken, is caught only under EC_RECHECK
(on the new test, and on the stdlib: hoare-sp 7 files, equiv-sp 16,
bdhoare-sp 8). The examples using sp also pass under EC_RECHECK=1.