[breaking] fix unsoundness in pHL while rule

[fdupress]

This fixes #212 and implements a version of the pHL while rule which does have a(n unpublished) pen-and-paper proof.

This (obviously) makes using the pHL while rule generally less simple, but particularly so when the loop condition itself is probabilistically modified by the loop body (as, for example, in rejection sampling). Examples of proofs illustrating this case can be found in theories/distributions/Dexcepted.ec (starting line 299, including the conseq) and examples/PIR.ec (starting line 202, including also the conseq).

[chdoc]

@fdupress Is it intentional that the proc* and by [] changes are also part of this PR?

[fdupress]

I suspect PY's force-push to main. I'll check the log and rebase if needed. Thanks for pointing it out.

[fdupress]

@strub did your merge of hakyber-jasmin-eclib eat up all of yesterday's merges?

[strub]

🙈 🙉 🙊

[chdoc]

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.

[bgregoir]

@christian. I think you are perfectly write.
I have the impression that we should add a side condition ensuring that the bound is 1 the the test is false. But I will reread the proof of the rule first.

[bgregoir]

In fact I have just realised that we have forgot to implement the side condition in the paper on delta in the paper. I will send the paper to Christian.

[bgregoir]

The old unpublished paper.

…

On 13 Jul 2022, at 18:56, Christian Doczkal ***@***.***> wrote: Am I seeing ghosts, or does this not actually fix #212 <#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. — Reply to this email directly, view it on GitHub <#226 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAFBT3D4AZUNPL4EP4U4OJLVT3YNRANCNFSM53ICPWHQ>. You are receiving this because your review was requested.

[bgregoir]

I have re-read the paper.
There is two rules one for <= and one for >=.
The proof for <= is trivial. The basic idea is that the semantic of the while [while e do c] = lub_n [while_n e do c].
Where while_n e do c is a n unrolling of the loop followed by an if e then abord.
The the correctness follow from the premises and the fact that
(forall n, f_n <= delta) => lub_n f_n <= delta.
The second rule is for >=.
The idea of the proof is to split into two part.
part 1: proof that the loop terminate with probability 1.
Then use the rule for <=.
I think that the proof to show the termination is relatively simple to follow.

[fdupress]

@bgregoir I move discussions back over to the issue itself (#212) after doing some root causing yesterday. There are two different things going on, including a missing check on the value of the bound in the equality case.

I can probably take a call some time today, but might need time to park some things. My intuition there was also that the proofs for <= and >= were correct, but that no argument was given for the rule for = (and indeed, the check I identify as missing would stop Christian's proof).

Then on top of that, EasyCrypt somehow allows the lower-bound rule to be used to prove an upper-bound. This seems like a problem.

[bgregoir]

I think that we have now what was written in the paper.
@chdoc if you want to play with it.

[chdoc]

I looked at the while >= rule, and at first glance that appears to conform to the rule in the paper. From the usability perspective, I think it would be preferable if the while tactic would work on arbitrary programs whose last instruction is a while, taking the first argument to be the $\Psi$ from the rule and having $I$ as an optional argument that defaults to the value given for $\Psi$. If I didn't miss anything, the instances for the existing proofs (as well as my tests) all have $\Psi = I$.

IIUC, the while <= rule is currently disabled. Trying to use it I get: "only judgments with an lower/eq-bounded are supported".

[bgregoir]

On 15 Jul 2022, at 14:40, Christian Doczkal ***@***.***> wrote: I looked at the while >= rule, and at first glance that appears to conform to the rule in the paper. From the usability perspective, I think it would be preferable if the while tactic would work on arbitrary programs whose last instruction is a while, taking the first argument to be the $\Psi$ from the rule and having $I$ as an optional argument that defaults to the value given for $\Psi$. If I didn't miss anything, the instances for the existing proofs (as well as my tests) all have $\Psi = I$.

I agree that this is not convenient. But I have the impression that we need to apply a seq rule, and I don’t know which one apply. Ideas are welcome.

IIUC, the while <= rule is currently disabled. Trying to use it I get: "only judgments with an lower/eq-bounded are supported".

Yes, if you want to prove <= you can use directly the other rule : while inv.

…

— Reply to this email directly, view it on GitHub <#226 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAFBT3HBGQXZMIAX3WZSA33VUFL3LANCNFSM53ICPWHQ>. You are receiving this because you were mentioned.

[fdupress]

I looked at the while >= rule, and at first glance that appears to conform to the rule in the paper. From the usability perspective, I think it would be preferable if the while tactic would work on arbitrary programs whose last instruction is a while, taking the first argument to be the $\Psi$ from the rule and having $I$ as an optional argument that defaults to the value given for $\Psi$. If I didn't miss anything, the instances for the existing proofs (as well as my tests) all have $\Psi = I$.

I agree that this is not convenient. But I have the impression that we need to apply a seq rule, and I don’t know which one apply. Ideas are welcome.

Now that I've had time to think after our call, Benjamin: the approach taken elsewhere in pHL with the automated seqs is that the suffix "absorbs" the entire probability bound. (So if you have to prove {P} c; c' {Q} =p, the automated seq if, for example, c' is a random sampling is equivalent to seq |c| X 1%r p 0%r _ (with X the weakest precondition produced by the actual tactic on c'). Anything else requires an explicit seq (or the magical additional arguments that nobody knows exist...)

IIUC, the while <= rule is currently disabled. Trying to use it I get: "only judgments with an lower/eq-bounded are supported".

Yes, if you want to prove <= you can use directly the other rule : while inv.

Just to clarify, this is where I was saying that EasyCrypt let you use the rule for >= to prove <=. This was not good at all.

[fdupress]

I think this is ready for a fresh review and merge. I'll create a new issue regarding the usability, and potentially baking in a default seq for the >= and = rules.

[chdoc]

Now that I've had time to think after our call, Benjamin: the approach taken elsewhere in pHL with the automated seqs is that the suffix "absorbs" the entire probability bound. (So if you have to prove {P} c; c' {Q} =p, the automated seq if, for example, c' is a random sampling is equivalent to seq |c| X 1%r p 0%r _ (with X the weakest precondition produced by the actual tactic on c').

I think it would be good if the tactic for while would be in line with that the remaining pHL tactics are doing. However, my understanding is that the tactic currently also requires a manual conseq for just about every use. So maybe this should be merged as while_bare, while_internal or something like this, so that it can be used but it's clear that this is not intended as the final user-facing tactic.

Anything else requires an explicit seq (or the magical additional arguments that nobody knows exist...)

I guess this is because pHL is one of the most scarcely documented parts of EC. For this rule it would really be nice to have some documentation, even if it is only some plain text description in the example file. Otherwise the only documentation is an unpublished draft.

[strub]

@fdupress Could you squash this PR with a message that summarises the changes? Then, I think we are good to go.

[chdoc]

I still think this should be something like while[core] or while[noseq] in the same vein as conseq[noframe] so that we can implement something more user friendly for while (without the flag).

[fdupress]

@strub Rebased and squashed, with a hopefully meaningful message. I could also clarify the full rules in there, but I'd rather do it somewhere where they can be typeset properly.

@chdoc Your comment is noted, but I think we'll introduce the option when we have variants, rather than forcing an option right off the bat without a clear plan to have a sane default behaviour.

[chdoc]

@chdoc Your comment is noted, but I think we'll introduce the option when we have variants, rather than forcing an option right off the bat without a clear plan to have a sane default behaviour.

Do as you wish, my hope was that this would clearly document that this is not a finished product and keep proofs using the "core" rule working if we introduce something more user friendly. But then, adapting the proofs would be trivial (add a flag) and maybe prompt people (us?) to use the user-friendly rule instead. 🤷‍♂️