unsoundness with probabilistic while

[chdoc]

Turns out, the while <invariant> <measure> <upper bound> <probability of decrease> rule is unsound as well:

(the extra-logical w : statement made me very suspicious)

require import AllCore Distr.
type r_t, c_t.
op[lossless] dC : c_t distr. 
op p : c_t -> bool.

axiom mu_p : 0%r < mu dC p.

module M = { 
  proc p() = { 
    var c;
    var e <- true; 
    while (e) { 
      c <$ dC;
      if (p c) e <- false;
    } 
  }
}.

lemma good &m : Pr [ M.p() @ &m : true ] = 1%r.
proof.
byphoare => //; proc; sp. 
while true (b2i e) 1 (mu dC p) => //; 1:smt().
- move => ih; seq 2 : true 1%r 1%r 0%r _ => //.
  auto => />; smt(dC_ll).
- auto => />; smt(dC_ll).
- by rewrite mu_p /= => z; wp; rnd p; auto => />.   
qed.

lemma bad &m : Pr [ M.p() @ &m : true ] = 0%r.
proof.
byphoare => //; proc; sp. 
while true (b2i e) 1 (mu dC p) => //; 1:smt().
- move => ih. 
  seq 2 : true 1%r 0%r 0%r _ => //. 
- auto => />; smt(dC_ll).
- by rewrite mu_p /= => z; wp; rnd p; auto => />.   
qed.

lemma ugly &m : false.
proof.
suff : 0%r = 1%r by done. 
by rewrite -(good &m) -(bad &m).
qed.

[fdupress]

Yeah.

In the inductive step, we assume something about the behaviour of the loop wrapped in a conditional. For example, in your bad lemma, we get the following first goal:

&m: {}
w: statement
ih: phoare[ if (e) {...} : true ==> true] = 0%r
------------------------------------------------------------------------------------------------------------------
Context : {e : bool, c : c_t}
Bound   : [=] 0%r

pre = true /\ e

(1--)  c <$ dC                  
(2--)  if (p c) {               
(2.1)    e <- false             
(2--)  }                        
(3--)  if (e) {                 
(3.1)    w                      
(3--)  }                        

post = true

The assumption ih here, is obviously false (when e is initially false, it terminates trivially, regardless of the loop's behaviour). The assumption ih should be on w only (the program itself).

I think this is enough to fix it, but I'd like to see the original pHL rule this is implementing (or to take the time to write a proof for this).

[chdoc]

I wasn't even aware that there is an (abstract) type statement that can be exposed to the user and used in statement judgments generated by tactics. I suppose since statement is not actually a type in the global context, there is no term of this type either. Are there any other tactics that introduce the statement type?

[fdupress]

I'm not aware of any others that use the statement meta-type, but there are a couple that create goals that can't be expressed in the user-facing syntax. (Judgments on statements, mostly.)

In this case, the w : statement is meant as a self-reference to the program (c <$ dC; if (p c) { e <- false; } if (e) { w }) itself, but we then botch the induction hypothesis, expressing it on a derived program, and possibly forgetting a precondition.

I'll be taking a stab at writing and sketching a proof for the rule in the next couple of days. @strub is also hoping that that will let us find a tactic that implements it without exposing the extra-logical self-reference. For example, we could build the seq ...; if ... into the tactic at virtually no cost, since the probability split and the proofs for the suffix are necessarily trivial.

[chdoc]

For example, we could build the seq ...; if ... into the tactic at virtually no cost, since the probability split and the proofs for the suffix are necessarily trivial.

That was my thought as well. If w is abstract and the only thing one knows is the hypothesis generated by the tactic...

[strub]

One fix is to implement @fdupress's proposal: the induction hypothesis should be on w only. I am going to implement this fix first, but this does not preclude coming with a better while rules in the future.

[fdupress]

So it turns out we can finish the proof for PIR. (See commit 68f0b01). This has me suspicious, but Benjamin believes it. Benjamin also believes the inductive case should be as follows instead (note the absence of if on line 3. I'm also suspicious of this. We should discuss it some more.

&m: {}
w: statement
ih: phoare[ w : true ==> true] = 0%r
------------------------------------------------------------------------------------------------------------------
Context : {e : bool, c : c_t}
Bound   : [=] 0%r

pre = true /\ e

(1--)  c <$ dC                  
(2--)  if (p c) {               
(2.1)    e <- false             
(2--)  }                                      
(3--)  w

post = true

[fdupress]

After another call with @bgregoir , where I finally understood the Universe, I've just pushed a further simplified while rule for pHL, which aligns (as far as I understand!) with the 2014 draft and its proof.

The general proof pattern is a bit heavier, but remains generally understandable: some of the conditional reasoning takes place in the bound itself, instead of happening solely in code.

PR coming up Soon™.

[fdupress]

From @chdoc over in the PR (#226)

Am I seeing ghosts, or does this not actually fix #212 ?

lemma bad &m : Pr [ M.p() @ &m : true ] = 0%r.
proof.
byphoare => //; proc; sp. 
while true (b2i e) 1 (mu dC p) => //; 1:smt().
- move => ih; seq 2 : true 1%r 0%r 0%r _ => //. 
- auto => />; smt(dC_ll).
- by rewrite mu_p /= => z; wp; rnd p; auto => />.   
qed.

Sure, I no longer get this spurious if around the w : statement but the proof actually never looked at this ...

Also, this seems not just an issue of (wrongly) combining the <= and >= rules into an = rule, as I can also prove:

lemma bad05 &m : Pr [ M.p() @ &m : true ] <= 1%r/2%r.
proof.
byphoare => //; proc; sp. 
while true (b2i e) 1 (mu dC p) => //; 1:smt().
- move => ih. seq 2 : true 1%r (1%r/2%r) 0%r _ => //. 
- auto => />; smt(dC_ll).
- by rewrite mu_p /= => z; wp; rnd p; auto => />.   
qed.

You're not seeing ghosts.

Looking a bit deeper, I see two more issues:

1. Your bad05 example is doing something really weird, and allowing you to use the rule for lower bounds to prove an upper bound. It's a sign that there's something fishy going on, but it doesn't look like the upper-bound variant of the while rule is rotten. (Which is good, given its simplicity.) I suspect the implicit seq and conseq are done in TCB, and done badly. They should be shoved out of the TCB.

2. I strongly believe that the rule for equality should check also the "loop not entered" condition for upper bounds. (If the precondition holds, the loop condition doesn't, and the postcondition also holds, then the bound should be 1.) The proofs I've seen cover the rules for lower and upper bounds (and they make sense), but not the combined rule.

@bgregoir any opinions on this?

[strub]

@fdupress Where are we standing? Is your commit ready for a PR?

[fdupress]

The PR is still there, with Benjamin's commit on top, and verification that it implements the rules.

It could be improved for usability, but it's ready to merge for soundness.

[strub]

Oh, there is already a PR 😅