The lower-bound while inv vrnt k eps rule (t_bdhoare_while_rev_geq_r) only emits !Q => bd = 0%r for the loop-exit case; when the loop exits with Q the probability is 1, but nothing requires bd <= 1%r. With a loop that is never entered every other obligation is vacuous, so phoare[...] >= 2%r is provable and contradicts Pr[...] = 1%r. This is not a negative-bound issue (#1100-#1102) and is not addressed by #1105, which only adds 0 <= bd.
MRE:
require import AllCore.
module M = { proc f() : unit = { while (false) {} } }.
lemma f_bad : phoare[M.f : true ==> true] >= 2%r.
proof.
proc.
while (true) 0 0 1%r.
+ done.
+ done.
+ done.
+ by move=> _; exfalso.
+ by exfalso.
+ split; first done.
by move=> z; exfalso.
qed.
lemma bad &m : false.
proof.
have h1 : Pr[M.f() @ &m : true] = 1%r by byphoare => //; proc; rcondf 1; auto.
have h2 : 2%r <= Pr[M.f() @ &m : true] by byphoare f_bad.
smt().
qed.
Root cause: src/phl/ecPhlWhile.ml, t_bdhoare_while_rev_geq_r, pre_bound_concl (l. 240-250): the FHeq case checks bd = if Q then 1%r else 0%r, the FHge case only !Q => bd = 0%r (since the 2022 rewrite 70ac960). For FHge the rule should emit (Q => bd <= 1%r) /\ (!Q => bd = 0%r).
The lower-bound
while inv vrnt k epsrule (t_bdhoare_while_rev_geq_r) only emits!Q => bd = 0%rfor the loop-exit case; when the loop exits withQthe probability is 1, but nothing requiresbd <= 1%r. With a loop that is never entered every other obligation is vacuous, sophoare[...] >= 2%ris provable and contradictsPr[...] = 1%r. This is not a negative-bound issue (#1100-#1102) and is not addressed by #1105, which only adds0 <= bd.MRE:
Root cause:
src/phl/ecPhlWhile.ml,t_bdhoare_while_rev_geq_r,pre_bound_concl(l. 240-250): theFHeqcase checksbd = if Q then 1%r else 0%r, theFHgecase only!Q => bd = 0%r(since the 2022 rewrite 70ac960). ForFHgethe rule should emit(Q => bd <= 1%r) /\ (!Q => bd = 0%r).