fix(phl): check the bound of the upper-bound while rule on all memories

[Yiping106283]

Fixes #1102.

Summary

The pHL while tactic (invariant only, <=) accepted phoare[M.p : true ==> false] <= (-1%r) for while (true) {}, and likewise with the invariant false and a diverging prefix (the variant noted by @oskgo in #1119). Following #1095, the conditions on the bound are now emitted by the rule as separate goals quantified over all memories, and the while tactic tries t_trivial on them. The semantics of phoare judgements are unchanged.

A distinct bug of the same rule, the bound being written by the statements preceding the loop, is not fixed here (its goals hold for that example); see #1124 and the companion PR #1131.

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

The rule is a fixpoint induction whose base case (the loop diverges: probability 0) and exit case need 0%r <= bd, and whose exit case needs inv /\ !e /\ post => bd = 1%r. The exit condition was emitted inside the post-condition of the hoare judgment on the prefix, which only has to hold on its terminating runs, and 0%r <= bd was not required at all, so a diverging loop -- or a diverging prefix with the invariant false -- proved any bound.

Fix

The prefix goal becomes hoare[s : pre ==> inv]; the exit condition forall &hr, inv /\ !e /\ post => bd = 1%r and the non-negativity forall &hr, pre \/ inv => 0%r <= bd are emitted by the rule as separate goals quantified over all memories (always, in this order, after the body and prefix goals). pre \/ inv is exactly what the derivation consumes: pre for the mass lost to a diverging prefix, inv for the base and !post-exit cases of the induction. The while tactic (process_while) tries t_trivial on the two of them so trivial cases stay effort-free.

The exit condition is kept as bd = 1%r (the condition the rule always had, merely relocated); the exact need is 1%r <= bd, and it can be relaxed to that at zero cost if preferred.

Impact

• Behavioural change: while inv on a <= judgement now yields four goals instead of two (body, prefix, exit bound, non-negativity); the last two are closed automatically when trivial (literal bounds such as 1%r, 0%r with post = false, or 0%r <= bd in context). A while whose old prefix goal was closed by auto/skip with the exit condition inside the post-condition now closes the relocated goals separately.
• Library and examples: examples/PRG.ec closes the two relocated goals (one line each). No library file is affected.

Test

• tests/phoare-while-neg-bound.ec (invariants true and false): the remaining goal 0%r <= -1%r is introduced with move=> &hr _ (which fails when the goal is not emitted) and asserted unprovable with fail (by smt()).
• make unit and make stdlib pass; examples/PRG.ec compiles with the fixed binary.