From 91fc06122ddae4ab0b62a2f6a37f969bdb496c80 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 12 May 2018 14:53:37 -0400 Subject: [PATCH] Start of SessionTypes --- SessionTypes.v | 225 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 225 insertions(+) create mode 100644 SessionTypes.v diff --git a/SessionTypes.v b/SessionTypes.v new file mode 100644 index 0000000..8c70346 --- /dev/null +++ b/SessionTypes.v @@ -0,0 +1,225 @@ +(** Formal Reasoning About Programs + * Chapter 20: Session Types + * Author: Adam Chlipala + * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) + +Require Import Frap MessagesAndRefinement. + +Set Implicit Arguments. +Set Asymmetric Patterns. + + +(** * Defining the Type System *) + +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. +Notation "??? ch ( A ) ; k" := (TRecv ch A k%st) (right associativity, at level 45, ch at level 0) : st_scope. +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 + +| HtInternalChoice1 : forall pr t1 t2, + hasty pr t1 + -> hasty pr (InternalChoice t1 t2) +| HtInternalChoice2 : forall pr t1 t2, + hasty pr t2 + -> hasty pr (InternalChoice t1 t2) +| HtExternalChoice : forall pr t1 t2, + hasty pr t1 + -> hasty pr t2 + -> hasty pr (ExternalChoice t1 t2). + + +(** * 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. + +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. + + +(** * 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) + | TPar t1 t2 => TPar (complement t1) (complement t2) + | TDup t1 => TDup (complement t1) + | TDone => TDone + + | InternalChoice t1 t2 => ExternalChoice (complement t1) (complement t2) + | ExternalChoice t1 t2 => InternalChoice (complement t1) (complement t2) + end. + +Definition add2_client (input output : channel) : proc := + Dup (!!input(42); + ??output(_ : nat); + Done). + +Theorem add2_client_typed : forall input output, + input <> output + -> hasty (add2_client input output) (complement (TDup (???input(nat); !!!output(nat); TDone))). +Proof. + hasty. +Qed.