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

src/phl/README.md

@@ -157,5 +157,8 @@ src/phl/
   logic rules in `rules/<logic>/`; `proc I` is derived (consequence + rule).
 - A rule relating two logics (e.g. the `pr` bridges) lives with the logic of
   its conclusion.
+- A rule concluding a probability statement from a judgement (`byphoare`,
+  `byehoare`, `byequiv`: `Ec<Logic>Deno`) lives with the logic of that
+  judgement.
 - Program transformations use the transformation rule of each logic; only
   their catalogue entries live in `rules/transforms/`.

src/phl/REFACTORING.md

@@ -177,6 +177,9 @@ uniform across logics or relate several judgements:
   in `rules/eager/`);
 - a rule relating judgements of two logics (the `pr` bridges, `hoare` from
   `phoare`, …) lives with the logic of its conclusion;
+- a rule concluding a statement on probabilities from a judgement
+  (`byphoare`, `byehoare`, `byequiv`) lives with the logic of that
+  judgement (`EcBdHoareDeno`, `EcEHoareDeno`, `EcEquivDeno`);
 - program transformations go through the transformation rule of each logic
   (`Ec<Logic>Transform`); only their catalogue entries live in
   `rules/transforms/`.