refactor(pl): pr bridges as recheckable per-logic rules

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the bridge tactics relating
judgements: bypr, pr_bounded, hoare, phoare split and
hoare split:

• rules/hoare/ecHoareOfBdHoare.ml: hoare [c : P ==> Q] from
  phoare [c : P ==> !Q] = 0%r (no exceptional postcondition);
  rules/bdhoare/ecBdHoareOfHoare.ml: the converse. The hoare tactic
  on a phoare goal is derived: the bound-changing consequence to
  = 0%r, then the rule.
• rules/bdhoare/ecBdHoarePr.ml: phoare [f : P ==> Q] ~ d from
  forall &m, 0%r <= d /\ (P => Pr[f(args) @ &m : Q] ~ d);
  rules/hoare/ecHoarePr.ml derives the hoare form from it and the view
  above. rules/equiv/ecEquivPr.ml: equiv [f1 ~ f2 : P ==> Q] from
  the equality of the distributions of two observed expressions; the
  node records their common type, re-checked by the builder.
• rules/bdhoare/ecBdHoarePrBounded.ml: a probability is in [0, 1] and
  that of false is 0, plus the premise forms P => 1%r <= d /
  P => d <= 0%r (the bound-changing consequence would add a
  0%r <= d conjunct, so they are kept as rules).
• rules/bdhoare/ecBdHoareSplit.ml: inclusion-exclusion on a conjunction
  or a disjunction, and the complement rule; the bound change and the
  phoare split b1 b2 : R case analysis are derived.
• rules/hoare/ecHoareSplit.ml: hoare split, derived from the
  consequence rules (no rule of its own).
• Each rule (statement and/or procedure form) is documented as an
  inference rule in its .mli and emits a node with a registered
  checker; side conditions (bound = 0%r, shape of the postcondition,
  bound combining the premises' bounds, ...) are part of the subgoal
  builders, so the checkers re-validate them.
• EcPhlPr, EcPhlCoreView, EcPhlBdHoare, EcPhlHiBdHoare and EcPhlHoare
  are reduced to dispatchers and adapters; their interfaces are
  unchanged. EcPhlPr.t_prfalse, which has no caller, is not migrated
  and is flagged as unsound in a comment.

Behaviour is preserved: on the new test, goals after every bridge
tactic and the error messages of every failing invocation are identical
to those of the unmodified build.

A new test, tests/pr-bridges.ec, exercises every rule reachable from the
surface syntax and the error paths (the procedure forms of the split
rules are not reachable: phoare split cannot type its bounds on a
procedure goal). 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,
except the unreachable ones; on the stdlib where the rule is used
there: hoareF-of-bdhoare 2 files, bdhoareS-of-hoare 9,
bdhoareF-of-hoare 4, bdhoareF-pr 9, equivF-pr 8, bdhoareS-prbounded 6,
bdhoareF-prbounded 4, bdhoareS-split-or 1).