Commit 16bf2d36 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak comments a bit.

parent ee3c6ec1
Pipeline #21629 passed with stage
in 17 minutes and 21 seconds
(** This file defines the core of the Actris logic:
- It defines dependent separation protocols and the various operations on it
dual, append, branching
like dual, append, and branching.
- It defines the connective [c ↣ prot] for ownership of channel endpoints.
- It proves Actris's specifications of [send] and [receive] w.r.t. dependent
separation protocols.
Dependent separation protocols are defined by instanting the parametrized
Dependent separation protocols are defined by instantiating the parameterized
version in [proto_model] with type of values [val] of HeapLang and the
propositions [iProp] of Iris.
......@@ -35,9 +35,10 @@ describes that channel endpoint [c] adheres to protocol [prot]. This connective
is modeled using Iris invariants and ghost state along with the logical
connectives of the channel encodings [is_chan] and [chan_own].
Lastly, relevant typeclasses 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 protocol connectives. *)
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
protocol connectives. *)
From actris.channel Require Export channel.
From actris.channel Require Import proto_model.
From iris.base_logic.lib Require Import invariants.
......@@ -530,7 +531,7 @@ Section proto.
by iApply (iProto_le_trans with "Hle").
Qed.
(** ** Auxiliary definitions and invariants *)
(** ** Lemmas about the auxiliary definitions and invariants *)
Global Instance proto_interp_ne : NonExpansive2 (proto_interp (Σ:=Σ) vs).
Proof. induction vs; solve_proper. Qed.
Global Instance proto_interp_proper vs :
......@@ -618,7 +619,7 @@ Section proto.
Arguments proto_interp : simpl never.
(** ** Initialization of a channel *)
(** ** Helper lemma for initialization of a channel *)
Lemma proto_init E cγ c1 c2 p :
is_chan protoN cγ c1 c2 -
chan_own cγ Left [] - chan_own cγ Right [] ={E}=
......@@ -641,7 +642,8 @@ Section proto.
iFrame "Hrstf Hinv Hcctx". iSplit; [done|]. iApply iProto_le_refl.
Qed.
(** ** Accessor style lemmas *)
(** ** Accessor style lemmas, used as helpers to prove the specifications of
[send] and [recv]. *)
Lemma proto_send_acc {TT} c (pc : TT val * iProp Σ * iProto Σ) (x : TT) :
c iProto_message Send pc -
(pc x).1.2 -
......
(** This file defines the model of dependent separation protocols, along with
various operations on the connective, such as append and map.
various operations, such as append and map.
Important: This file should not be used directly, but rather the wrappers in
[proto_channel] should be used.
Dependent separation protocols are designed with inspiration from session types,
mimicking their constructors [!T.st], [?T.st] and [END], respectively,
representing sending and receiving messages of type [T] and termination. The
main difference is that the dependent separation protocols are defined over
separation logic propositions, instead of types.
Dependent Separation Protocols are modeled as the solution of the following
recursive domain equation:
Dependent Separation Protocols are modeled as the following type:
[proto := 1 + (action * (V → (▶ proto → PROP) → PROP))]
[proto = 1 + (action * (V → (▶ proto → PROP) → PROP))]
Here, the left-hand side of the sum is used for the terminated process, while
the right-hand side is used for the communication constructors. The type
......@@ -20,18 +15,16 @@ the right-hand side is used for the communication constructors. The type
[Receive]. Compared to having an additional sum in [proto], this makes it
possible to factorize the code in a better way.
The remainder [V → (▶ [proto] → PROP) → PROP)] is a continuation that depends
on the communicated value [V] and the dependent tail [▶ proto → PROP] from
protocols guarded under laters to the propositions of the logic.
The type [proto] is defined as a solution to a recursive domain equation, as
it is self-referential under the guard of [▶].
The remainder [V → (▶ proto → PROP) → PROP)] is a predicate that ranges over
the communicated value [V] and the tail protocol [▶ proto → PROP]. Note that in
order to solve this recursive domain equation using Iris's COFE solver, the
recursive occurrences of [proto] appear under the guard [▶].
On top of the type [proto], we define the constructors:
- [proto_end], which constructs the left-side of the sum.
- [proto_msg], which takes an action and a continuation and constructs the
right-hand side of the sum accodingly.
- [proto_msg], which takes an action and a predicate and constructs the
right-hand side of the sum accordingly.
The defined functions on the type [proto] are:
......
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