Library iris.chan2heap.refine_protocol
From iris.algebra Require Import upred_big_op sts.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth sts saved_prop.
From iris.proofmode Require Import weakestpre invariants sts.
From iris.chan_lang Require Export lang derived refine refine_heap refine_heap_proofmode protocol.
From iris.chan2heap Require Export chan2heap.
From iris.chan_lang Require Import tactics.
From iris.heap_lang Require Import lang heap proofmode notation.
Import heap_lang.
Import uPred.
Inductive prot_mod {T: Type} : protocol T → list (val × chan_lang.val) → protocol T → Prop :=
| prot_mod_nil S S':
prot_eq S S' →
prot_mod S [] S'
| prot_mod_recv Φ S S' v l:
prot_mod S l S' →
prot_mod (prot_recv Φ S) (v::l) S'
| prot_mod_left S1 S2 S' l:
prot_mod S1 l S' →
prot_mod (prot_ext S1 S2) ((InjLV (LitV LitUnit), (chan_lang.LitV chan_lang.LitUnit))::l) S'
| prot_mod_right S1 S2 S' l:
prot_mod S2 l S' →
prot_mod (prot_ext S1 S2) ((InjRV (LitV LitUnit), (chan_lang.LitV chan_lang.LitUnit))::l) S'.
Instance prot_mod_proper T: Proper ((≡) ==> (=) ==> (≡) ==> iff) (@prot_mod T).
Proof.
intros p1 p1' Heq1 l1 l2 → p2 p2' Heq2.
split.
- intros Hmodc. revert p1' p2' Heq1 Heq2. induction Hmodc; auto.
× econstructor; setoid_subst; eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
- intros Hmodc. revert p1 p2 Heq1 Heq2. induction Hmodc; auto.
× econstructor; setoid_subst; eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
Qed.
Lemma prot_mod_app {T} (p1: protocol T) la p2 lb p3:
prot_mod p1 la p2 →
prot_mod p2 lb p3 →
prot_mod p1 (la ++ lb) p3.
Proof.
revert lb p3.
induction 1; auto; intros;
try (rewrite -app_comm_cons;
econstructor; eauto).
rewrite H. auto.
Qed.
Inductive prot_red {Ty} : protocol Ty → protocol Ty → Prop :=
| prot_send_red T S: prot_red (prot_send T S) S
| prot_recv_red T S: prot_red (prot_recv T S) S
| prot_intL_red S1 S2: prot_red (prot_int S1 S2) S1
| prot_intR_red S1 S2: prot_red (prot_int S1 S2) S2
| prot_extL_Red S1 S2: prot_red (prot_ext S1 S2) S1
| prot_extR_Red S1 S2: prot_red (prot_ext S1 S2) S2.
Section definitions.
Local Open Scope nat_scope.
Record session := Session { left_state: list choice; right_state: list choice;
left_ptr: loc; right_ptr: loc;
left_count: nat; right_count: nat}.
Global Instance sessionT_inhabited: Inhabited session :=
populate (Session [] [] 1%positive 1%positive 0 0).
Add Printing Constructor session.
Inductive token := left_tok (n: nat) | right_tok (n: nat).
Global Instance left_tok_inj : Inj (=) (=) left_tok.
Proof. by injection 1. Qed.
Global Instance right_tok_inj : Inj (=) (=) right_tok.
Proof. by injection 1. Qed.
Inductive prot_prim_step : relation session :=
| left_prim_step c pl tl tl' pr tr nl nr:
prot_prim_step (Session pl pr tl tr nl nr) (Session (pl ++ [c]) pr tl' tr (S nl) nr)
| right_prim_step c pr tr tr' pl tl nl nr:
prot_prim_step (Session pl pr tl tr nl nr) (Session pl (pr ++ [c]) tl tr' nl (S nr)).
Definition tok (s : session) : set token :=
{[ t | ∃ i, ((t = left_tok i) ∧ (i ≤ left_count s)) ∨
((t = right_tok i) ∧ (i ≤ right_count s))]}.
Global Arguments tok !_ /.
Canonical Structure sts := sts.STS prot_prim_step tok.
Definition up_left_tok (k: nat) : set token := {[ t | ∃ n, t = left_tok n ∧ n > k]}.
Definition up_right_tok (k: nat) : set token := {[ t | ∃ n, t = right_tok n ∧ n > k]}.
Definition up_left (p: list choice) (l: loc) (n: nat) : set session :=
{[ s' | left_state s' = p ∧
left_ptr s' = l ∧
left_count s' = n]}.
Definition up_right (p: list choice) (l: loc) (n: nat) : set session :=
{[ s' | right_state s' = p ∧
right_ptr s' = l ∧
right_count s' = n]}.
Definition up_exact s : set session := {[s]}.
Lemma up_left_closed p l n:
sts.closed (up_left p l n) (up_left_tok n).
Proof.
split.
- intros s'.
destruct 1 as (?&?&?).
set_unfold.
intros t (n'&[(?&?)|(?&?)]).
× subst. intros (n''&Hn&?).
inversion Hn; subst; omega.
× intros (?&?&?); congruence.
- intros s1 s2 (?&?&?) [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans.
× exfalso.
assert (left_tok (S nl) ∈ sts.tok (Session (pl ++ [c]) pr tl tr (S nl) nr)) as Hin1.
{ simpl. set_solver. }
assert (left_tok (S nl) ∉ sts.tok (Session (pl ++ [c]) pr tl tr nl nr)) as Hnin1.
{ simpl. set_unfold. intros (x&[(Hn&Hl)|(Hn&Hl)]).
× inversion Hn. subst. clear -Hl. omega.
× congruence. }
assert (left_tok (S nl) ∈ T1) as Hin2.
{ set_solver. }
assert (left_tok (S nl) ∈ up_left_tok n) as Hin3.
{ simpl in ×. subst. rewrite /up_left_tok. set_unfold.
eexists; split; auto. }
set_solver.
× set_unfold. subst. split_and!; auto.
Qed.
Lemma up_right_closed p l n:
sts.closed (up_right p l n) (up_right_tok n).
Proof.
split.
- intros s'.
destruct 1 as (?&?&?).
set_unfold.
intros t (n'&[(?&?)|(?&?)]).
× intros (?&?&?); congruence.
× subst. intros (n''&Hn&?).
inversion Hn; subst; omega.
- intros s1 s2 (?&?&?) [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans.
× set_unfold. subst. split_and!; auto.
× exfalso.
assert (right_tok (S nr) ∈ sts.tok (Session pl (pr ++ [c]) tl tr nl (S nr))) as Hin1.
{ simpl. set_solver. }
assert (right_tok (S nr) ∉ sts.tok (Session pl (pr ++ [c]) tl tr nl nr)) as Hnin1.
{ simpl. set_unfold. intros (x&[(Hn&Hl)|(Hn&Hl)]).
× congruence.
× inversion Hn. subst. clear -Hl. omega. }
assert (right_tok (S nr) ∈ T1) as Hin2.
{ set_solver. }
assert (right_tok (S nr) ∈ up_right_tok n) as Hin3.
{ simpl in ×. subst. rewrite /up_right_tok. set_unfold.
eexists; split; auto. }
set_solver.
Qed.
Definition upd_left (s: session) c (l: loc) :=
Session (left_state s ++ [c]) (right_state s) l (right_ptr s) (S (left_count s)) (right_count s).
Definition upd_right (s: session) c (l: loc) :=
Session (left_state s) (right_state s ++ [c]) (left_ptr s) l (left_count s) (S (right_count s)).
Lemma tok_up_left_all pl pr tl tr nl nr:
sts.tok (Session pl pr tl tr nl nr) ∪ up_left_tok nl ≡
{[ s | ∃ i, s = left_tok i]} ∪ {[ s | ∃ i, s = right_tok i ∧ i ≤ nr]}.
Proof.
set_unfold. split.
- intros [(n&[(?&?)|(?&?)])|(n&Heq)]; naive_solver.
- intros [(n&Heq)|(n&Heq&Hle)].
× subst; case (le_gt_dec n nl); naive_solver.
× subst; naive_solver.
Qed.
Lemma tok_up_right_all pl pr tl tr nl nr:
sts.tok (Session pl pr tl tr nl nr) ∪ up_right_tok nr ≡
{[ s | ∃ i, s = right_tok i]} ∪ {[ s | ∃ i, s = left_tok i ∧ i ≤ nl]}.
Proof.
set_unfold. split.
- intros [(n&[(?&?)|(?&?)])|(n&Heq)]; naive_solver.
- intros [(n&Heq)|(n&Heq&Hle)].
× subst; case (le_gt_dec n nr); naive_solver.
× subst; naive_solver.
Qed.
Lemma left_step c pl tl tl' pr tr nl nr:
sts.steps (Session pl pr tl tr nl nr, up_left_tok nl)
(Session (pl ++ [c]) pr tl' tr (S nl) nr, up_left_tok (S nl)).
Proof.
apply rtc_once.
constructor; first constructor; auto.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&Heq&?). subst. inversion Heq. omega.
× intros (n'&?&?). congruence.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&Heq&?). subst. inversion Heq. omega.
× intros (n'&?&?). congruence.
- rewrite ?tok_up_left_all. auto.
Qed.
Lemma right_step c pr tr tr' pl tl nl nr:
sts.steps (Session pl pr tl tr nl nr, up_right_tok nr)
(Session pl (pr ++ [c]) tl tr' nl (S nr), up_right_tok (S nr)).
Proof.
apply rtc_once.
constructor; first constructor; auto.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&?&?). congruence.
× intros (n'&Heq&?). subst. inversion Heq. omega.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&?&?). congruence.
× intros (n'&Heq&?). subst. inversion Heq. omega.
- rewrite ?tok_up_right_all. auto.
Qed.
End definitions.
Class protG Σ := ProtG {
prot_stsG :> stsG lang.heap_lang Σ sts;
}.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth sts saved_prop.
From iris.proofmode Require Import weakestpre invariants sts.
From iris.chan_lang Require Export lang derived refine refine_heap refine_heap_proofmode protocol.
From iris.chan2heap Require Export chan2heap.
From iris.chan_lang Require Import tactics.
From iris.heap_lang Require Import lang heap proofmode notation.
Import heap_lang.
Import uPred.
Inductive prot_mod {T: Type} : protocol T → list (val × chan_lang.val) → protocol T → Prop :=
| prot_mod_nil S S':
prot_eq S S' →
prot_mod S [] S'
| prot_mod_recv Φ S S' v l:
prot_mod S l S' →
prot_mod (prot_recv Φ S) (v::l) S'
| prot_mod_left S1 S2 S' l:
prot_mod S1 l S' →
prot_mod (prot_ext S1 S2) ((InjLV (LitV LitUnit), (chan_lang.LitV chan_lang.LitUnit))::l) S'
| prot_mod_right S1 S2 S' l:
prot_mod S2 l S' →
prot_mod (prot_ext S1 S2) ((InjRV (LitV LitUnit), (chan_lang.LitV chan_lang.LitUnit))::l) S'.
Instance prot_mod_proper T: Proper ((≡) ==> (=) ==> (≡) ==> iff) (@prot_mod T).
Proof.
intros p1 p1' Heq1 l1 l2 → p2 p2' Heq2.
split.
- intros Hmodc. revert p1' p2' Heq1 Heq2. induction Hmodc; auto.
× econstructor; setoid_subst; eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
- intros Hmodc. revert p1 p2 Heq1 Heq2. induction Hmodc; auto.
× econstructor; setoid_subst; eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
× intros. inversion Heq1. subst. econstructor. eauto.
Qed.
Lemma prot_mod_app {T} (p1: protocol T) la p2 lb p3:
prot_mod p1 la p2 →
prot_mod p2 lb p3 →
prot_mod p1 (la ++ lb) p3.
Proof.
revert lb p3.
induction 1; auto; intros;
try (rewrite -app_comm_cons;
econstructor; eauto).
rewrite H. auto.
Qed.
Inductive prot_red {Ty} : protocol Ty → protocol Ty → Prop :=
| prot_send_red T S: prot_red (prot_send T S) S
| prot_recv_red T S: prot_red (prot_recv T S) S
| prot_intL_red S1 S2: prot_red (prot_int S1 S2) S1
| prot_intR_red S1 S2: prot_red (prot_int S1 S2) S2
| prot_extL_Red S1 S2: prot_red (prot_ext S1 S2) S1
| prot_extR_Red S1 S2: prot_red (prot_ext S1 S2) S2.
Section definitions.
Local Open Scope nat_scope.
Record session := Session { left_state: list choice; right_state: list choice;
left_ptr: loc; right_ptr: loc;
left_count: nat; right_count: nat}.
Global Instance sessionT_inhabited: Inhabited session :=
populate (Session [] [] 1%positive 1%positive 0 0).
Add Printing Constructor session.
Inductive token := left_tok (n: nat) | right_tok (n: nat).
Global Instance left_tok_inj : Inj (=) (=) left_tok.
Proof. by injection 1. Qed.
Global Instance right_tok_inj : Inj (=) (=) right_tok.
Proof. by injection 1. Qed.
Inductive prot_prim_step : relation session :=
| left_prim_step c pl tl tl' pr tr nl nr:
prot_prim_step (Session pl pr tl tr nl nr) (Session (pl ++ [c]) pr tl' tr (S nl) nr)
| right_prim_step c pr tr tr' pl tl nl nr:
prot_prim_step (Session pl pr tl tr nl nr) (Session pl (pr ++ [c]) tl tr' nl (S nr)).
Definition tok (s : session) : set token :=
{[ t | ∃ i, ((t = left_tok i) ∧ (i ≤ left_count s)) ∨
((t = right_tok i) ∧ (i ≤ right_count s))]}.
Global Arguments tok !_ /.
Canonical Structure sts := sts.STS prot_prim_step tok.
Definition up_left_tok (k: nat) : set token := {[ t | ∃ n, t = left_tok n ∧ n > k]}.
Definition up_right_tok (k: nat) : set token := {[ t | ∃ n, t = right_tok n ∧ n > k]}.
Definition up_left (p: list choice) (l: loc) (n: nat) : set session :=
{[ s' | left_state s' = p ∧
left_ptr s' = l ∧
left_count s' = n]}.
Definition up_right (p: list choice) (l: loc) (n: nat) : set session :=
{[ s' | right_state s' = p ∧
right_ptr s' = l ∧
right_count s' = n]}.
Definition up_exact s : set session := {[s]}.
Lemma up_left_closed p l n:
sts.closed (up_left p l n) (up_left_tok n).
Proof.
split.
- intros s'.
destruct 1 as (?&?&?).
set_unfold.
intros t (n'&[(?&?)|(?&?)]).
× subst. intros (n''&Hn&?).
inversion Hn; subst; omega.
× intros (?&?&?); congruence.
- intros s1 s2 (?&?&?) [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans.
× exfalso.
assert (left_tok (S nl) ∈ sts.tok (Session (pl ++ [c]) pr tl tr (S nl) nr)) as Hin1.
{ simpl. set_solver. }
assert (left_tok (S nl) ∉ sts.tok (Session (pl ++ [c]) pr tl tr nl nr)) as Hnin1.
{ simpl. set_unfold. intros (x&[(Hn&Hl)|(Hn&Hl)]).
× inversion Hn. subst. clear -Hl. omega.
× congruence. }
assert (left_tok (S nl) ∈ T1) as Hin2.
{ set_solver. }
assert (left_tok (S nl) ∈ up_left_tok n) as Hin3.
{ simpl in ×. subst. rewrite /up_left_tok. set_unfold.
eexists; split; auto. }
set_solver.
× set_unfold. subst. split_and!; auto.
Qed.
Lemma up_right_closed p l n:
sts.closed (up_right p l n) (up_right_tok n).
Proof.
split.
- intros s'.
destruct 1 as (?&?&?).
set_unfold.
intros t (n'&[(?&?)|(?&?)]).
× intros (?&?&?); congruence.
× subst. intros (n''&Hn&?).
inversion Hn; subst; omega.
- intros s1 s2 (?&?&?) [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans.
× set_unfold. subst. split_and!; auto.
× exfalso.
assert (right_tok (S nr) ∈ sts.tok (Session pl (pr ++ [c]) tl tr nl (S nr))) as Hin1.
{ simpl. set_solver. }
assert (right_tok (S nr) ∉ sts.tok (Session pl (pr ++ [c]) tl tr nl nr)) as Hnin1.
{ simpl. set_unfold. intros (x&[(Hn&Hl)|(Hn&Hl)]).
× congruence.
× inversion Hn. subst. clear -Hl. omega. }
assert (right_tok (S nr) ∈ T1) as Hin2.
{ set_solver. }
assert (right_tok (S nr) ∈ up_right_tok n) as Hin3.
{ simpl in ×. subst. rewrite /up_right_tok. set_unfold.
eexists; split; auto. }
set_solver.
Qed.
Definition upd_left (s: session) c (l: loc) :=
Session (left_state s ++ [c]) (right_state s) l (right_ptr s) (S (left_count s)) (right_count s).
Definition upd_right (s: session) c (l: loc) :=
Session (left_state s) (right_state s ++ [c]) (left_ptr s) l (left_count s) (S (right_count s)).
Lemma tok_up_left_all pl pr tl tr nl nr:
sts.tok (Session pl pr tl tr nl nr) ∪ up_left_tok nl ≡
{[ s | ∃ i, s = left_tok i]} ∪ {[ s | ∃ i, s = right_tok i ∧ i ≤ nr]}.
Proof.
set_unfold. split.
- intros [(n&[(?&?)|(?&?)])|(n&Heq)]; naive_solver.
- intros [(n&Heq)|(n&Heq&Hle)].
× subst; case (le_gt_dec n nl); naive_solver.
× subst; naive_solver.
Qed.
Lemma tok_up_right_all pl pr tl tr nl nr:
sts.tok (Session pl pr tl tr nl nr) ∪ up_right_tok nr ≡
{[ s | ∃ i, s = right_tok i]} ∪ {[ s | ∃ i, s = left_tok i ∧ i ≤ nl]}.
Proof.
set_unfold. split.
- intros [(n&[(?&?)|(?&?)])|(n&Heq)]; naive_solver.
- intros [(n&Heq)|(n&Heq&Hle)].
× subst; case (le_gt_dec n nr); naive_solver.
× subst; naive_solver.
Qed.
Lemma left_step c pl tl tl' pr tr nl nr:
sts.steps (Session pl pr tl tr nl nr, up_left_tok nl)
(Session (pl ++ [c]) pr tl' tr (S nl) nr, up_left_tok (S nl)).
Proof.
apply rtc_once.
constructor; first constructor; auto.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&Heq&?). subst. inversion Heq. omega.
× intros (n'&?&?). congruence.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&Heq&?). subst. inversion Heq. omega.
× intros (n'&?&?). congruence.
- rewrite ?tok_up_left_all. auto.
Qed.
Lemma right_step c pr tr tr' pl tl nl nr:
sts.steps (Session pl pr tl tr nl nr, up_right_tok nr)
(Session pl (pr ++ [c]) tl tr' nl (S nr), up_right_tok (S nr)).
Proof.
apply rtc_once.
constructor; first constructor; auto.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&?&?). congruence.
× intros (n'&Heq&?). subst. inversion Heq. omega.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
× intros (n'&?&?). congruence.
× intros (n'&Heq&?). subst. inversion Heq. omega.
- rewrite ?tok_up_right_all. auto.
Qed.
End definitions.
Class protG Σ := ProtG {
prot_stsG :> stsG lang.heap_lang Σ sts;
}.
The Functors we need.
Definition protGF : gFunctorList := [stsGF sts; savedPropGF idCF].
Instance inGF_protG `{H : inGFs lang.heap_lang Σ protGF} : protG Σ.
Proof. destruct H as (?&?&?). split; apply _. Qed.
Section proof.
Context `{!protG Σ}.
Context `{!refineG heap_lang Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{!scheapG heap_lang Σ}.
Context `{!heap.heapG Σ}.
Context (N : namespace).
Context (code: Type).
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation protocol := (protocol code).
Implicit Type Θ : leibnizC code -n> (leibnizC val -n> leibnizC (chan_lang.val) -n> iProp).
Import heap_lang.
Definition some (v: val) := InjLV v.
Definition none := InjRV (LitV LitUnit).
Fixpoint link_list (root: loc) (l: list val) (endpt: loc) : iProp :=
match l with
| [] ⇒ (root ↦ none ★ ⧆(root = endpt))%I
| v :: l' ⇒ (∃ (next: loc), root ↦ some (#next, v) ★ link_list next l' endpt)%I
end.
Fixpoint link_list' (root: loc) (l: list val) (endpt: loc) : iProp :=
match l with
| [] ⇒ (⧆(root = endpt))%I
| v :: l' ⇒ (∃ (next: loc), root ↦ some (#next, v) ★ link_list' next l' endpt)%I
end.
Fixpoint prot_mod_prop Θ (p: protocol) (l: list (val × chan_lang.val)) : iProp :=
match p, l with
| _, [] ⇒ Emp%I
| prot_recv Φ p', (v1, v2) :: l' ⇒
(⧆Θ Φ v1 v2 ★ prot_mod_prop Θ p' l')%I
| prot_ext pl pr, (v1, v2) :: l' ⇒
match v1, v2 with
| InjLV (#()), chan_lang.InjLV (chan_lang.LitV chan_lang.LitUnit) ⇒ prot_mod_prop Θ pl l'
| InjRV (#()), chan_lang.InjRV (chan_lang.LitV chan_lang.LitUnit) ⇒ prot_mod_prop Θ pr l'
| _, _ ⇒ False%I
end
| _, _ :: _ ⇒ False%I
end.
Instance prot_mod_prop_ne: Proper ((dist n) ==> (≡) ==> (=) ==> dist n) prot_mod_prop.
Proof.
intros n i1 i2 Hequivi p1 p2 Hequiv l ? <-.
revert i1 i2 Hequivi p1 p2 Hequiv.
induction l; intros.
- simpl. destruct p1, p2; auto.
- simpl. inversion Hequiv; subst; eauto;
destruct a. rewrite IHl; eauto.
destruct v; auto;
apply sep_ne; auto; rewrite (Hequivi Φ); auto; eauto.
destruct v; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
Qed.
Instance prot_mod_prop_proper: Proper ((≡) ==> (≡) ==> (=) ==> (≡)) prot_mod_prop.
Proof.
intros i1 i2 Hequivi p1 p2 Hequiv l ? <-.
revert i1 i2 Hequivi p1 p2 Hequiv.
induction l; intros.
- simpl. destruct p1, p2; auto.
- simpl. inversion Hequiv; subst; eauto;
destruct a. rewrite IHl; eauto.
destruct v; auto;
apply sep_proper; auto; rewrite (Hequivi Φ); auto; eauto.
destruct v; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
Qed.
Global Instance affine_false {M: ucmraT}: (@AffineP M) False%I.
Proof. rewrite /AffineP. apply False_elim. Qed.
Instance prot_mod_prop_affine Θ p l: AffineP (prot_mod_prop Θ p l).
Proof.
revert p.
induction l.
- destruct p; try apply _.
- destruct p; rewrite //=; try apply _.
destruct a. apply _.
destruct a; destruct v; try apply _.
destruct v; try apply _.
destruct l0; try apply _.
destruct v0; try apply _.
destruct v0; try apply _.
destruct l0; try apply _.
destruct v; try apply _.
destruct l0; try apply _.
destruct v0; try apply _.
destruct v0; try apply _.
destruct l0; try apply _.
Qed.
Instance link_list_affine t1 l t2: AffineP (link_list t1 l t2).
Proof.
revert t1 t2.
induction l; rewrite //=; try apply _.
Qed.
Instance link_list'_affine t1 l t2: AffineP (link_list' t1 l t2).
Proof.
revert t1 t2.
induction l; rewrite //=; try apply _.
Qed.
Lemma link_list_end_pt root l ept:
link_list root l ept ⊣⊢ (link_list' root l ept ★ ept ↦ none)%I.
Proof.
apply (anti_symm (⊢)).
- revert root ept. induction l; intros root ept.
× simpl. iIntros "(Hpt&%)". subst.
iFrame "Hpt". apply affine_intro; first apply _.
auto.
× simpl. iIntros "Hll". iDestruct "Hll" as (next) "(Hpt&Hll)".
rewrite (IHl). iDestruct "Hll" as "(Hwand&Hept)". iFrame "Hept".
iExists next. by iFrame "Hpt".
- revert root ept. induction l; intros root ept.
× simpl. iIntros "(%&Hown)". subst. iFrame "Hown".
apply affine_intro; first apply _. auto.
× simpl. iIntros "(Hunroll&Hpt)".
iDestruct "Hunroll" as (n) "(?&Hll)". iCombine "Hll" "Hpt" as "Hll". rewrite IHl.
iExists n. by iFrame "Hll".
Qed.
Lemma link_list_end_pt_join root l ept (ept': loc) (v: val):
(link_list' root l ept ★ ept ↦ InjLV (#ept', v) ★ ept' ↦ none)%I
⊢ link_list root (l ++ [v]) ept'.
Proof.
revert root ept ept' v.
induction l.
- simpl. intros.
iIntros "(%&Hpt&Hpt')". subst. iExists ept'.
iFrame "Hpt". iFrame "Hpt'".
apply affine_intro; auto; apply _.
- simpl. intros.
iIntros "(Hun&Hpt&Hpt')". iDestruct "Hun" as (n) "(Hptn&Hll)".
iExists n. iFrame "Hptn". iCombine "Hll" "Hpt" as "Hll".
iCombine "Hll" "Hpt'" as "Hll". rewrite -assoc. rewrite IHl.
auto.
Qed.
Definition prot_inv Θ (c: chan_lang.loc) (pl pr: protocol) (s: session) : iProp :=
((∃ (l: list (heap_lang.val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c (map snd l, []) ★
link_list (right_ptr s) (map fst l) (left_ptr s) ★
prot_mod_prop Θ pr' l ★
⧆■(prot_mod pr' l (dual pl')))
∨
(∃ (l: list (val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c ([], map snd l) ★
link_list (left_ptr s) (map fst l) (right_ptr s) ★
prot_mod_prop Θ pl' l ★
⧆■(prot_mod pl' l (dual pr')))
)%I.
Instance prot_inv_ne n: Proper (dist n ==> (=) ==> (=) ==> (=) ==> (=) ==> dist n) prot_inv.
Proof.
intros t1 t2 Hdt ?? → ?? → ?? → ?? →.
rewrite /prot_inv.
apply or_ne;
repeat apply exist_ne=>?; repeat apply sep_ne; try eauto;
eapply prot_mod_prop_ne; eauto.
Qed.
Instance prot_inv_proper: Proper ((≡) ==> (=) ==> (=) ==> (≡) ==> (=) ==> (≡)) prot_inv.
Proof.
intros t1 t2 Hdt ?? → ?? → ?? ? ?? →.
rewrite /prot_inv.
apply or_proper;
repeat apply exist_proper=>?; repeat apply sep_proper; try eauto.
- setoid_subst. eauto.
- eapply prot_mod_prop_proper; eauto.
- setoid_subst. eauto.
- eapply prot_mod_prop_proper; eauto.
Qed.
Definition prot_ctx (γ : gname) Θ c pl pr : iProp :=
(⧆■ (heapN ⊥ N) ★ ⧆■(scheapN ⊥ N) ★ ⧆■(heapN ⊥ scheapN)
★ heap_ctx ★ scheap_ctx ★ sts_ctx γ N (prot_inv Θ c pl pr))%I.
Instance prot_ctx_ne n: Proper ((=) ==> dist n ==> (=) ==> (=) ==> (=) ==> dist n)
prot_ctx.
Proof.
intros ?? → t1 t2 Hdt ?? → ?? → ?? →.
rewrite /prot_ctx.
repeat apply sep_ne; try eauto.
eapply sts_ctx_ne; intros. intros ?.
eapply prot_inv_ne; eauto.
Qed.
Instance prot_ctx_proper: Proper ((=) ==> (≡) ==> (=) ==> (=) ==> (=) ==> (≡))
prot_ctx.
Proof.
intros ?? → t1 t2 Hdt ?? → ?? → ?? →.
rewrite /prot_ctx.
repeat apply sep_proper; try eauto.
eapply sts_ctx_proper; intros. intros ?.
eapply prot_inv_proper; eauto.
Qed.
Definition prot_mapsto Θ (c: loc × side) (l : loc) (p : protocol) : iProp :=
(∃ pl pr γ choices n, prot_ctx γ Θ (fst c) pl pr ★
match (snd c) with
| cleft ⇒ (sts_ownS γ (up_left choices l n) (up_left_tok n) ★
⧆■ (prot_modc pl choices p))
| cright ⇒ (sts_ownS γ (up_right choices l n) (up_right_tok n) ★
⧆■ (prot_modc pr choices p))
end)%I.
Instance prot_mapsto_affine: AffineP (prot_mapsto Θ c l p).
Proof.
intros. rewrite /prot_mapsto.
destruct c, s; simpl; apply _.
Qed.
Lemma prot_mapsto_ne n: Proper (dist n ==> (=) ==> (=) ==> (≡) ==> dist n) prot_mapsto.
Proof.
intros t1 t2 Hdt ?? → ?? → p1 p2 Hep.
rewrite /prot_mapsto.
repeat apply exist_ne=>?.
apply sep_ne.
- eapply prot_ctx_ne; eauto.
- destruct y, s; simpl; rewrite Hep; eauto.
Qed.
Lemma prot_mapsto_proper: Proper ((≡) ==> (=) ==> (=) ==> (≡) ==> (≡)) prot_mapsto.
Proof.
intros t1 t2 Hdt ?? → ?? → p1 p2 Hep.
rewrite /prot_mapsto.
repeat apply exist_proper=>?.
apply sep_proper.
- eapply prot_ctx_proper; eauto.
- destruct y, s; simpl; rewrite Hep; eauto.
Qed.
Lemma dual_involutive (p: protocol): p ≡ dual (dual p).
Proof.
revert p. cofix; intros p. rewrite (unfold_prot (dual _)).
destruct p; simpl; econstructor; try eapply dual_involutive.
Qed.
Lemma prot_inv_left_orient Θ p Φ c pl pr s:
(⧆▷ prot_inv Θ c pl pr s ★
⧆ ■ prot_modc pl (left_state s) (prot_send Φ p))
⊢ (⧆▷(∃ (l: list (val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c (map snd l, []) ★
link_list (right_ptr s) (map fst l) (left_ptr s) ★
prot_mod_prop Θ pr' l ★
⧆■(prot_mod pr' l (dual pl'))) ★ ⧆ ■ prot_modc pl (left_state s) (prot_send Φ p)).
Proof.
iIntros "(Hinv&%)".
rewrite pure_equiv //= -emp_True right_id.
rewrite /prot_inv. apply affine_intro; first apply _.
rewrite affine_elim. iNext.
iDestruct "Hinv" as "[Hl|Hr]"; auto.
iDestruct "Hr" as (l pl' pr') "(%&%&?&?&?&%)".
destruct l.
- iExists []. iExists pl'. iExists (pr').
iSplitL "". { apply affine_intro; first apply _; auto. }
iSplitL "". { apply affine_intro; first apply _; auto. }
iFrame "~1".
iSplitR ""; last first.
× iSplitL "".
** simpl. destruct pr'; auto.
** iPureIntro.
inversion H3. subst.
econstructor. rewrite H4. apply dual_involutive.
× simpl.
iDestruct "~" as "(Hpt&%)".
rewrite H4. iFrame "Hpt".
rewrite pure_equiv; first rewrite -emp_True //=; destruct pl'; auto.
- assert (pl' ≡ (prot_send Φ p)) as Hequiv.
{ eapply prot_modc_inj; eauto. }
exfalso. rewrite Hequiv in H3 ×. inversion 1.
Qed.
Lemma prot_inv_right_orient Θ p Φ c pl pr s:
(⧆▷ prot_inv Θ c pl pr s ★
⧆ ■ prot_modc pr (right_state s) (prot_send Φ p))
⊢ (⧆▷(∃ (l: list (val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c ([], map snd l) ★
link_list (left_ptr s) (map fst l) (right_ptr s) ★
prot_mod_prop Θ pl' l ★
⧆■(prot_mod pl' l (dual pr'))) ★ ⧆ ■ prot_modc pr (right_state s) (prot_send Φ p)).
Proof.
iIntros "(Hinv&%)".
rewrite pure_equiv //= -emp_True right_id.
rewrite /prot_inv. apply affine_intro; first apply _.
rewrite affine_elim. iNext.
iDestruct "Hinv" as "[Hl|Hr]"; auto.
iDestruct "Hl" as (l pl' pr') "(%&%&?&?&?&%)".
destruct l.
- iExists []. iExists pl'. iExists pr'.
iSplitL "". { apply affine_intro; first apply _; auto. }
iSplitL "". { apply affine_intro; first apply _; auto. }
iFrame "~1".
iSplitR ""; last first.
× iSplitL "".
** simpl. destruct pl'; auto.
** rewrite pure_equiv; first rewrite -emp_True //=.
inversion H3. subst.
econstructor. rewrite H4. apply dual_involutive.
× simpl.
iDestruct "~" as "(Hpt&%)".
rewrite H4. iFrame "Hpt".
rewrite pure_equiv; first rewrite -emp_True //=; destruct pr'; auto.
- assert (pr' ≡ (prot_send Φ p)) as Hequiv.
{ eapply prot_modc_inj; eauto. }
exfalso. rewrite Hequiv in H3 ×. inversion 1.
Qed.
Context (Hgt: 99 < Kd).
Global Instance protocol_inhabited: Inhabited protocol :=
populate (prot_end).
Lemma prot_mod_prop_recv_snoc Θ p l Φ p' vh vc:
prot_mod p l (prot_recv Φ p') →
(⧆ Θ Φ vh vc ★ prot_mod_prop Θ p l) ⊢ prot_mod_prop Θ p (l ++ [(vh, vc)]).
Proof.
remember (prot_recv Φ p') as p'' eqn:Hp''.
intros Hmod.
revert Φ Hp'' vh vc.
induction Hmod; intros; subst.
- inversion H0. simpl. destruct p; auto.
- simpl. destruct v as (vh'&vc').
rewrite -IHHmod; eauto.
iIntros "(H1&H2&H3)". iFrame "H1". iFrame "H2". auto.
- simpl. iIntros "(_&?)"; auto.
- simpl. iIntros "(_&?)"; auto.
Qed.
Lemma prot_mod_recv_snoc (p: protocol) l Φ p' vh vc:
prot_mod p l (prot_recv Φ p') →
prot_mod p (l ++ [(vh, vc)]) p'.
Proof.
remember (prot_recv Φ p') as p'' eqn:Hp''.
intros Hmod.
revert Φ Hp'' vh vc.
induction Hmod; intros; subst.
- simpl. inversion H0; subst. do 2 econstructor; eauto.
- simpl. econstructor; eauto.
- simpl. econstructor; eauto.
- simpl. econstructor; eauto.
Qed.
Lemma prot_mod_prop_emp Θ p: prot_mod_prop Θ p [] ⊣⊢ Emp.
Proof.
destruct p; auto.
Qed.
Lemma fresh_inv Θ (c: chan_lang.loc) l (p: protocol) :
(l ↦ InjRV #() ★ c ↦c ([], []) ★ heap_ctx ★ scheap_ctx)
⊢ prot_inv Θ c p (dual p) {| left_state := []; right_state := [];
left_ptr := l; right_ptr := l;
left_count := 0; right_count := 0|}.
Proof.
rewrite /prot_inv.
iIntros "(Hptr&Hch&#?&#?)".
iLeft. iExists []. iExists p. iExists (dual p). simpl.
rewrite pure_equiv; last (econstructor; reflexivity).
rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True ?left_id.
iFrame "Hch". iFrame "Hptr".
rewrite pure_equiv // -emp_True ?left_id.
rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True ?right_id.
iClear "~". iClear "~1". destruct p; eauto.
Qed.
Lemma alloc_spec Θ (p: protocol) i K d d':
(d > 1 ∧ d ≤ Kd)%nat →
(d' ≤ Kd)%nat →
(⧆■ (heapN ⊥ N) ★ ⧆■(scheapN ⊥ N) ★ ⧆■(heapN ⊥ scheapN)
★ heap_ctx ★ scheap_ctx ★ ownT i chan_lang.Alloc K d)%I
⊢ WP alloc {{ v, ∃ (l: loc) c, ⧆(v = (#l, #l)%V)
★ prot_mapsto Θ (c, cleft) l p
★ prot_mapsto Θ (c, cright) l (dual p)
★ ownT i (chan_lang.Pair (chan_lang.Lit (chan_lang.LitLoc c cleft))
(chan_lang.Lit (chan_lang.LitLoc c cright))) K d' }}.
Proof.
iIntros (??) "(%&%&%&#Hctx&#Hsctx&Hown)".
rewrite /alloc.
wp_alloc l.
refine_delay (d -1)%nat.
wp_let. refine_alloc d' c.
wp_value. iExists l. iExists c.
iFrame "Hown". rewrite pure_equiv // -emp_True ?left_id.
assert (nclose N ⊆ ⊤) as Hdisj; eauto with ndisj.
iPoseProof (sts_alloc (prot_inv Θ c p (dual p)) ⊤ N (Session [] [] l l O O) Hdisj)
as "Hshift".
iCombine "~" "~1" as "Hpts". iCombine "Hpts" "Hctx" as "Hpts'".
iCombine "Hpts'" "Hsctx" as "Hpts'".
rewrite -assoc.
rewrite -assoc.
iPoseProof (fresh_inv Θ _ _ p with "Hpts'") as "Hinv".
rewrite -{2}(affine_affine (prot_inv _ _ _ _ _)).
rewrite {2}(later_intro (prot_inv _ _ _ _ _)).
iSpecialize ("Hshift" with "Hinv").
iPvs "Hshift".
iDestruct "Hshift" as (γ) "(?&?)" .
pose (s := {| left_state := []; right_state := [];
left_ptr := l; right_ptr := l;
left_count := 0; right_count := 0 |}).
fold s.
iPoseProof (sts_own_weaken ⊤ γ s (up_left [] l 0 ∩ up_right [] l 0)
(⊤ ∖ sts.tok s) (up_left_tok 0 ∪ up_right_tok 0)
with "~") as "Htoks".
× set_unfold. intros ? [(n&->&Hgt')|(n&->&Hgt')]; split; auto;
intros (n'&[(?&?)|(?&?)]); assert (n = n') by congruence; subst; omega.
× set_unfold; auto.
× apply sts.closed_op; eauto using up_left_closed, up_right_closed.
× rewrite sts_ownS_op; eauto using up_left_closed, up_right_closed.
iPvs "Htoks".
iDestruct "Htoks" as "(Hleft&Hright)".
iPvsIntro. iDestruct "Hshift" as "#Hstsctx".
iSplitL "Hleft".
** rewrite /prot_mapsto.
iExists p. iExists (dual p). iExists γ. iExists []. iExists 0%nat.
simpl. iFrame "Hleft". rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True right_id.
rewrite /prot_ctx.
iFrame "Hctx". iFrame "Hsctx". iFrame "Hstsctx".
repeat progress (rewrite pure_equiv // -emp_True ?left_id //).
** rewrite /prot_mapsto.
iExists p. iExists (dual p). iExists γ. iExists []. iExists 0%nat.
simpl. iFrame "Hright". rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True right_id.
rewrite /prot_ctx.
iFrame "Hctx". iFrame "Hsctx". iFrame "Hstsctx".
repeat progress (rewrite pure_equiv // -emp_True ?left_id //).
** set_solver.
Qed.
Global Instance into_pure_affine M P φ : @IntoPure M P φ → @IntoPure M (⧆ P) φ.
Proof. rewrite /IntoPure=>->. by rewrite affine_elim. Qed.
Global Instance frame_affine {M} R P Q :
@Frame M R P Q → @Frame M (⧆R) P Q.
Proof. by rewrite /Frame affine_elim=>->. Qed.
Lemma recv_spec Θ Φ Ψ (p: protocol) c s l i K d d':
(d > 1 ∧ d < Kd - 1)%nat →
(d' < Kd - 1)%nat →
(∀ vh vc, (Θ Φ vh vc) ⊢ ▷ Ψ vh vc) →
(prot_mapsto Θ (c, s) l (prot_recv Φ p)
★ ownT i (Recv (chan_lang.Lit (chan_lang.LitLoc c s))) K d)
⊢ WP recv #l {{ v, ∃ (l': loc) vh vc, ⧆(v = (#l', vh)%V) ★ prot_mapsto Θ (c, s) l' p
★ ⧆ Ψ vh vc
★ ownT i (chan_lang.Pair (chan_lang.Lit (chan_lang.LitLoc c s))
(chan_lang.of_val vc)) K d' }}.
Proof.
iIntros (?? Hpsi) "(Hpt&Hown)".
iDestruct "Hpt" as (pl pr γ choices n) "(Hctx&Hside)".
rewrite /fst /snd.
destruct s.
- iDestruct "Hctx" as "(%&%&%&Hnp)".
iDestruct "Hside" as "(Hside&%)".
iLob as "IH".
rewrite /prot_ctx.
apply affine_intro; first apply _.
iIntros "! Hnp Hside Hown".
iDestruct "Hnp" as "(#?&#?&#?)".
rewrite /recv.
wp_rec. refine_delay1.
wp_focus (! #l)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
rewrite {3}/prot_inv.
rewrite later_or affine_or.
iDestruct "Hside" as "[Hs|Hs]".
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt. iDestruct "Hll" as "(Hll&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (left_ptr s ↦ _)).
wp_load.
rewrite (affine_elim (c ↦c _)).
refine_recv_miss Kd.
iExists s. iExists (up_left_tok (left_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pl' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
iSplitR "Hown".
** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iLeft. iExists lv.
iExists (prot_recv Φ p). iExists pr'.
rewrite ?map_app.
simpl map. simpl left_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
iFrame "~5". iCombine "Hll" "Hptr" as "Hll".
rewrite (affine_elim (link_list' _ _ _)).
rewrite -link_list_end_pt. iFrame "Hll".
simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. auto.
** iIntros "Hs'".
wp_match.
refine_delay1.
iNext.
refine_delay d%nat.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_left (left_state s) (left_ptr s) (left_count s))
(up_left_tok (left_count s)) (up_left_tok (left_count s)))
as "Hweaken";
eauto using up_left_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
iSpecialize ("IH" with "Hown").
iClear "~1". iClear "Hnp". iClear "~". iClear "Hc1". iClear "Hc2".
done.
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
destruct lv as [| vh lv'].
** simpl link_list.
iDestruct "Hll" as "(Hptr&Heq)".
iTimeless "Hptr". iTimeless "Heq".
rewrite (affine_elim (left_ptr s = right_ptr s)).
iDestruct "Heq" as "%".
rewrite (affine_elim (left_ptr s ↦ _)).
rewrite prot_mod_prop_emp.
wp_load. rewrite (affine_elim (c ↦c ([], []))).
refine_recv_miss Kd.
iExists s. iExists (up_left_tok (left_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pl' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
assert (pl' ≡ dual pr') as Hequiv'.
{ inversion H8. subst; eauto. }
iSplitR "Hown".
*** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iLeft. iExists [].
iExists (prot_recv Φ p). iExists pr'.
rewrite ?map_app.
simpl map. simpl left_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
rewrite -prot_mod_prop_emp.
iFrame "~5".
simpl link_list. rewrite H6. iFrame "Hptr".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto. }
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto.
econstructor. rewrite -Hequiv. rewrite Hequiv'.
eapply dual_involutive. }
*** iIntros "Hs'".
wp_match.
refine_delay1. iNext. refine_delay d%nat.
rewrite affine_elim.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_left (left_state s) (left_ptr s) (left_count s))
(up_left_tok (left_count s)) (up_left_tok (left_count s)))
as "Hweaken";
eauto using up_left_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
iSpecialize ("IH" with "Hown").
done.
** simpl link_list. iDestruct "Hll" as (n) "(Hptr&Hll)".
iTimeless "Hptr".
rewrite (affine_elim (left_ptr s ↦ _)).
iTimeless "Hs". rewrite (affine_elim (⧆■_)).
iDestruct "Hs" as "%".
assert (pl' ≡ prot_recv Φ p) as Hequiv.
{ eapply prot_modc_inj; eauto. }
rewrite Hequiv.
wp_load. destruct vh as (vh&vc).
rewrite (affine_elim (c ↦c _)).
refine_recv Kd.
iExists (upd_left s choice_next n).
iExists (up_left_tok (S (left_count s))).
iSplitL "".
{ simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
destruct s; eapply left_step. }
iDestruct "~5" as "(Hphi&Hprotmod)".
iClear "IH".
iDestruct "~4" as "%".
iSplitR "Hown Hphi Hptr".
*** apply affine_intro; first apply _.
iNext. rewrite /prot_inv. iRight.
iExists lv'. iExists p. iExists pr'.
iClear "~1".
iFrame "~3". simpl.
iFrame "Hll". iFrame "~2".
iFrame "Hprotmod".
iSplitL "".
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
eapply prot_modc_app; eauto. rewrite Hequiv. econstructor.
econstructor; reflexivity.
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
inversion H7; eauto.
*** iIntros "Hs".
wp_match. refine_delay1.
rewrite Hpsi.
iNext. refine_delay d'.
wp_value. iExists n. iExists vh. iExists vc.
iFrame "Hphi". iFrame "Hown".
iSplitL "".
{ iPvsIntro. apply affine_intro; first apply _. auto. }
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (left_state s ++ [choice_next]).
iExists (S (left_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~". iFrame "Hnp".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iClear "Hptr".
iSplitL "Hs".
**** iPoseProof (sts_own_weaken with "Hs"); eauto using up_left_closed; set_unfold; auto.
**** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. rewrite Hequiv; econstructor.
econstructor; reflexivity.
- iDestruct "Hctx" as "(%&%&%&Hnp)".
iDestruct "Hside" as "(Hside&%)".
iLob as "IH".
rewrite /prot_ctx.
apply affine_intro; first apply _.
iIntros "! Hnp Hside Hown".
iDestruct "Hnp" as "(#?&#?&#?)".
rewrite /recv.
wp_rec. refine_delay1.
wp_focus (! #l)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
rewrite {3}/prot_inv.
rewrite later_or affine_or.
iDestruct "Hside" as "[Hs|Hs]".
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
destruct lv as [| vh lv'].
** simpl link_list.
iDestruct "Hll" as "(Hptr&Heq)".
iTimeless "Hptr". iTimeless "Heq".
rewrite (affine_elim (right_ptr s = left_ptr s)).
iDestruct "Heq" as "%".
rewrite (affine_elim (right_ptr s ↦ _)).
rewrite prot_mod_prop_emp.
wp_load.
rewrite (affine_elim (c ↦c _)).
refine_recv_miss Kd.
iExists s. iExists (up_right_tok (right_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pr' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
assert (pr' ≡ dual pl') as Hequiv'.
{ inversion H8. subst; eauto. }
iSplitR "Hown".
*** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iLeft. iExists [].
iExists pl'. iExists (prot_recv Φ p).
rewrite ?map_app.
simpl map. simpl right_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
rewrite -prot_mod_prop_emp.
iFrame "~5".
simpl link_list. rewrite H6. iFrame "Hptr".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto. }
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto.
econstructor. rewrite -Hequiv. rewrite Hequiv'.
reflexivity. }
*** iIntros "Hs'".
wp_match. refine_delay1.
iNext. refine_delay d.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_right (right_state s) (right_ptr s) (right_count s))
(up_right_tok (right_count s))
(up_right_tok (right_count s)))
as "Hweaken";
eauto using up_right_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
iApply "IH"; done.
** simpl link_list. iDestruct "Hll" as (n) "(Hptr&Hll)".
iTimeless "Hptr".
rewrite (affine_elim (right_ptr s ↦ _)).
iTimeless "~2". rewrite (affine_elim (⧆■_)).
iDestruct "~2" as "%".
assert (pr' ≡ prot_recv Φ p) as Hequiv.
{ eapply prot_modc_inj; eauto. }
rewrite Hequiv.
wp_load. destruct vh as (vh&vc). rewrite (affine_elim (c ↦c _)). refine_recv Kd.
iExists (upd_right s choice_next n).
iExists (up_right_tok (S (right_count s))).
iSplitL "".
{ simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
destruct s; eapply right_step. }
iDestruct "~5" as "(Hphi&Hprotmod)".
iClear "IH".
iDestruct "~4" as "%".
iSplitR "Hown Hphi Hptr".
*** apply affine_intro; first apply _.
iNext. rewrite /prot_inv. iLeft.
iExists lv'. iExists pl'. iExists p.
iClear "~1".
iFrame "~3". simpl.
iFrame "Hll". iFrame "Hs".
iFrame "Hprotmod".
iSplitL "".
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
eapply prot_modc_app; eauto. rewrite Hequiv. econstructor.
econstructor; reflexivity.
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
inversion H7; eauto.
*** iIntros "Hs".
wp_match. refine_delay1.
rewrite Hpsi. iNext. refine_delay d'.
wp_value. iExists n. iExists vh. iExists vc.
iFrame "Hphi". iFrame "Hown".
iSplitL "".
{ iPvsIntro. apply affine_intro; first apply _. auto. }
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (right_state s ++ [choice_next]).
iExists (S (right_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~". iFrame "Hnp".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iClear "Hptr".
iSplitL "Hs".
**** iPoseProof (sts_own_weaken with "Hs"); eauto using up_right_closed; set_unfold; auto.
**** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. rewrite Hequiv; econstructor.
econstructor; reflexivity.
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt. iDestruct "Hll" as "(Hll&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (right_ptr s ↦ _)).
wp_load.
rewrite (affine_elim (c ↦c _)).
refine_recv_miss Kd.
iExists s. iExists (up_right_tok (right_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pr' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
iSplitR "Hown".
** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iRight. iExists lv.
iExists pl'. iExists (prot_recv Φ p).
rewrite ?map_app.
simpl map. simpl right_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
iFrame "~5". iCombine "Hll" "Hptr" as "Hll". rewrite (affine_elim (link_list' _ _ _)). rewrite -link_list_end_pt. iFrame "Hll".
simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. auto.
** iIntros "Hs'".
wp_match. refine_delay1.
iNext. refine_delay d%nat.
rewrite affine_elim.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_right (right_state s) (right_ptr s) (right_count s))
(up_right_tok (right_count s))
(up_right_tok (right_count s)))
as "Hweaken";
eauto using up_right_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
by iApply "IH".
Qed.
Lemma send_spec Θ Φ ec vc eh vh (p: protocol) c s l i K d d':
(d ≥ 5 ∧ d ≤ Kd)%nat →
(d' < Kd)%nat →
chan_lang.to_val ec = Some vc →
to_val eh = Some vh →
(⧆Θ Φ vh vc ★ prot_mapsto Θ (c, s) l (prot_send Φ p)
★ ownT i (Send (chan_lang.Lit (chan_lang.LitLoc c s)) ec) K d)
⊢ WP send #l eh {{ v, ∃ (l': loc), ⧆(v = #l') ★ prot_mapsto Θ (c, s) l' p
★ ownT i (chan_lang.Lit (chan_lang.LitLoc c s)) K d' }}.
Proof.
iIntros (Hdgt ???) "(?&Hpt&Hown)".
iDestruct "Hpt" as (pl pr γ choices n) "(Hctx&Hside)".
rewrite /fst /snd.
destruct s.
- rewrite /send.
rewrite /prot_ctx. iDestruct "Hctx" as "(%&%&%&#?&#?&#?)".
assert (is_Some (to_val eh)) by eauto.
assert (Closed [] eh).
{ replace eh with (of_val vh) by eauto using of_to_val. solve_closed. }
wp_letp. refine_delay1.
simpl_subst.
wp_alloc lnew. refine_delay1.
wp_let. refine_delay 0%nat.
wp_focus (InjL _).
wp_value. iPvsIntro. wp_value. iPvsIntro.
iDestruct "Hside" as "(?&?)".
wp_focus (#l <- _)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
iPoseProof (prot_inv_left_orient with "[Hside ~5]") as "Hside".
{ iFrame "Hside". done. }
iDestruct "Hside" as "(Hs&~5)".
iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt.
iDestruct "Hll" as "(Hll'&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (left_ptr s ↦ _)).
subst. wp_store.
iDestruct "Hs" as "%".
iDestruct "~6" as "%".
rewrite (affine_elim (c ↦c _)).
refine_send Kd.
iExists (upd_left s choice_next lnew).
iExists (up_left_tok (S (left_count s))).
iSplitL "".
× rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite /upd_left. destruct s. eapply left_step.
× iDestruct "~8" as "%".
iDestruct "~5" as "%".
iSplitR "Hown".
** apply affine_intro; first apply _.
iNext.
rewrite /prot_inv.
iLeft. iExists (lv ++ [(vh, vc)]).
iExists (p). iExists pr'.
rewrite ?map_app.
simpl map. simpl left_ptr.
iFrame "~7".
iClear "~1". iClear "~2". iClear "~3".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eapply prot_modc_app; eauto; econstructor.
econstructor; reflexivity.
}
iSplitL "".
{ simpl. rewrite pure_equiv //= -emp_True //=. }
iSplitL "Hll' Hptr ~4".
{ rewrite -link_list_end_pt_join.
iFrame "Hll'". iFrame "Hptr". auto. }
assert (pl' ≡ prot_send Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
rewrite Hequiv in H10 *=>H10.
rewrite (unfold_prot (dual (prot_send Φ p))) in H10.
simpl in H10.
iSplitR "".
*** rewrite -prot_mod_prop_recv_snoc; eauto. iFrame "~"; auto.
*** simpl. iPureIntro.
eapply prot_mod_recv_snoc; eauto.
** iIntros "Hs'".
wp_seq. refine_delay d'.
wp_value. iExists lnew.
rewrite pure_equiv //= -emp_True left_id.
iFrame "Hown".
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (left_state s ++ [choice_next]).
iExists (S (left_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~2". iFrame "~3".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iSplitL "Hs'".
*** iPoseProof (sts_own_weaken with "Hs'"); eauto using up_left_closed; set_unfold; auto.
*** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. econstructor.
econstructor; reflexivity; reflexivity.
× eauto.
× eauto.
× eauto. solve_closed.
- rewrite /send.
rewrite /prot_ctx. iDestruct "Hctx" as "(%&%&%&#?&#?&#?)".
assert (is_Some (to_val eh)) by eauto.
assert (Closed [] eh).
{ replace eh with (of_val vh) by eauto using of_to_val. solve_closed. }
wp_letp. refine_delay1.
simpl_subst.
wp_alloc lnew. refine_delay1.
wp_let. refine_delay 0%nat.
wp_focus (InjL _).
wp_value. iPvsIntro. wp_value. iPvsIntro.
iDestruct "Hside" as "(?&?)".
wp_focus (#l <- _)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
iPoseProof (prot_inv_right_orient with "[Hside ~5]") as "Hside".
{ iFrame "Hside"; done. }
iDestruct "Hside" as "(Hs&~5)".
iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt.
iDestruct "Hll" as "(Hll'&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (right_ptr s ↦ _)).
subst. wp_store.
iDestruct "Hs" as "%".
iDestruct "~6" as "%".
rewrite (affine_elim (c ↦c _)).
refine_send Kd.
iExists (upd_right s choice_next lnew).
iExists (up_right_tok (S (right_count s))).
iSplitL "".
× rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite /upd_right. destruct s. eapply right_step.
× iDestruct "~8" as "%".
iDestruct "~5" as "%".
iSplitR "Hown".
** apply affine_intro; first apply _.
iNext.
rewrite /prot_inv.
iRight. iExists (lv ++ [(vh, vc)]).
iExists pl'. iExists p.
rewrite ?map_app.
simpl map. simpl right_ptr.
iFrame "~7".
iClear "~1". iClear "~2". iClear "~3".
iSplitL "".
{ simpl. rewrite pure_equiv //= -emp_True //=. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eapply prot_modc_app; eauto; econstructor.
econstructor; reflexivity.
}
iSplitL "Hll' Hptr ~4".
{ rewrite -link_list_end_pt_join.
iFrame "Hll'". iFrame "Hptr". auto. }
assert (pr' ≡ prot_send Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
rewrite Hequiv in H10 *=>H10.
rewrite (unfold_prot (dual (prot_send Φ p))) in H10.
simpl in H10.
iSplitR "".
*** rewrite -prot_mod_prop_recv_snoc; eauto. iFrame "~"; auto.
*** simpl. iPureIntro; eapply prot_mod_recv_snoc; eauto.
** iIntros "Hs'".
wp_seq. refine_delay d'.
wp_value. iExists lnew.
rewrite pure_equiv //= -emp_True left_id.
iFrame "Hown".
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (right_state s ++ [choice_next]).
iExists (S (right_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~2". iFrame "~3".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iSplitL "Hs'".
*** iPoseProof (sts_own_weaken with "Hs'"); eauto using up_right_closed; set_unfold; auto.
*** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. econstructor.
econstructor; reflexivity; reflexivity.
× eauto.
× eauto.
× eauto. solve_closed.
Qed.
End proof.
Instance inGF_protG `{H : inGFs lang.heap_lang Σ protGF} : protG Σ.
Proof. destruct H as (?&?&?). split; apply _. Qed.
Section proof.
Context `{!protG Σ}.
Context `{!refineG heap_lang Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{!scheapG heap_lang Σ}.
Context `{!heap.heapG Σ}.
Context (N : namespace).
Context (code: Type).
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation protocol := (protocol code).
Implicit Type Θ : leibnizC code -n> (leibnizC val -n> leibnizC (chan_lang.val) -n> iProp).
Import heap_lang.
Definition some (v: val) := InjLV v.
Definition none := InjRV (LitV LitUnit).
Fixpoint link_list (root: loc) (l: list val) (endpt: loc) : iProp :=
match l with
| [] ⇒ (root ↦ none ★ ⧆(root = endpt))%I
| v :: l' ⇒ (∃ (next: loc), root ↦ some (#next, v) ★ link_list next l' endpt)%I
end.
Fixpoint link_list' (root: loc) (l: list val) (endpt: loc) : iProp :=
match l with
| [] ⇒ (⧆(root = endpt))%I
| v :: l' ⇒ (∃ (next: loc), root ↦ some (#next, v) ★ link_list' next l' endpt)%I
end.
Fixpoint prot_mod_prop Θ (p: protocol) (l: list (val × chan_lang.val)) : iProp :=
match p, l with
| _, [] ⇒ Emp%I
| prot_recv Φ p', (v1, v2) :: l' ⇒
(⧆Θ Φ v1 v2 ★ prot_mod_prop Θ p' l')%I
| prot_ext pl pr, (v1, v2) :: l' ⇒
match v1, v2 with
| InjLV (#()), chan_lang.InjLV (chan_lang.LitV chan_lang.LitUnit) ⇒ prot_mod_prop Θ pl l'
| InjRV (#()), chan_lang.InjRV (chan_lang.LitV chan_lang.LitUnit) ⇒ prot_mod_prop Θ pr l'
| _, _ ⇒ False%I
end
| _, _ :: _ ⇒ False%I
end.
Instance prot_mod_prop_ne: Proper ((dist n) ==> (≡) ==> (=) ==> dist n) prot_mod_prop.
Proof.
intros n i1 i2 Hequivi p1 p2 Hequiv l ? <-.
revert i1 i2 Hequivi p1 p2 Hequiv.
induction l; intros.
- simpl. destruct p1, p2; auto.
- simpl. inversion Hequiv; subst; eauto;
destruct a. rewrite IHl; eauto.
destruct v; auto;
apply sep_ne; auto; rewrite (Hequivi Φ); auto; eauto.
destruct v; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
Qed.
Instance prot_mod_prop_proper: Proper ((≡) ==> (≡) ==> (=) ==> (≡)) prot_mod_prop.
Proof.
intros i1 i2 Hequivi p1 p2 Hequiv l ? <-.
revert i1 i2 Hequivi p1 p2 Hequiv.
induction l; intros.
- simpl. destruct p1, p2; auto.
- simpl. inversion Hequiv; subst; eauto;
destruct a. rewrite IHl; eauto.
destruct v; auto;
apply sep_proper; auto; rewrite (Hequivi Φ); auto; eauto.
destruct v; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
destruct v; auto.
destruct l0; auto.
destruct v0; auto.
destruct v0; auto.
destruct l0; auto.
Qed.
Global Instance affine_false {M: ucmraT}: (@AffineP M) False%I.
Proof. rewrite /AffineP. apply False_elim. Qed.
Instance prot_mod_prop_affine Θ p l: AffineP (prot_mod_prop Θ p l).
Proof.
revert p.
induction l.
- destruct p; try apply _.
- destruct p; rewrite //=; try apply _.
destruct a. apply _.
destruct a; destruct v; try apply _.
destruct v; try apply _.
destruct l0; try apply _.
destruct v0; try apply _.
destruct v0; try apply _.
destruct l0; try apply _.
destruct v; try apply _.
destruct l0; try apply _.
destruct v0; try apply _.
destruct v0; try apply _.
destruct l0; try apply _.
Qed.
Instance link_list_affine t1 l t2: AffineP (link_list t1 l t2).
Proof.
revert t1 t2.
induction l; rewrite //=; try apply _.
Qed.
Instance link_list'_affine t1 l t2: AffineP (link_list' t1 l t2).
Proof.
revert t1 t2.
induction l; rewrite //=; try apply _.
Qed.
Lemma link_list_end_pt root l ept:
link_list root l ept ⊣⊢ (link_list' root l ept ★ ept ↦ none)%I.
Proof.
apply (anti_symm (⊢)).
- revert root ept. induction l; intros root ept.
× simpl. iIntros "(Hpt&%)". subst.
iFrame "Hpt". apply affine_intro; first apply _.
auto.
× simpl. iIntros "Hll". iDestruct "Hll" as (next) "(Hpt&Hll)".
rewrite (IHl). iDestruct "Hll" as "(Hwand&Hept)". iFrame "Hept".
iExists next. by iFrame "Hpt".
- revert root ept. induction l; intros root ept.
× simpl. iIntros "(%&Hown)". subst. iFrame "Hown".
apply affine_intro; first apply _. auto.
× simpl. iIntros "(Hunroll&Hpt)".
iDestruct "Hunroll" as (n) "(?&Hll)". iCombine "Hll" "Hpt" as "Hll". rewrite IHl.
iExists n. by iFrame "Hll".
Qed.
Lemma link_list_end_pt_join root l ept (ept': loc) (v: val):
(link_list' root l ept ★ ept ↦ InjLV (#ept', v) ★ ept' ↦ none)%I
⊢ link_list root (l ++ [v]) ept'.
Proof.
revert root ept ept' v.
induction l.
- simpl. intros.
iIntros "(%&Hpt&Hpt')". subst. iExists ept'.
iFrame "Hpt". iFrame "Hpt'".
apply affine_intro; auto; apply _.
- simpl. intros.
iIntros "(Hun&Hpt&Hpt')". iDestruct "Hun" as (n) "(Hptn&Hll)".
iExists n. iFrame "Hptn". iCombine "Hll" "Hpt" as "Hll".
iCombine "Hll" "Hpt'" as "Hll". rewrite -assoc. rewrite IHl.
auto.
Qed.
Definition prot_inv Θ (c: chan_lang.loc) (pl pr: protocol) (s: session) : iProp :=
((∃ (l: list (heap_lang.val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c (map snd l, []) ★
link_list (right_ptr s) (map fst l) (left_ptr s) ★
prot_mod_prop Θ pr' l ★
⧆■(prot_mod pr' l (dual pl')))
∨
(∃ (l: list (val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c ([], map snd l) ★
link_list (left_ptr s) (map fst l) (right_ptr s) ★
prot_mod_prop Θ pl' l ★
⧆■(prot_mod pl' l (dual pr')))
)%I.
Instance prot_inv_ne n: Proper (dist n ==> (=) ==> (=) ==> (=) ==> (=) ==> dist n) prot_inv.
Proof.
intros t1 t2 Hdt ?? → ?? → ?? → ?? →.
rewrite /prot_inv.
apply or_ne;
repeat apply exist_ne=>?; repeat apply sep_ne; try eauto;
eapply prot_mod_prop_ne; eauto.
Qed.
Instance prot_inv_proper: Proper ((≡) ==> (=) ==> (=) ==> (≡) ==> (=) ==> (≡)) prot_inv.
Proof.
intros t1 t2 Hdt ?? → ?? → ?? ? ?? →.
rewrite /prot_inv.
apply or_proper;
repeat apply exist_proper=>?; repeat apply sep_proper; try eauto.
- setoid_subst. eauto.
- eapply prot_mod_prop_proper; eauto.
- setoid_subst. eauto.
- eapply prot_mod_prop_proper; eauto.
Qed.
Definition prot_ctx (γ : gname) Θ c pl pr : iProp :=
(⧆■ (heapN ⊥ N) ★ ⧆■(scheapN ⊥ N) ★ ⧆■(heapN ⊥ scheapN)
★ heap_ctx ★ scheap_ctx ★ sts_ctx γ N (prot_inv Θ c pl pr))%I.
Instance prot_ctx_ne n: Proper ((=) ==> dist n ==> (=) ==> (=) ==> (=) ==> dist n)
prot_ctx.
Proof.
intros ?? → t1 t2 Hdt ?? → ?? → ?? →.
rewrite /prot_ctx.
repeat apply sep_ne; try eauto.
eapply sts_ctx_ne; intros. intros ?.
eapply prot_inv_ne; eauto.
Qed.
Instance prot_ctx_proper: Proper ((=) ==> (≡) ==> (=) ==> (=) ==> (=) ==> (≡))
prot_ctx.
Proof.
intros ?? → t1 t2 Hdt ?? → ?? → ?? →.
rewrite /prot_ctx.
repeat apply sep_proper; try eauto.
eapply sts_ctx_proper; intros. intros ?.
eapply prot_inv_proper; eauto.
Qed.
Definition prot_mapsto Θ (c: loc × side) (l : loc) (p : protocol) : iProp :=
(∃ pl pr γ choices n, prot_ctx γ Θ (fst c) pl pr ★
match (snd c) with
| cleft ⇒ (sts_ownS γ (up_left choices l n) (up_left_tok n) ★
⧆■ (prot_modc pl choices p))
| cright ⇒ (sts_ownS γ (up_right choices l n) (up_right_tok n) ★
⧆■ (prot_modc pr choices p))
end)%I.
Instance prot_mapsto_affine: AffineP (prot_mapsto Θ c l p).
Proof.
intros. rewrite /prot_mapsto.
destruct c, s; simpl; apply _.
Qed.
Lemma prot_mapsto_ne n: Proper (dist n ==> (=) ==> (=) ==> (≡) ==> dist n) prot_mapsto.
Proof.
intros t1 t2 Hdt ?? → ?? → p1 p2 Hep.
rewrite /prot_mapsto.
repeat apply exist_ne=>?.
apply sep_ne.
- eapply prot_ctx_ne; eauto.
- destruct y, s; simpl; rewrite Hep; eauto.
Qed.
Lemma prot_mapsto_proper: Proper ((≡) ==> (=) ==> (=) ==> (≡) ==> (≡)) prot_mapsto.
Proof.
intros t1 t2 Hdt ?? → ?? → p1 p2 Hep.
rewrite /prot_mapsto.
repeat apply exist_proper=>?.
apply sep_proper.
- eapply prot_ctx_proper; eauto.
- destruct y, s; simpl; rewrite Hep; eauto.
Qed.
Lemma dual_involutive (p: protocol): p ≡ dual (dual p).
Proof.
revert p. cofix; intros p. rewrite (unfold_prot (dual _)).
destruct p; simpl; econstructor; try eapply dual_involutive.
Qed.
Lemma prot_inv_left_orient Θ p Φ c pl pr s:
(⧆▷ prot_inv Θ c pl pr s ★
⧆ ■ prot_modc pl (left_state s) (prot_send Φ p))
⊢ (⧆▷(∃ (l: list (val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c (map snd l, []) ★
link_list (right_ptr s) (map fst l) (left_ptr s) ★
prot_mod_prop Θ pr' l ★
⧆■(prot_mod pr' l (dual pl'))) ★ ⧆ ■ prot_modc pl (left_state s) (prot_send Φ p)).
Proof.
iIntros "(Hinv&%)".
rewrite pure_equiv //= -emp_True right_id.
rewrite /prot_inv. apply affine_intro; first apply _.
rewrite affine_elim. iNext.
iDestruct "Hinv" as "[Hl|Hr]"; auto.
iDestruct "Hr" as (l pl' pr') "(%&%&?&?&?&%)".
destruct l.
- iExists []. iExists pl'. iExists (pr').
iSplitL "". { apply affine_intro; first apply _; auto. }
iSplitL "". { apply affine_intro; first apply _; auto. }
iFrame "~1".
iSplitR ""; last first.
× iSplitL "".
** simpl. destruct pr'; auto.
** iPureIntro.
inversion H3. subst.
econstructor. rewrite H4. apply dual_involutive.
× simpl.
iDestruct "~" as "(Hpt&%)".
rewrite H4. iFrame "Hpt".
rewrite pure_equiv; first rewrite -emp_True //=; destruct pl'; auto.
- assert (pl' ≡ (prot_send Φ p)) as Hequiv.
{ eapply prot_modc_inj; eauto. }
exfalso. rewrite Hequiv in H3 ×. inversion 1.
Qed.
Lemma prot_inv_right_orient Θ p Φ c pl pr s:
(⧆▷ prot_inv Θ c pl pr s ★
⧆ ■ prot_modc pr (right_state s) (prot_send Φ p))
⊢ (⧆▷(∃ (l: list (val × chan_lang.val)) pl' pr',
⧆■(prot_modc pl (left_state s) pl') ★
⧆■(prot_modc pr (right_state s) pr') ★
c ↦c ([], map snd l) ★
link_list (left_ptr s) (map fst l) (right_ptr s) ★
prot_mod_prop Θ pl' l ★
⧆■(prot_mod pl' l (dual pr'))) ★ ⧆ ■ prot_modc pr (right_state s) (prot_send Φ p)).
Proof.
iIntros "(Hinv&%)".
rewrite pure_equiv //= -emp_True right_id.
rewrite /prot_inv. apply affine_intro; first apply _.
rewrite affine_elim. iNext.
iDestruct "Hinv" as "[Hl|Hr]"; auto.
iDestruct "Hl" as (l pl' pr') "(%&%&?&?&?&%)".
destruct l.
- iExists []. iExists pl'. iExists pr'.
iSplitL "". { apply affine_intro; first apply _; auto. }
iSplitL "". { apply affine_intro; first apply _; auto. }
iFrame "~1".
iSplitR ""; last first.
× iSplitL "".
** simpl. destruct pl'; auto.
** rewrite pure_equiv; first rewrite -emp_True //=.
inversion H3. subst.
econstructor. rewrite H4. apply dual_involutive.
× simpl.
iDestruct "~" as "(Hpt&%)".
rewrite H4. iFrame "Hpt".
rewrite pure_equiv; first rewrite -emp_True //=; destruct pr'; auto.
- assert (pr' ≡ (prot_send Φ p)) as Hequiv.
{ eapply prot_modc_inj; eauto. }
exfalso. rewrite Hequiv in H3 ×. inversion 1.
Qed.
Context (Hgt: 99 < Kd).
Global Instance protocol_inhabited: Inhabited protocol :=
populate (prot_end).
Lemma prot_mod_prop_recv_snoc Θ p l Φ p' vh vc:
prot_mod p l (prot_recv Φ p') →
(⧆ Θ Φ vh vc ★ prot_mod_prop Θ p l) ⊢ prot_mod_prop Θ p (l ++ [(vh, vc)]).
Proof.
remember (prot_recv Φ p') as p'' eqn:Hp''.
intros Hmod.
revert Φ Hp'' vh vc.
induction Hmod; intros; subst.
- inversion H0. simpl. destruct p; auto.
- simpl. destruct v as (vh'&vc').
rewrite -IHHmod; eauto.
iIntros "(H1&H2&H3)". iFrame "H1". iFrame "H2". auto.
- simpl. iIntros "(_&?)"; auto.
- simpl. iIntros "(_&?)"; auto.
Qed.
Lemma prot_mod_recv_snoc (p: protocol) l Φ p' vh vc:
prot_mod p l (prot_recv Φ p') →
prot_mod p (l ++ [(vh, vc)]) p'.
Proof.
remember (prot_recv Φ p') as p'' eqn:Hp''.
intros Hmod.
revert Φ Hp'' vh vc.
induction Hmod; intros; subst.
- simpl. inversion H0; subst. do 2 econstructor; eauto.
- simpl. econstructor; eauto.
- simpl. econstructor; eauto.
- simpl. econstructor; eauto.
Qed.
Lemma prot_mod_prop_emp Θ p: prot_mod_prop Θ p [] ⊣⊢ Emp.
Proof.
destruct p; auto.
Qed.
Lemma fresh_inv Θ (c: chan_lang.loc) l (p: protocol) :
(l ↦ InjRV #() ★ c ↦c ([], []) ★ heap_ctx ★ scheap_ctx)
⊢ prot_inv Θ c p (dual p) {| left_state := []; right_state := [];
left_ptr := l; right_ptr := l;
left_count := 0; right_count := 0|}.
Proof.
rewrite /prot_inv.
iIntros "(Hptr&Hch&#?&#?)".
iLeft. iExists []. iExists p. iExists (dual p). simpl.
rewrite pure_equiv; last (econstructor; reflexivity).
rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True ?left_id.
iFrame "Hch". iFrame "Hptr".
rewrite pure_equiv // -emp_True ?left_id.
rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True ?right_id.
iClear "~". iClear "~1". destruct p; eauto.
Qed.
Lemma alloc_spec Θ (p: protocol) i K d d':
(d > 1 ∧ d ≤ Kd)%nat →
(d' ≤ Kd)%nat →
(⧆■ (heapN ⊥ N) ★ ⧆■(scheapN ⊥ N) ★ ⧆■(heapN ⊥ scheapN)
★ heap_ctx ★ scheap_ctx ★ ownT i chan_lang.Alloc K d)%I
⊢ WP alloc {{ v, ∃ (l: loc) c, ⧆(v = (#l, #l)%V)
★ prot_mapsto Θ (c, cleft) l p
★ prot_mapsto Θ (c, cright) l (dual p)
★ ownT i (chan_lang.Pair (chan_lang.Lit (chan_lang.LitLoc c cleft))
(chan_lang.Lit (chan_lang.LitLoc c cright))) K d' }}.
Proof.
iIntros (??) "(%&%&%&#Hctx&#Hsctx&Hown)".
rewrite /alloc.
wp_alloc l.
refine_delay (d -1)%nat.
wp_let. refine_alloc d' c.
wp_value. iExists l. iExists c.
iFrame "Hown". rewrite pure_equiv // -emp_True ?left_id.
assert (nclose N ⊆ ⊤) as Hdisj; eauto with ndisj.
iPoseProof (sts_alloc (prot_inv Θ c p (dual p)) ⊤ N (Session [] [] l l O O) Hdisj)
as "Hshift".
iCombine "~" "~1" as "Hpts". iCombine "Hpts" "Hctx" as "Hpts'".
iCombine "Hpts'" "Hsctx" as "Hpts'".
rewrite -assoc.
rewrite -assoc.
iPoseProof (fresh_inv Θ _ _ p with "Hpts'") as "Hinv".
rewrite -{2}(affine_affine (prot_inv _ _ _ _ _)).
rewrite {2}(later_intro (prot_inv _ _ _ _ _)).
iSpecialize ("Hshift" with "Hinv").
iPvs "Hshift".
iDestruct "Hshift" as (γ) "(?&?)" .
pose (s := {| left_state := []; right_state := [];
left_ptr := l; right_ptr := l;
left_count := 0; right_count := 0 |}).
fold s.
iPoseProof (sts_own_weaken ⊤ γ s (up_left [] l 0 ∩ up_right [] l 0)
(⊤ ∖ sts.tok s) (up_left_tok 0 ∪ up_right_tok 0)
with "~") as "Htoks".
× set_unfold. intros ? [(n&->&Hgt')|(n&->&Hgt')]; split; auto;
intros (n'&[(?&?)|(?&?)]); assert (n = n') by congruence; subst; omega.
× set_unfold; auto.
× apply sts.closed_op; eauto using up_left_closed, up_right_closed.
× rewrite sts_ownS_op; eauto using up_left_closed, up_right_closed.
iPvs "Htoks".
iDestruct "Htoks" as "(Hleft&Hright)".
iPvsIntro. iDestruct "Hshift" as "#Hstsctx".
iSplitL "Hleft".
** rewrite /prot_mapsto.
iExists p. iExists (dual p). iExists γ. iExists []. iExists 0%nat.
simpl. iFrame "Hleft". rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True right_id.
rewrite /prot_ctx.
iFrame "Hctx". iFrame "Hsctx". iFrame "Hstsctx".
repeat progress (rewrite pure_equiv // -emp_True ?left_id //).
** rewrite /prot_mapsto.
iExists p. iExists (dual p). iExists γ. iExists []. iExists 0%nat.
simpl. iFrame "Hright". rewrite pure_equiv; last (econstructor; reflexivity).
rewrite -emp_True right_id.
rewrite /prot_ctx.
iFrame "Hctx". iFrame "Hsctx". iFrame "Hstsctx".
repeat progress (rewrite pure_equiv // -emp_True ?left_id //).
** set_solver.
Qed.
Global Instance into_pure_affine M P φ : @IntoPure M P φ → @IntoPure M (⧆ P) φ.
Proof. rewrite /IntoPure=>->. by rewrite affine_elim. Qed.
Global Instance frame_affine {M} R P Q :
@Frame M R P Q → @Frame M (⧆R) P Q.
Proof. by rewrite /Frame affine_elim=>->. Qed.
Lemma recv_spec Θ Φ Ψ (p: protocol) c s l i K d d':
(d > 1 ∧ d < Kd - 1)%nat →
(d' < Kd - 1)%nat →
(∀ vh vc, (Θ Φ vh vc) ⊢ ▷ Ψ vh vc) →
(prot_mapsto Θ (c, s) l (prot_recv Φ p)
★ ownT i (Recv (chan_lang.Lit (chan_lang.LitLoc c s))) K d)
⊢ WP recv #l {{ v, ∃ (l': loc) vh vc, ⧆(v = (#l', vh)%V) ★ prot_mapsto Θ (c, s) l' p
★ ⧆ Ψ vh vc
★ ownT i (chan_lang.Pair (chan_lang.Lit (chan_lang.LitLoc c s))
(chan_lang.of_val vc)) K d' }}.
Proof.
iIntros (?? Hpsi) "(Hpt&Hown)".
iDestruct "Hpt" as (pl pr γ choices n) "(Hctx&Hside)".
rewrite /fst /snd.
destruct s.
- iDestruct "Hctx" as "(%&%&%&Hnp)".
iDestruct "Hside" as "(Hside&%)".
iLob as "IH".
rewrite /prot_ctx.
apply affine_intro; first apply _.
iIntros "! Hnp Hside Hown".
iDestruct "Hnp" as "(#?&#?&#?)".
rewrite /recv.
wp_rec. refine_delay1.
wp_focus (! #l)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
rewrite {3}/prot_inv.
rewrite later_or affine_or.
iDestruct "Hside" as "[Hs|Hs]".
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt. iDestruct "Hll" as "(Hll&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (left_ptr s ↦ _)).
wp_load.
rewrite (affine_elim (c ↦c _)).
refine_recv_miss Kd.
iExists s. iExists (up_left_tok (left_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pl' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
iSplitR "Hown".
** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iLeft. iExists lv.
iExists (prot_recv Φ p). iExists pr'.
rewrite ?map_app.
simpl map. simpl left_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
iFrame "~5". iCombine "Hll" "Hptr" as "Hll".
rewrite (affine_elim (link_list' _ _ _)).
rewrite -link_list_end_pt. iFrame "Hll".
simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. auto.
** iIntros "Hs'".
wp_match.
refine_delay1.
iNext.
refine_delay d%nat.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_left (left_state s) (left_ptr s) (left_count s))
(up_left_tok (left_count s)) (up_left_tok (left_count s)))
as "Hweaken";
eauto using up_left_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
iSpecialize ("IH" with "Hown").
iClear "~1". iClear "Hnp". iClear "~". iClear "Hc1". iClear "Hc2".
done.
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
destruct lv as [| vh lv'].
** simpl link_list.
iDestruct "Hll" as "(Hptr&Heq)".
iTimeless "Hptr". iTimeless "Heq".
rewrite (affine_elim (left_ptr s = right_ptr s)).
iDestruct "Heq" as "%".
rewrite (affine_elim (left_ptr s ↦ _)).
rewrite prot_mod_prop_emp.
wp_load. rewrite (affine_elim (c ↦c ([], []))).
refine_recv_miss Kd.
iExists s. iExists (up_left_tok (left_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pl' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
assert (pl' ≡ dual pr') as Hequiv'.
{ inversion H8. subst; eauto. }
iSplitR "Hown".
*** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iLeft. iExists [].
iExists (prot_recv Φ p). iExists pr'.
rewrite ?map_app.
simpl map. simpl left_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
rewrite -prot_mod_prop_emp.
iFrame "~5".
simpl link_list. rewrite H6. iFrame "Hptr".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto. }
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto.
econstructor. rewrite -Hequiv. rewrite Hequiv'.
eapply dual_involutive. }
*** iIntros "Hs'".
wp_match.
refine_delay1. iNext. refine_delay d%nat.
rewrite affine_elim.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_left (left_state s) (left_ptr s) (left_count s))
(up_left_tok (left_count s)) (up_left_tok (left_count s)))
as "Hweaken";
eauto using up_left_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
iSpecialize ("IH" with "Hown").
done.
** simpl link_list. iDestruct "Hll" as (n) "(Hptr&Hll)".
iTimeless "Hptr".
rewrite (affine_elim (left_ptr s ↦ _)).
iTimeless "Hs". rewrite (affine_elim (⧆■_)).
iDestruct "Hs" as "%".
assert (pl' ≡ prot_recv Φ p) as Hequiv.
{ eapply prot_modc_inj; eauto. }
rewrite Hequiv.
wp_load. destruct vh as (vh&vc).
rewrite (affine_elim (c ↦c _)).
refine_recv Kd.
iExists (upd_left s choice_next n).
iExists (up_left_tok (S (left_count s))).
iSplitL "".
{ simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
destruct s; eapply left_step. }
iDestruct "~5" as "(Hphi&Hprotmod)".
iClear "IH".
iDestruct "~4" as "%".
iSplitR "Hown Hphi Hptr".
*** apply affine_intro; first apply _.
iNext. rewrite /prot_inv. iRight.
iExists lv'. iExists p. iExists pr'.
iClear "~1".
iFrame "~3". simpl.
iFrame "Hll". iFrame "~2".
iFrame "Hprotmod".
iSplitL "".
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
eapply prot_modc_app; eauto. rewrite Hequiv. econstructor.
econstructor; reflexivity.
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
inversion H7; eauto.
*** iIntros "Hs".
wp_match. refine_delay1.
rewrite Hpsi.
iNext. refine_delay d'.
wp_value. iExists n. iExists vh. iExists vc.
iFrame "Hphi". iFrame "Hown".
iSplitL "".
{ iPvsIntro. apply affine_intro; first apply _. auto. }
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (left_state s ++ [choice_next]).
iExists (S (left_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~". iFrame "Hnp".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iClear "Hptr".
iSplitL "Hs".
**** iPoseProof (sts_own_weaken with "Hs"); eauto using up_left_closed; set_unfold; auto.
**** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. rewrite Hequiv; econstructor.
econstructor; reflexivity.
- iDestruct "Hctx" as "(%&%&%&Hnp)".
iDestruct "Hside" as "(Hside&%)".
iLob as "IH".
rewrite /prot_ctx.
apply affine_intro; first apply _.
iIntros "! Hnp Hside Hown".
iDestruct "Hnp" as "(#?&#?&#?)".
rewrite /recv.
wp_rec. refine_delay1.
wp_focus (! #l)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
rewrite {3}/prot_inv.
rewrite later_or affine_or.
iDestruct "Hside" as "[Hs|Hs]".
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
destruct lv as [| vh lv'].
** simpl link_list.
iDestruct "Hll" as "(Hptr&Heq)".
iTimeless "Hptr". iTimeless "Heq".
rewrite (affine_elim (right_ptr s = left_ptr s)).
iDestruct "Heq" as "%".
rewrite (affine_elim (right_ptr s ↦ _)).
rewrite prot_mod_prop_emp.
wp_load.
rewrite (affine_elim (c ↦c _)).
refine_recv_miss Kd.
iExists s. iExists (up_right_tok (right_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pr' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
assert (pr' ≡ dual pl') as Hequiv'.
{ inversion H8. subst; eauto. }
iSplitR "Hown".
*** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iLeft. iExists [].
iExists pl'. iExists (prot_recv Φ p).
rewrite ?map_app.
simpl map. simpl right_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
rewrite -prot_mod_prop_emp.
iFrame "~5".
simpl link_list. rewrite H6. iFrame "Hptr".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto. }
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=); auto.
econstructor. rewrite -Hequiv. rewrite Hequiv'.
reflexivity. }
*** iIntros "Hs'".
wp_match. refine_delay1.
iNext. refine_delay d.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_right (right_state s) (right_ptr s) (right_count s))
(up_right_tok (right_count s))
(up_right_tok (right_count s)))
as "Hweaken";
eauto using up_right_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
iApply "IH"; done.
** simpl link_list. iDestruct "Hll" as (n) "(Hptr&Hll)".
iTimeless "Hptr".
rewrite (affine_elim (right_ptr s ↦ _)).
iTimeless "~2". rewrite (affine_elim (⧆■_)).
iDestruct "~2" as "%".
assert (pr' ≡ prot_recv Φ p) as Hequiv.
{ eapply prot_modc_inj; eauto. }
rewrite Hequiv.
wp_load. destruct vh as (vh&vc). rewrite (affine_elim (c ↦c _)). refine_recv Kd.
iExists (upd_right s choice_next n).
iExists (up_right_tok (S (right_count s))).
iSplitL "".
{ simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
destruct s; eapply right_step. }
iDestruct "~5" as "(Hphi&Hprotmod)".
iClear "IH".
iDestruct "~4" as "%".
iSplitR "Hown Hphi Hptr".
*** apply affine_intro; first apply _.
iNext. rewrite /prot_inv. iLeft.
iExists lv'. iExists pl'. iExists p.
iClear "~1".
iFrame "~3". simpl.
iFrame "Hll". iFrame "Hs".
iFrame "Hprotmod".
iSplitL "".
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
eapply prot_modc_app; eauto. rewrite Hequiv. econstructor.
econstructor; reflexivity.
**** simpl. rewrite pure_equiv; first (apply affine_intro; auto; apply _).
inversion H7; eauto.
*** iIntros "Hs".
wp_match. refine_delay1.
rewrite Hpsi. iNext. refine_delay d'.
wp_value. iExists n. iExists vh. iExists vc.
iFrame "Hphi". iFrame "Hown".
iSplitL "".
{ iPvsIntro. apply affine_intro; first apply _. auto. }
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (right_state s ++ [choice_next]).
iExists (S (right_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~". iFrame "Hnp".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iClear "Hptr".
iSplitL "Hs".
**** iPoseProof (sts_own_weaken with "Hs"); eauto using up_right_closed; set_unfold; auto.
**** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. rewrite Hequiv; econstructor.
econstructor; reflexivity.
× iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt. iDestruct "Hll" as "(Hll&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (right_ptr s ↦ _)).
wp_load.
rewrite (affine_elim (c ↦c _)).
refine_recv_miss Kd.
iExists s. iExists (up_right_tok (right_count s)).
iSplitL "".
{ iClear "IH".
rewrite pure_equiv; first (apply affine_intro; first apply _; auto).
econstructor. }
iDestruct "~2" as "%".
iDestruct "~4" as "%".
iDestruct "Hs" as "%".
assert (pr' ≡ prot_recv Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
iSplitR "Hown".
** iClear "IH".
apply affine_intro; first apply _.
iNext. rewrite /prot_inv.
iRight. iExists lv.
iExists pl'. iExists (prot_recv Φ p).
rewrite ?map_app.
simpl map. simpl right_ptr.
iFrame "~3". iClear "~1". iClear "Hnp". iClear "~".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eauto. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. eauto. }
iFrame "~5". iCombine "Hll" "Hptr" as "Hll". rewrite (affine_elim (link_list' _ _ _)). rewrite -link_list_end_pt. iFrame "Hll".
simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite -Hequiv. auto.
** iIntros "Hs'".
wp_match. refine_delay1.
iNext. refine_delay d%nat.
rewrite affine_elim.
iCombine "Hnp" "~" as "Hc1".
iCombine "Hc1" "~1" as "Hc2".
rewrite assoc.
iSpecialize ("IH" with "Hc2").
iPoseProof (sts_own_weaken ⊤ γ s
(up_right (right_state s) (right_ptr s) (right_count s))
(up_right_tok (right_count s))
(up_right_tok (right_count s)))
as "Hweaken";
eauto using up_right_closed.
{ set_unfold. auto. }
iSpecialize ("Hweaken" with "Hs'").
iPvs "Hweaken".
iSpecialize ("IH" with "Hweaken").
by iApply "IH".
Qed.
Lemma send_spec Θ Φ ec vc eh vh (p: protocol) c s l i K d d':
(d ≥ 5 ∧ d ≤ Kd)%nat →
(d' < Kd)%nat →
chan_lang.to_val ec = Some vc →
to_val eh = Some vh →
(⧆Θ Φ vh vc ★ prot_mapsto Θ (c, s) l (prot_send Φ p)
★ ownT i (Send (chan_lang.Lit (chan_lang.LitLoc c s)) ec) K d)
⊢ WP send #l eh {{ v, ∃ (l': loc), ⧆(v = #l') ★ prot_mapsto Θ (c, s) l' p
★ ownT i (chan_lang.Lit (chan_lang.LitLoc c s)) K d' }}.
Proof.
iIntros (Hdgt ???) "(?&Hpt&Hown)".
iDestruct "Hpt" as (pl pr γ choices n) "(Hctx&Hside)".
rewrite /fst /snd.
destruct s.
- rewrite /send.
rewrite /prot_ctx. iDestruct "Hctx" as "(%&%&%&#?&#?&#?)".
assert (is_Some (to_val eh)) by eauto.
assert (Closed [] eh).
{ replace eh with (of_val vh) by eauto using of_to_val. solve_closed. }
wp_letp. refine_delay1.
simpl_subst.
wp_alloc lnew. refine_delay1.
wp_let. refine_delay 0%nat.
wp_focus (InjL _).
wp_value. iPvsIntro. wp_value. iPvsIntro.
iDestruct "Hside" as "(?&?)".
wp_focus (#l <- _)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
iPoseProof (prot_inv_left_orient with "[Hside ~5]") as "Hside".
{ iFrame "Hside". done. }
iDestruct "Hside" as "(Hs&~5)".
iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt.
iDestruct "Hll" as "(Hll'&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (left_ptr s ↦ _)).
subst. wp_store.
iDestruct "Hs" as "%".
iDestruct "~6" as "%".
rewrite (affine_elim (c ↦c _)).
refine_send Kd.
iExists (upd_left s choice_next lnew).
iExists (up_left_tok (S (left_count s))).
iSplitL "".
× rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite /upd_left. destruct s. eapply left_step.
× iDestruct "~8" as "%".
iDestruct "~5" as "%".
iSplitR "Hown".
** apply affine_intro; first apply _.
iNext.
rewrite /prot_inv.
iLeft. iExists (lv ++ [(vh, vc)]).
iExists (p). iExists pr'.
rewrite ?map_app.
simpl map. simpl left_ptr.
iFrame "~7".
iClear "~1". iClear "~2". iClear "~3".
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eapply prot_modc_app; eauto; econstructor.
econstructor; reflexivity.
}
iSplitL "".
{ simpl. rewrite pure_equiv //= -emp_True //=. }
iSplitL "Hll' Hptr ~4".
{ rewrite -link_list_end_pt_join.
iFrame "Hll'". iFrame "Hptr". auto. }
assert (pl' ≡ prot_send Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
rewrite Hequiv in H10 *=>H10.
rewrite (unfold_prot (dual (prot_send Φ p))) in H10.
simpl in H10.
iSplitR "".
*** rewrite -prot_mod_prop_recv_snoc; eauto. iFrame "~"; auto.
*** simpl. iPureIntro.
eapply prot_mod_recv_snoc; eauto.
** iIntros "Hs'".
wp_seq. refine_delay d'.
wp_value. iExists lnew.
rewrite pure_equiv //= -emp_True left_id.
iFrame "Hown".
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (left_state s ++ [choice_next]).
iExists (S (left_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~2". iFrame "~3".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iSplitL "Hs'".
*** iPoseProof (sts_own_weaken with "Hs'"); eauto using up_left_closed; set_unfold; auto.
*** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. econstructor.
econstructor; reflexivity; reflexivity.
× eauto.
× eauto.
× eauto. solve_closed.
- rewrite /send.
rewrite /prot_ctx. iDestruct "Hctx" as "(%&%&%&#?&#?&#?)".
assert (is_Some (to_val eh)) by eauto.
assert (Closed [] eh).
{ replace eh with (of_val vh) by eauto using of_to_val. solve_closed. }
wp_letp. refine_delay1.
simpl_subst.
wp_alloc lnew. refine_delay1.
wp_let. refine_delay 0%nat.
wp_focus (InjL _).
wp_value. iPvsIntro. wp_value. iPvsIntro.
iDestruct "Hside" as "(?&?)".
wp_focus (#l <- _)%E.
iSts γ as s Hin;
first (rewrite /= ?to_of_val; try fast_done).
destruct Hin as (?&?&?).
subst.
iPoseProof (prot_inv_right_orient with "[Hside ~5]") as "Hside".
{ iFrame "Hside"; done. }
iDestruct "Hside" as "(Hs&~5)".
iDestruct "Hs" as (lv pl' pr') "(?&?&?&Hll&?&?)".
rewrite link_list_end_pt.
iDestruct "Hll" as "(Hll'&Hptr)".
iTimeless "Hptr".
rewrite (affine_elim (right_ptr s ↦ _)).
subst. wp_store.
iDestruct "Hs" as "%".
iDestruct "~6" as "%".
rewrite (affine_elim (c ↦c _)).
refine_send Kd.
iExists (upd_right s choice_next lnew).
iExists (up_right_tok (S (right_count s))).
iSplitL "".
× rewrite pure_equiv; first (rewrite -emp_True //=).
rewrite /upd_right. destruct s. eapply right_step.
× iDestruct "~8" as "%".
iDestruct "~5" as "%".
iSplitR "Hown".
** apply affine_intro; first apply _.
iNext.
rewrite /prot_inv.
iRight. iExists (lv ++ [(vh, vc)]).
iExists pl'. iExists p.
rewrite ?map_app.
simpl map. simpl right_ptr.
iFrame "~7".
iClear "~1". iClear "~2". iClear "~3".
iSplitL "".
{ simpl. rewrite pure_equiv //= -emp_True //=. }
iSplitL "".
{ simpl. rewrite pure_equiv; first (rewrite -emp_True //=).
eapply prot_modc_app; eauto; econstructor.
econstructor; reflexivity.
}
iSplitL "Hll' Hptr ~4".
{ rewrite -link_list_end_pt_join.
iFrame "Hll'". iFrame "Hptr". auto. }
assert (pr' ≡ prot_send Φ p) as Hequiv by (eapply prot_modc_inj; eauto).
rewrite Hequiv in H10 *=>H10.
rewrite (unfold_prot (dual (prot_send Φ p))) in H10.
simpl in H10.
iSplitR "".
*** rewrite -prot_mod_prop_recv_snoc; eauto. iFrame "~"; auto.
*** simpl. iPureIntro; eapply prot_mod_recv_snoc; eauto.
** iIntros "Hs'".
wp_seq. refine_delay d'.
wp_value. iExists lnew.
rewrite pure_equiv //= -emp_True left_id.
iFrame "Hown".
rewrite /prot_mapsto.
simpl. iExists pl. iExists pr.
iExists γ. iExists (right_state s ++ [choice_next]).
iExists (S (right_count s)).
rewrite /prot_ctx.
iFrame "~1". iFrame "~2". iFrame "~3".
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
rewrite pure_equiv //= -emp_True left_id.
iSplitL "Hs'".
*** iPoseProof (sts_own_weaken with "Hs'"); eauto using up_right_closed; set_unfold; auto.
*** iPvsIntro. rewrite pure_equiv; first rewrite -emp_True //=.
eapply prot_modc_app; eauto. econstructor.
econstructor; reflexivity; reflexivity.
× eauto.
× eauto.
× eauto. solve_closed.
Qed.
End proof.