[strub]

For phoare[while e do c : P ==> Q] >= bd (resp. = bd), the rule of
while I v k eps (t_bdhoare_while_rev_geq_r) only required, when the
loop is not entered, !Q => bd = 0%r (resp.
bd = if Q then 1 else 0), never bd <= 1%r elsewhere. With a loop
that is never entered, every other goal is vacuous, so (#1127)

phoare[M.f : true ==> true] >= 2%r

was accepted for while (false) {}, from which false follows.

Requiring Q => bd <= 1%r on loop exit, as suggested in #1127, is not
enough. The rule is an induction on the iterations of the loop that
starts from the probability 1: it needs bd <= 1%r in every memory
satisfying the pre-condition. Otherwise, the hypothesis of the
inductive goal holds for no statement, and that goal can be proved for
a bound that grows along the iterations. For a loop that exits with
probability 1/2 and otherwise increments i, the bound

if b then 2 ^ i + 1 else 1

satisfies every goal, including the suggested one (it is 1 on exit),
with >= as with =, and gives false as well.

The rule now also emits

forall &hr, P => bd <= 1%r

as a last goal, which it tries to close with trivial (as #1130 does
for the upper-bound rule), so constant bounds such as 1%r need no
extra step. This premise loses no valid judgement: Pr[...] >= bd, and
a fortiori Pr[...] = bd, implies it. Three proofs with an = bound
that is not a constant need one more step to establish it:
theories/distributions/Dexcepted.ec, and examples/PIR.ec (twice) and
examples/vonNeumann.eca.

Fixes #1127.

Origin: the rule was introduced in edb2017 (2013-09-20, first
released in r2022.04); 70ac960 (2022-06-19) added the exit check on
Q for = only.

Test: tests/phoare-while-geq-bound.ec (the #1127 reproducer and the
growing bound, with >= and with =; the previous build proves
them). unit (140 files), stdlib (128) and examples (49) pass.

[oskgo]

I tried to break it for a while with no success. I'm convinced that this is enough to deal with false induction hypotheses.