flat.v 20.4 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
From iris.program_logic Require Export auth weakestpre saved_prop.
Zhen Zhang's avatar
Zhen Zhang committed
2
3
4
5
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
Zhen Zhang's avatar
Zhen Zhang committed
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
From iris.algebra Require Import upred frac agree excl dec_agree upred_big_op gset gmap.
From iris.tests Require Import misc atomic treiber_stack.

Definition doOp : val :=
  λ: "f" "p",
     match: !"p" with
       InjL "x" => "p" <- InjR ("f" "x")
     | InjR "_" => #()
     end.

Definition doOp' (f:val) : val :=
  λ: "p",
     match: !"p" with
       InjL "x" => "p" <- InjR (f "x")
     | InjR "_" => #()
     end.

Definition try_srv : val :=
  λ: "lk" "s" "f",
    if: try_acquire "lk"
      then let: "hd" := !"s" in
           let: "f'" := doOp "f" in
           iter "hd" "f'";;
           release "lk"
      else #().

Definition loop: val :=
  rec: "loop" "f" "p" "s" "lk" :=
    match: !"p" with
    InjL "_" =>
        try_srv "lk" "s" "f";;
        "loop" "f" "p" "s" "lk"
    | InjR "r" => "r"
    end.

Definition install : val :=
  λ: "x" "s",
     let: "p" := ref (InjL "x") in
     push "s" "p";;
     "p".

Definition mk_flat : val :=
Zhen Zhang's avatar
Zhen Zhang committed
48
  λ: "f",
Zhen Zhang's avatar
Zhen Zhang committed
49
50
   let: "lk" := newlock #() in
   let: "s" := new_stack #() in
Zhen Zhang's avatar
Zhen Zhang committed
51
52
53
   λ: "x",
      let: "p" := install "x" "s" in
      loop "f" "p" "s" "lk".
Zhen Zhang's avatar
Zhen Zhang committed
54
55
56
57

Global Opaque doOp try_srv install loop mk_flat.

Definition reqR := prodR fracR (dec_agreeR val). (* request x should be kept same *)
Zhen Zhang's avatar
Zhen Zhang committed
58
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Zhen Zhang's avatar
Zhen Zhang committed
59
60
61
62
63
Definition tokmR := evmapR loc toks. (* tie each slot to tokens *)
Definition reqmR := evmapR loc val. (* tie each slot to request value *)
Class flatG Σ := FlatG {
  req_G :> inG Σ reqR;
  tok_G :> inG Σ (authR tokmR);
Zhen Zhang's avatar
Zhen Zhang committed
64
  sp_G  :> savedPropG Σ (cofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
65
66
67
68
}.

Definition flatΣ : gFunctors :=
  #[ GFunctor (constRF reqR);
Zhen Zhang's avatar
Zhen Zhang committed
69
70
     GFunctor (constRF (authR tokmR));
     savedPropΣ (cofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
71
72
73
   ].

Instance subG_flatΣ {Σ} : subG flatΣ Σ  flatG Σ.
Zhen Zhang's avatar
Zhen Zhang committed
74
Proof. intros [?%subG_inG [?%subG_inG [? _]%subG_inv]%subG_inv]%subG_inv. split; apply _. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
75
76
77

Section proof.
  Context `{!heapG Σ, !lockG Σ, !evidenceG loc val Σ, !flatG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
78
79
80
81
82
83
84
85
86
  Context (R: iProp Σ).

  Definition init_s (ts: toks) :=
    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ())  own γ3 (Excl ()))%I.

  Definition installed_s (ts: toks) (f x: val) :=
    let '(γx, γ1, _, γ4, γq) := ts in
    ( (P: val  iProp Σ) Q, own γx ((1/2)%Qp, DecAgree x)  P x  ({{ R  P x }} f x {{ v, R  Q x v }}) 
                             saved_prop_own γq (Q x)  own γ1 (Excl ())  own γ4 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
87
88

  Definition received_s (ts: toks) (x: val) γr :=
Zhen Zhang's avatar
Zhen Zhang committed
89
90
91
    let '(γx, _, _, γ4, _) := ts in
    (own γx ((1/2/2)%Qp, DecAgree x)  own γr (Excl ())  own γ4 (Excl ()))%I.

Zhen Zhang's avatar
Zhen Zhang committed
92
  Definition finished_s (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
93
94
95
96
    let '(γx, γ1, _, γ4, γq) := ts in
    ( Q: val  val  iProp Σ,
       own γx ((1/2)%Qp, DecAgree x)  saved_prop_own γq (Q x) 
       Q x y  own γ1 (Excl ())  own γ4 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
97
98
99
100

  Definition evm := ev loc toks.
  
  (* p slot invariant *)
Zhen Zhang's avatar
Zhen Zhang committed
101
  Definition p_inv (γm γr: gname) (f v: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
102
103
104
105
106
    ( (ts: toks) (p : loc),
       v = #p  evm γm p ts 
       ((* INIT *)
        ( y: val, p {1/2} InjRV y  init_s ts)
        (* INSTALLED *)
Zhen Zhang's avatar
Zhen Zhang committed
107
        ( x: val, p {1/2} InjLV x  installed_s ts f x) 
Zhen Zhang's avatar
Zhen Zhang committed
108
109
110
111
112
        (* RECEIVED *)
        ( x: val, p {1/2} InjLV x  received_s ts x γr) 
        (* FINISHED *)
        ( x y: val, p {1/2} InjRV y  finished_s ts x y)))%I.

Zhen Zhang's avatar
Zhen Zhang committed
113
  Definition srv_stack_inv γs γm γr s f := ( xs, is_stack' (p_inv γm γr f) γs xs s)%I.
Zhen Zhang's avatar
Zhen Zhang committed
114
115
116
117
118
119

  Definition srv_tokm_inv γm := ( m : tokmR, own γm ( m)  [ map] p  _  m,  v, p {1/2} v)%I.

  Lemma install_push_spec
        (Φ: val  iProp Σ)
        (p: loc) (γs γm γr: gname) (ts: toks)
Zhen Zhang's avatar
Zhen Zhang committed
120
        (s: loc) (f x: val) :
Zhen Zhang's avatar
Zhen Zhang committed
121
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
122
123
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm) 
    evm γm p ts  installed_s ts f x 
Zhen Zhang's avatar
Zhen Zhang committed
124
125
126
127
128
    p {1/2} InjLV x  (( hd, evs γs hd #p) - Φ #())
     WP push #s #p {{ Φ }}.
  Proof.
    iIntros (HN) "(#Hh & #? & Hpm & Hs & Hp & HΦ)".
    rewrite /srv_stack_inv.
Zhen Zhang's avatar
Zhen Zhang committed
129
    iDestruct (push_spec N (p_inv γm γr f) (fun v => ( hd, evs γs hd #p)  v = #())%I
Zhen Zhang's avatar
Zhen Zhang committed
130
131
132
133
134
135
136
137
138
139
               with "[-HΦ]") as "Hpush"=>//.
    - iFrame "Hh". iSplitL "Hp Hs Hpm"; last eauto.
      iExists ts. iExists p. iSplit=>//. iFrame "Hpm".
      iRight. iLeft. iExists x. iFrame.
    - iApply wp_wand_r.
      iSplitL "Hpush"; first done.
      iIntros (?) "[? %]". subst.
      by iApply "HΦ".
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
140
141
142
  Definition installed_recp (ts: toks) (x: val) (Q: val  val  iProp Σ) :=
    let '(γx, _, γ3, _, γq) := ts in
    (own γ3 (Excl ())  own γx ((1/2)%Qp, DecAgree x)  saved_prop_own γq (Q x))%I.
Zhen Zhang's avatar
Zhen Zhang committed
143
144

  Lemma install_spec
Zhen Zhang's avatar
Zhen Zhang committed
145
146
        (Φ: val  iProp Σ) P Q
        (f x: val) (γs γm γr: gname) (s: loc):
Zhen Zhang's avatar
Zhen Zhang committed
147
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
148
149
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm)  P x  ({{ R  P x }} f x {{ v, R  Q x v }}) 
    ( (p: loc) (ts: toks), installed_recp ts x Q - evm γm p ts -( hd, evs γs hd #p) - Φ #p)
Zhen Zhang's avatar
Zhen Zhang committed
150
151
     WP install x #s {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
152
    iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
153
154
155
156
157
158
    wp_seq. wp_let. wp_alloc p as "Hl".
    iApply pvs_wp.
    iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
    iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
    iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
    iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
Zhen Zhang's avatar
Zhen Zhang committed
159
160
    iVs (saved_prop_alloc (F:=(cofe_funCF val idCF)) (Q x)%I) as (γq) "#?".
    iInv N as "[Hrs >Hm]" "Hclose".
Zhen Zhang's avatar
Zhen Zhang committed
161
162
163
164
165
166
    iDestruct "Hm" as (m) "[Hm HRm]".
    destruct (m !! p) eqn:Heqn.
    - (* old name *)
      iDestruct (big_sepM_delete (fun p _ =>  v : val, p {1 / 2} v)%I m with "HRm") as "[Hp HRm]"=>//.
      iDestruct "Hp" as (?) "Hp". iExFalso. iApply bogus_heap; last by iFrame "Hh Hl Hp". auto.
    - (* fresh name *)
Zhen Zhang's avatar
Zhen Zhang committed
167
      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as "==>[Hm1 Hm2]"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
168
169
      iDestruct "Hl" as "[Hl1 Hl2]".
      iVs ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
Zhen Zhang's avatar
Zhen Zhang committed
170
      + iNext. iFrame. iExists ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4, γq))]}  m). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
171
172
173
174
175
176
177
178
179
        rewrite <-(insert_singleton_op m)=>//.
        iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
        iSplitL "Hl1"; last by iAssumption. eauto.
      + iDestruct (pack_ev with "Hm2") as "Hev".
        iDestruct (dup_ev with "Hev") as "==>[Hev1 Hev2]".
        iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
        iVsIntro. wp_let. wp_bind ((push _) _).
        iApply install_push_spec=>//.
        iFrame "#". rewrite /evm /installed_s.
Zhen Zhang's avatar
Zhen Zhang committed
180
181
182
        iFrame.
        iSplitL "Hpx Hx1 Hf".
        { iExists P, Q. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
183
        iIntros "Hhd". wp_seq. iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
184
185
186
        iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hev1 Hhd]")=>//.
        { rewrite /installed_recp. iFrame. iFrame "#". }
        by iApply ("HΦ" with "Hev1").
Zhen Zhang's avatar
Zhen Zhang committed
187
188
189
  Qed.

  Lemma loop_iter_list_spec Φ (f: val) (s hd: loc) (γs γm γr: gname) xs:
Zhen Zhang's avatar
Zhen Zhang committed
190
191
    heapN  N 
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm)  own γr (Excl ())  R 
Zhen Zhang's avatar
Zhen Zhang committed
192
193
194
    is_list' γs hd xs  (own γr (Excl ()) - R - Φ #())
     WP doOp f {{ f', WP iter #hd f' {{ Φ }} }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
195
    iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
196
197
198
199
    iApply pvs_wp.
    iDestruct (dup_is_list' with "[Hlist']") as "==>[Hl1 Hl2]"; first by iFrame.
    iDestruct (dup_is_list' with "[Hl2]") as "==>[Hl2 Hl3]"; first by iFrame.
    iVsIntro. wp_seq.
Zhen Zhang's avatar
Zhen Zhang committed
200
201
    iDestruct (iter_spec _ (p_inv γm γr f) (fun v => v = #()  own γr (Excl ())  R)%I γs s
                         (is_list' γs hd xs  own γr (Excl ())  R)%I (srv_tokm_inv γm) xs hd
Zhen Zhang's avatar
Zhen Zhang committed
202
203
204
                         (doOp' f) (doOp' f)
                         with "[-Hl1 HΦ]") as "Hiter"=>//.
    - rewrite /f_spec.
Zhen Zhang's avatar
Zhen Zhang committed
205
206
207
      iIntros (Φ' p _ Hin) "(#Hh & #? & (Hls & Ho2 & HR) & HΦ')".
      wp_let. wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
      iDestruct "Hs" as (xs' hd') "[>Hhd [>Hxs HRs]]".
Zhen Zhang's avatar
Zhen Zhang committed
208
      iDestruct (dup_is_list' with "[Hls]") as "==>[Hls1 Hls2]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
209
210
211
212
213
214
      iDestruct "HRs" as (m) "[>Hom HRs]".
      (* acccess *)
      iDestruct (access with "[Hom HRs Hls1]") as (hd'' ?) "(Hrest & HRx & % & Hom)"=>//; first iFrame.
      iDestruct "HRx" as (v') "[>% [Hpinv' >Hhd'']]". inversion H1. subst.
      iDestruct "Hpinv'" as (ts p'') "[>% [>Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst.
      + iDestruct "Hp" as (y) "(>Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
215
216
217
        wp_load. iVs ("Hclose" with "[-HΦ' Ho2 HR Hls2]").
        { iNext. iFrame. iExists xs', hd'.
          iFrame "Hhd Hxs". iExists m.
Zhen Zhang's avatar
Zhen Zhang committed
218
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[Hrest Hhd'' Hevm Hp Hs]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
219
220
221
222
          iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
          iSplitR; first done. iFrame. iLeft. iExists y. iFrame. }
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
      + iDestruct "Hp" as (x') "(Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
223
224
225
        wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
        iDestruct "Hs" as  (P Q) "(Hx & Hpx & Hf & HoQ& Ho1 & Ho4)".
        iDestruct (dup_ev with "Hevm") as "==>[Hevm1 Hevm2]".
Zhen Zhang's avatar
Zhen Zhang committed
226
227
228
229
230
        iAssert (|=r=> own γx (((1/2/2)%Qp, DecAgree x') 
                               ((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as "==>[Hx1 Hx2]".
        { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
          rewrite -{1}(Qp_div_2 (1/2)%Qp).
          by apply pair_l_frac_op'. }
Zhen Zhang's avatar
Zhen Zhang committed
231
        iVs ("Hclose" with "[-Hf Hls2 Ho1 Hx2 HR Hevm2 HoQ Hpx HΦ']").
Zhen Zhang's avatar
Zhen Zhang committed
232
233
234
235
        { iNext. iFrame. iExists xs', hd'.
          iFrame "Hhd Hxs". iExists m.
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
          simpl. iFrame. iExists #p''. iSplitR; auto. rewrite /allocated.
Zhen Zhang's avatar
Zhen Zhang committed
236
          iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
Zhen Zhang's avatar
Zhen Zhang committed
237
238
          iFrame. iRight. iRight. iLeft. iExists x'. iFrame. }
        iVsIntro. wp_match.
Zhen Zhang's avatar
Zhen Zhang committed
239
        wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf HR".
Zhen Zhang's avatar
Zhen Zhang committed
240
241
        { iApply "Hf". iFrame. }
        iIntros (v) "[HR HQ]".
Zhen Zhang's avatar
Zhen Zhang committed
242
243
244
        wp_value. iVsIntro. iInv N as "[Hs >Hm]" "Hclose".
        iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
        iDestruct "HRs" as (m') "[>Hom HRs]".
Zhen Zhang's avatar
Zhen Zhang committed
245
        iDestruct (dup_is_list' with "[Hls2]") as "==>[Hls2 Hls3]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
246
247
248
249
250
        iDestruct (access with "[Hom HRs Hls2]") as (hd'''' q) "(Hrest & HRx & % & Hom)"=>//; first iFrame.
        iDestruct "HRx" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H2. subst.
        iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>Hevm Hps]]".
        inversion H3. subst.
        destruct (decide (γ1 = γ1'  γx = γx'  γ3 = γ3'  γ4 = γ4'  γq = γq')) as [[? [? [? [? ?]]]]|Hneq]; subst.
Zhen Zhang's avatar
Zhen Zhang committed
251
252
        {
          iDestruct "Hps" as "[Hp | [Hp | [Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
253
          * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
254
            iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
255
          * iDestruct "Hp" as (?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
256
            iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
257
          * iDestruct "Hp" as (x5) ">(Hp & Hx & Ho2 & Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
            iDestruct "Hm" as (m2) "[Hom2 HRm]".
            destruct (m2 !! p'''') eqn:Heqn.
            {
              iDestruct (big_sepM_delete _ m2 with "HRm") as "[HRk HRm]"=>//.
              iDestruct "HRk" as (?) "HRk".
              iDestruct (heap_mapsto_op_1 with "[HRk Hp]") as "[% Hp]"; first by iFrame.
              rewrite Qp_div_2. wp_store.
              (* now close the invariant *)
              iDestruct (m_frag_agree with "[Hx Hx2]") as "==>[Hx %]"; first iFrame.
              subst. rewrite Qp_div_2. iVs ("Hclose" with "[-HΦ' Ho2 HR Hls3]").
              { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
                iAssert (srv_tokm_inv γm) with "[Hp1 HRm Hom2]" as "HRm".
                { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
                  iFrame. eauto. }
                iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
                iExists m'. iFrame.
                iDestruct (big_sepM_delete _ m' with "[-]") as "?"=>//.
                { simpl. iFrame. iExists #p''''.
Zhen Zhang's avatar
Zhen Zhang committed
276
277
                  iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
                  iSplitR; first auto. iFrame "Hevm". iRight. iRight.
Zhen Zhang's avatar
Zhen Zhang committed
278
                  iRight. iExists x5, v. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
279
                  iExists Q. iFrame.                  
Zhen Zhang's avatar
Zhen Zhang committed
280
281
282
283
284
                }
              }
              iApply "HΦ'". by iFrame.
            }
            { iExFalso. iApply (map_agree_none' _ _ _ m2)=>//. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
285
          * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
286
287
            iApply excl_falso. iFrame.
        }
Zhen Zhang's avatar
Zhen Zhang committed
288
289
290
        { iDestruct (ev_agree with "[Hevm Hevm2]") as "==>[_ [_ %]]"; first iFrame.
          inversion H4. subst. by contradiction Hneq. }
      + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (y) "(_ & _ & >Ho2' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
291
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
292
293
      + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
        iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
294
295
296
297
        wp_load. iVs ("Hclose" with "[-HΦ' HR Ho2 Hls2]").
        { iNext. iFrame. iExists xs', hd'.
          iFrame "Hhd Hxs". iExists m.
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
298
299
300
          iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
          iSplitR; auto. iFrame. iRight. iRight. iRight. iExists x', y. iFrame.
          iExists Q. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
301
302
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
    - apply to_of_val.
Zhen Zhang's avatar
Zhen Zhang committed
303
    - rewrite /srv_stack_inv. iFrame "#". iFrame. iIntros "(? & ? & ?)". by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
304
305
306
307
    - iApply wp_wand_r. iSplitL "Hiter"; first done.
      iIntros (?) "[% [Ho2 HR]]". subst. iApply ("HΦ" with "Ho2 HR").
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
308
  Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
Zhen Zhang's avatar
Zhen Zhang committed
309
  Definition finished_recp (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
310
311
    let '(γx, _, _, _, γq) := ts in
    ( Q, own γx ((1 / 2)%Qp, DecAgree x)  saved_prop_own γq (Q x)  Q x y)%I.
Zhen Zhang's avatar
Zhen Zhang committed
312
313
314

  Lemma try_srv_spec Φ (s: loc) (lk: val) (f: val)
        (γs γr γm γlk: gname):
Zhen Zhang's avatar
Zhen Zhang committed
315
316
    heapN  N 
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm) 
Zhen Zhang's avatar
Zhen Zhang committed
317
318
319
    is_lock N γlk lk (own γr (Excl ())  R)  Φ #()
     WP try_srv lk #s f {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
320
    iIntros (?) "(#? & #? & #? & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
321
322
323
324
325
326
    wp_seq. wp_let. wp_let.
    wp_bind (try_acquire _). iApply try_acquire_spec.
    iFrame "#". iSplit; last by wp_if.
    (* acquired the lock *)
    iIntros "Hlocked [Ho2 HR]".
    wp_if. wp_bind (! _)%E.
Zhen Zhang's avatar
Zhen Zhang committed
327
328
    iInv N as "[H >Hm]" "Hclose".
    iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
Zhen Zhang's avatar
Zhen Zhang committed
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
    wp_load. iDestruct (dup_is_list' with "[Hxs]") as "==>[Hxs1 Hxs2]"; first by iFrame.
    iVs ("Hclose" with "[Hs Hxs1 HRs Hm]").
    { iNext. iFrame. iExists xs', hd'. by iFrame. }
    iVsIntro. wp_let. wp_bind (doOp f).
    iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
    { iApply (loop_iter_list_spec (fun v => own γr (Excl ())  R  v = #()))%I=>//.
      iFrame "#". iFrame. iIntros "? ?". by iFrame. }
    iIntros (f') "Hf'".
    wp_let. wp_bind ((iter _) _).
    iApply wp_wand_r. iSplitL "Hf'"; first iApply "Hf'".
    iIntros (?) "[Ho2 [HR %]]". subst.
    wp_seq. iApply release_spec.
    iFrame "#". iFrame.
  Qed.
    
  Lemma loop_spec Φ (p s: loc) (lk: val) (f: val)
        (γs γr γm γlk: gname) (ts: toks):
Zhen Zhang's avatar
Zhen Zhang committed
346
347
    heapN  N 
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm) 
Zhen Zhang's avatar
Zhen Zhang committed
348
349
350
351
352
    is_lock N γlk lk (own γr (Excl ())  R) 
    own_γ3 ts  evm γm p ts 
    ( hd, evs γs hd #p)  ( x y, finished_recp ts x y - Φ y)
     WP loop f #p #s lk {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
353
    iIntros (HN) "(#Hh & #? & #? & Ho3 & Hev & Hhd & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
354
    iLöb as "IH". wp_rec. repeat wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
355
356
357
    wp_bind (! _)%E. iInv N as "[Hinv >?]" "Hclose".
    iDestruct "Hinv" as (xs hd) "[>Hs [>Hxs HRs]]".
    iDestruct "HRs" as (m) "[>Hom HRs]".
Zhen Zhang's avatar
Zhen Zhang committed
358
359
    iDestruct "Hhd" as (hdp ?) "Hhd".
    destruct (m !! hdp) eqn:Heqn.
Zhen Zhang's avatar
Zhen Zhang committed
360
361
362
    - iDestruct (big_sepM_delete_later _ m with "HRs") as "[Hp Hrs]"=>//.
      iDestruct "Hp" as (?) "[>% [Hpr ?]]"; subst.
      iDestruct "Hpr" as (ts' p') "(>% & >Hp' & Hp)".
Zhen Zhang's avatar
Zhen Zhang committed
363
364
      subst. iDestruct (map_agree_eq' _ _ γs m with "[Hom Hhd]") as "(Hom & Hhd & %)"=>//.
      { iFrame. rewrite /ev. eauto. }
Zhen Zhang's avatar
Zhen Zhang committed
365
      inversion H0. subst.
Zhen Zhang's avatar
Zhen Zhang committed
366
      iDestruct (ev_agree with "[Hev Hp']") as "==>[Hγs2 [Hγs %]]"; first iFrame. subst.
Zhen Zhang's avatar
Zhen Zhang committed
367
      destruct ts as [[[[γx γ1] γ3] γ4] γq].
Zhen Zhang's avatar
Zhen Zhang committed
368
      iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
369
      + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
Zhen Zhang's avatar
Zhen Zhang committed
370
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
371
      + iDestruct "Hp" as (x) "(>Hp & Hs')".
Zhen Zhang's avatar
Zhen Zhang committed
372
373
374
        wp_load. iVs ("Hclose" with "[-Hγs2 Ho3 HΦ Hhd]").
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
375
          iFrame. iExists #p'. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
376
          iSplitR; first auto. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
377
          iRight. iLeft. iExists x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
378
379
380
381
382
383
384
385
386
387
        iVsIntro. wp_match.
        wp_bind (try_srv _ _ _). iApply try_srv_spec=>//.
        iFrame "#". wp_seq.
        iAssert ( hd, evs γs hd #p')%I with "[Hhd]" as "Hhd"; eauto.
        by iApply ("IH" with "Ho3 Hγs2 Hhd").
      + iDestruct "Hp" as (x) "(Hp & Hx & Ho2 & Ho4)".
        wp_load.
        iVs ("Hclose" with "[-Hγs Ho3 HΦ Hhd]").
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
388
          iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
389
          iSplitR; first auto. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
390
          iRight. iRight. iLeft. iExists x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
391
392
393
394
395
        iVsIntro. wp_match.
        wp_bind (try_srv _ _ _). iApply try_srv_spec=>//.
        iFrame "#". wp_seq.
        iAssert ( hd, evs γs hd #p')%I with "[Hhd]" as "Hhd"; eauto.
        by iApply ("IH" with "Ho3 Hγs Hhd").
Zhen Zhang's avatar
Zhen Zhang committed
396
397
       + iDestruct "Hp" as (x y) "[>Hp Hs']". iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
          wp_load. iVs ("Hclose" with "[-Hγs Ho4 HΦ Hx HoQ HQ]").
Zhen Zhang's avatar
Zhen Zhang committed
398
399
          { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
            iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
400
            iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
401
402
403
            iSplitR; first auto. iFrame.
            iLeft. iExists y. iFrame. }
          iVsIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
404
          iExists Q. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
405
406
407
408
    - iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame "Hom".
      rewrite /ev. eauto.
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
409
410
411
  Definition flatten (f' f: val) :=
    ( P Q, ( x:val, {{ R  P x }} f x {{ v, R  Q x v }}) 
            ( x:val, {{ P x }} f' x {{ v,  Q x v }}))%I.
Zhen Zhang's avatar
Zhen Zhang committed
412

Zhen Zhang's avatar
Zhen Zhang committed
413
  Lemma mk_flat_spec (f: val) :
Zhen Zhang's avatar
Zhen Zhang committed
414
415
     (Φ: val  iProp Σ),
      heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
416
      heap_ctx  R  ( f',  flatten f' f - Φ f')  WP mk_flat f {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
417
418
419
420
421
422
423
424
425
426
  Proof.
    iIntros (Φ HN) "(#Hh & HR & HΦ)".
    iVs (own_alloc (Excl ())) as (γr) "Ho2"; first done.
    iVs (own_alloc ( (: tokmR)   )) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
    iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
    { iExists . iFrame. by rewrite big_sepM_empty. }
    wp_seq. wp_bind (newlock _).
    iApply (newlock_spec _ (own γr (Excl ())  R))%I=>//.
    iFrame "Hh Ho2 HR". iIntros (lk γlk) "#Hlk".
    wp_let. wp_bind (new_stack _).
Zhen Zhang's avatar
Zhen Zhang committed
427
    iApply (new_stack_spec' _ (p_inv γm γr f))=>//.
Zhen Zhang's avatar
Zhen Zhang committed
428
    iFrame "Hh Hm". iIntros (γ s) "#Hss".
Zhen Zhang's avatar
Zhen Zhang committed
429
430
    wp_let. iVsIntro. iApply "HΦ". rewrite /flatten.
    iAlways. iIntros (P Q) "#Hf".
Zhen Zhang's avatar
Zhen Zhang committed
431
432
    iIntros (x) "!# Hp". wp_let.
    wp_bind ((install _) _).
Zhen Zhang's avatar
Zhen Zhang committed
433
434
435
    iApply (install_spec _ P Q)=>//.
    iFrame "#". iFrame "Hp". iSplitR; first iApply "Hf".
    iIntros (p [[[[γx γ1] γ3] γ4] γq]) "(Ho3 & Hx & HoQ) Hev Hhd".
Zhen Zhang's avatar
Zhen Zhang committed
436
437
    wp_let. iApply loop_spec=>//.
    iFrame "#". iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
438
439
440
441
442
443
    iIntros (? ?) "Hs".
    iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
    destruct (decide (x = a)) as [->|Hneq].
    - iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
      iNext. admit. (* iRewrite "Heq" in "HQ'". *)
    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
Zhen Zhang's avatar
Zhen Zhang committed
444
445
      iDestruct (own_valid with "Hx") as %[_ H1].
      rewrite pair_op //= dec_agree_ne in H1=>//.
Zhen Zhang's avatar
Zhen Zhang committed
446
  Admitted.
Zhen Zhang's avatar
Zhen Zhang committed
447
448

End proof.