[strub]

The bound of phoare[s; i : P ==> Q] cmp bd is interpreted in the
initial memory. Two pHL rules also used a bound in the memory reached
after s, without relating the two values:

• call (t_bdhoare_call) gives the bound of the goal (or its
  optional bound parameter) to the specification of the called
  procedure, which interprets it in the memory the procedure starts
  from: after s, and with the local variables of the callee instead
  of those of the caller. A bound written by s, or mentioning a
  local variable (read as the callee's variable of the same name),
  gave a false judgement.
• rnd phi d1 d2 d3 d4 checks phi => mu d E <= d2 (resp. d4)
  after s, but d1 * d2 + d3 * d4 <= bd in the initial memory.

All three allowed deriving false, e.g. (#1124)
phoare[M.g : !M.x ==> res] <= b2r M.x for
M.x <- true; r <@ f(); return true;, and likewise
phoare[N.g : true ==> res] <= b2r x for r <@ f(!x); return r;
where f(x) returns x.

Both rules now reject such bounds (as #1131 does for while): call
fails when the bound depends on a local variable or on a variable
written by s, rnd phi d1 d2 d3 d4 when d2 or d4 depends on a
variable written by s. A seq-style non-modification goal would be
more permissive, but no in-tree proof needs it: an instrumented build
saw 221 pHL call applications in unit, stdlib and examples, none
with a local or prefix-written bound, and no use of
rnd phi d1 d2 d3 d4. A bound can still be frozen in a logical
variable first.

Fixes the call and rnd phi d1 d2 d3 d4 parts of #1124 (its
while part is #1131).

Origin: the pHL call rule, 75d66ec (2013-06-06), and
rnd phi d1 d2 d3 d4, addc94d (2013-07-07); both first released in
r2022.04.

Test: tests/phoare-call-prefix-bound.ec and
tests/phoare-rnd-prefix-bound.ec (the previous build accepts every
fail line). unit (122 files), stdlib (128) and examples (49) pass.