SessionTypes: starting with a more basic version

SessionTypes.v

@@ -9,6 +9,167 @@ Set Implicit Arguments.
 Set Asymmetric Patterns.
 
 
+(** * Basic Two-Party Session Types *)
+
+Module BasicTwoParty.
+
+(** ** Defining the type system *)
+
+Inductive type :=
+| TSend (ch : channel) (A : Set) (t : type)
+| TRecv (ch : channel) (A : Set) (t :  type)
+| TDone.
+
+Delimit Scope st_scope with st.
+Bind Scope st_scope with type.
+Notation "!!! ch ( A ) ; k" := (TSend ch A k%st) (right associativity, at level 45, ch at level 0) : st_scope.
+Notation "??? ch ( A ) ; k" := (TRecv ch A k%st) (right associativity, at level 45, ch at level 0) : st_scope.
+
+Inductive hasty : proc -> type -> Prop :=
+| HtSend : forall ch (A : Set) (v : A) k t,
+    hasty k t
+    -> hasty (Send ch v k) (TSend ch A t)
+| HtRecv : forall ch (A : Set) (k : A -> _) t,
+    (forall v, hasty (k v) t)
+    -> hasty (Recv ch k) (TRecv ch A t)
+| HtDone :
+    hasty Done TDone.
+
+
+(** * Examples of typed processes *)
+
+(* Recall our first example from last chapter. *)
+Definition addN (k : nat) (input output : channel) : proc :=
+  ??input(n : nat);
+  !!output(n + k);
+  Done.
+
+Ltac hasty := simplify; repeat ((constructor; simplify)
+                                || match goal with
+                                   | [ |- hasty _ (match ?E with _ => _ end) ] => cases E
+                                   | [ |- hasty (match ?E with _ => _ end) _ ] => cases E
+                                   end).
+
+Theorem addN_typed : forall k input output,
+    hasty (addN k input output) (???input(nat); !!!output(nat); TDone).
+Proof.
+  hasty.
+Qed.
+
+
+(** * Complementing types *)
+
+Fixpoint complement (t : type) : type :=
+  match t with
+  | TSend ch A t1 => TRecv ch A (complement t1)
+  | TRecv ch A t1 => TSend ch A (complement t1)
+  | TDone => TDone
+  end.
+
+Definition add2_client (input output : channel) : proc :=
+  !!input(42);
+  ??output(_ : nat);
+  Done.
+
+Theorem add2_client_typed : forall input output,
+    hasty (add2_client input output) (complement (???input(nat); !!!output(nat); TDone)).
+Proof.
+  hasty.
+Qed.
+
+(** * Parallel execution preserves the existence of complementary session types. *)
+
+Definition trsys_of pr := {|
+  Initial := {pr};
+  Step := lstepSilent
+|}.
+(* Note: here we force silent steps, so that all channel communication is
+ * internal. *)
+
+Hint Constructors hasty.
+
+Lemma input_typed : forall pr ch A v pr',
+    lstep pr (Input {| Channel := ch; TypeOf := A; Value := v |}) pr'
+    -> forall t, hasty pr t
+                 -> exists k, pr = Recv ch k /\ pr' = k v.
+Proof.
+  induct 1; invert 1; eauto.
+Qed.
+
+Lemma output_typed : forall pr ch A v pr',
+    lstep pr (Output {| Channel := ch; TypeOf := A; Value := v |}) pr'
+    -> forall t, hasty pr t
+                 -> exists k, pr = Send ch v k /\ pr' = k.
+Proof.
+  induct 1; invert 1; eauto.
+Qed.
+
+Lemma complementarity_forever : forall pr1 pr2 t,
+    hasty pr1 t
+    -> hasty pr2 (complement t)
+    -> invariantFor (trsys_of (pr1 || pr2))
+                    (fun pr => exists pr1' pr2' t',
+                         pr = pr1' || pr2'
+                         /\ hasty pr1' t'
+                         /\ hasty pr2' (complement t')).
+Proof.
+  simplify.
+  apply invariant_induction; simplify.
+
+  propositional; subst.
+  eauto 6.
+
+  clear pr1 pr2 t H H0.
+  first_order; subst.
+  invert H2.
+
+  invert H6; invert H0.
+  invert H6; invert H1.
+  eapply input_typed in H4; eauto.
+  eapply output_typed in H5; eauto.
+  first_order; subst.
+  invert H0.
+  invert H1.
+  eauto 7.
+  eapply input_typed in H5; eauto.
+  eapply output_typed in H4; eauto.
+  first_order; subst.
+  invert H0.
+  invert H1.
+  eauto 10.
+Qed.
+
+Theorem no_deadlock : forall pr1 pr2 t,
+    hasty pr1 t
+    -> hasty pr2 (complement t)
+    -> invariantFor (trsys_of (pr1 || pr2))
+                    (fun pr => pr = (Done || Done)
+                               \/ exists pr', lstep pr Silent pr').
+Proof.
+  simplify.
+  eapply invariant_weaken.
+  eapply complementarity_forever; eauto.
+
+  clear pr1 pr2 t H H0.
+  simplify; first_order; subst.
+  invert H0; invert H1; simplify; eauto.
+Qed.
+
+Example adding_no_deadlock : forall k input output,
+    input <> output
+    -> invariantFor (trsys_of (addN k input output
+                               || add2_client input output))
+               (fun pr => pr = (Done || Done)
+                          \/ exists pr', lstep pr Silent pr').
+Proof.
+  simplify.
+  eapply no_deadlock with (t := (???input(nat); !!!output(nat); TDone)%st);
+    hasty.
+Qed.
+
+End BasicTwoParty.
+
+
 (** * Two-Party Session Types *)
 
 Module TwoParty.
@@ -35,28 +196,12 @@ Inductive hasty : proc -> type -> Prop :=
 | HtDone :
     hasty Done TDone.
 
-
-(** * Examples of typed processes *)
-
-(* Recall our first example from last chapter. *)
-Definition addN (k : nat) (input output : channel) : proc :=
-  ??input(n : nat);
-  !!output(n + k);
-  Done.
-
 Ltac hasty := simplify; repeat ((constructor; simplify)
                                 || match goal with
                                    | [ |- hasty _ (match ?E with _ => _ end) ] => cases E
                                    | [ |- hasty (match ?E with _ => _ end) _ ] => cases E
                                    end).
 
-Theorem addN_typed : forall k input output,
-    hasty (addN k input output) (???input(_ : nat); !!!output(_ : nat); TDone).
-Proof.
-  hasty.
-Qed.
-
-
 (** * Complementing types *)
 
 Fixpoint complement (t : type) : type :=
@@ -66,17 +211,6 @@ Fixpoint complement (t : type) : type :=
   | TDone => TDone
   end.
 
-Definition add2_client (input output : channel) : proc :=
-  !!input(42);
-  ??output(_ : nat);
-  Done.
-
-Theorem add2_client_typed : forall input output,
-    hasty (add2_client input output) (complement (???input(_ : nat); !!!output(_ : nat); TDone)).
-Proof.
-  hasty.
-Qed.
-
 (** ** Example *)
 
 Section online_store.
@@ -207,7 +341,7 @@ Theorem no_deadlock : forall pr1 pr2 t,
     -> hasty pr2 (complement t)
     -> invariantFor (trsys_of (pr1 || pr2))
                     (fun pr => pr = (Done || Done)
-                               \/ exists l' pr', lstep pr l' pr').
+                               \/ exists pr', lstep pr Silent pr').
 Proof.
   simplify.
   eapply invariant_weaken.
@@ -216,8 +350,6 @@ Proof.
   clear pr1 pr2 t H H0.
   simplify; first_order; subst.
   invert H0; invert H1; simplify; eauto.
-  Unshelve.
-  assumption.
 Qed.
 
 Example online_store_no_deadlock : forall request_product in_stock_or_not
@@ -230,7 +362,7 @@ Example online_store_no_deadlock : forall request_product in_stock_or_not
                                       send_payment_info payment_success add_review
                                       in_stock payment_checker))
                (fun pr => pr = (Done || Done)
-                          \/ exists l' pr', lstep pr l' pr').
+                          \/ exists pr', lstep pr Silent pr').
 Proof.
   simplify.
   eapply no_deadlock with (t := customer_type request_product in_stock_or_not
@@ -1145,12 +1277,12 @@ Section online_store_with_warehouse.
       {| Sender := Merchant';
          Receiver := Customer' |}.
 
-  Example online_store_no_deadlock' : forall product payment_info in_stock good_infos,
+  Example online_store_no_deadlock' : forall product payment_info payment_checker in_stock,
       NoDup [request_product; in_stock_or_not; send_payment_info; payment_success; add_review;
              merchant_to_warehouse; warehouse_to_merchant]
       -> invariantFor (trsys_of (customer' product payment_info
-                                 || (merchant' in_stock
+                                 || (merchant' payment_checker
-                                     || (warehouse good_infos || Done))))
+                                     || (warehouse in_stock || Done))))
                       (fun pr => inert pr
                                  \/ exists pr', lstep pr Silent pr').
   Proof.