Add doc and examples

Author: lyonel2017

doc/tactics/async-while.rst

@@ -0,0 +1,90 @@
+========================================================================
+Tactic: ``asyncwhile`` Tactic
+========================================================================
+
+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
+on loop which are not in lockstep.
+
+------------------------------------------------------------------------
+Syntax
+------------------------------------------------------------------------
+
+The general form of the tactic is:
+
+.. admonition:: Syntax
+
+  ``async while [f1,k1] [f2,k2] (L1) (L2) : (I)``
+
+Here:
+
+- ``L1`` and  ``L2`` are the left and right condition to control if we
+  consider the lockstep case, or the oneside case,
+- ``k1`` and ``k2`` are natural number
+- ``f1`` and ``f2`` are the unrolling condition, initial by the parameter
+  ``k1`` and ``k2``.
+
+Concretely, the tactic implements the following rulee::
+
+  I => (b1 <=> b2 /\ (!L1 /\ !L2 => f1 k1 /\ f2 k2)) \/ (L1 /\ b1) \/ (L2 /\ b2)
+  equiv[while b1 {c1} ~ while {b2} c2: I /\ b1 <=> b2 /\ !L1 /\ !L2 /\ f1 k1 /\ f2 k2 ==> I]
+  equiv[while b1 {c1} ~ skip: I /\ b1 /\ L1 /\ ==> I]
+  equiv[skip ~ while b2 {c2}: I /\ b2 /\ L2 /\ ==> I]
+  (Pre => I) /\  (I /\ !b1 /\ !b2  => Post)
+  -------------------------------------------------------------------------------------------
+            equiv[while b1 {c1} ~ while {b2} c2:  Pre ==> Post]
+
+The following example shows ``asynctwhile`` on a prhl goal. The program
+increments ``x`` until it reaches ``10``.
+
+.. ecproof::
+
+  require import AllCore.
+
+   module M = {
+     proc up_to_10(x : int) : int = {
+       while (x < 10) {
+         x <- x + 1;
+       }
+       return x;
+     }
+     proc up_to_10_by_2(x : int) : int = {
+       while (x < 10) {
+         x <- x + 1;
+         if ( x < 10)  x <- x + 1;
+       }
+       return x;
+     }
+
+   }.
+
+   lemma asynctwhile_example :
+   equiv[M.up_to_10 ~ M.up_to_10_by_2 : ={x} ==> ={res}].
+   proof.
+     proc.
+     async while
+     [ (fun r => x <= r + 1), (x{1} ) ]
+     [ (fun r => x <= r ), (x{2} ) ]
+     (!(x{1} < 10)) (!(x{2} < 10))
+     :
+     (x{1} = x{2})  => //=.
+       + move=> &1 &2.  smt.
+       + move => v1 v2 //=.
+       unroll {1} 1.
+       unroll {1} 2.
+       unroll {2} 1.
+       rcondt {1} 1. auto.
+       rcondt {2} 1. auto.
+       sp 1 1.
+       if. smt.
+       sp 1 1.
+       while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
+       !(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 )))  /\ ={x}); auto; smt.
+       while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
+       !(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 )))  /\ ={x}); auto; smt.
+       +  move => &2. exfalso=> &1 ?. smt.
+       +  move => &1. exfalso=> &2 ?. smt.
+       +  exfalso.  smt.
+       +  exfalso.  smt.
+    qed.

examples/async_while.ec

@@ -0,0 +1,88 @@
+require import AllCore.
+
+   module M = {
+     proc up_to_10(x : int) : int = {
+       while (x < 10) {
+         x <- x + 1;
+       }
+       return x;
+     }
+     proc up_to_10_by_2(x : int) : int = {
+       while (x < 10) {
+         x <- x + 1;
+         if ( x < 10)  x <- x + 1;
+       }
+       return x;
+     }
+
+   }.
+
+   lemma asynctwhile_example :
+   equiv[M.up_to_10 ~ M.up_to_10_by_2 : ={x} ==> ={res}].
+   proof.
+     proc.
+     async while
+     [ (fun r => x <= r + 1), (x{1} ) ]
+     [ (fun r => x <= r ), (x{2} ) ]
+     (!(x{1} < 10)) (!(x{2} < 10))
+     :
+     (x{1} = x{2})  => //=.
+       + move=> &1 &2.  smt.
+       + move => v1 v2 //=.
+       unroll {1} 1.
+       unroll {1} 2.
+       unroll {2} 1.
+       rcondt {1} 1. auto.
+       rcondt {2} 1. auto.
+       sp 1 1.
+       if. smt.
+       sp 1 1.
+       while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
+       !(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 )))  /\ ={x}); auto; smt.
+       while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
+       !(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 )))  /\ ={x}); auto; smt.
+       +  move => &2. exfalso=> &1 ?. smt.
+       +  move => &1. exfalso=> &2 ?. smt.
+       +  exfalso.  smt.
+       +  exfalso.  smt.
+   qed.
+
+
+ module M1 = {
+  proc spin_once(i1:bool): bool = {
+    while (i1) {
+      i1 <- !i1;
+    }
+    return i1;
+  }
+
+  proc spin(i2:bool): bool = {
+    while (i2) {
+    }
+    return i2;
+  }
+}.
+
+op b0:bool.
+op b1:bool.
+op b2:bool.
+op b3:bool.
+op b4:bool.
+op f1:int -> bool.
+op n1:int.
+op f2:int -> bool.
+op n2:int.
+
+equiv L: M1.spin_once ~ M1.spin:
+  b0 ==> b4.
+proof.
+proc.
+  async while [f1,n1] [f2,n2] (b1) (b2) : (b3).
+  - admit. (* soundness condition*)
+  - admit. (*left*)
+  - admit. (*right*)
+  - admit. (*lockstep equiv*)
+  - admit. (*losless left*)
+  - admit. (*losless right*)
+  - admit. (*invariant implies post*)
+qed.