flat.v 19.6 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
From iris.program_logic Require Export weakestpre saved_prop.
Zhen Zhang's avatar
Zhen Zhang committed
2 3 4
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
5
From iris.algebra Require Import auth upred frac agree excl dec_agree upred_big_op gset gmap.
Zhen Zhang's avatar
Zhen Zhang committed
6
From iris_atomic Require Import misc peritem sync evmap.
Zhen Zhang's avatar
Zhen Zhang committed
7 8 9 10

Definition doOp : val :=
  λ: "p",
     match: !"p" with
Zhen Zhang's avatar
Zhen Zhang committed
11
       InjL "req" => "p" <- InjR ((Fst "req") (Snd "req"))
Zhen Zhang's avatar
Zhen Zhang committed
12 13 14 15
     | InjR "_" => #()
     end.

Definition try_srv : val :=
16
  λ: "lk" "s",
Zhen Zhang's avatar
Zhen Zhang committed
17 18
    if: try_acquire "lk"
      then let: "hd" := !"s" in
19
           iter "hd" doOp;;
Zhen Zhang's avatar
Zhen Zhang committed
20 21 22 23
           release "lk"
      else #().

Definition loop: val :=
24
  rec: "loop" "p" "s" "lk" :=
Zhen Zhang's avatar
Zhen Zhang committed
25 26
    match: !"p" with
    InjL "_" =>
27 28
        try_srv "lk" "s";;
        "loop" "p" "s" "lk"
Zhen Zhang's avatar
Zhen Zhang committed
29 30 31 32
    | InjR "r" => "r"
    end.

Definition install : val :=
33 34
  λ: "f" "x" "s",
     let: "p" := ref (InjL ("f", "x")) in
Zhen Zhang's avatar
Zhen Zhang committed
35 36 37 38
     push "s" "p";;
     "p".

Definition mk_flat : val :=
39
  λ: <>,
Zhen Zhang's avatar
Zhen Zhang committed
40 41
   let: "lk" := newlock #() in
   let: "s" := new_stack #() in
42 43 44
   λ: "f" "x",
      let: "p" := install "f" "x" "s" in
      let: "r" := loop "p" "s" "lk" in
Zhen Zhang's avatar
Zhen Zhang committed
45
      "r".
Zhen Zhang's avatar
Zhen Zhang committed
46 47 48 49

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
50
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Zhen Zhang's avatar
Zhen Zhang committed
51
Definition tokmR : ucmraT := evmapR loc toks unitR. (* tie each slot to tokens *)
Zhen Zhang's avatar
Zhen Zhang committed
52 53 54
Class flatG Σ := FlatG {
  req_G :> inG Σ reqR;
  tok_G :> inG Σ (authR tokmR);
Zhen Zhang's avatar
Zhen Zhang committed
55
  sp_G  :> savedPropG Σ (cofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
56 57 58 59
}.

Definition flatΣ : gFunctors :=
  #[ GFunctor (constRF reqR);
Zhen Zhang's avatar
Zhen Zhang committed
60 61
     GFunctor (constRF (authR tokmR));
     savedPropΣ (cofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
62 63 64
   ].

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

Section proof.
Zhen Zhang's avatar
Zhen Zhang committed
68
  Context `{!heapG Σ, !lockG Σ, !evidenceG loc val unitR Σ, !flatG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
69 70 71 72

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

73
  Definition installed_s R (ts: toks) (f x: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
74
    let '(γx, γ1, _, γ4, γq) := ts in
75 76 77
    ( (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
78 79

  Definition received_s (ts: toks) (x: val) γr :=
Zhen Zhang's avatar
Zhen Zhang committed
80 81 82
    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
83
  Definition finished_s (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
84 85 86 87
    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
88 89 90 91

  Definition evm := ev loc toks.
  
  (* p slot invariant *)
92
  Definition p_inv R (γm γr: gname) (v: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
93 94 95 96 97
    ( (ts: toks) (p : loc),
       v = #p  evm γm p ts 
       ((* INIT *)
        ( y: val, p {1/2} InjRV y  init_s ts)
        (* INSTALLED *)
98
        ( f x: val, p {1/2} InjLV (f, x)  installed_s R ts f x) 
Zhen Zhang's avatar
Zhen Zhang committed
99
        (* RECEIVED *)
100
        ( f x: val, p {1/2} InjLV (f, x)  received_s ts x γr) 
Zhen Zhang's avatar
Zhen Zhang committed
101 102 103
        (* FINISHED *)
        ( x y: val, p {1/2} InjRV y  finished_s ts x y)))%I.

104
  Definition srv_stack_inv R γs γm γr s := ( xs, is_stack' (p_inv R γm γr) γs xs s)%I.
Zhen Zhang's avatar
Zhen Zhang committed
105 106 107

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

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

Zhen Zhang's avatar
Zhen Zhang committed
130 131 132
  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
133 134

  Lemma install_spec
135 136 137
        R P Q
        (f x: val) (γs γm γr: gname) (s: loc)
        (Φ: val  iProp Σ):
Zhen Zhang's avatar
Zhen Zhang committed
138
    heapN  N 
139 140
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm) 
    P x  ({{ R  P x }} f x {{ v, R  Q x v }}) 
Zhen Zhang's avatar
Zhen Zhang committed
141
    ( (p: loc) (ts: toks), installed_recp ts x Q - evm γm p ts -( hd, evs γs hd #p) - Φ #p)
142
     WP install f x #s {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
143
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
144
    iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
145
    wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
Zhen Zhang's avatar
Zhen Zhang committed
146 147 148 149 150
    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
151 152
    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
153 154 155 156 157 158
    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
159
      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as "==>[Hm1 #Hm2]"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
160 161
      iDestruct "Hl" as "[Hl1 Hl2]".
      iVs ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
Zhen Zhang's avatar
Zhen Zhang committed
162
      + iNext. iFrame. iExists (<[p := (, DecAgree (γx, γ1, γ3, γ4, γq))]> m). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
163 164
        iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
        iSplitL "Hl1"; last by iAssumption. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
165
      + iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
Zhen Zhang's avatar
Zhen Zhang committed
166 167
        iVsIntro. wp_let. wp_bind ((push _) _).
        iApply install_push_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
168 169
        iFrame "#". rewrite /evm /installed_s. iFrame.
        iSplitL "Hpx Hf".
Zhen Zhang's avatar
Zhen Zhang committed
170
        { iExists P, Q. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
171
        iIntros "Hhd". wp_seq. iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
172
        iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
Zhen Zhang's avatar
Zhen Zhang committed
173
        { rewrite /installed_recp. iFrame. iFrame "#". }
Zhen Zhang's avatar
Zhen Zhang committed
174
        by iApply ("HΦ" with "[]").
Zhen Zhang's avatar
Zhen Zhang committed
175 176
  Qed.

177
  Lemma loop_iter_doOp_spec R (s hd: loc) (γs γm γr: gname) xs Φ:
Zhen Zhang's avatar
Zhen Zhang committed
178
    heapN  N 
179
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm)  own γr (Excl ())  R 
Zhen Zhang's avatar
Zhen Zhang committed
180
    is_list' γs hd xs  (own γr (Excl ()) - R - Φ #())
181
     WP iter #hd doOp {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
182
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
183
    iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
184 185 186
    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.
187 188
    iVsIntro.
    iDestruct (iter_spec _ (p_inv R γm γr) (fun v => v = #()  own γr (Excl ())  R)%I γs s
Zhen Zhang's avatar
Zhen Zhang committed
189
                         (is_list' γs hd xs  own γr (Excl ())  R)%I (srv_tokm_inv γm) xs hd
190
                         doOp doOp
Zhen Zhang's avatar
Zhen Zhang committed
191 192
                         with "[-Hl1 HΦ]") as "Hiter"=>//.
    - rewrite /f_spec.
Zhen Zhang's avatar
Zhen Zhang committed
193 194 195
      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
196
      iDestruct (dup_is_list' with "[Hls]") as "==>[Hls1 Hls2]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
197 198
      iDestruct "HRs" as (m) "[>Hom HRs]".
      (* acccess *)
Zhen Zhang's avatar
Zhen Zhang committed
199 200 201
      iDestruct (access with "[Hom HRs Hls1]") as (hd'') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
      iDestruct "HRx" as (v') "[>% [Hpinv' >Hhd'']]". inversion H0. subst.
      iDestruct "Hpinv'" as (ts p'') "[>% [>#Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst.
Zhen Zhang's avatar
Zhen Zhang committed
202
      + iDestruct "Hp" as (y) "(>Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
203 204 205
        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
206
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[Hrest Hhd'' Hevm Hp Hs]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
207
          iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
Zhen Zhang's avatar
Zhen Zhang committed
208
          iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
209
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
210
      + iDestruct "Hp" as (f' x') "(Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
211
        wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
212
        iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf & HoQ& Ho1 & Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
213 214 215 216 217
        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
218
        iVs ("Hclose" with "[-Hf Hls2 Ho1 Hx2 HR HoQ Hpx HΦ']").
Zhen Zhang's avatar
Zhen Zhang committed
219 220 221 222
        { 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
223
          iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
224
          iFrame "#". iRight. iRight. iLeft. iExists f', x'. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
225
        iVsIntro. wp_match.
226 227
        wp_proj. wp_proj.
        wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf HR".
Zhen Zhang's avatar
Zhen Zhang committed
228 229
        { iApply "Hf". iFrame. }
        iIntros (v) "[HR HQ]".
Zhen Zhang's avatar
Zhen Zhang committed
230 231 232
        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
233
        iDestruct (dup_is_list' with "[Hls2]") as "==>[Hls2 Hls3]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
234
        iDestruct (access with "[Hom HRs Hls2]") as (hd'''') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
235
        iDestruct "HRx" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H2. subst.
Zhen Zhang's avatar
Zhen Zhang committed
236
        iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>#Hevm2 Hps]]".
Zhen Zhang's avatar
Zhen Zhang committed
237 238
        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
239 240
        {
          iDestruct "Hps" as "[Hp | [Hp | [Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
241
          * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
242
            iApply excl_falso. iFrame.
243
          * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
244
            iApply excl_falso. iFrame.
245
          * iDestruct "Hp" as (? x5) ">(Hp & Hx & Ho2 & Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
246 247 248 249 250 251 252 253
            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 *)
254
              iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
255 256 257 258 259 260 261 262 263
              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
264 265
                  iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
                  iSplitR; first auto. iFrame "Hevm". iRight. iRight.
Zhen Zhang's avatar
Zhen Zhang committed
266
                  iRight. iExists x5, v. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
267
                  iExists Q. iFrame.                  
Zhen Zhang's avatar
Zhen Zhang committed
268 269 270 271
                }
              }
              iApply "HΦ'". by iFrame.
            }
Zhen Zhang's avatar
Zhen Zhang committed
272
            { iExFalso. iApply (map_agree_none' _ _ _ m2)=>//. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
273
          * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
274 275
            iApply excl_falso. iFrame.
        }
Zhen Zhang's avatar
Zhen Zhang committed
276
        { iDestruct (evmap_frag_agree_split with "[]") as "%"; first iFrame "Hevm Hevm2".
Zhen Zhang's avatar
Zhen Zhang committed
277
          inversion H4. subst. by contradiction Hneq. }
278
      + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
279
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
280 281
      + 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
282 283 284 285
        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
286
          iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
Zhen Zhang's avatar
Zhen Zhang committed
287
          iSplitR; auto. iFrame "#". iRight. iRight. iRight. iExists x', y. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
288
          iExists Q. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
289 290
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
    - apply to_of_val.
Zhen Zhang's avatar
Zhen Zhang committed
291
    - rewrite /srv_stack_inv. iFrame "#". iFrame. iIntros "(? & ? & ?)". by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
292 293 294 295
    - 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
296
  Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
Zhen Zhang's avatar
Zhen Zhang committed
297
  Definition finished_recp (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
298 299
    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
300

301
  Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ :
Zhen Zhang's avatar
Zhen Zhang committed
302
    heapN  N 
303
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm) 
Zhen Zhang's avatar
Zhen Zhang committed
304
    is_lock N γlk lk (own γr (Excl ())  R)  Φ #()
305
     WP try_srv lk #s {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
306
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
307
    iIntros (?) "(#? & #? & #? & HΦ)".
308
    wp_seq. wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
309 310 311 312 313
    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
314 315
    iInv N as "[H >Hm]" "Hclose".
    iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
Zhen Zhang's avatar
Zhen Zhang committed
316 317 318
    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. }
319 320
    iVsIntro. wp_let.
    wp_bind (iter _ _).
Zhen Zhang's avatar
Zhen Zhang committed
321
    iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
322
    { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ())  R  v = #()))%I=>//.      
Zhen Zhang's avatar
Zhen Zhang committed
323
      iFrame "#". iFrame. iIntros "? ?". by iFrame. }
324 325 326
    iIntros (f') "[Ho [HR %]]". subst.
    wp_let. iApply release_spec. iFrame "#".
    iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
327
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
328

329 330
  Lemma loop_spec R (p s: loc) (lk: val)
        (γs γr γm γlk: gname) (ts: toks) Φ:
Zhen Zhang's avatar
Zhen Zhang committed
331
    heapN  N 
332
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm) 
Zhen Zhang's avatar
Zhen Zhang committed
333 334 335
    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)
336
     WP loop #p #s lk {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
337
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
338
    iIntros (HN) "(#Hh & #? & #? & Ho3 & #Hev & Hhd & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
339
    iLöb as "IH". wp_rec. repeat wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
340 341 342
    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
343
    iDestruct "Hhd" as (hdp) "Hhd".
Zhen Zhang's avatar
Zhen Zhang committed
344
    destruct (m !! hdp) eqn:Heqn.
Zhen Zhang's avatar
Zhen Zhang committed
345 346 347
    - 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
348 349
      subst. iDestruct (ev_map_witness _ _ _ m with "[Hom Hhd]") as %H=>//; first iFrame.
      rewrite Heqn in H. inversion H. subst.
Zhen Zhang's avatar
Zhen Zhang committed
350 351
      iDestruct (evmap_frag_agree_split with "[Hp']") as "%"; first iFrame "Hev Hp'". subst.
      destruct ts' as [[[[γx γ1] γ3] γ4] γq].
Zhen Zhang's avatar
Zhen Zhang committed
352
      iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
353
      + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
Zhen Zhang's avatar
Zhen Zhang committed
354
        iApply excl_falso. iFrame.
355
      + iDestruct "Hp" as (f x) "(>Hp & Hs')".
Zhen Zhang's avatar
Zhen Zhang committed
356
        wp_load. iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
Zhen Zhang's avatar
Zhen Zhang committed
357 358
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
359
          iFrame. iExists #p. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p.
Zhen Zhang's avatar
Zhen Zhang committed
360
          iSplitR; first auto. iFrame.
361
          iRight. iLeft. iExists f, x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
362
        iVsIntro. wp_match.
363
        wp_bind (try_srv _ _). iApply try_srv_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
364
        iFrame "#". wp_seq.
Zhen Zhang's avatar
Zhen Zhang committed
365
        iAssert ( hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
Zhen Zhang's avatar
Zhen Zhang committed
366
        by iApply ("IH" with "Ho3 Hhd").
367
      + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
368
        wp_load.
Zhen Zhang's avatar
Zhen Zhang committed
369
        iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
Zhen Zhang's avatar
Zhen Zhang committed
370 371
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
372
          iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
Zhen Zhang's avatar
Zhen Zhang committed
373
          iSplitR; first auto. iFrame.
374
          iRight. iRight. iLeft. iExists f, x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
375
        iVsIntro. wp_match.
376
        wp_bind (try_srv _ _). iApply try_srv_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
377
        iFrame "#". wp_seq.
Zhen Zhang's avatar
Zhen Zhang committed
378
        iAssert ( hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
Zhen Zhang's avatar
Zhen Zhang committed
379
        by iApply ("IH" with "Ho3 Hhd").
Zhen Zhang's avatar
Zhen Zhang committed
380
       + iDestruct "Hp" as (x y) "[>Hp Hs']". iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
381
          wp_load. iVs ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
Zhen Zhang's avatar
Zhen Zhang committed
382 383
          { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
            iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
384
            iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
Zhen Zhang's avatar
Zhen Zhang committed
385 386 387
            iSplitR; first auto. iFrame.
            iLeft. iExists y. iFrame. }
          iVsIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
388
          iExists Q. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
389 390 391 392
    - iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame "Hom".
      rewrite /ev. eauto.
  Qed.

393
  Lemma mk_flat_spec: mk_syncer_spec N mk_flat.
Zhen Zhang's avatar
Zhen Zhang committed
394
  Proof.
395
    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
396 397 398 399 400 401 402 403
    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 _).
404
    iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
Zhen Zhang's avatar
Zhen Zhang committed
405
    iFrame "Hh Hm". iIntros (γ s) "#Hss".
Zhen Zhang's avatar
Zhen Zhang committed
406
    wp_let. iVsIntro. iApply "HΦ". rewrite /synced.
407
    iAlways.
408
    iIntros (f). wp_let. iVsIntro. iAlways.
409
    iIntros (P Q x) "#Hf".
Zhen Zhang's avatar
Zhen Zhang committed
410
    iIntros "!# Hp". wp_let.
411 412
    wp_bind (install _ _ _).
    iApply (install_spec R P Q)=>//.
Zhen Zhang's avatar
Zhen Zhang committed
413 414
    iFrame "#". iFrame "Hp". iSplitR; first iApply "Hf".
    iIntros (p [[[[γx γ1] γ3] γ4] γq]) "(Ho3 & Hx & HoQ) Hev Hhd".
415
    wp_let. wp_bind (loop _ _ _).
Zhen Zhang's avatar
Zhen Zhang committed
416
    iApply loop_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
417
    iFrame "#". iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
418 419 420 421
    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.
Zhen Zhang's avatar
Zhen Zhang committed
422
      wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
Zhen Zhang's avatar
Zhen Zhang committed
423
      iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
Zhen Zhang's avatar
Zhen Zhang committed
424
    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
Zhen Zhang's avatar
Zhen Zhang committed
425 426
      iDestruct (own_valid with "Hx") as %[_ H1].
      rewrite pair_op //= dec_agree_ne in H1=>//.
Zhen Zhang's avatar
Zhen Zhang committed
427
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
428 429

End proof.