Conversation
lyonel2017
force-pushed
the
asynchile
branch
2 times, most recently
from
536fb81 to
07e7aa9
Compare
|
Now that you have a fresh understanding of how the tactic works, could you write up documentation? That would also make review simpler. |
| - ``f1`` and ``f2`` are the unrolling condition, initial by the parameter | ||
| ``k1`` and ``k2``. | ||
|
|
||
| Concretely, the tactic implements the following rulee:: |
There was a problem hiding this comment.
| Concretely, the tactic implements the following rulee:: | |
| Concretely, the tactic implements the following rule:: |
| ------------------------------------------------------------------------------------------- | ||
| equiv[while b1 {c1} ~ while {b2} c2: Pre ==> Post] | ||
|
|
||
| The following example shows ``asynctwhile`` on a prhl goal. The program |
There was a problem hiding this comment.
| The following example shows ``asynctwhile`` on a prhl goal. The program | |
| The following example shows ``async while`` on a prhl goal. The program |
| @@ -0,0 +1,91 @@ | |||
| ======================================================================== | |||
| Tactic: ``asyncwhile`` Tactic | |||
There was a problem hiding this comment.
| Tactic: ``asyncwhile`` Tactic | |
| Tactic: ``async while`` Tactic |
| Tactic: ``asyncwhile`` Tactic | ||
| ======================================================================== | ||
|
|
||
| The ``asyncwhile`` tactic applies to probabilistic relational Hoare Logic |
There was a problem hiding this comment.
| The ``asyncwhile`` tactic applies to probabilistic relational Hoare Logic | |
| The ``async while`` tactic applies to probabilistic relational Hoare Logic |
|
|
||
| The ``asyncwhile`` tactic applies to probabilistic relational Hoare Logic | ||
| goals where the programs contains a ``while`` loop. | ||
| Unlike the ``while`` tactic, the ``asyncwhile`` tactic allows to reason |
There was a problem hiding this comment.
| Unlike the ``while`` tactic, the ``asyncwhile`` tactic allows to reason | |
| Unlike the ``while`` tactic, the ``async while`` tactic allows to reason |
| [ (fun r => x <= r ), (x{2} ) ] | ||
| (!(x{1} < 10)) (!(x{2} < 10)) | ||
| : | ||
| (x{1} = x{2}) => //=. |
There was a problem hiding this comment.
I don't think you should use intro patterns to discharge trivial side conditions or simplify side conditions in doc examples. This hides the side condition from the reader.
| equiv[skip ~ while b2 {c2}: I /\ b2 /\ L2 /\ ==> I] | ||
| (Pre => I) /\ (I /\ !b1 /\ !b2 => Post) | ||
| ------------------------------------------------------------------------------------------- | ||
| equiv[while b1 {c1} ~ while {b2} c2: Pre ==> Post] |
There was a problem hiding this comment.
This does not match the implementation.
The first equiv should be using f1 k1 and f2 k2 in the loop condition.
Both the next equivs are instead a hoare statement about a single iteration together with a phoare statement about termination. This is different from what is written here. In the equivs written here the invariant is permitted to temporarily fail as long as it is restored before the end of the final iteration. In the equivs written here the invariant has to hold even after multiple iterations, while in the implemented tactic the invariant only needs to hold for a single iteration starting from where L1/L2 holds.
2 participants
Fix #774