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

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the upto tactic class (byupto):

• new module src/phl/rules/equiv/EcEquivUpto: the upto rule
  t_equiv_upto, concluding

  Pr[f1(a1) @ &m : E] = Pr[f2(a2) @ &m : E]
  

  without premise, for E of the form E' /\ !bad or !bad and f1, f2
  syntactically equal up to bad; parameterless node REquivUpto (bad is
  read from the event), checker "equiv-upto". The pure core rechecks
  every side condition (same memory, convertible arguments,
  alpha-equivalent events, shape of the event, the upto-bad check on
  the procedures), so the checker re-validates them; the rule reports
  their failure with the tactic's messages;

• the upto-bad check moves along, unchanged, as the side condition of
  the rule;

• byupto (process_upto) stays derived: the Pr[] - Pr[],
  Pr[] <= Pr[] + Pr[_], `|_| <= `|_| and `|_| <= maxr _ _
  forms apply a lemma of the real theory and close its premises with the
  rule and rewrite Pr (TEMPORARY dependency on EcPhlPrRw);

• EcPhlUpto reduced to the legacy entry points, interface unchanged.

Behaviour is preserved: same goals and same error messages, in the
same order (compared with the reference build on every error path of
the new test).

Validation: new test tests/upto.ec (the rule, the derived forms, an
abstract procedure with oracles, and every error path) passes with the
reference build and this one under EC_RECHECK=1, as do the existing
upto tests and examples/upto_syntaxtic.ec; stdlib and unit pass under
EC_RECHECK=1 with no RecheckFailure. The checker, when broken, is
caught only under EC_RECHECK=1 (stdlib: no use of byupto; unit: 2
files, tests/upto.ec and tests/upto_adv.ec; also
examples/upto_syntaxtic.ec).