pHL `rnd E` soundness

[lyonel2017]

require import AllCore Distr StdOrder.
import RealOrder.

module M = {
  proc f() : unit = { var x : int; while (true) { } x <$ dunit 0; }
}.

lemma h : phoare[ M.f : true ==> true ] <= (-1)%r.
proof.
proc.
rnd (fun (_ : int) => true).
while (true); auto.
qed.

lemma bad &m : false.
proof.
have hle : Pr[M.f() @ &m : true] <= (-1)%r by byphoare h.
have hge : 0%r <= Pr[M.f() @ &m : true] by rewrite Pr[mu_ge0].
have h0 : 0%r <= - 1%r.
- by move: (ler_trans Pr[M.f() @ &m : true] 0%r (-1)%r hge hle); rewrite fromintN.
have : 0%r < 0%r by apply (ler_lt_trans (- 1%r)) => //; apply ltrN10.
by rewrite ltrr.
qed.

[oskgo]

There is a bounds check being emitted here. The issue is that it is put into the postcondition of a hoare statement, which only has to be proven for the terminating case. The fix would be to remove the bound from the postcondition and prove it quantified over all memories instead.

The while variant flagged in #1102 also has a similar issue, which is not problem in the example in that issue, but is a problem in the following example where we use the loop invariant false instead of true:

require import Real.

module M = {proc p() = {while (true) {} while (true) {}}}.

lemma bad: phoare[M.p: true ==> false] <= (-1%r). 
proof.
proc.
while false.
auto.
while true (* This is the hoare variant, which is sound. We just use while for nontermination here *).
done.
done.
qed.

I wouldn't be surprised if there are similar issues in other tactics as well, but I haven't been able to find any more. Feel free to have a look if you have time/tokens.

[fdupress]

call also shifts the obligation that invariants are initially true into the postcondition, which seems to be the core of the problem here. It likely deserves a quick look.

[oskgo]

Putting an obligation into the postcondition is only problematic if the obligation is needed to justify the transformation rather than being a condition on the behavior of the transformed program.

In rnd and while we lift a bound, which is a condition on the program before transformation, into the conditions of the transformed program. I would be surprised if there is a tactic that does this with something other than bounds unless it's completely borked in multiple ways.

[Yiping106283]

A per-tactic fix in the #1095 style is in #1135 (the rule emits pre => 0%r <= bd as a separate goal, t_trivial tried on it). Note that this reproducer is still accepted by the #1105 branch (head bb75dba): the bound check stays in the hoare post-condition and never reaches the sites #1105 guards, so it needs its own fix either way; details in #1105 (comment).

[lyonel2017]

This is duplication of #1102. The pHL while tactic should not permits negative probabilities.
If you can push all the statement after the while into the post, you can proof false, thanks to the while (true):

require import AllCore Distr StdOrder.
import RealOrder.

module M = {
  proc g() : unit = { var x : int; while (true) { } x <- x; }
}.

lemma h2 : phoare[ M.g : true ==> true ] <= (-1)%r.
proof.
  proc.
wp.
while (true); auto.
qed.

lemma bad2 &m : false.
proof.
have hle : Pr[M.g() @ &m : true] <= (-1)%r by byphoare h2.
have hge : 0%r <= Pr[M.g() @ &m : true] by rewrite Pr[mu_ge0].
have h0 : 0%r <= - 1%r.
- by move: (ler_trans Pr[M.g() @ &m : true] 0%r (-1)%r hge hle); rewrite fromintN.
have : 0%r < 0%r by apply (ler_lt_trans (- 1%r)) => //; apply ltrN10.
by rewrite ltrr.
qed.

The generalization :

require import AllCore Distr StdOrder.
import RealOrder.

module M = {
  proc g() : unit = { var x : int; while (true) { } }
}.

op b : bool.

lemma h2 : phoare[ M.g : true ==> b ] <= (-1)%r.
proof.
  proc.
while (true); auto.
qed.

lemma bad2 &m : false.
proof.
have hle : Pr[M.g() @ &m : true => b] <= (-1)%r by byphoare h2.
have hge : 0%r <= Pr[M.g() @ &m : true => b] by rewrite Pr[mu_ge0].
have h0 : 0%r <= - 1%r.
- by move: (ler_trans Pr[M.g() @ &m : true => b] 0%r (-1)%r hge hle); rewrite fromintN.
have : 0%r < 0%r by apply (ler_lt_trans (- 1%r)) => //; apply ltrN10.
by rewrite ltrr.
qed.

[oskgo]

This is not a duplicate of #1102. In your original example the only problem happens with rnd. The while in your example (and the first while in mine) is only used to ensure nontermination so we never have to prove the post. It could be done by sampling from dnull instead.

The example I talk about in #1119 (comment) could be seen as a duplicate (or extension?) of #1102.

[Yiping106283]

To make the distinction concrete, here is the reproducer with the loop removed. The divergence now comes from dnull, so no while rule is involved at any point. It is accepted by current main and proves false:

require import AllCore Distr.

module M = {
  proc f() : unit = { var y : int; var x : int; y <$ dnull; x <$ dunit 0; }
}.

lemma h : phoare[ M.f : true ==> true ] <= (-1)%r.
proof.
proc.
rnd (fun (_ : int) => true).
auto => /> y; by rewrite supp_dnull.
qed.

lemma bad &m : false.
proof.
have hle : Pr[M.f() @ &m : true] <= (-1)%r by byphoare h.
have hge : 0%r <= Pr[M.f() @ &m : true] by rewrite Pr[mu_ge0].
smt().
qed.

rnd reduces the goal to hoare[y <$ dnull : true ==> mu (dunit 0) (fun _ => true) <= -1%r], whose post-condition is vacuous on the empty support. Note also that in the original reproducer the while (true) is applied after rnd, on a hoare goal, so it goes through the hoare while rule, not the pHL one that #1102 is about.

I checked the #1102 reproducer and both versions of this one against current main (6eeb6a0) and against the #1130 and #1135 branches: #1130 rejects the #1102 reproducer and accepts both versions of this one; #1135 rejects both versions of this one (the leftover goal is forall &hr, true => 0%r <= -1%r) and accepts the #1102 reproducer. So the two issues are independent and the two fixes are orthogonal. What they do share is the root cause: both rules only check the bound on the terminating runs and omit the premise 0%r <= bd that the probability-0 contribution of non-terminating runs requires. That premise has to be emitted by each rule separately, which is why the two fixes have the same shape and why neither can stand in for the other.