Commit d63c639a authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak comments.

parent d6c96f96
Pipeline #20403 failed with stage
in 0 seconds
(** This file contains the definition of the channels, encoded as a pair of (** This file contains the definition of the channels, encoded as a pair of
lock-protected buffers, on which we define the three message-passing primitives: lock-protected buffers, and their primitive proof rules. Actris's proof rules
for channels in terms of dependent separation protocols can be found in the file
[theories/channel/proto_channel.v].
In this file we define the three message-passing connectives:
- [new_chan] creates references to two empty buffers and a lock, and returns a - [new_chan] creates references to two empty buffers and a lock, and returns a
pair of endpoints, where the order of the two references determines the pair of endpoints, where the order of the two references determines the
...@@ -8,13 +12,18 @@ lock-protected buffers, on which we define the three message-passing primitives: ...@@ -8,13 +12,18 @@ lock-protected buffers, on which we define the three message-passing primitives:
- [recv] performs a busy loop until there is something in the second buffer, - [recv] performs a busy loop until there is something in the second buffer,
which it pops and returns, locking during each peek. which it pops and returns, locking during each peek.
The specifications are defined in terms of the logical connectives [is_chan] The logically-atomic basic (i.e. non dependent separation protocol)
and [chan_own]: proof rules [new_chan_spec], [send_spec] and [recv_spec] are defined in terms
of the logical connectives [is_chan] and [chan_own]:
- [is_chan γ v1 v2] is a persistent proposition expressing that [v1] and [v2] - [is_chan γ v1 v2] is a persistent proposition expressing that [v1] and [v2]
are the endpoints of a channel with logical name [γ]. are the endpoints of a channel with logical name [γ].
- [chan_own γ s vs] is an exclusive proposition expressing the buffer of side - [chan_own γ s vs] is an exclusive proposition expressing the buffer of side
[s] ([Left] or [Right]) has contents [vs]. *) [s] ([Left] or [Right]) has contents [vs].
Note that the specifications include 3 laters [▷] to account for the three
levels of indirection due to step-indexing in the model of dependent separation
protocols. *)
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.heap_lang Require Import lifting. From iris.heap_lang Require Import lifting.
...@@ -27,7 +36,7 @@ Instance side_inhabited : Inhabited side := populate Left. ...@@ -27,7 +36,7 @@ Instance side_inhabited : Inhabited side := populate Left.
Definition side_elim {A} (s : side) (l r : A) : A := Definition side_elim {A} (s : side) (l r : A) : A :=
match s with Left => l | Right => r end. match s with Left => l | Right => r end.
(** Message-Passing Primitives *) (** * The definition of the message-passing connectives *)
Definition new_chan : val := Definition new_chan : val :=
λ: <>, λ: <>,
let: "l" := lnil #() in let: "l" := lnil #() in
...@@ -58,7 +67,7 @@ Definition recv : val := ...@@ -58,7 +67,7 @@ Definition recv : val :=
| NONE => "go" "c" | NONE => "go" "c"
end. end.
(** Channel ghost functor *) (** * Setup of Iris's cameras *)
Class chanG Σ := { Class chanG Σ := {
chanG_lockG :> lockG Σ; chanG_lockG :> lockG Σ;
chanG_authG :> auth_exclG (listO valO) Σ; chanG_authG :> auth_exclG (listO valO) Σ;
...@@ -77,7 +86,7 @@ Section channel. ...@@ -77,7 +86,7 @@ Section channel.
chan_r_name : gname chan_r_name : gname
}. }.
(** The invariant of channels *) (** * The logical connectives *)
Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ := Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
( ls rs, ( ls rs,
llist sbi_internal_eq l ls own (chan_l_name γ) ( to_auth_excl ls) llist sbi_internal_eq l ls own (chan_l_name γ) ( to_auth_excl ls)
...@@ -103,10 +112,10 @@ Section channel. ...@@ -103,10 +112,10 @@ Section channel.
iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame. iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
Qed. Qed.
(** The ownership of channels *)
Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ := Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl vs)%I. own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl vs)%I.
(** * The proof rules *)
Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs). Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
Proof. by apply _. Qed. Proof. by apply _. Qed.
...@@ -208,5 +217,4 @@ Section channel. ...@@ -208,5 +217,4 @@ Section channel.
iIntros "!> !>" (v vs' ->) "Hvs". iIntros "!> !>" (v vs' ->) "Hvs".
iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures. iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures.
Qed. Qed.
End channel. End channel.
(** This file contains tactics for the message-passing connectives, (** This file contains the definitions of Actris's tactics for symbolic
as well as the necessary typeclasses. execution of message-passing programs. The API of these tactics is documented
This includes a way of reducing protocols to a normal form, to prepare in the [README.md] file. The implementation follows the same pattern for the
them for use in the appropriate specifications. implementation of these tactics that is used in Iris. In addition, it uses a
This normalisation includes e.g. resolving duals. standard pattern using type classes to perform the normalization.
The tactics are: In addition to the tactics for symbolic execution, this file defines the tactic
- [wp_send (x1 .. xn) with "selpat"] which resolves weakest preconditions of the [solve_proto_contractive], which can be used to automatically prove that
form [wp (send c v) Q], in the presence of an ownership of a send protocol recursive protocols are contractive. *)
[c ↣ <!> x .. y, MSG v; {{ P }}; prot] in the context. That is done by using
[x1 .. xn] to existentially quantify the variables [x .. y], and "ipat" to
resolve the predicate [P]. The result is continuing as [Q],
with [c ↣ prot] in the context.
- [wp_recv (x1 .. xn) as "ipat"] which conversely resolves [wp (recv c) Q] with
[c ↣ <?> x .. y, MSG v; {{ P }}; prot] in the context, where the variables
[x .. y] are introduced as [x1 .. xn], and the predicate [P] is introduces based
on the pattern [ipat].
- [wp_select with "selpat"] which resolves [wp (select c b) Q] with
[c ↣ prot1 {Q1}<+>{Q2} prot2] in the context. Here [selpat] is used to
resolve either [Q1] or [Q2], based on the chosen branch. The resulting
protocol is similarly [c ↣ prot1] or [c ↣ prot2] based on the chosen
branch.
- [wp_branch as ipat1 | ipat2] which resolves [wp (branch c e1 e2) Q] with
[c ↣ prot1 {Q1}<&>{Q2} prot2] in the context. The result is two subgoals,
in which [Q1] and [Q2] are introduced using [ipat1] and [ipat2], and the
protocol ownership is [c ↣ prot1] and [c ↣ prot2] respectively. *)
From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From actris Require Export proto_channel. From actris Require Export proto_channel.
From iris.proofmode Require Import coq_tactics reduction spec_patterns. From iris.proofmode Require Import coq_tactics reduction spec_patterns.
(** Classes *) (** * Tactics for proving contractiveness of protocols *)
Class ActionDualIf (d : bool) (a1 a2 : action) :=
dual_action_if : a2 = if d then action_dual a1 else a1.
Hint Mode ActionDualIf ! ! - : typeclass_instances.
(** Tactics for proving contractiveness of protocols *)
Ltac f_proto_contractive := Ltac f_proto_contractive :=
match goal with match goal with
| _ => apply iProto_branch_contractive | _ => apply iProto_branch_contractive
...@@ -53,7 +27,11 @@ Ltac f_proto_contractive := ...@@ -53,7 +27,11 @@ Ltac f_proto_contractive :=
Ltac solve_proto_contractive := Ltac solve_proto_contractive :=
solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]). solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]).
(** Normalization of protocols *) (** * Normalization of protocols *)
Class ActionDualIf (d : bool) (a1 a2 : action) :=
dual_action_if : a2 = if d then action_dual a1 else a1.
Hint Mode ActionDualIf ! ! - : typeclass_instances.
Instance action_dual_if_false a : ActionDualIf false a a := eq_refl. Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
Instance action_dual_if_true_send : ActionDualIf true Send Receive := eq_refl. Instance action_dual_if_true_send : ActionDualIf true Send Receive := eq_refl.
Instance action_dual_if_true_receive : ActionDualIf true Receive Send := eq_refl. Instance action_dual_if_true_receive : ActionDualIf true Receive Send := eq_refl.
...@@ -82,7 +60,6 @@ Section classes. ...@@ -82,7 +60,6 @@ Section classes.
Implicit Types p : iProto Σ. Implicit Types p : iProto Σ.
Implicit Types TT : tele. Implicit Types TT : tele.
(** Classes *)
Lemma proto_unfold_eq p1 p2 : p1 p2 ProtoUnfold p1 p2. Lemma proto_unfold_eq p1 p2 : p1 p2 ProtoUnfold p1 p2.
Proof. rewrite /ProtoNormalize=> Hp d pas q ->. by rewrite Hp. Qed. Proof. rewrite /ProtoNormalize=> Hp d pas q ->. by rewrite Hp. Qed.
...@@ -166,7 +143,8 @@ Section classes. ...@@ -166,7 +143,8 @@ Section classes.
destruct d; by rewrite /= -?iProto_app_branch -?iProto_dual_branch. destruct d; by rewrite /= -?iProto_app_branch -?iProto_dual_branch.
Qed. Qed.
(** Automatically perform normalization of protocols in the proof mode *) (** Automatically perform normalization of protocols in the proof mode when
using [iAssumption] and [iFrame]. *)
Global Instance mapsto_proto_from_assumption q c p1 p2 : Global Instance mapsto_proto_from_assumption q c p1 p2 :
ProtoNormalize false p1 [] p2 ProtoNormalize false p1 [] p2
FromAssumption q (c p1) (c p2). FromAssumption q (c p1) (c p2).
...@@ -183,8 +161,8 @@ Section classes. ...@@ -183,8 +161,8 @@ Section classes.
Qed. Qed.
End classes. End classes.
(** Symbolic execution tactics *) (** * Symbolic execution tactics *)
(* TODO: strip laters *) (* TODO: Maybe strip laters from other hypotheses in the future? *)
Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
c p (pc : TT val * iProp Σ * iProto Σ) Φ : c p (pc : TT val * iProp Σ * iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p)%I envs_lookup i Δ = Some (false, c p)%I
......
(** This file contains an instantiation of the (** This file defines the core of the Actris logic:
Dependent Separation Protocols and an integration with the channel encodings.
For starters this means fixing the types of messages to the - It defines dependent separation protocols and the various operations on it
value type of the language [val] and the logic to the Iris logic [iProp Σ]. dual, append, 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
version in [proto_model] with type of values [val] of HeapLang and the
propositions [iProp] of Iris.
In doing so we define ways of constructing instances of the instantiated type In doing so we define ways of constructing instances of the instantiated type
via two constructors: via two constructors:
- [iProto_end] which is identical to [proto_end] - [iProto_end], which is identical to [proto_end].
- [iProto_message] which takes an action and a continuation to construct - [iProto_message], which takes an action and a continuation to construct
the corresponding message protocols. the corresponding message protocols.
For convenience sake the following notation is provided: For convenience sake, we provide the following notations:
- [END] which is simply [iProto_end] - [END], which is simply [iProto_end].
- [<!> x .. y, MSG v; {{ P }}; prot] and - [<!> x1 .. xn, MSG v; {{ P }}; prot] and [<?> x1 .. xn, MSG v; {{ P }}; prot],
- [<?> x .. y, MSG v; {{ P }}; prot] which constructs an instance of which construct an instance of [iProto_message] with the appropriate
iProto_message with an appropriate continuation. continuation.
Said continuation ultimately establishes the following: Futhermore, we define the following operations:
- Existential quantification of variables [x .. y]. - [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
- The equivalence [v = w], where [w] is the value that is eventually exchanged. - [iProto_app], which appends two protocols as described in proto_model.v
- Ownership of the predicate [P]
- A continuation as [prot] An encoding of the usual branching connectives [prot1 {Q1}<+>{Q2} prot2] and
[prot1 {Q1}<&>{Q2} prot2], inspired by session types, is also included in this
Futhermore type-specific variants of dual and append are provided: file.
- [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 The logical connective for protocol ownership is denoted as [c ↣ prot]. It
describes that channel endpoint [c] adheres to protocol [prot]. This connective
An encoding of branching behaviour is additionally included, defined is modeled using Iris invariants and ghost state along with the logical
in terms of sending and receiving boolean flags: connectives of the channel encodings [is_chan] and [chan_own].
- [prot1 {Q1}<+>{Q2} prot2] and
- [prot1 {Q1}<&>{Q2} prot2] which defines ownership of Q1 or Q2, and continues as Lastly, relevant typeclasses are defined for each of the above notions, such as
Q1 or Q2, based on the exchanged flag. contractiveness and non-expansiveness, after which the specifications of the
message-passing primitives are defined in terms of the protocol connectives. *)
The logical connective of protocol ownership is then defined:
- [c ↣ prot] which describes that channel endpoint [c] adheres
to protocol [prot], achieved through 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.*)
From actris.channel Require Export channel. From actris.channel Require Export channel.
From actris.channel Require Import proto_model. From actris.channel Require Import proto_model.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
...@@ -51,7 +50,7 @@ Definition start_chan : val := λ: "f", ...@@ -51,7 +50,7 @@ Definition start_chan : val := λ: "f",
let: "cc" := new_chan #() in let: "cc" := new_chan #() in
Fork ("f" (Snd "cc"));; Fst "cc". Fork ("f" (Snd "cc"));; Fst "cc".
(** Camera setup *) (** * Setup of Iris's cameras *)
Class proto_chanG Σ := { Class proto_chanG Σ := {
proto_chanG_chanG :> chanG Σ; proto_chanG_chanG :> chanG Σ;
proto_chanG_authG :> auth_exclG (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))) Σ; proto_chanG_authG :> auth_exclG (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))) Σ;
...@@ -64,12 +63,12 @@ Definition proto_chanΣ := #[ ...@@ -64,12 +63,12 @@ Definition proto_chanΣ := #[
Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ proto_chanG Σ. Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ proto_chanG Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed. Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
(** Types *) (** * Types *)
Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ). Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
Delimit Scope proto_scope with proto. Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto. Bind Scope proto_scope with iProto.
(** Operators *) (** * Operators *)
Definition iProto_end_def {Σ} : iProto Σ := proto_end. Definition iProto_end_def {Σ} : iProto Σ := proto_end.
Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed. Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
Definition iProto_end := iProto_end_aux.(unseal). Definition iProto_end := iProto_end_aux.(unseal).
...@@ -79,7 +78,7 @@ Arguments iProto_end {_}. ...@@ -79,7 +78,7 @@ Arguments iProto_end {_}.
Program Definition iProto_message_def {Σ} {TT : tele} (a : action) Program Definition iProto_message_def {Σ} {TT : tele} (a : action)
(pc : TT val * iProp Σ * iProto Σ) : iProto Σ := (pc : TT val * iProp Σ * iProto Σ) : iProto Σ :=
proto_message a (λ v, λne f, x : TT, proto_message a (λ v, λne f, x : TT,
(* Need the laters to make [iProto_message] contractive *) (** We need the later to make [iProto_message] contractive *)
v = (pc x).1.1 v = (pc x).1.1
(pc x).1.2 (pc x).1.2
f (Next (pc x).2))%I. f (Next (pc x).2))%I.
...@@ -163,7 +162,7 @@ Notation "<?> 'MSG' v ; p" := ...@@ -163,7 +162,7 @@ Notation "<?> 'MSG' v ; p" :=
Notation "'END'" := iProto_end : proto_scope. Notation "'END'" := iProto_end : proto_scope.
(** Dual *) (** * Operations *)
Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ := Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
proto_map action_dual cid cid p. proto_map action_dual cid cid p.
Arguments iProto_dual {_} _%proto. Arguments iProto_dual {_} _%proto.
...@@ -173,7 +172,6 @@ Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ := ...@@ -173,7 +172,6 @@ Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
Arguments iProto_dual_if {_} _ _%proto. Arguments iProto_dual_if {_} _ _%proto.
Instance: Params (@iProto_dual_if) 2 := {}. Instance: Params (@iProto_dual_if) 2 := {}.
(** Branching *)
Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ) Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
(p1 p2 : iProto Σ) : iProto Σ := (p1 p2 : iProto Σ) : iProto Σ :=
(<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto. (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
...@@ -189,13 +187,12 @@ Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope ...@@ -189,13 +187,12 @@ Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope
Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope. Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope. Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
(** Append *)
Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2. Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
Arguments iProto_app {_} _%proto _%proto. Arguments iProto_app {_} _%proto _%proto.
Instance: Params (@iProto_app) 1 := {}. Instance: Params (@iProto_app) 1 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope. Infix "<++>" := iProto_app (at level 60) : proto_scope.
(** Auxiliary definitions and invariants *) (** * Auxiliary definitions and invariants *)
Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ := Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
match vs with match vs with
| [] => p1 iProto_dual p2 | [] => p1 iProto_dual p2
...@@ -234,6 +231,7 @@ Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ := ...@@ -234,6 +231,7 @@ Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
Definition protoN := nroot .@ "proto". Definition protoN := nroot .@ "proto".
(** * The connective for ownership of channel ends *)
Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ} Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
(c : val) (p : iProto Σ) : iProp Σ := (c : val) (p : iProto Σ) : iProp Σ :=
( s (c1 c2 : val) γ, ( s (c1 c2 : val) γ,
...@@ -248,12 +246,13 @@ Instance: Params (@mapsto_proto) 4 := {}. ...@@ -248,12 +246,13 @@ Instance: Params (@mapsto_proto) 4 := {}.
Notation "c ↣ p" := (mapsto_proto c p) Notation "c ↣ p" := (mapsto_proto c p)
(at level 20, format "c ↣ p"). (at level 20, format "c ↣ p").
(** * Proofs *)
Section proto. Section proto.
Context `{!proto_chanG Σ, !heapG Σ}. Context `{!proto_chanG Σ, !heapG Σ}.
Implicit Types p : iProto Σ. Implicit Types p : iProto Σ.
Implicit Types TT : tele. Implicit Types TT : tele.
(** Non-expansiveness of operators *) (** ** Non-expansiveness of operators *)
Lemma iProto_message_contractive {TT} a Lemma iProto_message_contractive {TT} a
(pc1 pc2 : TT val * iProp Σ * iProto Σ) n : (pc1 pc2 : TT val * iProp Σ * iProto Σ) n :
(.. x, (pc1 x).1.1 = (pc2 x).1.1) (.. x, (pc1 x).1.1 = (pc2 x).1.1)
...@@ -307,7 +306,7 @@ Section proto. ...@@ -307,7 +306,7 @@ Section proto.
by apply iProto_message_proper=> /= -[]. by apply iProto_message_proper=> /= -[].
Qed. Qed.
(** Dual *) (** ** Dual *)
Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ). Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ). Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ).
...@@ -341,7 +340,7 @@ Section proto. ...@@ -341,7 +340,7 @@ Section proto.
by apply iProto_message_proper=> /= -[]. by apply iProto_message_proper=> /= -[].
Qed. Qed.
(** Append *) (** ** Append *)
Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ). Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ).
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance iProto_app_proper : Proper (() ==> () ==> ()) (@iProto_app Σ). Global Instance iProto_app_proper : Proper (() ==> () ==> ()) (@iProto_app Σ).
...@@ -377,7 +376,7 @@ Section proto. ...@@ -377,7 +376,7 @@ Section proto.
iProto_dual (p1 <++> p2) (iProto_dual p1 <++> iProto_dual p2)%proto. iProto_dual (p1 <++> p2) (iProto_dual p1 <++> iProto_dual p2)%proto.
Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed. Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.
(** Auxiliary definitions and invariants *) (** ** Auxiliary definitions and invariants *)
Global Instance proto_interp_ne : NonExpansive2 (proto_interp vs). Global Instance proto_interp_ne : NonExpansive2 (proto_interp vs).
Proof. induction vs; solve_proper. Qed. Proof. induction vs; solve_proper. Qed.
Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs). Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs).
...@@ -457,7 +456,7 @@ Section proto. ...@@ -457,7 +456,7 @@ Section proto.
Arguments proto_interp : simpl never. Arguments proto_interp : simpl never.
(** The actual specs *) (** ** Initialization of a channel *)
Lemma proto_init E cγ c1 c2 p : Lemma proto_init E cγ c1 c2 p :
is_chan protoN cγ c1 c2 - is_chan protoN cγ c1 c2 -
chan_own cγ Left [] - chan_own cγ Right [] ={E}= chan_own cγ Left [] - chan_own cγ Right [] ={E}=
...@@ -478,7 +477,7 @@ Section proto. ...@@ -478,7 +477,7 @@ Section proto.
- iExists Right, c1, c2, pγ; iFrame; auto. - iExists Right, c1, c2, pγ; iFrame; auto.
Qed. Qed.
(** Accessor style lemmas *) (** ** Accessor style lemmas *)
Lemma proto_send_acc {TT} E c (pc : TT val * iProp Σ * iProto Σ) : Lemma proto_send_acc {TT} E c (pc : TT val * iProp Σ * iProto Σ) :
protoN E protoN E
c iProto_message Send pc - s c1 c2 γ, c iProto_message Send pc - s c1 c2 γ,
...@@ -611,7 +610,7 @@ Section proto. ...@@ -611,7 +610,7 @@ Section proto.
iExists x. iFrame "Hv HP". by iRewrite "Hq". iExists x. iFrame "Hv HP". by iRewrite "Hq".
Qed. Qed.
(** Specifications of send and receive *) (** ** Specifications of [send] and [receive] *)
Lemma new_chan_proto_spec : Lemma new_chan_proto_spec :
{{{ True }}} {{{ True }}}
new_chan #() new_chan #()
...@@ -648,6 +647,8 @@ Section proto. ...@@ -648,6 +647,8 @@ Section proto.
iMod ("H" $! x with "Hf Hvs"); auto. iMod ("H" $! x with "Hf Hvs"); auto.
Qed. Qed.
(** A version written without Texan triples that is more convenient to use
(via [iApply] in Coq. *)
Lemma send_proto_spec {TT} Ψ c v (pc : TT val * iProp Σ * iProto Σ) : Lemma send_proto_spec {TT} Ψ c v (pc : TT val * iProp Σ * iProto Σ) :
c iProto_message Send pc - c iProto_message Send pc -
(.. x : TT, (.. x : TT,
...@@ -688,6 +689,8 @@ Section proto. ...@@ -688,6 +689,8 @@ Section proto.
iDestruct "H" as (x ->) "H". by iApply "HΨ". iDestruct "H" as (x ->) "H". by iApply "HΨ".
Qed. Qed.
(** A version written without Texan triples that is more convenient to use
(via [iApply] in Coq. *)
Lemma recv_proto_spec {TT} Ψ c (pc : TT val * iProp Σ * iProto Σ) : Lemma recv_proto_spec {TT} Ψ c (pc : TT val * iProp Σ * iProto Σ) :
c iProto_message Receive pc - c iProto_message Receive pc -
(.. x : TT, c (pc x).2 - (pc x).1.2 - Ψ (pc x).1.1) - (.. x : TT, c (pc x).2 - (pc x).1.2 - Ψ (pc x).1.1) -
...@@ -698,7 +701,7 @@ Section proto. ...@@ -698,7 +701,7 @@ Section proto.
iApply ("H" with "[$] [$]"). iApply ("H" with "[$] [$]").
Qed. Qed.
(** Branching *) (** ** Specifications for branching *)
Lemma select_spec c (b : bool) P1 P2 p1 p2 : Lemma select_spec c (b : bool) P1 P2 p1 p2 :
{{{ c (p1 <{P1}+{P2}> p2) if b then P1 else P2 }}} {{{ c (p1 <{P1}+{P2}> p2) if b then P1 else P2 }}}
send c #b send c #b
......
(** This file defines the model of Dependent Separation Protocols, (** This file defines the model of dependent separation protocols, along with
along with various operations on the connective, such as append various operations on the connective, such as append and map.
and map and the necessary typeclass instances.