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

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the call tactic class (call in
every logic, with a specification, an invariant call (: I), the upto
form call (: bad, I, J), one-sided call{i}, and call /fc):

• rules/hoare/EcHoareCall: rule

  hoare [f : P ==> Q | E_f] |-
  hoare [lv <@ f(a) : P[arg := a] /\ W ==> R | E]
  

  on the call alone, W being the weakest precondition of the call
  computed as before
  (forall result (mod f), Q[res := result] => R[lv := result], and
  the exceptional conditions).

• rules/ehoare/EcEHoareCall: the existing core rule on the call alone,
  now a recheckable node; call /fc moves there.

• rules/equiv/EcEquivCall: the two-sided rule on the two calls alone,
  and the one-sided rule on lv <@ f(a) ~ skip (premise
  phoare [f : P ==> Q] = 1%r).

• rules/bdhoare/EcBdHoareCall: the bdhoare rule keeps its composite
  statement on c; lv <@ f(a) (implicit seq and framing): the bdhoare
  seq rule also bounds the runs of the prefix ending outside the
  intermediate assertion, which this rule does not. It is documented as
  such and is now a recheckable node, whose builder re-checks the
  conditions on the bound of fix: reject a pHL bound read in another memory by call / rnd #1189.

• The surface tactics are derived: seq before the call(s), with the
  weakest precondition of the call(s) as intermediate assertion, then
  the rule; the specification premise comes first, as before. Their
  side conditions are re-checked by the builders of the rules.

• rules/EcPlCall: the result assignment and argument substitution
  shared by the rules.

• The typing of the cut of call (specification, invariant, upto) moves
  to each logic's module (process_<logic>_call_cut). EcPhlCall is
  reduced to the dispatchers and positional adapters; its interface is
  unchanged.

Behaviour is preserved: the goal traces (compile -trace) of the 81
files of theories/, tests/ and examples/ using call that compile are
identical (the order of the module restrictions in a printed context of
examples/prg-tutorial/PRGc.ec differs, as it follows identifier
creation), and so are the error messages of the 25 failing calls of
the new test.

call /fc types its cut as call does (the fix of #1196 on main,
carried over). The documentation records one soundness issue, not
addressed here: the bdhoare rule with an explicit bound for the
procedure (OCaml API only, never given by the tactics) is unsound for
=, and for >= with a non-positive bound.

Validation: tests/call-rules.ec (every rule in every logic, the
derived forms and their error paths; it also passes with the previous
build); stdlib (128 files) and unit (147) under EC_RECHECK=1 with no
RecheckFailure; the 25 examples using call under EC_RECHECK=1. Each
checker, when broken, is caught only under EC_RECHECK=1, on the new
test and on the stdlib: hoare-call 12 files, bdhoare-call 21,
equiv-call 28, equiv-call-onesided 5, ehoare-call 0 (unused there).