logrel.v 10.6 KB
Newer Older
1
2
3
4
5
6
7
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From osiris Require Import typing auth_excl channel.
From iris.algebra Require Import list auth excl.
8
From iris.base_logic Require Import invariants.
9
10
11
12
13

Section logrel.
  Context `{!heapG Σ, !lockG Σ} (N : namespace).
  Context `{!auth_exclG (list val) Σ}.
  Context `{!auth_exclG stype Σ}.
14

15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
  Record st_name := SessionType_name {
    st_c_name : chan_name;
    st_l_name : gname;
    st_r_name : gname
  }.

  Definition stmapsto_frag γ (st : stype) s : iProp Σ :=
    let γ :=
        match s with
        | Left  => st_l_name γ
        | Right => st_r_name γ
        end in
    own γ (  to_auth_excl st)%I.

  Definition stmapsto_full γ (st : stype) s : iProp Σ :=
    let γ :=
        match s with
        | Left  => st_l_name γ
        | Right => st_r_name γ
        end in
    own γ ( to_auth_excl st)%I.

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
37
38
39
40
41
42
43
44
  Fixpoint st_eval (vs : list val) (st1 st2 : stype) : Prop :=
    match vs with
    | [] => st1 = dual_stype st2
    | v::vs => match st2 with
               | TRecv P st2 => P v  st_eval vs st1 (st2 v)
               | _ => False
               end
    end.
45

46
  Lemma st_eval_send (P : val -> Prop) st l str v :
47
48
      P v  st_eval l (TSend P st) str  st_eval (l ++ [v]) (st v) str.
  Proof.
49
    intro HP.
50
51
    revert str.
    induction l; intros str.
52
53
54
55
56
    - inversion 1. simpl.
      destruct str; inversion H1; subst. eauto.
    - intros. simpl.
      destruct str; inversion H.
      split=> //.
57
58
59
      apply IHl=> //.
  Qed.

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
60
61
62
63
64
65
66
67
68
69
70
  Lemma st_eval_recv (P : val  Prop) st1 l st2 v :
     st_eval (v :: l) st1 (TRecv P st2)   st_eval l st1 (st2 v)  P v.
  Proof.
    intros Heval.
    generalize dependent st1.
    induction l; intros.
    - inversion Heval; subst. split=> //.
     - inversion Heval; subst. simpl.
      constructor=> //.
  Qed.

71
72
  Definition inv_st (γ :st_name) (c : val) : iProp Σ :=
    ( l r stl str,
73
      chan_frag (st_c_name γ) c l r 
74
75
      stmapsto_full γ stl Left  
      stmapsto_full γ str Right 
76
      ((r = []  st_eval l stl str) 
77
78
79
80
       (l = []  st_eval r str stl)))%I.

  Definition st_ctx (γ : st_name) (st : stype) (c : val) : iProp Σ :=
    (chan_ctx N (st_c_name γ) c  inv N (inv_st γ c))%I.
81

82
83
  Definition st_frag  (γ : st_name) (st : stype) (s : side) : iProp Σ :=
    stmapsto_frag γ st s.
84

85
86
  Definition interp_st (γ : st_name) (st : stype)
      (c : val) (s : side) : iProp Σ :=
87
    (st_frag γ st s  st_ctx γ st c)%I.
88

89
90
91
92
  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st γ sτ c s)
    (at level 10, s at next level, sτ at next level, γ at next level,
     format "⟦  c  @  s  :  sτ  ⟧{ γ }").

93
94
  Lemma new_chan_vs st E c cγ :
    is_chan N cγ c [] [] ={E}=
95
       lγ rγ,
96
        let γ := SessionType_name cγ lγ rγ in
97
         c @ Left : st {γ}   c @ Right : dual_stype st {γ}.
98
  Proof.
99
    iIntros "[#Hcctx Hcf]".
100
101
102
103
104
105
    iMod (own_alloc ( (to_auth_excl st) 
                      (to_auth_excl st)))
      as (lγ) "[Hlsta Hlstf]"; first done.
    iMod (own_alloc ( (to_auth_excl (dual_stype st)) 
                      (to_auth_excl (dual_stype st))))
      as (rγ) "[Hrsta Hrstf]"; first done.
106
    pose (SessionType_name cγ lγ rγ) as stγ.
107
    iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
108
    { iNext. rewrite /inv_st. eauto 10 with iFrame. }
109
110
111
112
    iModIntro.
    iExists _, _.
    iFrame. simpl.
    repeat iSplitL=> //.
113
  Qed.
114

115
116
117
  Lemma new_chan_st_spec st :
    {{{ True }}}
      new_chan #()
118
119
    {{{ c γ, RET c;   c @ Left : st {γ} 
                      c @ Right : dual_stype st {γ} }}}.
120
121
122
123
124
125
126
127
128
129
130
131
  Proof.
    iIntros (Φ _) "HΦ".
    iApply (wp_fupd).
    iApply (new_chan_spec)=> //.
    iModIntro.
    iIntros (c γ) "[Hc Hctx]".
    iMod (new_chan_vs st  c γ with "[-HΦ]") as "H".
    { rewrite /is_chan. eauto with iFrame. }
    iDestruct "H" as (lγ rγ) "[Hl Hr]".
    iApply "HΦ".
    iModIntro.
    iFrame.
132
133
  Qed.

134
135
  Coercion side_to_side (s : side) : channel.side :=
    match s with Left => channel.Left | Right => channel.Right end.
136

137
  Lemma send_vs c γ s (P : val  Prop) st E :
138
139
140
    N  E 
     c @ s : TSend P st {γ} ={E,E∖↑N}=
       l r, chan_frag (st_c_name γ) c l r 
141
       ( v, P v -
142
               chan_frag_snoc (st_c_name γ) c l r s v
143
              ={E N,E}=  c @ s : st v {γ}).
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
  Proof.
    iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
    iMod (inv_open with "Hinv") as "Hinv'"=> //.
    iDestruct "Hinv'" as "[Hinv' Hinvstep]".
    iDestruct "Hinv'" as (l r stl str) "(>Hcf & Hstla & Hstra & Hinv')".
    iModIntro.
    rewrite /stmapsto_frag /stmapsto_full.
    iExists l, r.
    iIntros "{$Hcf} !>" (v HP) "Hcf".
    destruct s.
    - iRename "Hstf" into "Hstlf".
      iDestruct (excl_eq with "Hstla Hstlf") as %<-.
      iMod (excl_update _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
      iMod ("Hinvstep" with "[-Hstlf]") as "_".
      { iNext.
        iExists _,_,_,_. iFrame.
        iLeft.
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
          iDestruct "Heval" as %Heval.
        - iSplit=> //.
          iPureIntro.
          by eapply st_eval_send.
166
        - destruct r; inversion Heval; subst.
167
168
          iSplit=> //.
          iPureIntro.
169
170
171
172
173
          simpl.
          rewrite (involutive (st v)).
          rewrite -(involutive (dual_stype (st v))).
          split=> //.
      }
174
175
176
177
178
179
      iModIntro. iFrame "Hcctx ∗ Hinv".
    - iRename "Hstf" into "Hstrf".
      iDestruct (excl_eq with "Hstra Hstrf") as %<-.
      iMod (excl_update _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
      iMod ("Hinvstep" with "[-Hstrf]") as "_".
      { iNext.
180
        iExists _,_, _, _. iFrame.
181
182
183
        iRight.
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
          iDestruct "Heval" as %Heval.
184
        - destruct l; inversion Heval; subst.
185
186
          iSplit=> //.
          iPureIntro.
187
188
189
190
          simpl.
          rewrite (involutive (st v)).
          rewrite -(involutive (dual_stype (st v))).
          split=> //.
191
192
193
194
195
196
197
198
199
        - iSplit=> //.
          iPureIntro.
          by eapply st_eval_send. }
      iModIntro. iFrame "Hcctx ∗ Hinv".
  Qed.

  Lemma send_st_spec st γ c s (P : val  Prop) v :
    P v 
    {{{  c @ s : TSend P st {γ} }}}
200
      send c #s v
201
202
203
204
205
206
207
208
209
210
    {{{ RET #();  c @ s : st v {γ} }}}.
  Proof.
    iIntros (HP Φ) "Hsend HΦ".
    iApply (send_spec with "[#]").
    { iDestruct "Hsend" as "[? [$ ?]]". }
    iMod (send_vs with "Hsend") as (ls lr) "[Hch H]"; first done.
    iModIntro. iExists ls, lr. iFrame "Hch".
    iIntros "!> Hupd". iApply "HΦ".
    iApply ("H" $! v HP with "[Hupd]"). by destruct s.
  Qed.
211

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
212
213
  Lemma try_recv_vs c γ s (P : val  Prop) st E :
    N  E 
214
215
     c @ s : TRecv P st {γ}
    ={E,E∖↑N}=
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
216
       l r, chan_frag (st_c_name γ) c l r 
217
      ( ((try_recv_fail (st_c_name γ) c l r s ={E∖↑N,E}=
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
218
            c @ s : TRecv P st {γ}) 
219
         ( v, try_recv_succ (st_c_name γ) c l r s v ={E∖↑N,E}=
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
                c @ s : (st v) {γ}  P v))).
  Proof.
    iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
    iMod (inv_open with "Hinv") as "Hinv'"=> //.
    iDestruct "Hinv'" as "[Hinv' Hinvstep]".
    iDestruct "Hinv'" as (l r stl str) "(>Hcf & Hstla & Hstra & Hinv')".
    iModIntro.
    rewrite /stmapsto_frag /stmapsto_full.
    iExists l, r.
    iIntros "{$Hcf} !>".
    destruct s.
    - iRename "Hstf" into "Hstlf".
      iDestruct (excl_eq with "Hstla Hstlf") as %<-.
      iSplit=> //.
      + iIntros "[Hfail Hemp]".
        iMod ("Hinvstep" with "[-Hstlf]") as "_".
        { iNext. iExists l,r,_,_. iFrame. }
        iModIntro. iFrame "Hcctx ∗ Hinv".
      + simpl. iIntros (v) "Hsucc".
        rewrite /try_recv_succ. simpl.
        iDestruct "Hsucc" as (r') "[Hsucc Hr]".
        iDestruct "Hr" as %Hr.
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; first inversion Hr.
        iMod (excl_update _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
        subst.
        iDestruct "Heval" as %Heval.
        apply st_eval_recv in Heval as [Heval HP].
        iMod ("Hinvstep" with "[-Hstlf]") as "_".
        { iExists _,_,_,_. iFrame. iRight=> //. }
        by iFrame (HP) "Hcctx Hinv".
    - iRename "Hstf" into "Hstrf".
      iDestruct (excl_eq with "Hstra Hstrf") as %<-.
      iSplit=> //.
      + iIntros "[Hfail Hemp]".
        iMod ("Hinvstep" with "[-Hstrf]") as "_".
        { iNext. iExists l,r,_,_. iFrame. }
        iModIntro. iFrame "Hcctx ∗ Hinv".
      +  simpl. iIntros (v) "Hsucc".
        rewrite /try_recv_succ. simpl.
        iDestruct "Hsucc" as (r') "[Hsucc Hr]".
        iDestruct "Hr" as %Hl.
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last inversion Hl.
        iMod (excl_update _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
        subst.
        iDestruct "Heval" as %Heval.
        apply st_eval_recv in Heval as [Heval HP].
        iMod ("Hinvstep" with "[-Hstrf]") as "_".
        { iExists _,_,_,_. iFrame. iLeft=> //. }
        by iFrame (HP) "Hcctx Hinv".
  Qed.

271
272
  Lemma try_recv_st_spec st γ c s (P : val  Prop) :
    {{{  c @ s : TRecv P st {γ} }}}
273
      try_recv c #s
274
275
276
277
278
279
280
281
    {{{ v, RET v; (v = NONEV   c @ s : TRecv P st {γ}) 
                  ( w, v = SOMEV w   c @ s : st w {γ}  P w)}}}.
  Proof.
    iIntros (Φ) "Hrecv HΦ".
    iApply (try_recv_spec with "[#]").
    { iDestruct "Hrecv" as "[? [$ ?]]". }
    iMod (try_recv_vs with "Hrecv") as (ls lr) "[Hch H]"; first done.
    iModIntro. iExists ls, lr. iFrame "Hch".
282
283
284
    iIntros "!>".
    iSplit.
    - iIntros "Hupd".
285
286
      iDestruct "H" as "[H _]".
      iMod ("H" with "Hupd") as "H".
287
288
289
290
      iModIntro.
      iApply "HΦ"=> //.
      eauto with iFrame.
    - iIntros (v) "Hupd".
291
292
      iDestruct "H" as "[_ H]".
      iMod ("H" with "Hupd") as "H".
293
294
295
      iModIntro.
      iApply "HΦ"=> //.
      eauto with iFrame.
296
297
  Qed.

298
299
  Lemma recv_st_spec st γ c s (P : val  Prop) :
    {{{  c @ s : TRecv P st {γ} }}}
300
      recv c #s
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
    {{{ v, RET v;  c @ s : st v {γ}  P v}}}.
  Proof.
    iIntros (Φ) "Hrecv HΦ".
    iLöb as "IH". wp_rec.
    wp_apply (try_recv_st_spec with "Hrecv").
    iIntros (v) "H".
    iDestruct "H" as "[H | H]".
    - iDestruct "H" as "[Hv H]".
      iDestruct "Hv" as %->.
      wp_pures.
      iApply ("IH" with "[H]")=> //.
    - iDestruct "H" as (w) "[Hv H]".
      iDestruct "Hv" as %->.
      wp_pures.
      iApply "HΦ".
      iFrame.
  Qed.

319
End logrel.