unsoundness in pHL `while` with non-strict variant

[oskgo]

The tactic does not place any requirement on what happens to the variant when it does not decrease. It is allowed to increase without bound.

See the following example proving that a biased 1D random walk always reaches 0, which is not true.

require import AllCore DBool List.
import Biased.

module M = {
  proc p(n, bias) = {
    var b;
    while (0 < n) {
      b <$ dbiased bias;
      if (b) {
        n <- n-1;
      } else {
        n <- n+1;
      }
    }
  }
}.

lemma L: phoare[M.p: 0%r < bias <= 1%r ==> true] >= 1%r.
proof.
proc.
exlim bias => p.
while (bias = p /\ 0%r < bias <= 1%r) n n p => //.
- smt().
- move => wh.
  seq 2: (bias = p /\ 0%r < bias <= 1%r) => //.
  + auto.
    smt(dbiasedE).
  conseq wh.
  smt().
- auto.
  smt(dbiasedE).
split => [/#|z].
seq 1: (n=z /\ b) => //.
- rnd; auto.
  smt(dbiasedE).
auto.
smt().
qed.

[fdupress]

@bgregoir we need you to dig up the TACAS'14 draft again.