From 35d15a765db32639935ec63900005447642c4f9a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 16 May 2021 11:55:01 -0400 Subject: [PATCH] Revising for the final week of class --- MessagesAndRefinement.v | 56 ++++++++++++++++++++--------------------- SessionTypes.v | 30 +++++++++++----------- frap_book.tex | 3 +-- 3 files changed, 44 insertions(+), 45 deletions(-) diff --git a/MessagesAndRefinement.v b/MessagesAndRefinement.v index 0e3238a..5a4aac4 100644 --- a/MessagesAndRefinement.v +++ b/MessagesAndRefinement.v @@ -29,11 +29,11 @@ Notation channel := nat (only parsing). (* Here are the basic syntactic constructions of processes. *) Inductive proc := | NewChannel (notThese : list channel) (k : channel -> proc) -(* Pick a new channel name [ch] not found in [notThese], and continue like +(* Pick a new channel name [ch] not found in [notThese] and continue like * [k ch]. *) | BlockChannel (ch : channel) (pr : proc) -(* Act like [pr], but prevent interaction with other processes through channel +(* Act like [pr] but prevent interaction with other processes through channel * [ch]. We effectively force [ch] to be *private*. *) | Send (ch : channel) {A : Type} (v : A) (k : proc) @@ -146,7 +146,7 @@ Inductive lstep : proc -> label -> proc -> Prop := | LStepDup : forall pr, lstep (Dup pr) Silent (Par (Dup pr) pr) -(* A channel allocation operation nondeterministically picks the new channel ID, +(* A channel-allocation operation nondeterministically picks the new channel ID, * only checking that it isn't in the provided blacklist. We install a [Block] * node to keep this channel truly private. *) | LStepNew : forall chs ch k, @@ -241,7 +241,7 @@ Inductive couldGenerate : proc -> list action -> Prop := (* Skip ahead to [refines_couldGenerate] to see the top-level connection from * [refines]. *) -Hint Constructors couldGenerate : core. +Global Hint Constructors couldGenerate : core. Lemma lstepSilent_couldGenerate : forall pr1 pr2, lstepSilent^* pr1 pr2 @@ -251,7 +251,7 @@ Proof. induct 1; eauto. Qed. -Hint Resolve lstepSilent_couldGenerate : core. +Global Hint Resolve lstepSilent_couldGenerate : core. Lemma simulates_couldGenerate' : forall (R : proc -> proc -> Prop), (forall pr1 pr2, R pr1 pr2 @@ -305,8 +305,8 @@ Ltac inverter := | [ H : lstepSilent _ _ |- _ ] => invert H end. -Hint Constructors lstep : core. -Hint Unfold lstepSilent : core. +Global Hint Constructors lstep : core. +Global Hint Unfold lstepSilent : core. Ltac lists' := repeat match goal with @@ -316,7 +316,7 @@ Ltac lists' := Ltac lists := solve [ lists' ]. -Hint Extern 1 (NoDup _) => lists : core. +Global Hint Extern 1 (NoDup _) => lists : core. (** * Examples *) @@ -361,7 +361,7 @@ Inductive R_add2 : proc -> proc -> Prop := (Block intermediate; Done || Done) Done. -Hint Constructors R_add2 : core. +Global Hint Constructors R_add2 : core. Theorem add2_once_refines_addN : forall input output, input <> output @@ -462,9 +462,9 @@ Inductive RDup (R : proc -> proc -> Prop) : proc -> proc -> Prop := -> RDup R pr2 pr2' -> RDup R (Par pr1 pr2) (Par pr1' pr2'). -Hint Constructors RDup : core. +Global Hint Constructors RDup : core. -Hint Unfold lstepSilent : core. +Global Hint Unfold lstepSilent : core. Lemma lstepSilent_Par1 : forall pr1 pr1' pr2, lstepSilent^* pr1 pr1' @@ -480,7 +480,7 @@ Proof. induct 1; eauto. Qed. -Hint Resolve lstepSilent_Par1 lstepSilent_Par2 : core. +Global Hint Resolve lstepSilent_Par1 lstepSilent_Par2 : core. Lemma refines_Dup_Action : forall R : _ -> _ -> Prop, (forall pr1 pr2, R pr1 pr2 @@ -593,7 +593,7 @@ Inductive RPar (R1 R2 : proc -> proc -> Prop) : proc -> proc -> Prop := -> R2 pr2 pr2' -> RPar R1 R2 (pr1 || pr2) (pr1' || pr2'). -Hint Constructors RPar : core. +Global Hint Constructors RPar : core. Lemma refines_Par_Action : forall R1 R2 : _ -> _ -> Prop, (forall pr1 pr2, R1 pr1 pr2 @@ -706,8 +706,8 @@ Inductive RBlock (R : proc -> proc -> Prop) : proc -> proc -> Prop := R pr1 pr2 -> RBlock R (Block ch; pr1) (Block ch; pr2). -Hint Constructors RBlock : core. -Hint Unfold notUse : core. +Global Hint Constructors RBlock : core. +Global Hint Unfold notUse : core. Lemma lstepSilent_Block : forall ch pr1 pr2, lstepSilent^* pr1 pr2 @@ -716,7 +716,7 @@ Proof. induct 1; eauto. Qed. -Hint Resolve lstepSilent_Block : core. +Global Hint Resolve lstepSilent_Block : core. Theorem refines_Block : forall pr1 pr2 ch, pr1 <| pr2 @@ -743,7 +743,7 @@ Inductive RBlock2 : proc -> proc -> Prop := | RBlock2_1 : forall ch1 ch2 pr, RBlock2 (Block ch1; Block ch2; pr) (Block ch2; Block ch1; pr). -Hint Constructors RBlock2 : core. +Global Hint Constructors RBlock2 : core. Theorem refines_Block2 : forall ch1 ch2 pr, Block ch1; Block ch2; pr <| Block ch2; Block ch1; pr. @@ -783,7 +783,7 @@ Inductive neverUses (ch : channel) : proc -> Prop := | NuDone : neverUses ch Done. -Hint Constructors neverUses : core. +Global Hint Constructors neverUses : core. Lemma neverUses_step : forall ch pr1, neverUses ch pr1 @@ -793,14 +793,14 @@ Proof. induct 1; invert 1; eauto. Qed. -Hint Resolve neverUses_step : core. +Global Hint Resolve neverUses_step : core. Inductive RBlockS : proc -> proc -> Prop := | RBlockS1 : forall ch pr1 pr2, neverUses ch pr2 -> RBlockS (Block ch; pr1 || pr2) ((Block ch; pr1) || pr2). -Hint Constructors RBlockS : core. +Global Hint Constructors RBlockS : core. Lemma neverUses_notUse : forall ch pr l, neverUses ch pr @@ -824,7 +824,7 @@ Proof. simplify; auto. Qed. -Hint Resolve neverUses_notUse : core. +Global Hint Resolve neverUses_notUse : core. Theorem refines_BlockS : forall ch pr1 pr2, neverUses ch pr2 @@ -1008,7 +1008,7 @@ Inductive RTree (t : tree) (input output : channel) : proc -> proc -> Prop := (Block output'; threads || Done) Done. -Hint Constructors TreeThreads RTree : core. +Global Hint Constructors TreeThreads RTree : core. Lemma TreeThreads_actionIs : forall ch maySend pr, TreeThreads ch maySend pr @@ -1055,7 +1055,7 @@ Proof. induct 1; eauto. Qed. -Hint Resolve TreeThreads_silent TreeThreads_maySend TreeThreads_action TreeThreads_weaken : core. +Global Hint Resolve TreeThreads_silent TreeThreads_maySend TreeThreads_action TreeThreads_weaken : core. Lemma TreeThreads_inTree_par' : forall n ch t, TreeThreads ch (mem n t) (inTree_par' n t ch). @@ -1066,7 +1066,7 @@ Proof. cases (mem n t2); simplify; eauto. Qed. -Hint Resolve TreeThreads_inTree_par' : core. +Global Hint Resolve TreeThreads_inTree_par' : core. (* Finally, the main theorem: *) Theorem refines_inTree_par : forall t input output, @@ -1186,7 +1186,7 @@ Inductive Rhandoff (ch : channel) (A : Type) (v : A) (k : A -> proc) : proc -> p -> manyOf (??ch(x : A); k x) recvs -> Rhandoff ch v k (Block ch; Done || recvs) rest. -Hint Constructors manyOf manyOfAndOneOf Rhandoff : core. +Global Hint Constructors manyOf manyOfAndOneOf Rhandoff : core. Lemma manyOf_action : forall this pr, manyOf this pr @@ -1226,7 +1226,7 @@ Proof. invert H1; eauto. Qed. -Hint Resolve manyOf_silent manyOf_rendezvous : core. +Global Hint Resolve manyOf_silent manyOf_rendezvous : core. Lemma manyOfAndOneOf_output : forall ch (A : Type) (k : A -> _) rest ch0 (A0 : Type) (v0 : A0) pr, manyOfAndOneOf (Recv ch k) rest pr @@ -1260,7 +1260,7 @@ Proof. induct 1; simplify; eauto. Qed. -Hint Resolve manyOf_manyOfAndOneOf : core. +Global Hint Resolve manyOf_manyOfAndOneOf : core. Lemma no_rendezvous : forall ch0 (A0 : Type) (v : A0) pr1 rest (k : A0 -> _), manyOfAndOneOf (??ch0 (x : _); k x) rest pr1 @@ -1335,7 +1335,7 @@ Proof. invert H. Qed. -Hint Resolve manyOfAndOneOf_silent manyOf_rendezvous : core. +Global Hint Resolve manyOfAndOneOf_silent manyOf_rendezvous : core. Lemma manyOfAndOneOf_action : forall ch (A : Type) (k : A -> _) rest pr, manyOfAndOneOf (Recv ch k) rest pr diff --git a/SessionTypes.v b/SessionTypes.v index c62cea0..2baab3f 100644 --- a/SessionTypes.v +++ b/SessionTypes.v @@ -36,7 +36,7 @@ Inductive type := (* This type applies to a process that begins by sending a value of type [A] * over channel [ch], then continuing according to type [t]. *) -| TRecv (ch : channel) (A : Type) (t : type) +| TRecv (ch : channel) (A : Type) (t : type) (* This type is the dual of the last one: the process begins by receiving a * value of type [A] from channel [ch]. *) @@ -128,7 +128,7 @@ Definition trsys_of pr := {| (* Note: here we force silent steps, so that all channel communication is * internal. *) -Hint Constructors hasty : core. +Global Hint Constructors hasty : core. (* The next two lemmas state some inversions that connect stepping and * typing. *) @@ -347,7 +347,7 @@ Definition trsys_of pr := {| Step := lstepSilent |}. -Hint Constructors hasty : core. +Global Hint Constructors hasty : core. Lemma input_typed : forall pr ch A v pr', lstep pr (Action (Input {| Channel := ch; TypeOf := A; Value := v |})) pr' @@ -515,7 +515,7 @@ Definition trsys_of pr := {| Step := lstepSilent |}. -Hint Constructors hasty : core. +Global Hint Constructors hasty : core. (* We prove that the type system rules out fancier constructs. *) @@ -546,7 +546,7 @@ Proof. assumption. Qed. -Hint Immediate hasty_not_Block hasty_not_Dup hasty_not_Par : core. +Global Hint Immediate hasty_not_Block hasty_not_Dup hasty_not_Par : core. (* Next, we characterize how channels must be mapped, given typing of a * process. *) @@ -605,7 +605,7 @@ Inductive typed_multistate party (channels : channel -> parties party) (t : type -> typed_multistate channels t ps pr2 -> typed_multistate channels t (p :: ps) (pr1 || pr2). -Hint Constructors typed_multistate : core. +Global Hint Constructors typed_multistate : core. (* This fancier typing judgment gets a fancier tactic for type-checking. *) @@ -652,7 +652,7 @@ Proof. assumption. Qed. -Hint Immediate no_silent_steps : core. +Global Hint Immediate no_silent_steps : core. Lemma complementarity_forever_done : forall party (channels : _ -> parties party) pr pr', lstep pr Silent pr' @@ -676,7 +676,7 @@ Proof. assumption. Qed. -Hint Immediate mayNotSend_really : core. +Global Hint Immediate mayNotSend_really : core. Lemma may_not_output : forall (party : Type) pr pr' ch (A : Type) (v : A), lstep pr (Action (Output {| Channel := ch; Value := v |})) pr' @@ -692,7 +692,7 @@ Proof. assumption. Qed. -Hint Immediate may_not_output : core. +Global Hint Immediate may_not_output : core. Lemma output_is_legit : forall (party : Type) pr pr' ch (A : Type) (v : A), lstep pr (Action (Output {| Channel := ch; Value := v |})) pr' @@ -815,7 +815,7 @@ Proof. induct 1; eauto. Qed. -Local Hint Immediate hasty_relax : core. +Global Hint Immediate hasty_relax : core. Lemma complementarity_preserve_unused : forall party (channels : _ -> parties party) pr ch (A : Type) (t : A -> _) all_parties, @@ -1058,7 +1058,7 @@ Inductive inert : proc -> Prop := -> inert pr2 -> inert (pr1 || pr2). -Hint Constructors inert : core. +Global Hint Constructors inert : core. (* Now a few more fiddly lemmas. See you again at the [Theorem]. *) @@ -1070,7 +1070,7 @@ Proof. invert H; eauto. Qed. -Hint Immediate typed_multistate_inert : core. +Global Hint Immediate typed_multistate_inert : core. Lemma deadlock_find_receiver : forall party (channels : _ -> parties party) all_parties ch (A : Type) (k : A -> _) pr, @@ -1420,7 +1420,7 @@ Inductive mayTouch : proc -> channel -> Prop := mayTouch pr1 ch -> mayTouch (Dup pr1) ch. -Hint Constructors mayTouch : core. +Global Hint Constructors mayTouch : core. Import BasicTwoParty Multiparty. @@ -1435,7 +1435,7 @@ Proof. end. Qed. -Hint Immediate lstep_mayTouch : core. +Global Hint Immediate lstep_mayTouch : core. Lemma Input_mayTouch : forall pr ch (A : Type) (v : A) pr', lstep pr (Action (Input {| Channel := ch; Value := v |})) pr' @@ -1451,7 +1451,7 @@ Proof. induct 1; eauto. Qed. -Hint Immediate Input_mayTouch Output_mayTouch : core. +Global Hint Immediate Input_mayTouch Output_mayTouch : core. Lemma independent_execution : forall pr1 pr2 pr, lstepSilent^* (pr1 || pr2) pr diff --git a/frap_book.tex b/frap_book.tex index 0305d0f..2b02f53 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -5607,7 +5607,7 @@ In the \emph{synchronous}\index{synchronous message passing} or \emph{rendezvous The threads of the two complementary operations \emph{rendezvous} and pass the message in one atomic step. Packages of semantics and proof techniques for such languages are often called \emph{process algebras}\index{process algebra}, as they support an algebraic style of reasoning about the source code of message-passing programs. -That is, we prove laws very similar to the familiar equations of algebra, and use those laws to ``rewrite'' inside larger processes, by replacing their subprocesses with others we have shown suitably equivalent. +That is, we prove laws very similar to the familiar equations of algebra and use those laws to ``rewrite'' inside larger processes, by replacing their subprocesses with others we have shown suitably equivalent. It's a powerful technique for highly modular proofs, which we develop in the rest of this chapter for one concrete synchronous language. Well-known process algebras include the $\pi$-calculus\index{$\pi$-calculus} and the Calculus of Communicating Systems\index{Calculus of Communicating Systems}; the one we focus on is idiosyncratic and designed partly to make the Coq proofs manageable. @@ -5722,7 +5722,6 @@ Instead, we formalize refinement via \emph{simulation}, very similarly to how we Intuitively, $R$ is a simulation when, starting in a pair of related processes, any step on the left can be matched by a step on the right, taking us back into $R$. The conditions are naturally illustrated with commuting diagrams\index{commuting diagram}. - \[ \begin{tikzcd} p_1 \arrow{r}{R} \arrow{d}{\forall \longrightarrow} & p_2 \arrow{d}{\exists \longrightarrow^*} \\