refinement.v

From Coq.Lists Require Import List.
From iris.algebra Require Import csum excl auth list gmap.
From iris.program_logic Require Import adequacy ectxi_language.

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.

Definition locO := leibnizO loc.

Definition queueN : namespace := nroot .@ "queue".
Definition nodesN : namespace := nroot .@ "nodes".

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

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)))).

Section Queue_refinement.
  Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}.

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

  (* 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.

  (* 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").

  (* 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.
   *)

  Definition noneV := InjLV UnitV.
  Definition someV v := InjRV v.

  Local Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).

  Lemma fracAgree_agree γ (q1 q2 : Qp) v1 v2 :
    own γ (q1, to_agree v1) -∗ own γ (q2, to_agree v2) -∗ ⌜v1 = v2⌝.
  Proof.
    iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ Hv%agree_op_invL'].
  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".
    iDestruct (own_valid with "Hl") as %Hv%pair_valid.
    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.

  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.

  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).

  (* Represents the information that the location ℓ points to a series of nodes
     correscponding to the list `xs`.
   *)
  Fixpoint isNodeList γ κ (ℓ : loc) (xs : list val) : iProp Σ :=
    match xs with
    | nil => ∃ ℓ2 q, ℓ ↦ᵢ{1/2} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV noneV ∗ own γ (◓ ℓ)
    | x :: xs' =>
      (∃ ℓ2 ℓnext q ι,
          own κ (◯ {[ ℓ2 := to_agree (ι, ℓnext) ]})
        ∗ own ι (●{1/2} nodeLive)
        ∗ ℓ ↦ᵢ{q} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓnext)))
        ∗ isNodeList γ κ ℓnext xs')
    end.

  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 *)
  Definition isMSQueue γ κ (τi : D) (ℓq : loc) (xsᵢ : list val) : iProp Σ :=
    (∃ ℓsentinel ℓhdPt ι,
        ℓq ↦ᵢ{1/2} (LocV ℓsentinel) (* queue own half the pointer, the sentinels owns the other half. *)
        ∗ node_mapsto κ ℓsentinel ι ℓhdPt
        ∗ own ι (●{1/2} nodeSentinel)
        ∗ isNodeList γ κ ℓhdPt xsᵢ).

 (* 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.

  Definition nodesInv γ κ ℓq : iProp Σ :=
    ∃ (m : gmap loc (gname * loc)),
      own κ (● (to_agree <$> m) : nodeUR) ∗
      map_map γ κ ℓq m.

  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.

  Lemma insert_node_subset γ κ ℓq ℓs ι ℓn m m' :
    ⌜m' ⊆ m⌝ -∗
    ⌜m !! ℓs = None⌝ -∗
    own κ (● (to_agree <$> m) : nodeUR) -∗
    ▷ (map_map γ κ ℓq m') -∗
    sentinelInv γ κ ι ℓq ℓs ℓn
    ==∗
    own κ (● (to_agree <$> (<[ℓs := (ι, ℓn)]> m)) : nodeUR) ∗
    ▷ (map_map γ κ ℓq (<[ℓs := (ι, ℓn)]> m')) ∗
    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.
    iExistsFrame.
  Qed.

  Lemma insert_node γ κ ℓq ℓs ι ℓn m :
    ⌜m !! ℓs = None⌝ -∗
    own κ (● (to_agree <$> m) : nodeUR) -∗
    map_map γ κ ℓq m -∗
    sentinelInv γ κ ι ℓq ℓs ℓn
    ==∗
    own κ (● (to_agree <$> (<[ℓs := (ι, ℓn)]> m)) : nodeUR) ∗
    map_map γ κ ℓq (<[ℓs := (ι, ℓn)]> m) ∗
    node_mapsto κ ℓs ι ℓn.
  Proof.
    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.
    iExistsFrame.
  Qed.

  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.
  Proof.
    move /singleton_included_l=> -[y].
    rewrite lookup_fmap fmap_Some_equiv => -[[x [-> ->]]].
    by move /Some_included_total /to_agree_included /leibniz_equiv_iff ->.
  Qed.

  Lemma auth_node_mapsto_Some γ m ℓs ι ℓn :
    own γ (● (to_agree <$> m) : nodeUR) -∗
    node_mapsto γ ℓs ι ℓn -∗
    ⌜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' :
    node_mapsto γ ℓs ι ℓn -∗ node_mapsto γ ℓs ι' ℓn' -∗ ⌜ι = ι'⌝ ∗ ⌜ℓn = ℓn'⌝.
  Proof.
    iIntros "a b".
    unfold node_mapsto.
    iDestruct (own_valid_2 with "a b") as %Hv.
    rewrite -auth_frag_op in Hv.
    apply (auth_frag_valid (_ ⋅ _)) in Hv. (* Why is this necessary? *)
    rewrite singleton_op in Hv.
    apply singleton_valid, agree_op_invL' in Hv.
    inversion Hv.
    done.
  Qed.

  (* Reinsert a node that has been taken out. *)
  Lemma reinsert_node_Some γ κ ℓq ℓs ι ℓn (m : gmap loc (gname * loc)) :
    m !! ℓs = Some (ι, ℓn) →
    map_map γ κ ℓq (delete ℓs m) -∗
    sentinelInv γ κ ι ℓq ℓs ℓn
    -∗
    map_map γ κ ℓq m.
  Proof.
    iIntros (eq) "mon new".
    iDestruct (big_sepM_insert_delete with "[new $mon]") as "mon".
    { iExists ι, ℓn. iFrame. done. }
    rewrite insert_id; done.
  Qed.

  (* Reinsert a node that has been taken out. *)
  Lemma reinsert_node γ κ ℓq ℓs ι ℓn (m : gmap loc (gname * loc)) :
    own κ (● (to_agree <$> m) : nodeUR) -∗
    node_mapsto κ ℓs ι ℓn -∗
    map_map γ κ ℓq (delete ℓs m) -∗
    sentinelInv γ κ ι ℓq ℓs ℓn
    -∗
    own κ (● (to_agree <$> m) : nodeUR) ∗
    map_map γ κ ℓq m.
  Proof.
    iIntros "ownM frag mon new".
    iDestruct (own_valid_2 with "ownM frag") as %[inc _]%auth_both_valid.
    iFrame.
    iApply (reinsert_node_Some with "mon"); first by apply map_singleton_included.
    iFrame.
  Qed.

  Lemma node_lookup γ κ (ι : gname) (ℓq ℓs ℓn : loc) (m : gmap loc (gname * loc)) :
    own κ (● (to_agree <$> m) : nodeUR) -∗
    ▷ map_map γ κ ℓq m -∗
    node_mapsto κ ℓs ι ℓn -∗
    ▷ sentinelInv γ κ ι ℓq ℓs ℓn ∗
    own κ (● (to_agree <$> m) : nodeUR) ∗
    ▷ map_map γ κ ℓq (delete ℓs m).
  Proof.
    iIntros "ownM mon frag".
    iDestruct (auth_node_mapsto_Some with "ownM frag") as %S.
    iDestruct (big_sepM_later with "mon") as "mon".
    iDestruct (big_sepM_delete with "mon") as "[singl mon]"; first done.
    iDestruct "singl" as (a b) "[eq sentInv]".
    iDestruct (big_sepM_later with "mon") as "mon".
    iFrame.
    iNext.
    iDestruct "eq" as %[= <- <-].
    iFrame.
  Qed.

  Definition queueInv γ κ τi ℓq ℓs ℓlock: iProp Σ :=
    (∃ xsᵢ xsₛ,
        isMSQueue γ κ τi ℓq xsᵢ
      ∗ isCGQueue ℓs xsₛ
      ∗ ℓlock ↦ₛ (#♭v false)
      ∗ [∗ list] xᵢ ; xₛ ∈ xsᵢ ; xsₛ, τi (xᵢ, xₛ))%I.

  (* With the token and the nodeList one can perform a CAS on the last node. *)
  Lemma enqueue_cas E γ κ xs x (m : gmap loc (gname * loc)) (ℓsentinel ℓq ℓ ℓ2 ℓhdPt ℓnil ℓtail ℓnode : loc) :
    {{{
      ⌜ℓsentinel ≠ ℓnode⌝ ∗
      own κ (● (to_agree <$> m) : nodeUR) ∗
      ▷ map_map γ κ ℓq (delete ℓsentinel m) ∗
      inv nodesN (nodesInv γ κ ℓq) ∗
      ℓ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 *)
      ▷ isNodeList γ κ ℓhdPt xs ∗
      ℓ ↦ᵢ{1/2} (LocV ℓ2) ∗
      own γ (◓ ℓ) (* Proof that ℓ is the pointer pointing to nil. *)
    }}}
    CAS (Loc ℓ) (Loc ℓ2) (Loc ℓnode) @ E
    {{{ RET (BoolV true);
      ∃ ι,
      own κ (● (to_agree <$> (<[ℓnode := (ι, ℓtail)]> m)) : nodeUR) ∗
      ▷ map_map γ κ ℓq (delete ℓsentinel (<[ℓnode := (ι, ℓtail)]>m)) ∗
      ℓnode ↦ᵢ{1/2} (FoldV (InjRV (PairV (InjRV x) (LocV ℓtail)))) ∗
      isNodeList γ κ ℓhdPt (xs ++ [x]) ∗
      node_mapsto κ ℓnode ι ℓtail ∗
      ℓ ↦ᵢ{1/2} (LocV ℓnode)
    }}}.
  Proof.
    iIntros (ϕ) "(% & authM & bigSep & #nodesInv & nilPts & tailPts & nodePts & nodeList & ℓPts & tok) Hϕ".
    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 %]".
      inversion_clear H6.
      rewrite Qp_half_half.
      iMod (fracAgree_update with "tok tok'") as "[tok tok']".
      iMod (own_alloc (● nodeLive ⋅ ◯ _)) as (ι) "[[authNodeState authNodeState'] fragNodeState]".
      { by apply auth_both_valid. }
      destruct (m !! ℓnode) as [v|] eqn:Eq.
      { iDestruct (big_sepM_lookup with "bigSep") as "conj".
        { rewrite lookup_delete_ne; done. }
        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'']]".
      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''".
        iSplitL "tailPts' nilPts' tok"; iExistsFrame. }
      iApply (wp_cas_suc with "ℓpts").
      iNext. iIntros "[[ℓpts _] [ℓpts' ℓpts'']]".
      iApply "Hϕ". iExists _.
      rewrite delete_insert_ne; last done.
      iFrame "frag nodePts". iFrame.
      simpl.
      iExistsN. iFrame "frag nodePts'". iFrame.
      iFrame. iExists _, _. iFrame "tailPts". iFrame.
    - iDestruct "nodeList" as (ℓ0 ℓnext q ι) "(FOO & BAR & BAZ & HIHI & nodeListTail)".
      iApply ("IH" with "authM bigSep nilPts tailPts nodePts nodeListTail ℓPts tok").
      iNext.
      iDestruct 1 as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & nodeListTail & ℓPts)".
      iApply "Hϕ".
      iExistsFrame.
  Qed.

  (* This lemma has been commited upstream to Iris and will be available in the future. *)
  Lemma auth_update_core_id_frac {A : ucmraT} (a b : A) `{!CoreId b} q :
    b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
  Proof. Admitted.

  Lemma MS_CG_counter_refinement :
    [] ⊨ MS_queue ≤log≤ CG_queue :
      (TForall (TProd
                  (TArrow TUnit (TMaybe (TVar 0)))
                (TArrow (TVar 0) TUnit)
               )
      ).
  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]")
      as (ℓlock) "[Hj lockPts]"; auto.
    iMod (do_step_pure _ j K with "[$Hj]") as "Hj"; auto.
    iApply wp_pure_step_later; auto. iNext.

    (* Stepping through the specs allocation *)
    iMod (step_alloc  _ j (LetInCtx _ :: K) with "[$Hj]") as (list) "[Hj listPts']"; auto.
    simpl.
    iMod (do_step_pure _ j K with "[$Hj]") as "Hj"; auto.

    (* 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.
    iNext. iIntros (nil) "[nilPts nilPts'] /=".
    iApply wp_alloc; first done.
    iNext. iIntros (tail) "[tailPts tailPts'] /=".
    iApply wp_value.
    iApply wp_alloc; first done. iNext.
    iIntros (ℓsentinel) "[sentinelPts sentinelPts'] /=".
    iApply wp_alloc; first done. iNext.
    iIntros (ℓq) "[qPts qPts'] /=".
    iApply wp_pure_step_later; auto. iNext.

    (* Allocate the nodes invariant. *)
    iMod (own_alloc (● nodeSentinel ⋅ ◯ nodeSentinel))
      as (ι) "[[authNodeSentinel authNodeSentinel'] fragNodeSentinel]".
    { by apply auth_both_valid. }
    iMod (own_alloc (● (node_singleton ℓsentinel ι  tail) ⋅ ◯ (node_singleton ℓsentinel ι tail))) as (κ) "ownO".
    { apply auth_both_valid. split; first done. apply singleton_valid. done. }
    iDestruct "ownO" as "[authO fragO]".
    (* 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.
    iMod (inv_alloc nodesN _ (nodesInv _ _ ℓq) with "[authO fragNodeSentinel qPts' authNodeSentinel' sentinelPts' token1 tailPts nilPts]") as "#nodesInv".
    { iNext.
      iExists {[ℓsentinel := (ι, tail) : leibnizO (gname * loc)]}.
      iSplitL "authO".
      { rewrite map_fmap_singleton. iAssumption. }
      rewrite /map_map big_sepM_singleton.
      iExistsN. iSplit; auto.
      iExists (1/2)%Qp, _. iFrame "sentinelPts'".
      iSplitL "tailPts nilPts token1"; iExistsFrame. }
    iMod (inv_alloc queueN _ (queueInv _ _ τi ℓq list _)
            with "[qPts lockPts listPts' sentinelPts tailPts' nilPts' token2 authNodeSentinel fragO]")
      as "#Hinv".
    { iNext. iExists [], []. simpl. iExistsFrame. }
    iApply wp_value.
    iAsimpl.
    iExists (PairV (CG_dequeueV _ _) (CG_enqueueV _ _)).
    simpl. rewrite CG_dequeue_to_val CG_enqueue_to_val.
    iFrame.
    clear j K ι ℓsentinel.
    iExists (_, _), (_, _).
    iSplitL; first auto.
    iSplit.
    - (* dequeue *)
      iIntros (vv) "!> [-> ->]".
      iIntros (j K) "Hj". simpl.
      rewrite with_lock_of_val.
      iLöb as "Hlat".
      iApply wp_pure_step_later; auto. iNext. iAsimpl.
      iApply (wp_bind (fill [LetInCtx _])).
      iInv queueN as (xs xsₛ) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
      rewrite /isMSQueue.
      iDestruct "isMSQ" as (ℓsentinel ℓhdPt ι)
                             "(qPts & >#fragO & >nodeState & nodeList)".
      iMod (own_update with "nodeState") as "[authNodeState nodeState]".
      { by apply (auth_update_core_id_frac _ nodeSentinel). }
      iApply (wp_load with "qPts"). iNext. iIntros "qPts".
      iMod ("Hclose" with "[qPts lofal Hlink Hsq authNodeState nodeList]") as "_".
      { iNext. iExistsFrame. }
      simpl.
      iModIntro.
      iApply wp_pure_step_later; auto. iNext. iAsimpl.
      iApply (wp_bind (fill [LetInCtx _])).
      iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
      iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)".
      iDestruct "sentInv" as (q x) "([sentinelPts sentinelPts'] & nextNode & rest)".
      iApply (wp_load with "sentinelPts").
      iNext. iIntros "sentinelPts".
      iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' nextNode rest]") as "(authM & bigSep)".
      { iExistsFrame. }
      iMod ("closeNodesInv" with "[authM bigSep]") as "_". { iExistsFrame. }
      iModIntro.
      clear m.
      iApply (wp_bind (fill [CaseCtx _ _])).
      iApply wp_pure_step_later; auto. iNext.
      iApply wp_value.
      simpl. iAsimpl.
      iApply wp_pure_step_later; auto. iNext. simpl.
      iApply wp_value.
      iApply wp_pure_step_later; auto. iNext.
      iApply (wp_bind (fill [CaseCtx _ _])).
      iAsimpl.
      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.
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
      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]".
      + (* xs is the empty list *)
        iDestruct "Left" as (q0) ">(hdPtPts & [nPts nPts'] & tok)".
        simpl.
        iDestruct "disj" as "[>[_ pts] | [sent | >live]]".
        1: { 
          iDestruct "pts" as (q1 x1 b ℓnext) "(hdPtPts' & nextPts)".
          iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= ->].
          iDestruct (mapsto_agree with "nPts nextPts") as %[=].
        }
        2: { iDestruct (state_leq with "live nodeState") as %le. inversion le. }
        iDestruct "sent" as ">(authState & qPts)".
        iInv queueN as (xs2 xsₛ2) "(isMSQ & >Hsq & >lofal & Hlink)" "closeQueueInv".
        rewrite /isMSQueue.
        iDestruct "isMSQ" as (ℓsentinel2 ℓhdPt2 ι2)
                             "(>qPts2 & >#fragO' & >nodeState' & nodeList)".
        (* We can conclude that the queue still points to the same sentinel that
           we read previously. *)
        iDestruct (mapsto_agree with "qPts qPts2") as %[= <-].
        iDestruct (node_mapsto_agree with "fragO fragO'") as %[<- <-].
        iClear "fragO'".
        (* Since the sentinel is the same and the sentinel points to a cons and
           not a nil the queue cannot be empty. *)
        destruct xs2 as [|x2 xs2'].
        2: {
          iDestruct "nodeList" as (ℓ2 next q1 ι0) "(_ & _ & >hdPtPts' & >ℓ2Pts & _)".
          iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= <-].
          iDestruct (mapsto_agree with "nPts ℓ2Pts") as %[=].
        }
        destruct xsₛ2 as [|x2' xsₛ2'].
        2: { iDestruct (big_sepL2_length with "Hlink") as ">%". inversion H6. }
        simpl.
        (* We now step over the specification code. *)
        iMod (steps_CG_dequeue_nil with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)".
        { solve_ndisj. }
        iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts".
        (* We now close all the invariants that we opened. *)
        iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts authState qPts2 hdPtPts nPts' tok]") as "(authM & bigSep)".
        { iExistsN. iFrame. iSplitL "hdPtPts nPts' tok"; iExistsFrame. }
        iMod ("closeQueueInv" with "[qPts lofal Hsq nodeList nodeState']") as "_".
        { iNext. iExists [], []. simpl. iExistsFrame. }
        iModIntro.
        iMod ("closeNodesInv" with "[authM bigSep]") as "_".
        { iNext. iExistsFrame. }
        iModIntro.
        iApply (wp_load with "nPts"). iNext. iIntros "otherPts".
        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 *)
        iDestruct "Right" as (q0 ι2 next) "(>[hdPtPts hdPtPts'] & #nextMapsto)".
        iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts".
        simpl.
        iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' disj hdPtPts']") as "(authM & bigSep)".
        { iExistsFrame. }
        iMod ("closeNodesInv" with "[authM bigSep]") as "_".
        { iNext. iExists _. iFrame. }
        iModIntro. clear m.
        iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
        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".
        simpl.
        iDestruct (reinsert_node with "authM nextMapsto bigSep [otherPts' rest]") as "(authM & bigSep)".
        { iExistsFrame. }
        iMod ("closeNodesInv" with "[authM bigSep]") as "_".
        { iNext. iExists _. iFrame. }
        iModIntro. clear m.
        iApply wp_pure_step_later; auto. iNext.
        iApply wp_value.
        iApply wp_pure_step_later; auto. iNext.
        iApply (wp_bind (fill [IfCtx _ _])).
        iAsimpl.
        iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])).
        iApply (wp_bind (fill [LoadCtx])).
        iApply wp_pure_step_later; auto. iNext.
        iApply wp_value. simpl.
        iApply (wp_load with "hdPtPts"). iNext. iIntros "hdPtPts".
        simpl.
        iInv queueN as (xs2 xsₛ2) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
        rewrite /isMSQueue.
        iDestruct "isMSQ" as (ℓsentinel2 ℓhdPt2 ι')
                             "(>qPts & >#fragO' & >sentinelState & nodeList)".
        (* We now open the nodes invariant. *)
        iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
        iDestruct (node_lookup with "authM bigSep fragO'") as "(sentInv & authM & bigSep)".
        iDestruct "sentInv" as (v3 q3)  "(>sentinelPts' & next & [[>ownO _]|[>snd| >ownO]])";
        try iDestruct (state_agree with "sentinelState ownO") as %[=].
        iDestruct "snd" as "(ownO & qPts2)".
        iCombine "sentinelState ownO" as "sentinelState".
        iDestruct (mapsto_combine with "qPts qPts2") as "[qPts %]".
        rewrite Qp_half_half.
        iDestruct (auth_node_mapsto_Some with "authM fragO'") as %sentSome.
        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. *)
          iDestruct (mapsto_agree with "sentinelPts sentinelPts'") as %[= <- <-].
          (* xs2 is not necessarily equal to xs, but, since the CAS succeeded,
             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. *)
          destruct xs2 as [|x2' xs2']; simpl.
          { iDestruct "nodeList" as (ℓ2 q1) "(ℓhdPts & ℓ2Pts & tok)".
            iDestruct (mapsto_agree with "ℓhdPts hdPtPts") as %[= ->].
            iDestruct (mapsto_agree with "otherPts ℓ2Pts") as %[=]. }
          destruct xsₛ2 as [|xₛ2' xsₛ2']; first done.
          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.
          { 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.
          iDestruct "conjunct" as (ιtemp ℓtemp [= <- <-] q'' x'') "(hdPtPts'' & nn & [[st _]|[[st _]|st]])";
          try iDestruct (state_agree with "st nodeState'") as %[=].
          iCombine "nodeState' st" as "nodeState'".
          iMod (update_live_sentinel with "nodeState'") as "[nodeState1 nodeState2]".
          iDestruct (mapsto_agree with "otherPts tailPts") as %[= -> ->].
          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. }
          (* 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']".
          iMod (update_sentinel_dead with "sentinelState") as "sentinelState".
          (* iDestruct (big_sepM_insert_delete with "[$bigSep]") as "bigSep". *)
          iDestruct (reinsert_node_Some with "bigSep [qPts' nodeState2 nn hdPtPts'']") as "bigSep".
          { done. }
          { iExistsFrame. }
          iDestruct (reinsert_node_Some with "bigSep [sentinelPts sentinelState hdPtPts' tailPts]") as "bigSep".
          { apply sentSome. }
          { iDestruct "hdPtPts'" as "[hdPtPts1 hdPtPts2]".
            iDestruct "tailPts" as "[tailPts1 tailPts2]".
            iExistsN. iFrame. iSplitL "hdPtPts1"; iExistsFrame. }
          iMod ("closeNodesInv" with "[authM bigSep]") as "_".
          { iNext. iExistsFrame. }
          iModIntro.
          (* We are now ready to reestablish the invariant. *)
          iMod ("Hclose" with "[qPts lofal Hlink Hsq nodeList nodeState1]") as "_".
          { iNext. iExistsFrame. }
          (* 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 _).
          iExistsFrame.
        * (* The queue no longer points to the same sentinel. This case should
             be easy with lob induction. *)
          iApply (wp_cas_fail with "qPts"). congruence.
          iNext. iIntros "qPts".
          iDestruct "sentinelState" as "[sentinelState sentinelState']".
          iDestruct "qPts" as "[qPts qPts']".
          iDestruct (reinsert_node_Some with "bigSep [qPts' fragO' next sentinelState sentinelPts']") as "bigSep".
          { eassumption. }
          { iExistsFrame. }
          iMod ("closeNodesInv" with "[authM bigSep]") as "_".
          { iNext. iExistsFrame. }
          iModIntro.
          iMod ("Hclose" with "[qPts lofal Hsq nodeList sentinelState' Hlink]") as "_".
          { iNext. iExistsFrame. }
          iModIntro.
          iApply wp_pure_step_later; auto. iNext.
          iApply ("Hlat" with "[$Hj]").
    - (* enqueue *)
      iIntros ([v1 v2]) "!> #Hrel".
      iIntros (j K) "Hj". simpl.
      rewrite with_lock_of_val.
      iApply wp_pure_step_later; auto. iNext.
      iApply (wp_bind (fill [LetInCtx _])).
      iAsimpl.
      (* 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.
      iInv queueN as (xs xsₛ) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
      iDestruct "isMSQ" as (ℓsentinel ℓhdPt ι)
                             "(qPts & >#fragO & >sentState & nodeList)".
      iApply (wp_load with "qPts").
      iNext. iIntros "qPts". 
      iMod ("Hclose" with "[qPts lofal Hlink Hsq sentState nodeList]") as "_".
      { iNext. iExistsFrame. }
      iModIntro.
      (* Lookup node *)
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
      iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)".
      iDestruct "sentInv" as (q x) "([sentinelPts sentinelPts'] & nextNode & rest)".
      iApply (wp_load with "sentinelPts").
      iNext. iIntros "sentinelPts". 
      simpl.
      iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' nextNode rest]") as "(authM & bigSep)".
      (* Reinsert node *)
      { iExistsFrame. }
      iMod ("closeNodesInv" with "[authM bigSep]") as "_".
      { iNext. iExistsFrame. }
      iModIntro.
      clear m.
      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.
      simpl.
      (* We are now done evaluating the argument. *)
      iLöb as "Hlat" forall (x ι ℓhdPt ℓsentinel q) "fragO".
      iApply wp_pure_step_later; auto. iNext. iAsimpl.
      iApply (wp_bind (fill [LetInCtx _])).
      (* Lookup node *)
      iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
      iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)".
      iDestruct "sentInv" as (q' x') "(sentinelPts' & next & rest)".
      iDestruct "next"