feat(phl): support backward ecall on bdHoare/phoare goals

[mbbarbosa]

Extend backward ecall to bdHoare statement goals, so a bdHoare/phoare contract can be applied to the last call of a phoare goal — mirroring the existing hoare backward ecall.

• ecPhlExists.ml: add t_ecall_bdhoare_bwd / process_ecall_bdhoare, and dispatch FbdHoareS in process_ecall (phoare added to the no-xhl error kinds). Program-variable contract arguments are handled via the existing ecall abstraction machinery; a trivial probability split routes the suffix call through t_bdhoare_seq, lifting the hoare prefix subgoal via t_hoareS_conseq_bdhoare.
• ecPhlConseq.mli: expose t_hoareS_conseq_bdhoare / t_hoareF_conseq_bdhoare.

[strub]

Pushed a few changes on top of this:

1. Reject out-of-scope phoare goals up-front. The trivial probability split in t_ecall_bdhoare_bwd (f1=f2=1, g1=g2=0) only discharges the bound side-conditions when the goal — and the contract — are lossless = 1%r. For any other comparison/bound (e.g. phoare[…] <= 1/2), the tactic previously failed opaquely deep inside t_call/apply, with a message referencing a synthesized <= 1%r goal the user never wrote and blaming the contract for "not applying". Added two guards in t_ecall_bdhoare_bwd — one on the goal, one on the contract — that tc_error with an explanatory message ("only supported for lossless = 1%r goals" / "requires a lossless = 1%r contract") instead.

2. Dropped the unused t_hoareF_conseq_bdhoare export. Only the S variant is used (by t_ecall_bdhoare_bwd); the F export had no users outside ecPhlConseq.ml. The implementation stays — only the .mli line was removed.

3. Fixed the stale header comment on t_ecall_bdhoare_bwd: it claimed the tactic does not elaborate a seq and yields "the same shape as plain call", but it does use t_bdhoare_seq and hands back the lifted lossless prefix.

4. Added tests/phoare-ecall-bwd.ec — the lossless backward ecall positive path plus the forward / side-annotation / non-lossless-goal / non-lossless-contract rejections.