flat.v 19.6 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2
(* Flat Combiner *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

106
  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
107 108 109

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

110
  Lemma install_push_spec R
Zhen Zhang's avatar
Zhen Zhang committed
111
        (p: loc) (γs γm γr: gname) (ts: toks)
112
        (s: loc) (f x: val) (Φ: val  iProp Σ) :
Zhen Zhang's avatar
Zhen Zhang committed
113
    heapN  N 
114 115 116
    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
117 118 119 120
     WP push #s #p {{ Φ }}.
  Proof.
    iIntros (HN) "(#Hh & #? & Hpm & Hs & Hp & HΦ)".
    rewrite /srv_stack_inv.
121
    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
122 123 124
               with "[-HΦ]") as "Hpush"=>//.
    - iFrame "Hh". iSplitL "Hp Hs Hpm"; last eauto.
      iExists ts. iExists p. iSplit=>//. iFrame "Hpm".
125
      iRight. iLeft. iExists f, x. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
126 127 128 129 130 131
    - iApply wp_wand_r.
      iSplitL "Hpush"; first done.
      iIntros (?) "[? %]". subst.
      by iApply "HΦ".
  Qed.

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

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

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

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

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

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

End proof.