SessionTypes: simplified and proved a key invariant

MessagesAndRefinement.v

@@ -335,7 +335,7 @@ Definition add2_once (input output : channel) : proc :=
  * of the first process as the fancy *implementation* and the second process as
  * the simpler *specification*. *)
 Inductive R_add2 : proc -> proc -> Prop :=
-| Initial : forall input output,
+| Starting : forall input output,
     input <> output
     -> R_add2
          (New[input;output](ch); ??input(n : nat); !!ch(n + 1); Done

SessionTypes.v

@@ -14,14 +14,11 @@ Set Asymmetric Patterns.
 Inductive type :=
 | TSend (ch : channel) (A : Set) (t : type)
 | TRecv (ch : channel) (A : Set) (t : type)
-| TPar (t1 t2 : type)
-| TDup (t : type)
 | TDone
 
 | InternalChoice (t1 t2 : type)
 | ExternalChoice (t1 t2 : type).
 
-Infix "||" := Par : st_scope.
 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.
@@ -29,116 +26,13 @@ Notation "??? ch ( A ) ; k" := (TRecv ch A k%st) (right associativity, at level
 Infix "|?|" := InternalChoice (at level 40) : st_scope.
 Infix "?|?" := ExternalChoice (at level 40) : st_scope.
 
-
-Inductive ignoresChannel (ch : channel) : type -> Prop :=
-| IcSend : forall ch' A t,
-    ch' <> ch
-    -> ignoresChannel ch t
-    -> ignoresChannel ch (TSend ch' A t)
-| IcRecv : forall ch' A t,
-    ch' <> ch
-    -> ignoresChannel ch t
-    -> ignoresChannel ch (TRecv ch' A t)
-| IcPar : forall t1 t2,
-    ignoresChannel ch t1
-    -> ignoresChannel ch t2
-    -> ignoresChannel ch (TPar t1 t2)
-| IcDup : forall t,
-    ignoresChannel ch t
-    -> ignoresChannel ch (TDup t)
-| IcDone :
-    ignoresChannel ch TDone
-
-| IcInternalChoice : forall t1 t2,
-    ignoresChannel ch t1
-    -> ignoresChannel ch t2
-    -> ignoresChannel ch (InternalChoice t1 t2)
-| IcExternalChoice : forall t1 t2,
-    ignoresChannel ch t1
-    -> ignoresChannel ch t2
-    -> ignoresChannel ch (ExternalChoice t1 t2).
-
-Inductive hideChannel (ch : channel) : type -> type -> Prop :=
-| HideIgnored : forall t,
-    ignoresChannel ch t
-    -> hideChannel ch t t
-
-| HideExtSend1 : forall ch' A t1 t2 t',
-    ch' <> ch
-    -> ignoresChannel ch' t2
-    -> hideChannel ch (TPar t1 t2) t'
-    -> hideChannel ch (TPar (TSend ch' A t1) t2) (TSend ch' A t')
-| HideExtRecv1 : forall ch' A t1 t2 t',
-    ch' <> ch
-    -> ignoresChannel ch' t2
-    -> hideChannel ch (TPar t1 t2) t'
-    -> hideChannel ch (TPar (TRecv ch' A t1) t2) (TRecv ch' A t')
-| HideExtSend2 : forall ch' A t1 t2 t',
-    ch' <> ch
-    -> ignoresChannel ch' t2
-    -> hideChannel ch (TPar t1 t2) t'
-    -> hideChannel ch (TPar t1 (TSend ch' A t2)) (TSend ch' A t')
-| HideExtRecv2 : forall ch' A t1 t2 t',
-    ch' <> ch
-    -> ignoresChannel ch' t2
-    -> hideChannel ch (TPar t1 t2) t'
-    -> hideChannel ch (TPar t1 (TRecv ch' A t2)) (TRecv ch' A t')
-
-| HideRendezvous1 : forall A t1 t2 t',
-    hideChannel ch (TPar t1 t2) t'
-    -> hideChannel ch (TPar (TSend ch A t1) (TRecv ch A t2)) t'
-| HideRendezvous2 : forall A t1 t2 t',
-    hideChannel ch (TPar t1 t2) t'
-    -> hideChannel ch (TPar (TRecv ch A t1) (TSend ch A t2)) t'.
-
-Fixpoint shrink (t : type) : type :=
-  match t with
-  | TSend ch A t1 => TSend ch A (shrink t1)
-  | TRecv ch A t1 => TRecv ch A (shrink t1)
-  | TPar t1 t2 =>
-    let t1' := shrink t1 in
-    let t2' := shrink t2 in
-    match t1', t2' with
-    | TDone, _ => t2'
-    | _, TDone => t1'
-    | _, _ => TPar t1' t2'
-    end
-  | TDup t1 =>
-    let t1' := shrink t1 in
-    match t1' with
-    | TDone => TDone
-    | _ => TDup t1'
-    end
-  | TDone => TDone
-
-  | InternalChoice t1 t2 => InternalChoice (shrink t1) (shrink t2)
-  | ExternalChoice t1 t2 => ExternalChoice (shrink t1) (shrink t2)
-  end.
-
 Inductive hasty : proc -> type -> Prop :=
-| HtNewChannel : forall notThese k t tc tcs,
-    (forall ch, ~In ch notThese -> hasty (k ch) (t ch))
-    -> (forall ch, ~In ch notThese -> hideChannel ch (t ch) tc)
-    -> shrink tc = tcs
-    -> hasty (NewChannel notThese k) tcs
-| HtBlockChannel : forall ch pr t tc tcs,
-    hasty pr t
-    -> hideChannel ch t tc
-    -> shrink tc = tcs
-    -> hasty (BlockChannel ch pr) tcs
 | 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)
-| HtPar : forall pr1 pr2 t1 t2,
-    hasty pr1 t1
-    -> hasty pr2 t2
-    -> hasty (Par pr1 pr2) (TPar t1 t2)
-| HtDup : forall pr t,
-    hasty pr t
-    -> hasty (Dup pr) (TDup t)
 | HtDone :
     hasty Done TDone
 
@@ -162,37 +56,10 @@ Definition addN (k : nat) (input output : channel) : proc :=
   !!output(n + k);
   Done.
 
+Ltac hasty := simplify; repeat (constructor; simplify).
+
 Theorem addN_typed : forall k input output,
     hasty (addN k input output) (???input(nat); !!!output(nat); TDone).
-Proof.
-  simplify.
-  repeat (constructor; simplify).
-Qed.
-
-Definition add2 (input output : channel) : proc :=
-  Dup (New[input;output](intermediate);
-        addN 1 input intermediate
-        || addN 1 intermediate output).
-
-Ltac hide1 := apply HideRendezvous1 || apply HideRendezvous2
-              || (eapply HideIgnored; repeat constructor; equality)
-              || (eapply HideExtSend1; [ equality | repeat constructor; equality | ])
-              || (eapply HideExtRecv1; [ equality | repeat constructor; equality | ])
-              || (eapply HideExtSend2; [ equality | repeat constructor; equality | ])
-              || (eapply HideExtRecv2; [ equality | repeat constructor; equality | ]).
-
-Ltac hide := repeat hide1.
-
-Ltac hasty1 :=
-  match goal with
-  | [ |- hasty _ _ ] => econstructor; simplify
-  end.
-
-Ltac hasty := simplify; repeat hasty1; simplify; hide; try equality.
-
-Theorem add2_typed : forall input output,
-    input <> output
-    -> hasty (add2 input output) (TDup (???input(nat); !!!output(nat); TDone)).
 Proof.
   hasty.
 Qed.
@@ -204,8 +71,6 @@ 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)
-  | TPar t1 t2 => TPar (complement t1) (complement t2)
-  | TDup t1 => TDup (complement t1)
   | TDone => TDone
 
   | InternalChoice t1 t2 => ExternalChoice (complement t1) (complement t2)
@@ -213,13 +78,126 @@ Fixpoint complement (t : type) : type :=
   end.
 
 Definition add2_client (input output : channel) : proc :=
-  Dup (!!input(42);
+  !!input(42);
   ??output(_ : nat);
-       Done).
+  Done.
 
 Theorem add2_client_typed : forall input output,
     input <> output
-    -> hasty (add2_client input output) (complement (TDup (???input(nat); !!!output(nat); TDone))).
+    -> 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 hasty_not_NewChannel : forall chs pr t,
+    hasty (NewChannel chs pr) t
+    -> False.
+Proof.
+  induct 1; auto.
+Qed.
+
+Lemma hasty_not_BlockChannel : forall ch pr t,
+    hasty (BlockChannel ch pr) t
+    -> False.
+Proof.
+  induct 1; auto.
+Qed.
+
+Lemma hasty_not_Dup : forall pr t,
+    hasty (Dup pr) t
+    -> False.
+Proof.
+  induct 1; auto.
+Qed.
+
+Lemma hasty_not_Par : forall pr1 pr2 t,
+    hasty (pr1 || pr2) t
+    -> False.
+Proof.
+  induct 1; auto.
+Qed.
+
+Hint Immediate hasty_not_NewChannel hasty_not_BlockChannel hasty_not_Dup hasty_not_Par.
+
+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; simplify; try solve [ exfalso; eauto ].
+  induct H; 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; simplify; try solve [ exfalso; eauto ].
+  induct H; eauto.
+Qed.
+
+Lemma complementarity_rendezvous : forall ch (A : Set) (k1 : A -> _) t,
+  hasty (Recv ch k1) t
+  -> forall (v : A) k2, hasty (Send ch v k2) (complement t)
+    -> exists t', hasty (k1 v) t' /\ hasty k2 (complement t').
+Proof.
+  induct 1; invert 1; simplify; eauto.
+Qed.
+
+Lemma complement_inverse : forall t,
+    t = complement (complement t).
+Proof.
+  induct t; simplify; equality.
+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; try solve [ exfalso; eauto ].
+
+  invert H6; try solve [ exfalso; eauto ].
+
+  eapply input_typed in H4; eauto.
+  eapply output_typed in H5; eauto.
+  first_order; subst.
+  eapply complementarity_rendezvous in H0; eauto.
+  first_order.
+
+  eapply input_typed in H5; eauto.
+  eapply output_typed in H4; eauto.
+  first_order; subst.
+  rewrite complement_inverse in H0.
+  eapply complementarity_rendezvous in H1; eauto.
+  first_order.
+  rewrite complement_inverse in H.
+  first_order.
+Qed.