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

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the deno tactic class:
byphoare, byehoare and byequiv (including its upto-bad forms
Pr[..] <= Pr[..] + Pr[..] and byequiv : B):

• rules/bdhoare/ecBdHoareDeno.ml: Pr[f(args) @ &n : E] ~ d (<=,
  =, >=) from phoare [f : P ==> Q] ~ d, P on the arguments and
  memory of the goal and forall &m, E [=>] Q. The d = Pr[..] form is
  derived (symmetry, then the rule).
• rules/ehoare/ecEHoareDeno.ml: Pr[f(args) @ &n : E] <= d from
  ehoare [f : P ==> Q], P <= d%xr, forall &m, E%xr <= Q and
  0%r <= d (side conditions unchanged).
• rules/equiv/ecEquivDeno.ml: Pr[f1 ..] = Pr[f2 ..] (resp. <=) from
  equiv [f1 ~ f2 : P ==> Q], P on the arguments and memories of the
  goal and forall &1 &2, Q => (E1 <=> E2) (resp. =>). The upto-bad
  forms stay derived from it and the lemmas of Real.
• Each rule is documented as an inference rule in its .mli and emits a
  node recording P and Q, with a registered checker; the shape of
  the goal is re-validated by the shared subgoal builder, as is a new
  side condition: the memories of P and Q do not occur free in the
  goal (they are bound around the bound d or the events in the
  premises; the surface tactics always use fresh memories).
• EcPhlDeno is reduced to the dispatcher and the legacy adapters; its
  interface is unchanged.

Behaviour is preserved: on the new test, the goals after every
byphoare / byehoare / byequiv invocation and the error messages of
every failing one are identical to those of the unmodified build.

A new test, tests/deno.ec, exercises every rule and derived form (cut,
proof term, every comparison and orientation, eq flag, upto-bad forms
directly and through the consequence rule) and the error paths. The
stdlib, the unit tests and the examples pass under EC_RECHECK=1 with no
RecheckFailure. Each of the 3 checkers, when deliberately broken, is
caught only under EC_RECHECK (on the new test; on the stdlib where the
rule is used there: bdhoare-deno 19 files, equiv-deno 31; byehoare is
not used by the stdlib).