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

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the circuit tactic class
(circuit, circuit simplify, extens), which closed or rewrote goals
with the opaque VBdep validation:

• circuit: trusted rules without premise EcHoareCircuit,
  EcEquivCircuit and, on a goal that is not a statement judgement,
  EcFolCircuit (new rules/fol/, for the rules whose conclusion is a
  plain formula). Parameterless nodes; the checkers ("hoare-circuit",
  "equiv-circuit", "fol-circuit") re-run the circuit decision, a
  deterministic function of the goal and its hypotheses (expensive:
  only under EC_RECHECK).
• circuit simplify: trusted rule EcHoareCircuitSimplify, whose
  premise has the postcondition simplified by circuits; the checker
  ("hoare-circuit-simplify") re-runs the simplification.
• extens: trusted rules EcHoareExtens (one premise per value of a
  program variable of a type bound to a bitstring; node: the resolved
  variable) and EcFolExtens (all p (iota_ s n) from its n
  instances); checkers "hoare-extens" and "fol-extens". The tactic is
  derived: the rule, then the given tactic on each premise, which must
  close it. The proofs of the instances are now kept in the proof tree
  (and rechecked), instead of being discarded.
• The translation of the precondition and the decision of the
  postcondition, shared by the hoare and equiv rules, move to
  rules/EcPlCircuit.
• EcPhlBDep is reduced to the dispatchers and the derived extens;
  its interface is unchanged.

Behaviour is preserved, error messages included.

Validation: new test tests/circuits/circuit_rules.ec (every rule, every
error path), passing with and without the change, the error messages
compared; stdlib + unit under EC_RECHECK=1. Each checker, when broken,
is caught only under EC_RECHECK; the rules are not used by the stdlib,
only by tests/circuits.