phl: recheckable proof-nodes and the basis of the program-logic refactoring

[strub]

First PR of a stack that reorganizes 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.

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.
• EcPhlRecheck: 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.

[strub]

Superseded by #1154 (the branch was renamed to pl/recheck-basis, which closed this PR).