logrel.v 10.7 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
136
137
138
139
140
141
  (* Definition to_side (s : side) : chan:= *)
  (*   match s with *)
  (*   | Left  => true *)
  (*   | Right => false *)
  (*   end. *)

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

143
  Lemma send_vs c γ s (P : val  Prop) st E :
144
145
146
    N  E 
     c @ s : TSend P st {γ} ={E,E∖↑N}=
       l r, chan_frag (st_c_name γ) c l r 
147
       ( v, P v -
148
               chan_frag_snoc (st_c_name γ) c l r s v
149
              ={E N,E}=  c @ s : st v {γ}).
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
  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.
172
        - destruct r; inversion Heval; subst.
173
174
          iSplit=> //.
          iPureIntro.
175
176
177
178
179
          simpl.
          rewrite (involutive (st v)).
          rewrite -(involutive (dual_stype (st v))).
          split=> //.
      }
180
181
182
183
184
185
      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.
186
        iExists _,_, _, _. iFrame.
187
188
189
        iRight.
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
          iDestruct "Heval" as %Heval.
190
        - destruct l; inversion Heval; subst.
191
192
          iSplit=> //.
          iPureIntro.
193
194
195
196
          simpl.
          rewrite (involutive (st v)).
          rewrite -(involutive (dual_stype (st v))).
          split=> //.
197
198
199
200
201
202
203
204
205
        - 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 {γ} }}}
206
      send c #s v
207
208
209
210
211
212
213
214
215
216
    {{{ 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.
217

Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
218
219
  Lemma try_recv_vs c γ s (P : val  Prop) st E :
    N  E 
220
221
     c @ s : TRecv P st {γ}
    ={E,E∖↑N}=
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
222
       l r, chan_frag (st_c_name γ) c l r 
223
      ( ((try_recv_fail (st_c_name γ) c l r s ={E∖↑N,E}=
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
224
            c @ s : TRecv P st {γ}) 
225
         ( v, try_recv_succ (st_c_name γ) c l r s v ={E∖↑N,E}=
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
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
271
272
273
274
275
276
                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.

277
278
  Lemma try_recv_st_spec st γ c s (P : val  Prop) :
    {{{  c @ s : TRecv P st {γ} }}}
279
      try_recv c #s
280
281
282
283
284
285
286
287
    {{{ 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".
288
289
290
    iIntros "!>".
    iSplit.
    - iIntros "Hupd".
291
292
      iDestruct "H" as "[H _]".
      iMod ("H" with "Hupd") as "H".
293
294
295
296
      iModIntro.
      iApply "HΦ"=> //.
      eauto with iFrame.
    - iIntros (v) "Hupd".
297
298
      iDestruct "H" as "[_ H]".
      iMod ("H" with "Hupd") as "H".
299
300
301
      iModIntro.
      iApply "HΦ"=> //.
      eauto with iFrame.
302
303
  Qed.

304
305
  Lemma recv_st_spec st γ c s (P : val  Prop) :
    {{{  c @ s : TRecv P st {γ} }}}
306
      recv c #s
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
    {{{ 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.

325
End logrel.