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

src/phl/README.md

@@ -162,5 +162,8 @@ src/phl/
   judgement.
 - The failure-event lemma (`fel`, `EcBdHoareFel`) concludes a probability
   bound from phoare premises; it lives in `rules/bdhoare/`.
+- The upto rule of `byupto` (`EcEquivUpto`, a premise-free rule concluding
+  `Pr[f1 : E /\ !bad] = Pr[f2 : E /\ !bad]` for procedures equal up to
+  `bad`) is relational: it lives in `rules/equiv/`.
 - Program transformations use the transformation rule of each logic; only
   their catalogue entries live in `rules/transforms/`.

src/phl/REFACTORING.md

@@ -185,6 +185,10 @@ uniform across logics or relate several judgements:
   `rules/bdhoare/`; it is stated on the whole procedure body (an implicit
   seq at the end of the initialization, there being no seq rule on
   probabilities);
+- the upto rule (`EcEquivUpto`, `byupto`), whose conclusion is an
+  equality of probabilities of two procedures, is relational and lives in
+  `rules/equiv/`; the forms of `byupto` other than `Pr[_] = Pr[_]` are
+  derived (a lemma of the real theory, the rule and `rewrite Pr`);
 - program transformations go through the transformation rule of each logic
   (`Ec<Logic>Transform`); only their catalogue entries live in
   `rules/transforms/`.