feat(pl): recheckable proof-nodes for program-logic rules

[strub]

First PR of a stack that reorganizes the program-logic tactics
(src/phl) into a uniform four-layer structure per tactic (dispatch,
elaboration, rule, checker), one tactic class per PR. The design and
the per-tactic recipe are in src/phl/REFACTORING.md; src/phl/README.md
is the short reference. This supersedes the draft #1041.

The design also fixes two conventions every migrated rule follows: a
trusted rule is stated on exactly the statement it governs, with no
implicit seq-ing or framing (splitting is the seq rule's job, framing
that of a single frame rule per logic; surface tactics acting on
larger programs are derived compositions), and each rule is
documented in its .mli as an inference rule, separately from the
derived tactics.

Today a low-level tactic closes its goal with an opaque VExtern node:
the tag records that a rule fired, not with which parameters, so a
proof step cannot be re-validated. This PR adds the kernel support for
recheckable nodes, without migrating any rule yet:

• ecCoreGoal: an open rule type and a VRule of rule * handle list
  validation node, emitted by FApi.xrule / xrule1 / xrule_hyps /
  xrule1_hyps; a registry of rule checkers (register_rule_checker) and
  a driver, recheck_proofenv, that reruns the checker of every VRule
  node of a proof (raising RecheckFailure on mismatch). Nodes without a
  registered checker, and VExtern nodes, are skipped.
• ecScope: the driver runs at qed when EC_RECHECK is set, so normal
  runs pay nothing.
• EcPlRecheck: shared checker scaffolding. A checker rebuilds the
  subgoals from the recorded parameters and compares them, up to
  conversion, with the stored ones.

No behaviour change: with no rule migrated, the stdlib and the unit
tests pass unchanged, with and without EC_RECHECK=1.