From 0c8b2e21947d44ee33dfc3127fed1f683a1c413f Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 6 May 2020 20:45:40 +0200
Subject: [PATCH] Updated header for proto.v
---
theories/channel/proto.v | 58 +++++++++++++++++++++-------------------
1 file changed, 31 insertions(+), 27 deletions(-)
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 067baf5..012eb27 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -2,23 +2,46 @@
separation protocols and the various operations on it like dual, append, and
branching.
-Dependent separation protocols are defined by instantiating the parameterized
-version in [proto_model] with type of propositions [iProp] of Iris. We define
-ways of constructing instances of the instantiated type via two constructors:
+Dependent separation protocols [iProto] are defined by instantiating the
+parameterized version in [proto_model] with the type of propositions [iProp] of Iris.
+We define ways of constructing instances of the instantiated type via two
+constructors:
- [iProto_end], which is identical to [proto_end].
-- [iProto_message], which takes an action and a continuation to construct
- the corresponding message protocols.
+- [iProto_message], which takes an [action] and an [iMsg] which is a
+ sequence of binders [iMsg_exist] terminated by the payload
+ constructed with [iMsg_base] based on arguments v, P and prot
+ which are the value, the carried proposition and the [iProto] tail
+ respectively.
For convenience sake, we provide the following notations:
- [END], which is simply [iProto_end].
-- [<!> x1 .. xn, MSG v; {{ P }}; prot] and [<?> x1 .. xn, MSG v; {{ P }}; prot],
- which construct an instance of [iProto_message] with the appropriate
- continuation.
+- [∃ x,m] which is [iMsg_exist] with argument m.
+- [MSG v ; {{ P }}; prot] which is [iMsg_Base with
+- [<a> m] which is [iProto_message] with arguments a and m.
+
+We also include custom notation to more easily construct complete constructions:
+- [<a x1 .. xn> m] which is [<a> ∃ x1, .. ∃ xn, m]
+- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol
Futhermore, we define the following operations:
- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
- [iProto_app], which appends two protocols as described in proto_model.v
+In addition we define the [iProto_le] subprotocol relation, which generalises
+the following inductive definition for asynchronous subtyping on session types:
+
+ p1 <: p2 p1 <: p2 p1 <: !B.p3 ?A.p3 <: p2
+---------- ---------------- ---------------- ----------------------------
+end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2 ?A.p1 <: !B.p2
+
+Example:
+
+!R <: !R ?Q <: ?Q ?Q <: ?Q
+------------------- --------------
+?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
+------------------------------------
+ ?P.?Q.!R <: !R.?P.?Q
+
Lastly, relevant type classes instances are defined for each of the above
notions, such as contractiveness and non-expansiveness, after which the
specifications of the message-passing primitives are defined in terms of the
@@ -210,25 +233,6 @@ Arguments iProto_dual_if {_ _} _ _%proto.
Instance: Params (@iProto_dual_if) 3 := {}.
(** * Protocol entailment *)
-(* The definition [iProto_le] generalizes the following inductive definition
-for subtyping on session types:
-
- p1 <: p2 p1 <: p2
----------- ---------------- ----------------
-end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2
-
- p1 <: !B.p3 ?A.p3 <: p2
-----------------------------
- ?A.p1 <: !B.p2
-
-Example:
-
-!R <: !R ?Q <: ?Q ?Q <: ?Q
-------------------- --------------
-?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
-------------------------------------
- ?P.?Q.!R <: !R.?P.?Q
-*)
Definition iProto_le_pre {Σ V}
(rec : iProto Σ V → iProto Σ V → iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
◇ (p1 ≡ END ∗ p2 ≡ END) ∨
--
GitLab