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

[Yiping106283]

Fixes #1102. Based on #1105 (negative-phoare-false, head bb75dba); this replaces the earlier version of this PR, which was based on main.

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). #1105 does not reach this: the rule never passes through conseq, bypr or exfalso, so with bb75dba the reproducer is still accepted. 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.

Under #1105's semantics a pHL judgement is false as soon as its bound is negative in some memory, whether or not that memory satisfies the pre-condition; the non-negativity side goal is therefore unconditional (forall &hr, 0%r <= bd) because a goal restricted to pre \/ inv, as in #1130, would still let the rule prove a judgement whose bound is negative outside those memories.

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 (stacked version to follow).

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, 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). 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 (the non-negativity one with ge0_qF, since the goal no longer carries card (fdom F.m) <= qF). No library file is affected. Overlap with Change pHL to prevent negative probabilities #1105's own script changes: in the same PRG.ec proof, Change pHL to prevent negative probabilities #1105's conseq goals inside the loop body already show 0%r <= (sumid ..)%r / card%r (twice), and the relocated while goal shows it once more for the whole loop; these are distinct goals of distinct rules (the while one is needed even when the body is closed without conseq), so nothing is discharged twice on one goal, but the three-line argument is repeated and could be factored into a have if preferred. No other theory or example is touched by both.

Test

• tests/phoare-while-neg-bound.ec (invariants true and false): the remaining goal forall &hr, 0%r <= -1%r is introduced with move=> &hr (which fails with "all goals are closed" on the Change pHL to prevent negative probabilities #1105 head, where the lemma goes through) and asserted unprovable with fail (by smt()).
• On Change pHL to prevent negative probabilities #1105 + this commit: make unit 96/96, make stdlib 128/128, make examples 49/49 (ECJOBS=3, local prover set). Reproducers: pHL seq permits negative probabilities #1100 and pHL call permits negative probabilities #1101 are rejected by Change pHL to prevent negative probabilities #1105, pHL while permits negative probabilities #1102 by this commit; the pHL rnd E soundness #1119 rnd reproducer is still accepted (separate PR).

Note on CI: the external-project checks fail here for the same reason as on #1105 itself — CI looks for a merge-<this branch> branch on each downstream repository and otherwise checks out their default branch, which does not have the #1105 script changes yet.