The pHL while variant in question proves termination of the while loop by proving that the provided variant decreases every iteration but is bounded below by 0, meaning that its initial value is a bound on the number of iterations.
The problem is that that the tactic derives the probability bound entirely from the probability of reaching the while statement with the invariant satisfied, failing to take into account the case where it is not satisfied.
MRE:
require import Real.
op b: bool.
module M = {proc p() = {while (b) {}}}.
lemma bad: phoare[M.p: true ==> true] = 0%r.
proof.
proc.
by while false 0.
qed.
This is unrelated to the recent issue with negative probabilities.
The pHL while variant in question proves termination of the while loop by proving that the provided variant decreases every iteration but is bounded below by 0, meaning that its initial value is a bound on the number of iterations.
The problem is that that the tactic derives the probability bound entirely from the probability of reaching the while statement with the invariant satisfied, failing to take into account the case where it is not satisfied.
MRE:
This is unrelated to the recent issue with negative probabilities.