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

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

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

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

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

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

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

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

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

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

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

  Definition init_s (ts: toks) :=
Zhen Zhang's avatar
Zhen Zhang committed
74
    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ())  own γ3 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
75

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

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

Zhen Zhang's avatar
Zhen Zhang committed
86
  Definition finished_s (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
87 88
    let '(γx, γ1, _, γ4, γq) := ts in
    ( Q: val  val  iProp Σ,
Zhen Zhang's avatar
Zhen Zhang committed
89 90
       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
91 92 93 94

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

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

Zhen Zhang's avatar
Zhen Zhang committed
109
  Definition srv_tokm_inv γm := ( m : tokmR, own γm ( m)  [ map] p  _  m,  v, p {1/2} v)%I.
Zhen Zhang's avatar
Zhen Zhang committed
110

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

133
  Definition installed_recp (ts: toks) (x: val) (Q: val  iProp Σ) :=
Zhen Zhang's avatar
Zhen Zhang committed
134
    let '(γx, _, γ3, _, γq) := ts in
Zhen Zhang's avatar
Zhen Zhang committed
135
    (own γ3 (Excl ())  own γx ((1/2)%Qp, DecAgree x)  saved_prop_own γq Q)%I.
Zhen Zhang's avatar
Zhen Zhang committed
136 137

  Lemma install_spec
138 139 140
        R P Q
        (f x: val) (γs γm γr: gname) (s: loc)
        (Φ: val  iProp Σ):
Zhen Zhang's avatar
Zhen Zhang committed
141
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
142 143 144
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm) 
    P  ({{ R  P }} f x {{ v, R  Q v }}) 
    ( (p: loc) (ts: toks), installed_recp ts x Q - evm γm p ts -( hd, evs γs hd #p) - Φ #p)
145
     WP install f x #s {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
146
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
147
    iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
148
    wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
Ralf Jung's avatar
Ralf Jung committed
149 150 151 152 153
    iApply fupd_wp.
    iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
    iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
    iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
    iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
154
    iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) Q) as (γq) "#?".
Zhen Zhang's avatar
Zhen Zhang committed
155
    iInv N as "[Hrs >Hm]" "Hclose".
Zhen Zhang's avatar
Zhen Zhang committed
156 157 158 159 160 161
    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 *)
Ralf Jung's avatar
Ralf Jung committed
162
      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as ">[Hm1 #Hm2]"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
163
      iDestruct "Hl" as "[Hl1 Hl2]".
Ralf Jung's avatar
Ralf Jung committed
164
      iMod ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
Zhen Zhang's avatar
Zhen Zhang committed
165
      + iNext. iFrame. iExists (<[p := (, DecAgree (γx, γ1, γ3, γ4, γq))]> m). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
166 167
        iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
        iSplitL "Hl1"; last by iAssumption. eauto.
Ralf Jung's avatar
Ralf Jung committed
168 169
      + iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
        iModIntro. wp_let. wp_bind ((push _) _).
Zhen Zhang's avatar
Zhen Zhang committed
170
        iApply install_push_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
171 172
        iFrame "#". rewrite /evm /installed_s. iFrame.
        iSplitL "Hpx Hf".
173 174 175 176
        { (* TODO: Something somewhere can be simplified so that we don't have
             to add these dummy arguments any more. *)
          iExists (fun _ => P), (fun _ => Q). by iFrame. }
        iIntros "Hhd". wp_seq. 
Zhen Zhang's avatar
Zhen Zhang committed
177
        iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
Zhen Zhang's avatar
Zhen Zhang committed
178
        { rewrite /installed_recp. iFrame. iFrame "#". }
Zhen Zhang's avatar
Zhen Zhang committed
179
        by iApply ("HΦ" with "[]").
Zhen Zhang's avatar
Zhen Zhang committed
180 181
  Qed.

182
  Lemma loop_iter_doOp_spec R (s hd: loc) (γs γm γr: gname) xs Φ:
Zhen Zhang's avatar
Zhen Zhang committed
183
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
184 185
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm)  own γr (Excl ())  R 
    is_list' γs hd xs  (own γr (Excl ()) - R - Φ #())
186
     WP iter #hd doOp {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
187
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
188
    iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
189
    iApply (iter_spec N (p_inv R γm γr) Φ
Zhen Zhang's avatar
Zhen Zhang committed
190 191
                      (* (fun v => v = #()  own γr (Excl ())  R)%I *)
                      γs s (own γr (Excl ())  R)%I (srv_tokm_inv γm) xs hd doOp doOp
Zhen Zhang's avatar
Zhen Zhang committed
192
            with "[-]")=>//.
Zhen Zhang's avatar
Zhen Zhang committed
193
    - rewrite /f_spec.
Zhen Zhang's avatar
Zhen Zhang committed
194 195 196 197
      iIntros (Φ' x _) "(#Hh & #? & Hev & [Hor HR] & HΦ')".
      iDestruct "Hev" as (xhd) "#Hev".
      wp_rec.  wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
      iDestruct "Hs" as (gxs ghd) "[>Hghd [>Hgxs HRs]]". (* global xs, hd *)
Zhen Zhang's avatar
Zhen Zhang committed
198 199
      iDestruct "HRs" as (m) "[>Hom HRs]".
      (* acccess *)
Zhen Zhang's avatar
Zhen Zhang committed
200 201 202
      iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
      iDestruct (big_sepM_delete_later (perR _) m with "HRs") as "[Hp HRm]"=>//.
      iDestruct "Hp" as (v') "[>% [Hpinv' >Hahd]]". inversion H. subst.
Zhen Zhang's avatar
Zhen Zhang committed
203
      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)".
Ralf Jung's avatar
Ralf Jung committed
205
        wp_load. iMod ("Hclose" with "[-Hor HR Hev HΦ']").
Zhen Zhang's avatar
Zhen Zhang committed
206 207 208
        { iNext. iFrame. iExists gxs, ghd.
          iFrame "Hghd Hgxs". iExists m.
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") 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. }
211
        iModIntro. wp_match. iApply ("HΦ'" with "[Hor HR]"). 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].
Zhen Zhang's avatar
Zhen Zhang committed
214
        iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
Ralf Jung's avatar
Ralf Jung committed
215 216
        iAssert (|==> own γx (((1/2/2)%Qp, DecAgree x') 
                               ((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as ">[Hx1 Hx2]".
Zhen Zhang's avatar
Zhen Zhang committed
217 218 219
        { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
          rewrite -{1}(Qp_div_2 (1/2)%Qp).
          by apply pair_l_frac_op'. }
Ralf Jung's avatar
Ralf Jung committed
220
        iMod ("Hclose" with "[-Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]").
Zhen Zhang's avatar
Zhen Zhang committed
221 222
        { iNext. iFrame. iExists gxs, ghd.
          iFrame "Hghd Hgxs". iExists m.
Zhen Zhang's avatar
Zhen Zhang committed
223 224
          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. }
Ralf Jung's avatar
Ralf Jung committed
227
        iModIntro. wp_match.
228
        wp_proj. wp_proj.
Zhen Zhang's avatar
Zhen Zhang committed
229 230
        wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
        { iApply "Hf'". iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
231
        iIntros (v) "[HR HQ]".
232
        wp_value. iInv N as "[Hs >Hm]" "Hclose".
Zhen Zhang's avatar
Zhen Zhang committed
233 234
        iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
        iDestruct "HRs" as (m') "[>Hom HRs]".
Zhen Zhang's avatar
Zhen Zhang committed
235 236 237
        iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
        iDestruct (big_sepM_delete_later (perR _) m' with "HRs") as "[Hp HRm]"=>//.
        iDestruct "Hp" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H1. 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 241
        inversion H2. subst.
        destruct (decide (γ1 = γ1'  γx = γx'  γ3 = γ3'  γ4 = γ4'  γq = γq'))
          as [[? [? [? [? ?]]]]|Hneq]; subst.
Zhen Zhang's avatar
Zhen Zhang committed
242 243
        {
          iDestruct "Hps" as "[Hp | [Hp | [Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
244
          * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
245
            iApply excl_falso. iFrame.
246
          * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
247
            iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
248 249 250 251 252 253 254 255 256
          * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
            iDestruct "Hm" as (m2) "[Hom2 HRp]".
            iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame.
            iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//.
            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.
Ralf Jung's avatar
Ralf Jung committed
257
            subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ']").
Zhen Zhang's avatar
Zhen Zhang committed
258 259 260 261 262 263 264 265 266 267 268 269
            { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
              iAssert (srv_tokm_inv γm) with "[Hp1 HRp Hom2]" as "HRp".
              { 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''''.
                iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
                iSplitR; first auto. iFrame "Hevm". iRight. iRight.
                iRight. iExists x5, v. iFrame.
                iExists Q. iFrame. 
Zhen Zhang's avatar
Zhen Zhang committed
270 271
              }
            }
Zhen Zhang's avatar
Zhen Zhang committed
272
            iApply "HΦ'". 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 H3. 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)".
Ralf Jung's avatar
Ralf Jung committed
282
        wp_load. iMod ("Hclose" with "[-HΦ' HR Hor]").
Zhen Zhang's avatar
Zhen Zhang committed
283 284
        { iNext. iFrame. iExists gxs, ghd.
          iFrame "Hghd Hgxs". iExists m.
Zhen Zhang's avatar
Zhen Zhang committed
285
          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. }
Ralf Jung's avatar
Ralf Jung committed
289
        iModIntro. wp_match.
Zhen Zhang's avatar
Zhen Zhang committed
290
        iApply "HΦ'". iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
291
    - apply to_of_val.
Zhen Zhang's avatar
Zhen Zhang committed
292 293
    - iFrame "#". iFrame. iIntros "[Hor HR]".
      iApply ("HΦ" with "Hor HR").
Zhen Zhang's avatar
Zhen Zhang committed
294 295
  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
    let '(γx, _, _, _, γq) := ts in
Zhen Zhang's avatar
Zhen Zhang committed
299
    ( 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 
Zhen Zhang's avatar
Zhen Zhang committed
303 304
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm) 
    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.
309 310
    wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
    iNext. iIntros ([]); last by (iIntros; wp_if).
Zhen Zhang's avatar
Zhen Zhang committed
311
    (* acquired the lock *)
312
    iIntros "[Hlocked [Ho2 HR]]".
Zhen Zhang's avatar
Zhen Zhang committed
313
    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]]".
Ralf Jung's avatar
Ralf Jung committed
316 317
    wp_load. iDestruct (dup_is_list' with "[Hxs]") as ">[Hxs1 Hxs2]"; first by iFrame.
    iMod ("Hclose" with "[Hs Hxs1 HRs Hm]").
Zhen Zhang's avatar
Zhen Zhang committed
318
    { iNext. iFrame. iExists xs', hd'. by iFrame. }
Ralf Jung's avatar
Ralf Jung committed
319
    iModIntro. wp_let.
320
    wp_bind (iter _ _).
Zhen Zhang's avatar
Zhen Zhang committed
321
    iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
Zhen Zhang's avatar
Zhen Zhang committed
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
    iIntros (f') "[Ho [HR %]]". subst.
Zhen Zhang's avatar
Zhen Zhang committed
325
    wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
326
    iNext. iIntros. done.
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 
Zhen Zhang's avatar
Zhen Zhang committed
332 333 334 335
    heap_ctx  inv N (srv_stack_inv R γs γm γr s  srv_tokm_inv γm) 
    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')".
Ralf Jung's avatar
Ralf Jung committed
356
        wp_load. iMod ("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. }
Ralf Jung's avatar
Ralf Jung committed
362
        iModIntro. 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.
Ralf Jung's avatar
Ralf Jung committed
369
        iMod ("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. }
Ralf Jung's avatar
Ralf Jung committed
375
        iModIntro. 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)".
Ralf Jung's avatar
Ralf Jung committed
381
          wp_load. iMod ("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
            iSplitR; first auto. iFrame.
            iLeft. iExists y. iFrame. }
Ralf Jung's avatar
Ralf Jung committed
387
          iModIntro. 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Φ".
Ralf Jung's avatar
Ralf Jung committed
396 397
    iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
    iMod (own_alloc ( (: tokmR)   )) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
Zhen Zhang's avatar
Zhen Zhang committed
398 399 400
    iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
    { iExists . iFrame. by rewrite big_sepM_empty. }
    wp_seq. wp_bind (newlock _).
Zhen Zhang's avatar
Zhen Zhang committed
401
    iApply (newlock_spec _ (own γr (Excl ())  R)%I with "[$Hh $Ho2 $HR]")=>//.
402
    iNext. iIntros (lk γlk) "#Hlk".
Zhen Zhang's avatar
Zhen Zhang committed
403
    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".
406
    wp_let. iApply "HΦ". rewrite /synced.
407
    iAlways.
408
    iIntros (f). wp_let. 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.