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

[strub]

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

• rules/<logic>/ec<Logic>FunDef.ml (hoare, ehoare, bdhoare, equiv): a
  concrete procedure by its body; parameterless node, the side
  condition (the procedure is not abstract) re-checked by the builder.
• rules/<logic>/ec<Logic>FunAbs.ml (hoare, ehoare, bdhoare, equiv): an
  abstract procedure with an invariant, stated on [f : I ==> I]
  exactly (bdhoare: >= 1%r); the node records the invariant, the
  builder re-checks that the procedure is abstract, the invariant
  independent of its globals, the oracles' memory restrictions
  (bdhoare) and that the goal is the conclusion of the rule (up to
  alpha-conversion). proc I is derived: the consequence rule to that
  conclusion, then the rule (bdhoare = 1%r through >= 1%r, as
  before). The hoare rule concludes with no exceptional postcondition;
  its .mli documents that it relies on unlisted exceptions being
  unconstrained.
• rules/equiv/ecEquivFunAbsUpto.ml: the abstract upto rule
  (proc B P Q, proc @[ll] ...), likewise stated on its own
  conclusion and derived through the consequence rule; its elaboration
  is shared with call.
• rules/<logic>/ec<Logic>FunToCode.ml (hoare, ehoare, bdhoare, equiv,
  and rules/eager/ecEagerFunToCode.ml): proc*, the procedure as a
  single call to fresh locals; parameterless nodes.
• rules/ecPlFun.ml: the computations shared by these rules (argument
  substitution, oracle restrictions, losslessness hypothesis of an
  abstract procedure, the single-call statement of proc*).
• EcPhlFun is reduced to the logic-agnostic dispatchers and the legacy
  adapters (interface unchanged, including FunAbsLow used by eager);
  the no-op FApi.t_low* wrappers are dropped. The dispatchers keep
  t_hF_or_bhF_or_eF (match on the goal, reducing it when it is not
  a judgement), as before.

Behaviour is preserved: on the new test, the transcripts of the
reference and new builds (all goals printed after each proc, and
every error message) are identical.

A new test, tests/proc.ec, exercises every rule in every logic (also
through call) and the error paths. The stdlib, the unit tests and
the examples pass under EC_RECHECK=1 with no RecheckFailure. Each of
the 14 checkers, when deliberately broken, is caught only under
EC_RECHECK, on the new test and, where the rule is used there, on the
stdlib (files: hoareF-fun-def 13, bdhoareF-fun-def 31, equivF-fun-def
32, hoareF-fun-abs 12, bdhoareF-fun-abs 2, equivF-fun-abs 29,
equivF-fun-abs-upto 9, equivF-fun-to-code 12; the ehoare rules and
the hoare, bdhoare and eager proc* rules are not used by the
stdlib).