phl: reorganize the program logic into a recheckable four-layer structure

[strub]

Tracking PR for the full src/phl refactoring. It lands incrementally on refactor-pl, one tactic at a time, and stays open until the reorganization is complete. Each tactic keeps behaviour identical and touches no proof scripts. Design, rationale and the per-tactic recipe live in src/phl/REFACTORING.md; the short structural convention is in src/phl/README.md.

Goal

Replace today's "one file per tactic, all logics inside, typing entangled with goal-inspecting dispatch, opaque proof-nodes" structure with a uniform four-layer spine per tactic:

• dispatch process_<tactic> — logic-agnostic, inspects the goal kind, routes;
• elaboration process_<logic>_<tac> — types the parse-tree args, builds params;
• rule (TCB) t_<logic>_<tac> — computes subgoals via a pure shared builder and emits a node recording its params;
• checker check_<logic>_<tac> — reruns the builder from the recorded params and is_conv-compares against the stored subgoals.

Today a proof-node (VExtern tc \Tag [...]`) records that a rule fired but not with what — the tag carries no parameters and is never inspected — so proofs cannot be re-validated. This refactor makes every TCB step carry its parameters and registers a checker for it.

Kernel (ecCoreGoal)

• open type rule = .. + VRule of rule * handle list (recheckable sibling of VExtern);
• FApi.xrule[1][_hyps] emitting VRule;
• checker registry (register_rule_checker) over the open rule type, recheck_proofenv driver, RecheckFailure.

The driver runs at qed (ecScope.save_r), gated by the EC_RECHECK env var. Unmigrated nodes and rules with no registered checker are skipped, so migration is incremental and normal runs pay nothing.

Layout (by family, then logic)

(include_subdirs unqualified) flattens src/ into one library, so subdirs need no dune changes (module names stay globally unique):

• rules/<logic>/ — genuine logic rules (hoare/ehoare/bdhoare/equiv/eager)
• codetx/ — logic-uniform program transforms (wp, sp, inline, swap, rcond, …)
• bridge/ — probabilistic / cross-logic (deno, pr, byequiv, fel, upto, eager)
• multi/ — multi-logic tactics with shared machinery (conseq, trans, sym)

Progress

Phase 0 — scaffolding ✅ kernel rule/VRule/xrule, checker registry + recheck_proofenv, EC_RECHECK hook, docs.

Tactic migrations (each = a commit; seq/hoare is the reference pilot):

• seq — hoare
• seq — ehoare / bdhoare / equiv (+ one-sided)
• skip
• wp / sp (codetx pilot)
• cond / match
• rnd
• while (+ async)
• call
• fun
• exists
• rcond / rmatch
• inline, swap, kill/alias/cfold (codetx)
• fission / fusion / unroll / splitwhile (looptx)
• deno, pr, byequiv, fel, upto, eager (bridge)
• conseq / trans / sym (multi-logic, last)

Validation (continuous)

Every increment keeps dune build clean, the test suite green (-no-eco), and a full EC_RECHECK=1 sweep over the stdlib at zero RecheckFailure. Current: 91 theories + 23 seq-using tests pass under EC_RECHECK=1.