Repository navigation
pHL seq permits negative probabilities #1100
Description
The pHL seq rule as documented in the refman is only sound for positive probabilities. More specifically we run into problems for the (<=) and (>=) cases, but not the (=) case.
MRE:
require import Real Distr.
module M = {proc p() = {}}.
lemma le0: phoare[M.p: true ==> true] <= 0%r.
proof.
proc.
by seq 0: (true) 1%r 1%r 1%r (-1%r).
qed.
module M' = {proc p() = {var r: bool; r <$ dnull;}}.
lemma ge2: phoare[M'.p: true ==> true] >= 2%r.
proof.
proc.
seq 0: (true) _ 0%r (-2%r) (-1%r) => //.
- hoare.
+ smt().
auto.
- auto.
smt().
qed.
Related to #1096.
Activity