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

[strub]

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

• new trusted rule per logic, t_<logic>_weakmem
  (rules/{hoare,ehoare,bdhoare,equiv}/Ec<Logic>WeakMem; equiv: one
  side at a time): weakening of the memory of a judgement on a statement
  by fresh local variables it does not mention. The node records the
  typed variables (and the side); the pure builder restricts the goal's
  memory and re-checks that the variables are the last declared ones,
  fresh in the rest of the memory and unused by the judgement (new
  shared computation EcPlWeakMem); checkers "hoare-weakmem",
  "ehoare-weakmem", "bdhoare-weakmem", "equiv-weakmem".
• the tactic is derived in each logic (t_<logic>_weakmem_hyp): it cuts
  the hypothesis weakened by the variables, and closes the cut
  judgement by the rule (on each weakened side) and the hypothesis; the
  visible goal is the implication the tactic always produced.
• EcPhlCodeTx.process_weakmem keeps the lookup of the hypothesis and the
  typing of the variables, and dispatches on the logic of the
  hypothesis; its interface is unchanged. The opaque `WeakenMem
  node is gone.

Behaviour is preserved: same visible goal, same error messages in the
same order.

Validation: new test tests/weakmem.ec (every logic, each side and both
sides for equiv, the error paths; passes with the reference build and
this one under EC_RECHECK=1, with identical goals and error messages);
stdlib and unit pass under EC_RECHECK=1 with no RecheckFailure; each
checker, when broken, is caught only under EC_RECHECK=1, on the new
test and, for "bdhoare-weakmem", on the stdlib (1 failure:
Dexcepted.ec, the only use of weakmem; the other three rules are not
used by the stdlib).