refactor(pl): explicit, recheckable frame rule per logic

[strub]

Third PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). Framing — generalizing a condition over the
variables a program writes — becomes explicit: it is done by one
trusted frame rule per logic, and by nothing else.

• rules/ecPlFrame.ml: the framing conditions (statement / procedure,
  one- / two-sided), i.e. the only place computing the written
  variables (s_write / f_write) and generalizing over them. Shared by
  the frame rules and by conseq auto.
• rules/hoare/ecHoareFrame.ml, rules/bdhoare/ecBdHoareFrame.ml,
  rules/equiv/ecEquivFrame.ml: the frame rules — framed weakening of
  the postcondition — for statements and procedures, each emitting a
  node recording the new postcondition and with a registered checker.
  The checker recomputes the written variables from the goal's own
  context, so this soundness-critical step is re-validated.
• EcPhlConseq: the former notmod rules and their condition builders
  are now adapters onto these modules; the framed consequence
  (t_*_conseq_nm) remains a derived composition of the frame rule and
  the (not yet migrated) consequence rule, and so do the seq derived
  forms that use it.

Behaviour is unchanged (ehoare framing, done through concave, is left
to the conseq migration). The stdlib and the unit tests pass under
EC_RECHECK=1 with no RecheckFailure; each of the six checkers, when
deliberately broken, is caught on the stdlib (hoareS 14 files, hoareF
3, bdhoareS 6, bdhoareF 8, equivS 13, equivF 17) and only under
EC_RECHECK.