pHL call permits negative probabilities

[oskgo]

We can use call on a lemma with negative probabilities to prove a negative bound on phoare statements where the call is unreachable.

MRE:

require import Real Distr.

module O = {proc p() = {}}.

lemma O_false: phoare[O.p: false ==> true] <= (-1%r) by done.

module M = {proc p() = {var r: bool; r<$dnull; O.p();}}.

lemma len1: phoare[M.p: true ==> false] <= (-1%r).
proof.
proc.
call O_false.
auto => />.
apply supp_dnull.
qed.