Commit 0c8b2e21 authored by Jonas Kastberg's avatar Jonas Kastberg

Updated header for proto.v

parent 80bc8c13
......@@ -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)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment