fix(phl): require the invariant on loop entry in the while variant rule

[Yiping106283]

Fixes #1103.

Summary

while I v (strict variant) accepted phoare[M.p : true ==> true] = 0%r for while (b) {} with the invariant false: the bound was derived only from the probability of reaching the loop with the invariant satisfied. The rule now additionally requires, for <= and =, that no terminating run of the prefix reaches the loop outside the invariant. The semantics of phoare judgements are unchanged.

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

From a memory satisfying I /\ G (the invariant together with the generalized termination and exit conditions), the loop terminates with probability 1 in a memory satisfying the post-condition, so Pr[s; while] >= Pr[s : I /\ G] always holds and the >= rule is sound. For <= and =, the runs of s that reach the loop outside I /\ G contribute an unknown probability (the loop may diverge or terminate anywhere), and the rule ignored them.

Fix

For <= and =, the rule emits the extra goal hoare[s : pre ==> I /\ G] stating that no terminating run of s reaches the loop outside the invariant, except when the bound is syntactically 1%r (then Pr[..] <= 1%r holds unconditionally, and = 1%r follows from the >= direction), so that losslessness proofs keep their two goals. The while tactic (process_while) tries EcPhlAuto.t_pl_trivial on the extra goal so trivial cases stay effort-free; the rule itself emits it unconditionally (#1095).

Two design points for review:

1. The 1%r exception departs from "always emit, let the caller try t_trivial". It is redundant there (see above) and it keeps every in-tree losslessness proof through while I v at exactly two goals. The uniform alternative is to always emit hoare[s : pre ==> I /\ G] (with t_pl_trivial tried on it), at the cost of one extra goal in every losslessness proof whose prefix does not trivially establish the invariant. Happy to switch if you prefer the uniform rule.
2. Completeness: for <= and = with a bound other than 1%r, the invariant must now hold on every terminating run of the prefix. A proof that bounds a probability decided before the loop (a sampled value, as in MEE-CBC below) can no longer go through while I v directly and needs a seq at the sampling. That is inherent to a hoare-shaped premise (the fully general premise is Pr[s : !(I /\ G)] <= bd' with bd + bd', which is what seq provides).

Impact

• Behavioural change: while I v on a <= or = judgement with a bound other than 1%r yields a third goal, hoare[s : pre ==> I /\ G], closed automatically when trivial. >= judgements and = 1%r/<= 1%r losslessness proofs are unchanged.
• Examples: examples/MEE-CBC/FunctionalSpec.ec (mee_encrypt_correct) relied on the unsound step (its invariant holds only when the sampled IV is the right one; the old script fails at qed on the fixed binary). It is restructured with seq at the sampling: the = 1%r branch goes through the loop rule, the = 0%r branch through hoare and the hoare while rule with the negated event added to the invariant. No library file is affected.

Test

• tests/phoare-while-vrnt-inv.ec: fail (by while false 0) for =, fail (by while false 0; auto) for <=; the >= direction and a = 1%r losslessness proof are still accepted.
• make unit and make stdlib pass; examples/MEE-CBC/FunctionalSpec.ec compiles with the fixed binary.