refactor(pl): proc rewrite / change as program transformations

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates proc rewrite (and proc rewrite /=), proc change, proc change circuit and idassign onto the
program transformations (one trusted transformation rule per logic + a
catalogue of entries):

• four catalogue entries in src/phl/rules/transforms/:
  EcTrExprChange (replaces expressions of a possibly nested range, or of
  the whole statement, in program order; each replacement is stated over
  recorded identifiers for the match-arm locals in scope, with type and
  capture side conditions), EcTrStmtChange (replaces a range by a
  statement over fresh locals, bound by the entry with
  EcMemory.bindall_fresh; the modified, observable and shared-read
  variables are computed by the entry, loop case included),
  EcTrCircuitChange (the circuit-equivalence check and its keep-set are
  run by the entry, under the goal's hypotheses) and EcTrIdAssign
  (inserts x <- x);
• two new obligation kinds in EcPlTransform, with their premise in each
  of the four transformation rules: OExprEq (forall &m, forall xs,
  e = e') and OLocalEquiv (equiv [s ~ s' : ={R} /\ F{1} ==> ={W}]),
  whose frame F is computed by each rule from its own precondition
  (shared helper EcPlTransform.frame; for ehoare, the boolean part P of
  a precondition P | f, and no frame otherwise);
• the transformation context gets the goal's hypotheses (trc_hyps),
  needed by the circuit checker;
• EcPhlRewrite and EcPhlRwPrgm reduced to derived tactics: they resolve
  their arguments, keep their checks and messages, and apply the
  transformation rule of the goal's logic (rw_prgm: hoare only);
  proc rewrite still discharges its equalities on the spot;
  interfaces unchanged; proc rewrite pre untouched (conseq).

Behaviour is preserved (goals and messages compared with the reference
build on the new test and on the existing tests, including the ehoare
frame fixed on main), except for phoare proc change: the variables
read by the bound are no longer observable (the bound is evaluated in
the initial memory), so the postcondition of the local equivalence may
have fewer equalities.

Validation: new test tests/rewrite-transform.ec (every tactic in every
logic where it exists, both equiv sides, nested positions with
match-arm locals, fresh locals, error paths); stdlib, unit and examples
under EC_RECHECK=1, zero RecheckFailure. Each new premise (OExprEq,
OLocalEquiv, in each of the four rules) and each new entry, when broken
in the checker only, is caught only under EC_RECHECK (files caught on
stdlib / unit / examples: equiv OExprEq 1/4/0, hoare OExprEq 0/4/0,
ehoare and bdhoare OExprEq 0/1/0, hoare and equiv OLocalEquiv 0/2/0,
ehoare and bdhoare OLocalEquiv 0/1/0, expr-change 1/5/0, stmt-change
0/2/0, circuit-change 0/3/0, idassign 0/1/0).