Tactic `async while` is unsound

[oskgo]

MRE:

module SpinTrue = {
  proc spin() = {
    while (true) {
    }
  }
}.

module SpinFalse = {
  proc spin() = {
    while (false) {
    }
  }
}.

equiv L: SpinFalse.spin ~ SpinTrue.spin:
  true ==> true.
proof.
proc.
async while [predT,1] [predT,1] true true: (false) => //.
qed.

Deriving false from L:

require import AllCore.

lemma LF &m: Pr[SpinFalse.spin()@&m:true]=1%r.
proof. byphoare => //; proc; rcondf 1 => //. qed.

lemma LT &m: Pr[SpinTrue .spin()@&m:true]=0%r.
proof. byphoare => //; proc; hoare; while (true) => //. qed.

lemma F: false.
suff//: forall &m, 1%r = 0%r.
move => &m.
rewrite -(LF &m) -(LT &m).
byequiv L => //.
qed.

[oskgo]

The fix wasn't sufficient. MRE:

module M = {
  proc spin_once(i:bool): bool = {
    while (i) {
      i <- !i;
    }
    return i;
  }
  
  proc spin(i:bool): bool = {
    while (i) {
    }
    return i;
  }
}.

equiv L: M.spin_once ~ M.spin:
  ={arg} ==> ={res}.
proof.
proc.
async while [predT,1] [predT,1] true true: (={i} /\ !i{1}) => //.
- move => />.
- move => v1 v2.
  conseq (: false ==> _); 1:smt(); auto.
- rcondf 1 => //; auto; smt().
rcondf 1 => //; auto; smt().
qed.

require import Real.

lemma bad: false.
proof.
suff//:forall &m, 1%r = 0%r.
move => &m.
have<-: Pr[M.spin_once(true)@&m:true]=1%r.
- byphoare (: arg ==> _) => //.
  proc.
  unroll 1.
  rcondf 2; auto.
have<-: Pr[M.spin(true)@&m:true]=0%r.
- byphoare (: arg==>_) => //.
  hoare; proc. while(i); auto.
byequiv L => //.
qed.

[fdupress]

https://arxiv.org/pdf/1710.09951

@bgregoir and @oskgo, do you want to have a chat and figure out how to go about fixing this one?

[lyonel2017]

I cannot reproduce this bug. I get stack in the proof of the equiv L.

[oskgo]

@lyonel2017 I can't reproduce it either, and I've checked on the commit just after the fix as well. I spent some time trying to come up with a different example. See if you can reproduce this:

module M = {
  proc spin_once(i:bool): bool = {
    while (i) {
      i <- !i;
    }
    return i;
  }
  
  proc spin(i:bool): bool = {
    while (i) {
    }
    return i;
  }
}.

equiv L: M.spin_once ~ M.spin:
  i{2} ==> true.
proof.
proc.
async while [predT,0] [predT,0] (!i{2}) (i{2} => i{1}): (i{2}) => //.
- move => &1 &2 => />.
- move => &2; auto => &1.
- move => v1 v2. 
  conseq (:false ==> _) => //.
  by move => &1 &2 [->].
- unroll 1; rcondf 2; auto => />.
by rcondf 1; auto => &2 />; case (i{1}) => ->.
qed.

require import Real.

lemma bad: false.
proof.
suff//:forall &m, 1%r = 0%r.
move => &m.
have<-: Pr[M.spin_once(true)@&m:true]=1%r.
- byphoare (: arg ==> _) => //.
  proc.
  unroll 1.
  rcondf 2; auto.
have<-: Pr[M.spin(true)@&m:true]=0%r.
- byphoare (: arg==>_) => //.
  hoare; proc. 
  while(i); auto.
byequiv L => //.
qed.

[lyonel2017]

I can reproduce the bug. Working on the fix.