fix(phl): reject a bound written by the prefix in the upper-bound while rule

[Yiping106283]

Fixes the while part of #1124.

Summary

The pHL while tactic (invariant only, <=) accepted phoare[P.p : true ==> true] <= (if P.y = 0 then 1%r else 0%r) for y <- 0; while (x < 1) { x <- x + 1; }, which is false whenever P.y <> 0 initially (the procedure terminates with probability 1). This is distinct from #1102: the goals introduced for #1102 (exit bound, non-negativity) hold for this bound with the invariant P.y = 0, and the two fixes are independent (this one applies on main with or without the #1102 PR #1130).

Root cause (src/phl/ecPhlWhile.ml, t_bdhoare_while_rev_r)

The bound of the conclusion is interpreted in the initial memory, while the body goal (bdhoare[w : inv ==> post] <= bd => bdhoare[c; w : inv /\ e ==> post] <= bd) interprets it in the memory the loop starts from. Nothing prevented the statements preceding the loop from writing the bound, in which case the two differ. The call and rnd phi d1 d2 d3 d4 rules have the same shape (#1124); rnd E is not affected, as it already binds the bound to a fresh local when the prefix writes it.

Fix

The tactic rejects a bound that depends on variables written by the statements preceding the loop (PV.indep env (s_write env rem_s) (PV.fv env m bd), error "The bound cannot depend on variables written by the statements preceding the loop"), as while ... : k eps (t_bdhoare_while_rev_geq_r) already does for its own arguments. This is over-strict for true judgements such as phoare[P.p : P.y = 0 ==> true] <= (P.y%r + 1%r) (workaround: conseq to a constant bound first). A more permissive, equally sound alternative is a seq-style non-modification goal forall r, hoare[s : pre /\ r = bd ==> r = bd] (condnm in src/phl/ecPhlSeq.ml), tried with t_pl_trivial and left to the user otherwise; the hard error was chosen for consistency within the file and can be switched if preferred.

Impact

• Behavioural change: while inv on a <= judgement now fails with a tactic error when the bound mentions a variable written before the loop. No library or example file is affected.

Test

• tests/phoare-while-prefix-bound.ec: fail (while (true)) on the false judgement above (with the bound P.y%r + 1%r).
• make unit and make stdlib pass.