Insufficient checking for bounds in conseq <equiv> <bdhoare> #836
Description
When investigating #834 I found this soundness issue in conseq:
require import Real Int.
module M = {
var b: bool
proc run() = {
M.b <- false;
}
}.
lemma dep_bound : phoare[M.run : M.b ==> !M.b] = (b2i M.b)%r.
proof. by proc; auto => &hr ->. qed.
equiv triv_equiv : M.run ~ M.run : true ==> ={M.b}.
proof. proc; auto. qed.
lemma bad_bound : phoare[M.run : true ==> !M.b] = (b2i M.b)%r.
proof.
conseq triv_equiv dep_bound => //=.
by exists true.
qed.
lemma bound1: phoare[M.run: true ==> !M.b] = 1%r.
proof. proc; auto. qed.
lemma bound0: phoare[M.run: !M.b ==> !M.b] = 0%r.
proof. conseq bad_bound => &hr -> //. qed.
lemma bad: false.
proof.
have Mb: forall &m, M.b{m}.
- suff: forall &m, !M.b{m} => 1%r = 0%r by done.
move => &m pre.
rewrite (:1%r = Pr[M.run() @&m: !M.b]).
+ by byphoare bound1.
+ by byphoare bound0.
suff: forall &m, 1%r = 0%r by done.
move => &m.
rewrite (:0%r = Pr[M.run()@&m: !M.b]).
- byphoare (:false) => //.
move => &hr.
apply (Mb &hr).
byphoare => //.
proc; auto.
qed.
This no longer reproduces on main due to #834, but reproduces on commits prior to #789.
The culprit is the conseq in bad_bound, which fails to properly take into account the fact that although the behaviour of M.p is independent of the initial state (as stated by triv_equiv), the bound in dep_bound is dependent.
A fix to #834 should take this into account.