proof.v 8.35 KB
Newer Older
1 2 3
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang.lib.barrier Require Export barrier.
Ralf Jung's avatar
Ralf Jung committed
4
From stdpp Require Import functions.
5
From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From iris.heap_lang Require Import proofmode.
Ralf Jung's avatar
Ralf Jung committed
7
From iris.heap_lang.lib.barrier Require Import protocol.
8
Set Default Proof Using "Type".
9

10
(** The CMRAs/functors we need. *)
11
Class barrierG Σ := BarrierG {
12 13
  barrier_stsG :> stsG Σ sts;
  barrier_savedPropG :> savedPropG Σ idCF;
14
}.
15
Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
16

17
Instance subG_barrierΣ {Σ} : subG barrierΣ Σ  barrierG Σ.
18
Proof. solve_inG. Qed.
19 20 21

(** Now we come to the Iris part of the proof. *)
Section proof.
22
Context `{!heapG Σ, !barrierG Σ} (N : namespace).
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Implicit Types I : gset gname.
24

25 26
Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
  ( Ψ : gname  iProp Σ,
27
     (P - [ set] i  I, Ψ i)  [ set] i  I, saved_prop_own i (Ψ i))%I.
28 29

Coercion state_to_val (s : state) : val :=
30
  match s with State Low _ => #false | State High _ => #true end.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Arguments state_to_val !_ / : simpl nomatch.
32

33
Definition state_to_prop (s : state) (P : iProp Σ) : iProp Σ :=
34
  match s with State Low _ => P | State High _ => True%I end.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Arguments state_to_prop !_ _ / : simpl nomatch.
36

37
Definition barrier_inv (l : loc) (P : iProp Σ) (s : state) : iProp Σ :=
38
  (l  s  ress (state_to_prop s P) (state_I s))%I.
39

40
Definition barrier_ctx (γ : gname) (l : loc) (P : iProp Σ) : iProp Σ :=
41
  sts_ctx γ N (barrier_inv l P).
42

43
Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
44
  ( γ, barrier_ctx γ l P  sts_ownS γ low_states {[ Send ]})%I.
45

46
Definition recv (l : loc) (R : iProp Σ) : iProp Σ :=
47
  ( γ P Q i,
48 49
    barrier_ctx γ l P  sts_ownS γ (i_states i) {[ Change i ]} 
    saved_prop_own i Q   (Q - R))%I.
50

51
Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) :
52
  PersistentP (barrier_ctx γ l P).
53 54
Proof. apply _. Qed.

55
(** Setoids *)
56 57
Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
Proof. solve_proper. Qed.
58 59
Global Instance state_to_prop_ne s :
  NonExpansive (state_to_prop s).
60
Proof. solve_proper. Qed.
61
Global Instance barrier_inv_ne n l :
62 63
  Proper (dist n ==> eq ==> dist n) (barrier_inv l).
Proof. solve_proper. Qed.
64
Global Instance barrier_ctx_ne γ l : NonExpansive (barrier_ctx γ l).
65
Proof. solve_proper. Qed. 
66
Global Instance send_ne l : NonExpansive (send l).
67
Proof. solve_proper. Qed.
68
Global Instance recv_ne l : NonExpansive (recv l).
69
Proof. solve_proper. Qed.
70 71

(** Helper lemmas *)
72
Lemma ress_split i i1 i2 Q R1 R2 P I :
73
  i  I  i1  I  i2  I  i1  i2 
74 75 76
  saved_prop_own i Q - saved_prop_own i1 R1 - saved_prop_own i2 R2 -
  (Q - R1  R2) - ress P I -
  ress P ({[i1;i2]}  I  {[i]}).
77
Proof.
78
  iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
79
  iDestruct (big_opS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
81
  - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
82
    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
83
    iDestruct (big_opS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
84
    iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
85
    rewrite -assoc_L !big_opS_fn_insert'; [|abstract set_solver ..].
86
    by iFrame.
87
  - rewrite -assoc_L !big_opS_fn_insert; [|abstract set_solver ..]. eauto.
88
Qed.
89 90

(** Actual proofs *)
91
Lemma newbarrier_spec (P : iProp Σ) :
92
  {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P  send l P }}}.
93
Proof.
94
  iIntros (Φ) "HΦ".
95
  rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
96
  iApply ("HΦ" with "[> -]").
97 98
  iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
  iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
99
    as (γ') "[#? Hγ']"; eauto.
100
  { iNext. rewrite /barrier_inv /=. iFrame.
101
    iExists (const P). rewrite !big_opS_singleton /=. eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  iAssert (barrier_ctx γ' l P)%I as "#?".
Ralf Jung's avatar
Ralf Jung committed
103
  { done. }
104
  iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
105
     sts_ownS γ' low_states {[Send]})%I with "[> -]" as "[Hr Hs]".
Robbert Krebbers's avatar
Robbert Krebbers committed
106
  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
107 108
    - set_solver.
    - iApply (sts_own_weaken with "Hγ'");
Robbert Krebbers's avatar
Robbert Krebbers committed
109
        auto using sts.closed_op, i_states_closed, low_states_closed;
110
        abstract set_solver. }
Ralf Jung's avatar
Ralf Jung committed
111
  iModIntro. iSplitL "Hr".
112
  - iExists γ', P, P, γ. iFrame. auto.
Ralf Jung's avatar
Ralf Jung committed
113
  - rewrite /send. auto.
114 115
Qed.

116
Lemma signal_spec l P :
117
  {{{ send l P  P }}} signal #l {{{ RET #(); True }}}.
118
Proof.
Ralf Jung's avatar
Ralf Jung committed
119
  rewrite /signal /=.
120
  iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_let.
121
  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
122
    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
123 124
  destruct p; [|done]. wp_store.
  iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
125
  iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
  iSplit; [iPureIntro; by eauto using signal_step|].
Ralf Jung's avatar
Ralf Jung committed
127
  rewrite /barrier_inv /ress /=. iNext. iFrame "Hl".
128
  iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
129
  iNext. iIntros "_"; by iApply "Hr".
130 131
Qed.

132
Lemma wait_spec l P:
133
  {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
134
Proof.
Ralf Jung's avatar
Ralf Jung committed
135
  rename P into R.
136
  iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
137
  iLöb as "IH". wp_rec. wp_bind (! _)%E.
138
  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
139 140
    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
  wp_load. destruct p.
141
  - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
Ralf Jung's avatar
Ralf Jung committed
142
    { iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
143
    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[> Hγ]" as "Hγ".
144
    { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
145
    iModIntro. wp_if.
Ralf Jung's avatar
Ralf Jung committed
146
    iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148
  - (* a High state: the comparison succeeds, and we perform a transition and
    return to the client *)
149
    iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
150
    iDestruct (big_opS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
151
    iAssert ( Ψ i   [ set] j  I  {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
152
    { iNext. iApply (big_opS_delete _ _ i); first done. by iApply "HΨ". }
153
    iMod ("Hclose" $! (State High (I  {[ i ]})) ( : set token) with "[HΨ' Hl Hsp]").
154
    { iSplit; [iPureIntro; by eauto using wait_step|].
Ralf Jung's avatar
Ralf Jung committed
155
      rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
156
    iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
157
    iModIntro. wp_if.
158
    iApply "HΦ". iApply "HQR". by iRewrite "Heq".
159 160
Qed.

161
Lemma recv_split E l P1 P2 :
162
  N  E  recv l (P1  P2) ={E}= recv l P1  recv l P2.
163
Proof.
Ralf Jung's avatar
Ralf Jung committed
164
  rename P1 into R1; rename P2 into R2.
165
  iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
166
  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
167
    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
168 169
  iMod (saved_prop_alloc_strong (R1: %CF (iProp Σ)) I) as (i1) "[% #Hi1]".
  iMod (saved_prop_alloc_strong (R2: %CF (iProp Σ)) (I  {[i1]}))
170
    as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
172
  iMod ("Hclose" $! (State p ({[i1; i2]}  I  {[i]}))
173 174
                   {[Change i1; Change i2 ]} with "[-]") as "Hγ".
  { iSplit; first by eauto using split_step.
Ralf Jung's avatar
Ralf Jung committed
175
    rewrite /barrier_inv /=. iNext. iFrame "Hl".
176
    by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
177
  iAssert (sts_ownS γ (i_states i1) {[Change i1]}
178
     sts_ownS γ (i_states i2) {[Change i2]})%I with "[> -]" as "[Hγ1 Hγ2]".
179 180 181 182 183
  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
    - abstract set_solver.
    - iApply (sts_own_weaken with "Hγ");
        eauto using sts.closed_op, i_states_closed.
      abstract set_solver. }
Ralf Jung's avatar
Ralf Jung committed
184
  iModIntro; iSplitL "Hγ1".
185 186
  - iExists γ, P, R1, i1. iFrame; auto.
  - iExists γ, P, R2, i2. iFrame; auto.
187 188
Qed.

189
Lemma recv_weaken l P1 P2 : (P1 - P2) - recv l P1 - recv l P2.
190
Proof.
Ralf Jung's avatar
Ralf Jung committed
191
  iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
192
  iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
193
  iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
194
Qed.
195

196
Lemma recv_mono l P1 P2 : (P1  P2)  recv l P1  recv l P2.
197
Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed.
198
End proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200

Typeclasses Opaque barrier_ctx send recv.