refinement.v 40.3 KB
Newer Older
1
From Coq.Lists Require Import List.
2
From iris.algebra Require Import csum excl auth list gmap.
3
From iris.program_logic Require Import adequacy ectxi_language.
4

5 6 7 8 9 10
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
  CG_queue MS_queue.
From iris.proofmode Require Import tactics.

11 12
Definition locO := leibnizO loc.

13
Definition queueN : namespace := nroot .@ "queue".
14
Definition nodesN : namespace := nroot .@ "nodes".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
15

16
Definition fracAgreeR : cmraT := prodR fracR (agreeR locO).
17
Definition exlTokR : cmraT := exclR (unitR).
18

19 20 21 22 23 24 25 26 27 28 29
Definition nodeStateR : cmraT := authUR mnatUR.

Definition nodeLive := 0 : mnat.
Definition nodeSentinel := 1 : mnat.
Definition nodeDead := 2 : mnat.

Canonical Structure gnameO := leibnizO gname.

Definition mapUR : ucmraT := gmapUR loc (agreeR (leibnizO (gname * loc))).
Definition nodeUR : ucmraT := authUR (gmapUR loc (agreeR (leibnizO (gname * loc)))).

30
Section Queue_refinement.
31
  Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}.
32 33 34

  Notation D := (prodO valO valO -n> iPropO Σ).

Simon Friis Vindum's avatar
Simon Friis Vindum committed
35 36 37 38 39
  (* Maybe commit this upstream. *)
  Lemma mapsto_exclusive l v1 v2 q : l ↦ᵢ v1 - l ↦ᵢ{q} v2 - False.
    iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]%Qp_not_plus_q_ge_1.
  Qed.

40 41 42 43 44 45 46 47
  (* Repeadetly introduce existential variables. *)
  Ltac iExistsN := repeat iExists _.

  (* Solve a goal that consists of introducing existentials, framing, and picking branches. *)
  Ltac iExistsFrame :=
    (repeat iExistsN || iFrame);
    (done || (iLeft; iExistsFrame) || (iRight; iExistsFrame) || fail "Could not solve goal").

Simon Friis Vindum's avatar
Simon Friis Vindum committed
48 49 50 51 52 53
  (* gname naming conventions:
     - γ for the fractional agreement used at the tail.
     - κ for the authorative finite map used in nodesInv.
     - ι for the authorative sum for the state of nodes.
   *)

54 55 56
  Definition noneV := InjLV UnitV.
  Definition someV v := InjRV v.

Simon Friis Vindum's avatar
Simon Friis Vindum committed
57 58 59
  Local Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).

  Lemma fracAgree_agree γ (q1 q2 : Qp) v1 v2 :
60
    own γ (q1, to_agree v1) - own γ (q2, to_agree v2) - v1 = v2.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
61
  Proof.
62
    iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ Hv%agree_op_invL'].
Simon Friis Vindum's avatar
Simon Friis Vindum committed
63 64 65 66 67 68 69 70 71 72
  Qed.

  Lemma fracAgree_combine γ (q1 q2 : Qp) v1 v2 :
    own γ (q1, to_agree v1)
    - own γ (q2, to_agree v2)
    - own γ ((q1 + q2)%Qp, to_agree v2)  v1 = v2.
  Proof.
    iIntros "Hl1 Hl2". 
    iDestruct (fracAgree_agree with "Hl1 Hl2") as %->.
    iCombine "Hl1 Hl2" as "Hl".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
73
    iDestruct (own_valid with "Hl") as %Hv%pair_valid.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
74 75 76 77 78 79 80 81 82 83 84 85 86
    eauto with iFrame.
  Qed.

  Lemma fracAgree_update γ v w u :
    own γ ( v) - own γ ( w) == own γ (1%Qp, to_agree u).
  Proof.
    iIntros "Hb1 Hb2".
    iDestruct (fracAgree_combine with "Hb1 Hb2") as "[tok <-]".
    rewrite Qp_half_half.
    iApply (own_update with "tok").
    by apply cmra_update_exclusive.
  Qed.

87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
  Lemma node_update ι (x y : mnat) : x  y  own ι ( x) == own ι ( y).
  Proof.
    iIntros. iApply (own_update with "[$]"). by eapply auth_update_auth, mnat_local_update.
  Qed.

  Lemma update_sentinel_dead ι : own ι ( nodeSentinel) == own ι ( nodeDead).
  Proof. iApply node_update. unfold nodeSentinel, nodeDead. lia. Qed.

  Lemma update_live_sentinel ι : own ι ( nodeLive) == own ι ( nodeSentinel).
  Proof. iApply node_update. unfold nodeLive, nodeSentinel. lia. Qed.

  Lemma state_agree ι q p s1 s2 : own ι ({q} s1) - own ι ({p} s2) - s1 = s2.
  Proof.
    iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %E%auth_auth_frac_op_invL.
  Qed.

103 104 105 106 107 108 109 110 111
  Lemma state_leq ι q (s1 s2 : mnat) : own ι ({q} s1) - own ι ( s2) - s2  s1.
  Proof.
    iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ [a%mnat_included _]]%auth_both_frac_valid.
  Qed.

  Definition node_singleton s ι n : mapUR := {[ s := to_agree ((ι, n) : leibnizO (gname * loc))]}.

  Definition node_mapsto κ s ι (n : loc) : iProp Σ :=
    own κ ( {[ s := to_agree ((ι, n) : leibnizO (gname * loc))]} : nodeUR).
112

113 114 115
  (* Represents the information that the location ℓ points to a series of nodes
     correscponding to the list `xs`.
   *)
116
  Fixpoint isNodeList γ κ ( : loc) (xs : list val) : iProp Σ :=
117
    match xs with
Simon Friis Vindum's avatar
Simon Friis Vindum committed
118
    | nil =>  2 q,  ↦ᵢ{1/2} (LocV 2)  2 ↦ᵢ{q} FoldV noneV  own γ ( )
119
    | x :: xs' =>
120
      ( 2 next q ι,
121
          own κ ( {[ 2 := to_agree (ι, next) ]})
122 123 124
         own ι ({1/2} nodeLive)
          ↦ᵢ{q} (LocV 2)  2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
         isNodeList γ κ next xs')
125 126
    end.

127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
  Definition nextNode γ κ into : iProp Σ :=
     n,
      ((* node is nil *) 
         q,
          into ↦ᵢ{1/2} (LocV n)  (* We own half the pointer into the node. *)
          n ↦ᵢ{q} (FoldV noneV) 
          own γ ( into)) (* Proof that ℓp is the actual pointer to nil in the queue. *)
       ((* non-nil *)
         q ιnext next,
          into ↦ᵢ{q} LocV n 
          node_mapsto κ n ιnext next
      ).

  (*
    ℓq is the queue pointer.
    ℓn is the "start" pointer of the node.
  *)
  Definition sentinelInv γ κ ι (q n toNext : loc) : iProp Σ :=
     q x,
      n ↦ᵢ{q} FoldV (someV (PairV x (LocV toNext))) 
        nextNode γ κ toNext 
      ((* ℓ is dead. It has been the sentinel, but no longer is. *)
        (own ι ( nodeDead) 
        (* We know that the node points to a non-nil node. *)
         q' x' b next, toNext ↦ᵢ{q'} LocV next  next ↦ᵢ{q'} FoldV (someV (PairV x' b)))
       (* ℓn is currently the sentinel. *)
        (own ι ({1/2} nodeSentinel) 
        q ↦ᵢ{1/2} (LocV n)) (* We own half the pointer into the sentinel. *)
       (* The node is part of the logical queue. *)
        (own ι ({1/2} nodeLive))).

  (* Predicate expressing that ℓq points to a queue with the values xs *)
Simon Friis Vindum's avatar
Simon Friis Vindum committed
159
  Definition isMSQueue γ κ (τi : D) (q : loc) (xs : list val) : iProp Σ :=
160
    ( sentinel hdPt ι,
Simon Friis Vindum's avatar
Simon Friis Vindum committed
161
        q ↦ᵢ{1/2} (LocV sentinel) (* queue own half the pointer, the sentinels owns the other half. *)
162
         node_mapsto κ sentinel ι hdPt
163
         own ι ({1/2} nodeSentinel)
164
         isNodeList γ κ hdPt xs).
165

166 167 168 169
 (* Ties the map to nodeInv  *)
  Definition map_map γ κ q (m : gmap loc (gname * loc)) : iProp Σ :=
    ([ map] s  a  m, ( ι n, a = (ι, n)  sentinelInv γ κ ι q s n))%I.

170
  Definition nodesInv γ κ q : iProp Σ :=
171
     (m : gmap loc (gname * loc)),
Simon Friis Vindum's avatar
Simon Friis Vindum committed
172
      own κ ( (to_agree <$> m) : nodeUR) 
173
      map_map γ κ q m.
174 175 176 177 178

  Lemma mapUR_alloc (m : mapUR) (i : loc) v :
    m !! i = None   m ~~>  (<[i := to_agree v]> m)   {[ i := to_agree v ]}.
  Proof. intros. by apply auth_update_alloc, alloc_singleton_local_update. Qed.

179 180
  Lemma insert_node_subset γ κ q s ι n m m' :
    m'  m -
181
    m !! s = None -
Simon Friis Vindum's avatar
Simon Friis Vindum committed
182
    own κ ( (to_agree <$> m) : nodeUR) -
183
     (map_map γ κ q m') -
184
    sentinelInv γ κ ι q s n
185
    ==
Simon Friis Vindum's avatar
Simon Friis Vindum committed
186
    own κ ( (to_agree <$> (<[s := (ι, n)]> m)) : nodeUR) 
187
     (map_map γ κ q (<[s := (ι, n)]> m')) 
188 189 190 191 192 193 194 195 196
    node_mapsto κ s ι n.
  Proof.
    iIntros (sub non) "auth mon sentInv".
    iMod (own_update with "auth") as "[auth frag]".
    { apply (mapUR_alloc _ s). rewrite lookup_fmap. rewrite non. done. }
    rewrite fmap_insert.
    iFrame.
    iApply big_sepM_insert. { by eapply lookup_weaken_None. }
    iModIntro.
197
    iExistsFrame.
198 199 200 201 202
  Qed.

  Lemma insert_node γ κ q s ι n m :
    m !! s = None -
    own κ ( (to_agree <$> m) : nodeUR) -
203
    map_map γ κ q m -
204 205 206
    sentinelInv γ κ ι q s n
    ==
    own κ ( (to_agree <$> (<[s := (ι, n)]> m)) : nodeUR) 
207
    map_map γ κ q (<[s := (ι, n)]> m) 
Simon Friis Vindum's avatar
Simon Friis Vindum committed
208
    node_mapsto κ s ι n.
209
  Proof.
210 211 212 213 214 215
    iIntros "% auth mon sentInv".
    iMod (own_update with "auth") as "[auth frag]".
    { apply (mapUR_alloc _ s). rewrite lookup_fmap. rewrite a. done. }
    rewrite fmap_insert.
    iFrame.
    iApply big_sepM_insert; first done.
216
    iExistsFrame.
217 218
  Qed.

219 220
  Lemma map_singleton_included (m : gmap loc (gname * loc)) (l : loc) v :
    ({[l := to_agree v]} : mapUR)  ((to_agree <$> m) : mapUR)  m !! l = Some v.
221
  Proof.
222 223 224 225
    move /singleton_included_l=> -[y].
    rewrite lookup_fmap fmap_Some_equiv => -[[x [-> ->]]].
    by move /Some_included_total /to_agree_included /leibniz_equiv_iff ->.
  Qed.
226

227
  Lemma auth_node_mapsto_Some γ m s ι n :
228 229
    own γ ( (to_agree <$> m) : nodeUR) -
    node_mapsto γ s ι n -
230 231 232 233 234 235
    m !! s = Some (ι, n).
  Proof.
    iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[E%map_singleton_included _]%auth_both_valid.
  Qed.

  Lemma node_mapsto_agree γ s ι ι' n n' :
Simon Friis Vindum's avatar
Simon Friis Vindum committed
236
    node_mapsto γ s ι n - node_mapsto γ s ι' n' - ⌜ι = ι'  ⌜ℓn = n'.
237 238 239 240 241
  Proof.
    iIntros "a b".
    unfold node_mapsto.
    iDestruct (own_valid_2 with "a b") as %Hv.
    rewrite -auth_frag_op in Hv.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
242
    apply (auth_frag_valid (_  _)) in Hv. (* Why is this necessary? *)
243
    rewrite singleton_op in Hv.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
244
    apply singleton_valid, agree_op_invL' in Hv.
245 246 247 248 249
    inversion Hv.
    done.
  Qed.

  (* Reinsert a node that has been taken out. *)
250
  Lemma reinsert_node_Some γ κ q s ι n (m : gmap loc (gname * loc)) :
251
    m !! s = Some (ι, n) 
252
    map_map γ κ q (delete s m) -
253
    sentinelInv γ κ ι q s n
254
    -
255
    map_map γ κ q m.
256 257 258
  Proof.
    iIntros (eq) "mon new".
    iDestruct (big_sepM_insert_delete with "[new $mon]") as "mon".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
259 260
    { iExists ι, n. iFrame. done. }
    rewrite insert_id; done.
261
  Qed.
262 263

  (* Reinsert a node that has been taken out. *)
264 265 266
  Lemma reinsert_node γ κ q s ι n (m : gmap loc (gname * loc)) :
    own κ ( (to_agree <$> m) : nodeUR) -
    node_mapsto κ s ι n -
267
    map_map γ κ q (delete s m) -
268
    sentinelInv γ κ ι q s n
269
    -
270
    own κ ( (to_agree <$> m) : nodeUR) 
271
    map_map γ κ q m.
272
  Proof.
273
    iIntros "ownM frag mon new".
274
    iDestruct (own_valid_2 with "ownM frag") as %[inc _]%auth_both_valid.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
275
    iFrame.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
276
    iApply (reinsert_node_Some with "mon"); first by apply map_singleton_included.
277 278 279
    iFrame.
  Qed.

280 281
  Lemma node_lookup γ κ (ι : gname) (q s n : loc) (m : gmap loc (gname * loc)) :
    own κ ( (to_agree <$> m) : nodeUR) -
282
     map_map γ κ q m -
283
    node_mapsto κ s ι n -
284
     sentinelInv γ κ ι q s n 
285
    own κ ( (to_agree <$> m) : nodeUR) 
286
     map_map γ κ q (delete s m).
287
  Proof.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
288
    iIntros "ownM mon frag".
289
    iDestruct (auth_node_mapsto_Some with "ownM frag") as %S.
290
    iDestruct (big_sepM_later with "mon") as "mon".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
291
    iDestruct (big_sepM_delete with "mon") as "[singl mon]"; first done.
292 293 294 295 296 297
    iDestruct "singl" as (a b) "[eq sentInv]".
    iDestruct (big_sepM_later with "mon") as "mon".
    iFrame.
    iNext.
    iDestruct "eq" as %[= <- <-].
    iFrame.
298
  Qed.
299

Simon Friis Vindum's avatar
Simon Friis Vindum committed
300 301
  Definition queueInv γ κ τi q s lock: iProp Σ :=
    ( xs xs,
Simon Friis Vindum's avatar
Simon Friis Vindum committed
302
        isMSQueue γ κ τi q xs
Simon Friis Vindum's avatar
Simon Friis Vindum committed
303 304
       isCGQueue s xs
       lock ↦ₛ (#v false)
305
       [ list] x ; x  xs ; xs, τi (x, x))%I.
306

307
  (* With the token and the nodeList one can perform a CAS on the last node. *)
308
  Lemma enqueue_cas E γ κ xs x (m : gmap loc (gname * loc)) (sentinel q  2 hdPt nil tail node : loc) :
Simon Friis Vindum's avatar
Simon Friis Vindum committed
309
    {{{
310 311
      ⌜ℓsentinel  node 
      own κ ( (to_agree <$> m) : nodeUR) 
312 313
       map_map γ κ q (delete sentinel m) 
      inv nodesN (nodesInv γ κ q) 
Simon Friis Vindum's avatar
Simon Friis Vindum committed
314 315 316
      nil ↦ᵢ FoldV (InjLV UnitV) 
      tail ↦ᵢ (LocV nil)  (* ℓtail points to the nil node *)
      node ↦ᵢ (FoldV (InjRV (PairV (InjRV x) (LocV tail))))  (* node contains x and points to nil *)
317
       isNodeList γ κ hdPt xs 
Simon Friis Vindum's avatar
Simon Friis Vindum committed
318
       ↦ᵢ{1/2} (LocV 2) 
Simon Friis Vindum's avatar
Simon Friis Vindum committed
319
      own γ ( ) (* Proof that ℓ is the pointer pointing to nil. *)
Simon Friis Vindum's avatar
Simon Friis Vindum committed
320 321 322
    }}}
    CAS (Loc ) (Loc 2) (Loc node) @ E
    {{{ RET (BoolV true);
323 324
       ι,
      own κ ( (to_agree <$> (<[node := (ι, tail)]> m)) : nodeUR) 
325
       map_map γ κ q (delete sentinel (<[node := (ι, tail)]>m)) 
Simon Friis Vindum's avatar
Simon Friis Vindum committed
326
      node ↦ᵢ{1/2} (FoldV (InjRV (PairV (InjRV x) (LocV tail)))) 
327
      isNodeList γ κ hdPt (xs ++ [x]) 
328
      node_mapsto κ node ι tail 
Simon Friis Vindum's avatar
Simon Friis Vindum committed
329 330 331
       ↦ᵢ{1/2} (LocV node)
    }}}.
  Proof.
332
    iIntros (ϕ) "(% & authM & bigSep & #nodesInv & nilPts & tailPts & nodePts & nodeList & ℓPts & tok) Hϕ".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
333 334 335 336 337 338 339
    iInduction xs as [|x' xs'] "IH" forall (hdPt).
    - iDestruct "nilPts" as "[nilPts nilPts']".
      iDestruct "tailPts" as "[tailPts tailPts']".
      iDestruct "nodeList" as (0 q) ">(ℓhdPt & ℓ0Pts &tok')".
      (* We need to be able to conclude that ℓhdPt is equal to ℓ. *)
      iDestruct (fracAgree_agree with "tok tok'") as %<-.
      iDestruct (mapsto_combine with "ℓhdPt ℓPts") as "[ℓpts %]".
340
      inversion_clear H6.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
341 342
      rewrite Qp_half_half.
      iMod (fracAgree_update with "tok tok'") as "[tok tok']".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
343 344 345
      iMod (own_alloc ( nodeLive   _)) as (ι) "[[authNodeState authNodeState'] fragNodeState]".
      { by apply auth_both_valid. }
      destruct (m !! node) as [v|] eqn:Eq.
346 347
      { iDestruct (big_sepM_lookup with "bigSep") as "conj".
        { rewrite lookup_delete_ne; done. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
348 349 350 351
        iDestruct "conj" as (ι0 n) "(>-> & sentInv)".
        iDestruct "sentInv" as (v' q0) "(>nodePts' & _)".
        iDestruct (mapsto_exclusive with "nodePts nodePts'") as %[]. }
      iDestruct "nodePts" as "[nodePts [nodePts' nodePts'']]".
352 353 354 355
      iMod (insert_node_subset _ _ _ _ _ _ m (delete sentinel m) with "[%] [% //] authM bigSep [authNodeState' nodePts'' tok tailPts' nilPts']")
         as "(authM & bigSep & #frag)".
      { apply delete_subseteq. }
      { iExists _, _. iFrame "nodePts''".
356
        iSplitL "tailPts' nilPts' tok"; iExistsFrame. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
357
      iApply (wp_cas_suc with "ℓpts").
358
      iNext. iIntros "[[ℓpts _] [ℓpts' ℓpts'']]".
359 360 361 362
      iApply "Hϕ". iExists _.
      rewrite delete_insert_ne; last done.
      iFrame "frag nodePts". iFrame.
      simpl.
363 364 365
      iExistsN. iFrame "frag nodePts'". iFrame.
      iFrame. iExists _, _. iFrame "tailPts". iFrame.
    - iDestruct "nodeList" as (0 next q ι) "(FOO & BAR & BAZ & HIHI & nodeListTail)".
366
      iApply ("IH" with "authM bigSep nilPts tailPts nodePts nodeListTail ℓPts tok").
367 368
      iNext.
      iDestruct 1 as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & nodeListTail & ℓPts)".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
369
      iApply "Hϕ".
370
      iExistsFrame.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
371
  Qed.
372

373
  (* This lemma has been commited upstream to Iris and will be available in the future. *)
374 375
  Lemma auth_update_core_id_frac {A : ucmraT} (a b : A) `{!CoreId b} q :
    b  a  {q} a ~~> {q} a   b.
376
  Proof. Admitted.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
377

378 379 380 381
  Lemma MS_CG_counter_refinement :
    []  MS_queue log CG_queue :
      (TForall (TProd
                  (TArrow TUnit (TMaybe (TVar 0)))
382
                (TArrow (TVar 0) TUnit)
383 384 385 386 387 388 389 390 391 392 393
               )
      ).
  Proof.
    iIntros (Δ vs ?) "#[Hspec HΓ]".
    iDestruct (interp_env_empty with "HΓ") as "->". iClear "HΓ".
    iIntros (j K) "Hj".
    iApply wp_value.
    iExists (TLamV _). iFrame "Hj". clear j K.
    iAlways. iIntros (τi) "%". iIntros (j K) "Hj /=".
    iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
    iMod (steps_newlock _ j (LetInCtx _ :: K) with "[$Hj]")
Simon Friis Vindum's avatar
Simon Friis Vindum committed
394 395
      as (lock) "[Hj lockPts]"; auto.
    iMod (do_step_pure _ j K with "[$Hj]") as "Hj"; auto.
396
    iApply wp_pure_step_later; auto. iNext.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
397

398
    (* Stepping through the specs allocation *)
Simon Friis Vindum's avatar
Simon Friis Vindum committed
399
    iMod (step_alloc  _ j (LetInCtx _ :: K) with "[$Hj]") as (list) "[Hj listPts']"; auto.
400
    simpl.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
401
    iMod (do_step_pure _ j K with "[$Hj]") as "Hj"; auto.
402 403 404 405 406 407 408 409

    (* Stepping through the initialization of the sentinel *)
    iApply (wp_bind (fill [LetInCtx _])).
    iApply (wp_bind (fill [AllocCtx])).
    iApply (wp_bind (fill [AllocCtx])).
    iApply (wp_bind (fill [PairRCtx (InjLV UnitV); InjRCtx; FoldCtx])).
    iApply (wp_bind (fill [AllocCtx])).
    iApply wp_alloc; first done.
410
    iNext. iIntros (nil) "[nilPts nilPts'] /=".
411
    iApply wp_alloc; first done.
412
    iNext. iIntros (tail) "[tailPts tailPts'] /=".
413 414
    iApply wp_value.
    iApply wp_alloc; first done. iNext.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
415
    iIntros (sentinel) "[sentinelPts sentinelPts'] /=".
416
    iApply wp_alloc; first done. iNext.
417
    iIntros (q) "[qPts qPts'] /=".
418
    iApply wp_pure_step_later; auto. iNext.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
419

420
    (* Allocate the nodes invariant. *)
Simon Friis Vindum's avatar
Simon Friis Vindum committed
421 422
    iMod (own_alloc ( nodeSentinel   nodeSentinel))
      as (ι) "[[authNodeSentinel authNodeSentinel'] fragNodeSentinel]".
423
    { by apply auth_both_valid. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
424 425
    iMod (own_alloc ( (node_singleton sentinel ι  tail)   (node_singleton sentinel ι tail))) as (κ) "ownO".
    { apply auth_both_valid. split; first done. apply singleton_valid. done. }
426
    iDestruct "ownO" as "[authO fragO]".
427 428 429
    (* We now want to allocate the invariant for the queue. To do that we first
       establish the node invariant for the empty node we have created. *)
    iMod (own_alloc (1%Qp, to_agree tail)) as (γ) "[token1 token2]"; first done.
430
    iMod (inv_alloc nodesN _ (nodesInv _ _ q) with "[authO fragNodeSentinel qPts' authNodeSentinel' sentinelPts' token1 tailPts nilPts]") as "#nodesInv".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
431 432 433
    { iNext.
      iExists {[sentinel := (ι, tail) : leibnizO (gname * loc)]}.
      iSplitL "authO".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
434
      { rewrite map_fmap_singleton. iAssumption. }
435 436
      rewrite /map_map big_sepM_singleton.
      iExistsN. iSplit; auto.
437
      iExists (1/2)%Qp, _. iFrame "sentinelPts'".
438
      iSplitL "tailPts nilPts token1"; iExistsFrame. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
439
    iMod (inv_alloc queueN _ (queueInv _ _ τi q list _)
440
            with "[qPts lockPts listPts' sentinelPts tailPts' nilPts' token2 authNodeSentinel fragO]")
441
      as "#Hinv".
442
    { iNext. iExists [], []. simpl. iExistsFrame. }
443
    iApply wp_value.
444
    iAsimpl.
445 446 447
    iExists (PairV (CG_dequeueV _ _) (CG_enqueueV _ _)).
    simpl. rewrite CG_dequeue_to_val CG_enqueue_to_val.
    iFrame.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
448
    clear j K ι sentinel.
449
    iExists (_, _), (_, _).
Simon Friis Vindum's avatar
Simon Friis Vindum committed
450
    iSplitL; first auto.
451
    iSplit.
452 453 454 455
    - (* dequeue *)
      iIntros (vv) "!> [-> ->]".
      iIntros (j K) "Hj". simpl.
      rewrite with_lock_of_val.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
456
      iLöb as "Hlat".
457
      iApply wp_pure_step_later; auto. iNext. iAsimpl.
458
      iApply (wp_bind (fill [LetInCtx _])).
Simon Friis Vindum's avatar
Simon Friis Vindum committed
459
      iInv queueN as (xs xs) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
460
      rewrite /isMSQueue.
461 462
      iDestruct "isMSQ" as (sentinel hdPt ι)
                             "(qPts & >#fragO & >nodeState & nodeList)".
463 464
      iMod (own_update with "nodeState") as "[authNodeState nodeState]".
      { by apply (auth_update_core_id_frac _ nodeSentinel). }
465
      iApply (wp_load with "qPts"). iNext. iIntros "qPts".
466
      iMod ("Hclose" with "[qPts lofal Hlink Hsq authNodeState nodeList]") as "_".
467
      { iNext. iExistsFrame. }
468 469
      simpl.
      iModIntro.
470
      iApply wp_pure_step_later; auto. iNext. iAsimpl.
471 472
      iApply (wp_bind (fill [LetInCtx _])).
      iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
473
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
474 475
      iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)".
      iDestruct "sentInv" as (q x) "([sentinelPts sentinelPts'] & nextNode & rest)".
476 477
      iApply (wp_load with "sentinelPts").
      iNext. iIntros "sentinelPts".
478
      iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' nextNode rest]") as "(authM & bigSep)".
479 480
      { iExistsFrame. }
      iMod ("closeNodesInv" with "[authM bigSep]") as "_". { iExistsFrame. }
481 482
      iModIntro.
      clear m.
483 484 485
      iApply (wp_bind (fill [CaseCtx _ _])).
      iApply wp_pure_step_later; auto. iNext.
      iApply wp_value.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
486 487
      simpl. iAsimpl.
      iApply wp_pure_step_later; auto. iNext. simpl.
488 489 490
      iApply wp_value.
      iApply wp_pure_step_later; auto. iNext.
      iApply (wp_bind (fill [CaseCtx _ _])).
491
      iAsimpl.
492 493 494 495 496
      iApply (wp_bind (fill [UnfoldCtx])).
      iApply (wp_bind (fill [LoadCtx])).
      iApply (wp_bind (fill [LoadCtx])).
      iApply wp_pure_step_later; auto. iNext.
      iApply wp_value. simpl.
497
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
498 499 500
      iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)".
      iDestruct "sentInv" as (q' x') "(sentinelPts' & next & disj)".
      iDestruct "next" as (n) "[Left | Right]".
501
      + (* xs is the empty list *)
502
        iDestruct "Left" as (q0) ">(hdPtPts & [nPts nPts'] & tok)".
503
        simpl.
504 505 506
        iDestruct "disj" as "[>[_ pts] | [sent | >live]]".
        1: { 
          iDestruct "pts" as (q1 x1 b next) "(hdPtPts' & nextPts)".
507
          iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= ->].
508
          iDestruct (mapsto_agree with "nPts nextPts") as %[=].
509
        }
510 511 512 513 514 515
        2: { iDestruct (state_leq with "live nodeState") as %le. inversion le. }
        iDestruct "sent" as ">(authState & qPts)".
        iInv queueN as (xs2 xs2) "(isMSQ & >Hsq & >lofal & Hlink)" "closeQueueInv".
        rewrite /isMSQueue.
        iDestruct "isMSQ" as (sentinel2 hdPt2 ι2)
                             "(>qPts2 & >#fragO' & >nodeState' & nodeList)".
516 517
        (* We can conclude that the queue still points to the same sentinel that
           we read previously. *)
518 519 520
        iDestruct (mapsto_agree with "qPts qPts2") as %[= <-].
        iDestruct (node_mapsto_agree with "fragO fragO'") as %[<- <-].
        iClear "fragO'".
521 522
        (* Since the sentinel is the same and the sentinel points to a cons and
           not a nil the queue cannot be empty. *)
523
        destruct xs2 as [|x2 xs2'].
524
        2: {
525
          iDestruct "nodeList" as (2 next q1 ι0) "(_ & _ & >hdPtPts' & >ℓ2Pts & _)".
526
          iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= <-].
527
          iDestruct (mapsto_agree with "nPts ℓ2Pts") as %[=].
528
        }
529
        destruct xs2 as [|x2' xs2'].
Simon Friis Vindum's avatar
Simon Friis Vindum committed
530
        2: { iDestruct (big_sepL2_length with "Hlink") as ">%". inversion H6. }
531
        simpl.
532 533 534
        (* We now step over the specification code. *)
        iMod (steps_CG_dequeue_nil with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)".
        { solve_ndisj. }
535
        iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts".
536
        (* We now close all the invariants that we opened. *)
537
        iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts authState qPts2 hdPtPts nPts' tok]") as "(authM & bigSep)".
538
        { iExistsN. iFrame. iSplitL "hdPtPts nPts' tok"; iExistsFrame. }
539
        iMod ("closeQueueInv" with "[qPts lofal Hsq nodeList nodeState']") as "_".
540
        { iNext. iExists [], []. simpl. iExistsFrame. }
541
        iModIntro.
542
        iMod ("closeNodesInv" with "[authM bigSep]") as "_".
543
        { iNext. iExistsFrame. }
544
        iModIntro.
545
        iApply (wp_load with "nPts"). iNext. iIntros "otherPts".
546 547 548 549 550 551 552
        iApply wp_pure_step_later; auto. iNext. simpl.
        iApply wp_value. simpl.
        iApply wp_pure_step_later; auto. iNext. simpl.
        iApply wp_value.
        iExists (noneV). iFrame.
        iLeft. iExists (_, _). simpl. done.
      + (* xs is not the empty list *)
553 554
        iDestruct "Right" as (q0 ι2 next) "(>[hdPtPts hdPtPts'] & #nextMapsto)".
        iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts".
555
        simpl.
556
        iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' disj hdPtPts']") as "(authM & bigSep)".
557
        { iExistsFrame. }
558 559 560
        iMod ("closeNodesInv" with "[authM bigSep]") as "_".
        { iNext. iExists _. iFrame. }
        iModIntro. clear m.
561
        iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
562 563 564
        iDestruct (node_lookup with "authM bigSep nextMapsto") as "(nextInv & authM & bigSep)".
        iDestruct "nextInv" as (q2 x2) "([otherPts otherPts'] & rest)".
        iApply (wp_load with "[$otherPts]"). iNext. iIntros "otherPts".
565
        simpl.
566
        iDestruct (reinsert_node with "authM nextMapsto bigSep [otherPts' rest]") as "(authM & bigSep)".
567
        { iExistsFrame. }
568 569 570
        iMod ("closeNodesInv" with "[authM bigSep]") as "_".
        { iNext. iExists _. iFrame. }
        iModIntro. clear m.
571
        iApply wp_pure_step_later; auto. iNext.
572
        iApply wp_value.
573 574
        iApply wp_pure_step_later; auto. iNext.
        iApply (wp_bind (fill [IfCtx _ _])).
575
        iAsimpl.
576 577 578 579
        iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])).
        iApply (wp_bind (fill [LoadCtx])).
        iApply wp_pure_step_later; auto. iNext.
        iApply wp_value. simpl.
580
        iApply (wp_load with "hdPtPts"). iNext. iIntros "hdPtPts".
581
        simpl.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
582
        iInv queueN as (xs2 xs2) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
583
        rewrite /isMSQueue.
584 585
        iDestruct "isMSQ" as (sentinel2 hdPt2 ι')
                             "(>qPts & >#fragO' & >sentinelState & nodeList)".
586
        (* We now open the nodes invariant. *)
587
        iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
588
        iDestruct (node_lookup with "authM bigSep fragO'") as "(sentInv & authM & bigSep)".
589
        iDestruct "sentInv" as (v3 q3)  "(>sentinelPts' & next & [[>ownO _]|[>snd| >ownO]])";
590
        try iDestruct (state_agree with "sentinelState ownO") as %[=].
591 592
        iDestruct "snd" as "(ownO & qPts2)".
        iCombine "sentinelState ownO" as "sentinelState".
593 594
        iDestruct (mapsto_combine with "qPts qPts2") as "[qPts %]".
        rewrite Qp_half_half.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
595
        iDestruct (auth_node_mapsto_Some with "authM fragO'") as %sentSome.
596 597 598 599 600 601 602 603
        destruct (decide (sentinel2 = sentinel)) as [|Hneq]; subst.
        * (* The queue still points to the same sentinel that we read earlier--the CAS succeeds *)
          iApply (wp_cas_suc with "qPts"); auto.
          iNext. iIntros "qPts".
          (* We have opened the queue invariant twice. Since the queue pointer
             still points to the same sentinel a lot of the existential variables
             we receieved the first time around are equal to the ones we have now.
             Establishing this is critical. *)
604
          iDestruct (mapsto_agree with "sentinelPts sentinelPts'") as %[= <- <-].
605
          (* xs2 is not necessarily equal to xs, but, since the CAS succeeded,
606 607
             it still has xs as a prefix. And since we know that xs is a cons xs2
             must also be a cons with the same element. *)
608
          destruct xs2 as [|x2' xs2']; simpl.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
609
          { iDestruct "nodeList" as (2 q1) "(ℓhdPts & ℓ2Pts & tok)".
610 611
            iDestruct (mapsto_agree with "ℓhdPts hdPtPts") as %[= ->].
            iDestruct (mapsto_agree with "otherPts ℓ2Pts") as %[=]. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
612
          destruct xs2 as [|x2' xs2']; first done.
613 614 615
          iDestruct "nodeList" as (tail next q1 ι3) "(#frag & nodeState' & hdPtPts' & tailPts & nodeList)".
          iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= ->].
          iAssert (delete sentinel m !! tail = Some (ι3, next)%I) as %Eq.
616 617 618 619 620 621 622 623
          { iDestruct (auth_node_mapsto_Some with "authM frag") as %Eq.
            destruct (decide (sentinel = tail)) as [->|Neq].
            - (* We derive a contradiction. *)
              iDestruct (node_mapsto_agree with "fragO' frag") as %[-> B].
              iDestruct (state_agree with "nodeState' sentinelState") as %[=].
            - iPureIntro. by apply lookup_delete_Some. }
          (* We lookup the current head of the list/new sentinel. *)
          iDestruct (big_sepM_delete with "bigSep") as "[conjunct bigSep]"; first apply Eq.
624
          iDestruct "conjunct" as (ιtemp temp [= <- <-] q'' x'') "(hdPtPts'' & nn & [[st _]|[[st _]|st]])";
625 626 627
          try iDestruct (state_agree with "st nodeState'") as %[=].
          iCombine "nodeState' st" as "nodeState'".
          iMod (update_live_sentinel with "nodeState'") as "[nodeState1 nodeState2]".
628
          iDestruct (mapsto_agree with "otherPts tailPts") as %[= -> ->].
629 630 631 632
          iDestruct "Hlink" as "[Hτi Hlink]".
          (* We step through the specificaion code. *)
          iMod (steps_CG_dequeue_cons with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)".
          { solve_ndisj. }
633 634 635
          (* We split qPts again such that we can put one half in the sentinel
             invariant and one half directly in the queue invariant. *)
          iDestruct "qPts" as "[qPts qPts']".
636 637
          iMod (update_sentinel_dead with "sentinelState") as "sentinelState".
          (* iDestruct (big_sepM_insert_delete with "[$bigSep]") as "bigSep". *)
638
          iDestruct (reinsert_node_Some with "bigSep [qPts' nodeState2 nn hdPtPts'']") as "bigSep".
639 640
          { done. }
          { iExistsFrame. }
641
          iDestruct (reinsert_node_Some with "bigSep [sentinelPts sentinelState hdPtPts' tailPts]") as "bigSep".
642
          { apply sentSome. }
643 644
          { iDestruct "hdPtPts'" as "[hdPtPts1 hdPtPts2]".
            iDestruct "tailPts" as "[tailPts1 tailPts2]".
645
            iExistsN. iFrame. iSplitL "hdPtPts1"; iExistsFrame. }
646
          iMod ("closeNodesInv" with "[authM bigSep]") as "_".
647
          { iNext. iExistsFrame. }
648
          iModIntro.
649
          (* We are now ready to reestablish the invariant. *)
650
          iMod ("Hclose" with "[qPts lofal Hlink Hsq nodeList nodeState1]") as "_".
651
          { iNext. iExistsFrame. }
652 653 654 655 656 657 658 659 660 661 662
          (* Step over the remainder of the code. *)
          iModIntro. simpl.
          iApply wp_pure_step_later; auto. iNext.
          iApply (wp_bind (fill [CaseCtx _ _; InjRCtx])).
          iApply wp_pure_step_later; auto. iNext.
          iApply wp_value. simpl.
          iApply (wp_bind (fill [InjRCtx])).
          iApply wp_pure_step_later; auto. iNext. simpl.
          iApply wp_value.
          iApply wp_value.
          iExists (InjRV _).
663
          iExistsFrame.
664 665
        * (* The queue no longer points to the same sentinel. This case should
             be easy with lob induction. *)
Simon Friis Vindum's avatar
Simon Friis Vindum committed
666 667 668 669
          iApply (wp_cas_fail with "qPts"). congruence.
          iNext. iIntros "qPts".
          iDestruct "sentinelState" as "[sentinelState sentinelState']".
          iDestruct "qPts" as "[qPts qPts']".
670
          iDestruct (reinsert_node_Some with "bigSep [qPts' fragO' next sentinelState sentinelPts']") as "bigSep".
Simon Friis Vindum's avatar
Simon Friis Vindum committed
671
          { eassumption. }
672
          { iExistsFrame. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
673
          iMod ("closeNodesInv" with "[authM bigSep]") as "_".
674
          { iNext. iExistsFrame. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
675
          iModIntro.
676
          iMod ("Hclose" with "[qPts lofal Hsq nodeList sentinelState' Hlink]") as "_".
677
          { iNext. iExistsFrame. }
Simon Friis Vindum's avatar
Simon Friis Vindum committed
678 679 680
          iModIntro.
          iApply wp_pure_step_later; auto. iNext.
          iApply ("Hlat" with "[$Hj]").
681 682 683 684
    - (* enqueue *)
      iIntros ([v1 v2]) "!> #Hrel".
      iIntros (j K) "Hj". simpl.
      rewrite with_lock_of_val.
685 686
      iApply wp_pure_step_later; auto. iNext.
      iApply (wp_bind (fill [LetInCtx _])).
Simon Friis Vindum's avatar
Simon Friis Vindum committed
687
      iAsimpl.
688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704
      (* Step ove the allocation and creation of the new node. *)
      iApply (wp_bind (fill [PairRCtx (InjRV _); InjRCtx; FoldCtx; AllocCtx])).
      iApply (wp_bind (fill [AllocCtx])).
      iApply wp_alloc; first done.
      iNext. iIntros (nil) "nilPts". simpl.
      iApply wp_alloc; first done.
      iNext. iIntros (tail) "tailPts". simpl.
      iApply wp_alloc; first done.
      iNext. iIntros (node) "nodePts /=".
      iApply wp_pure_step_later; auto. iNext.
      (* Evaluate the argument to the recursive function. *)
      iApply (wp_bind (fill [AppRCtx (RecV _)])).
      iApply (wp_bind (fill [SndCtx])).
      iApply (wp_bind (fill [CaseCtx _ _])).
      iApply (wp_bind (fill [UnfoldCtx])).
      iApply (wp_bind (fill [LoadCtx])).
      simpl.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
705
      iInv queueN as (xs xs) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
706 707
      iDestruct "isMSQ" as (sentinel hdPt ι)
                             "(qPts & >#fragO & >sentState & nodeList)".
708 709
      iApply (wp_load with "qPts").
      iNext. iIntros "qPts". 
710
      iMod ("Hclose" with "[qPts lofal Hlink Hsq sentState nodeList]") as "_".
711
      { iNext. iExistsFrame. }
712
      iModIntro.
713
      (* Lookup node *)
714
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
715 716
      iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)".
      iDestruct "sentInv" as (q x) "([sentinelPts sentinelPts'] & nextNode & rest)".
717 718 719
      iApply (wp_load with "sentinelPts").
      iNext. iIntros "sentinelPts". 
      simpl.
720 721
      iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' nextNode rest]") as "(authM & bigSep)".
      (* Reinsert node *)
722
      { iExistsFrame. }
723
      iMod ("closeNodesInv" with "[authM bigSep]") as "_".
724
      { iNext. iExistsFrame. }
725 726
      iModIntro.
      clear m.
727 728 729 730 731 732
      iApply wp_pure_step_later; auto. iNext.
      iApply wp_value. simpl.
      iApply wp_pure_step_later; auto. iNext. simpl.
      iApply wp_value.
      iApply wp_pure_step_later; auto. iNext.
      iApply wp_value.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
733
      simpl.
734
      (* We are now done evaluating the argument. *)
735
      iLöb as "Hlat" forall (x ι hdPt sentinel q) "fragO".
736
      iApply wp_pure_step_later; auto. iNext. iAsimpl.
737
      iApply (wp_bind (fill [LetInCtx _])).
738
      (* Lookup node *)
739
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
740 741 742
      iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)".
      iDestruct "sentInv" as (q' x') "(sentinelPts' & next & rest)".
      iDestruct "next"