From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode.
From iris.algebra.lib Require Import excl_auth.
From iris.base_logic.lib Require Import invariants.
From iris.base_logic.lib Require Import invariants mono_nat mono_list.
From iris_named_props Require Import custom_syntax.

From lmpmc Require Import basic_queue_spec upstream util.

Definition new_node : val := λ: "data",
  let: "ℓ_node" := AllocN #2 #() in
  "ℓ_node"       <- "data";;
  "ℓ_node" +ₗ #1 <- NONE;;
  "ℓ_node".

Definition new : val := λ: <>,
  let: "ℓ_node" := new_node #() in
  AllocN #2 "ℓ_node".

Definition set_tail : val := rec: "go" "ℓ_q" "ℓ_node" :=
  let: "ℓ_tail" := !("ℓ_q" +ₗ #1) in
  match: !("ℓ_tail" +ₗ #1) with
    NONE =>
      if: CAS ("ℓ_tail" +ₗ #1) NONE (SOME "ℓ_node") then
        #()
      else
        "go" "ℓ_q" "ℓ_node"
  | SOME "ℓ_next" =>
      CAS ("ℓ_q" +ₗ #1) "ℓ_tail" "ℓ_next";;
      "go" "ℓ_q" "ℓ_node"
  end.

Definition enqueue : val := λ: "ℓ_q" "data",
  set_tail "ℓ_q" (new_node "data").

Definition try_dequeue : val := rec: "go" "ℓ_q" :=
  let: "ℓ_head" := !"ℓ_q" in
  match: !("ℓ_head" +ₗ #1) with
    NONE => NONE
  | SOME "ℓ_next" =>
      let: "v" := !"ℓ_next" in
      if: CAS "ℓ_q" "ℓ_head" "ℓ_next" then
        SOME "v"
      else
        "go" "ℓ_q"
  end.

Class basic_queueG Σ := BasicQueueG
  { basic_queue_mono_natG  :: mono_natG Σ;
    basic_queue_mono_listG :: mono_listG (prodO locO valO) Σ; }.

Definition basic_queueΣ : gFunctors :=
  #[ mono_natΣ; mono_listΣ (prodO locO valO) ].

#[global] Instance subG_basic_queueΣ {Σ} : subG basic_queueΣ Σ → basic_queueG Σ.
Proof. solve_inG. Qed.

Section basic_queue.
  Context `{!heapGS Σ, !basic_queueG Σ}.

  Record gstate :=
    { γ_hist : gname;
      γ_hpos : gname; }.
  Definition gstate_to_pair (γ : gstate) :=
    (γ.(γ_hist), γ.(γ_hpos)).
  Definition gstate_of_pair '(γ_hist, γ_hpos) :=
    {| γ_hist := γ_hist; γ_hpos := γ_hpos |}.
  Instance gstate_eq_dec : EqDecision gstate := ltac:(solve_decision).
  Instance gstate_countable : Countable gstate.
  Proof.
    refine {| encode := encode ∘ gstate_to_pair;
              decode := fmap gstate_of_pair ∘ decode; |}.
    intros []. by rewrite /= decode_encode.
  Qed.

  Definition node_repr (ℓ : loc) (data : val) (mℓ_next : option loc) : iProp Σ :=
    ("Hndata" ∷ ℓ        ↦□ data) ∗
    ("Hnnext" ∷ (ℓ +ₗ 1) ↦   loc_opt_hl mℓ_next).

  Definition loc_at (hist : list (loc * val)) i :=
    hist.*1 !! i.
  Definition val_at (hist : list (loc * val)) i :=
    hist.*2 !! i.

  Lemma loc_at_prefix xs xs' i ℓ :
    loc_at xs i = Some ℓ → xs `prefix_of` xs' → loc_at xs' i = Some ℓ.
  Proof.
    unfold loc_at. intros Hxs Hpre.
    eapply prefix_lookup_Some; first exact Hxs.
    by apply prefix_of_fmap.
  Qed.

  Lemma val_at_prefix xs xs' i ℓ :
    val_at xs i = Some ℓ → xs `prefix_of` xs' → val_at xs' i = Some ℓ.
  Proof.
    unfold val_at. intros Hxs Hpre.
    eapply prefix_lookup_Some; first exact Hxs.
    by apply prefix_of_fmap.
  Qed.

  Lemma loc_at_val_at_Some xs i ℓ :
    loc_at xs i = Some ℓ → ∃ v, val_at xs i = Some v.
  Proof.
    unfold loc_at, val_at. rewrite [xs.*2 !! i]list_lookup_fmap.
    intros [[ℓ' v] [-> ->]]%list_lookup_fmap_Some_1. by exists v.
  Qed.

  Lemma loc_at_val_at_combine {hist i ℓ v} :
    loc_at hist i = Some ℓ →
    val_at hist i = Some v →
    hist !! i = Some (ℓ, v).
  Proof.
    unfold loc_at, val_at. intros Hloc Hval.
    rewrite list_lookup_fmap in Hloc.
    rewrite list_lookup_fmap in Hval.
    destruct (hist !! i) as [[ℓ' v']|]; last done.
    simpl in *. congruence.
  Qed.

  Lemma loc_at_Some_length hist i ℓ :
    loc_at hist i = Some ℓ → i < length hist.
  Proof.
    intros Hloc%lookup_lt_Some.
    by rewrite length_fmap in Hloc.
  Qed.

  Lemma loc_at_drop hist n i ℓ :
    loc_at hist (n + i) = Some ℓ →
    loc_at (drop n hist) i = Some ℓ.
  Proof.
    unfold loc_at. intros Hloc.
    by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap.
  Qed.

  Lemma loc_at_drop_2 hist n i :
    loc_at (drop n hist) i = loc_at hist (n + i).
  Proof. by rewrite /loc_at list_lookup_fmap lookup_drop -list_lookup_fmap. Qed.

  Lemma val_at_drop hist n i ℓ :
    val_at hist (n + i) = Some ℓ →
    val_at (drop n hist) i = Some ℓ.
  Proof.
    unfold val_at. intros Hval.
    by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap.
  Qed.

  Definition hist_repr (hist : list (loc * val)) : iProp Σ :=
    [∗ list] i ↦ '(ℓ, data) ∈ hist, node_repr ℓ data (loc_at hist (S i)).

  Lemma hist_repr_peek_1 hist i ℓ data :
    loc_at hist i = Some ℓ →
    val_at hist i = Some data → 
    hist_repr hist -∗
    node_repr ℓ data (loc_at hist (S i)) ∗
    (node_repr ℓ data (loc_at hist (S i)) -∗ hist_repr hist).
  Proof.
    iIntros "%Hloc %Hval Hrepr".
    pose proof (loc_at_val_at_combine Hloc Hval) as Hi.
    iPoseProof (big_sepL_lookup_acc with "Hrepr") as "[Hnode Hclose]".
    { apply Hi. }
    iFrame.
  Qed.

  Lemma hist_repr_peek_2 hist i ℓ :
    loc_at hist i = Some ℓ →
    hist_repr hist -∗
    ∃ data, node_repr ℓ data (loc_at hist (S i)) ∗
            (node_repr ℓ data (loc_at hist (S i)) -∗ hist_repr hist).
  Proof.
    iIntros "%Hloc Hrepr".
    assert (∃ v, val_at hist i = Some v) as [v Hval].
    { by apply loc_at_val_at_Some in Hloc. }
    iExists v. by iApply hist_repr_peek_1.
  Qed.

  Lemma hist_repr_peek_3 hist i ℓ :
    loc_at hist i = Some ℓ →
    hist_repr hist -∗
    (ℓ +ₗ 1) ↦ loc_opt_hl (loc_at hist (S i)) ∗
    ((ℓ +ₗ 1) ↦ loc_opt_hl (loc_at hist (S i)) -∗ hist_repr hist).
  Proof.
    iIntros "%Hloc Hrepr".
    iDestruct (hist_repr_peek_2 with "[$]") as "(%v & @ & Hclose)"; first done.
    iFrame. iIntros "Hnnext". iApply "Hclose". iFrame.
  Qed.

  Lemma loc_at_None hist pos :
    loc_at hist pos = None → hist !! pos = None.
  Proof.
    rewrite /loc_at list_lookup_fmap.
    by destruct (hist !! pos).
  Qed.

  Lemma loc_at_length hist pos :
    loc_at hist pos = None → length hist ≤ pos.
  Proof.
    intros H%loc_at_None.
    by apply lookup_ge_None.
  Qed.

  Lemma hist_repr_proj hist i ℓ :
    loc_at hist i = Some ℓ →
    hist_repr hist -∗
    (∃ v, (ℓ +ₗ 1) ↦ v) ∗ hist_repr (drop (S i) hist).
  Proof.
    iIntros "%Hℓi Hrepr".
    iDestruct (big_sepL_take_drop _ _ (S i) with "Hrepr") as "[Hrepr1 Hrepr2]".

    rewrite /loc_at list_lookup_fmap in Hℓi.
    destruct (hist !! i) as [[ℓ' v]|] eqn:Hi; last done.
    simpl in *. injection Hℓi as ->.

    iDestruct (big_sepL_lookup_acc with "Hrepr1") as "[Hrepr Hclose]".
    { rewrite lookup_take_lt //. lia. }
    iSimplifyEq. iDestruct "Hrepr" as "@". iFrame.
    iClear "Hndata Hclose".
    
    iAssert (hist_repr (drop (S i) hist)) with "[Hrepr2]" as "Hrepr2".
    { unfold hist_repr. iApply (big_sepL_mono with "Hrepr2").
      iIntros (k [ℓ' v'] Hk) "Hrepr".
      by rewrite loc_at_drop_2 Nat.add_succ_l Nat.add_succ_r. }
    done.
  Qed.

  Lemma loc_at_inj_aux hist i j ℓ :
    i < j →
    loc_at hist i = Some ℓ →
    loc_at hist j = Some ℓ →
    hist_repr hist -∗
    False.
  Proof.
    iIntros "%ij %Hloci %Hlocj Hrepr".
    assert (i < length hist). { by eapply loc_at_Some_length. }
    assert (j < length hist). { by eapply loc_at_Some_length. }
    assert (∃ n, j = S i + n) as [n ->].
    { exists (j - i - 1). lia. }
    iPoseProof (hist_repr_proj hist i ℓ Hloci with "Hrepr") as "[[%ni Hℓi] Hrepr']".
    
    assert (Hlocj' : loc_at (drop (S i) hist) n = Some ℓ).
    { by apply loc_at_drop. }
    
    iPoseProof (hist_repr_proj _ n ℓ Hlocj' with "Hrepr'") as "[[%nj Hℓj] _]".
    by iCombine "Hℓi Hℓj" gives %[? _].
  Qed.

  Lemma loc_at_inj {hist i j ℓ} :
    loc_at hist i = Some ℓ →
    loc_at hist j = Some ℓ →
    hist_repr hist -∗
    ⌜i = j⌝.
  Proof.
    iIntros "%Hloci %Hlocj Hrepr".
    destruct (loc_at_val_at_Some hist i ℓ Hloci) as [vi Hvali].
    destruct (loc_at_val_at_Some hist j ℓ Hlocj) as [vj Hvalj].
    destruct (decide (i < j)) as [Hij|Hij].
    - (* i < j *)
      by iPoseProof (loc_at_inj_aux with "Hrepr") as "H".
    - (* i ≥ j *)
      destruct (decide (j < i)) as [Hji|Hji].
      + (* j < i *)
        by iPoseProof (loc_at_inj_aux with "Hrepr") as "H".
      + (* i = j *)
        iPureIntro. lia.
  Qed.

  Definition queue_repr_1 (γs : gstate) ℓ_q (vs : list val) : iProp Σ :=
    ∃ (hist : list (loc * val)) (ℓ_head ℓ_tail : loc) (hpos tpos : nat),
      ("Hhead"   ∷ ℓ_q ↦ #ℓ_head) ∗
      ("Htail"   ∷ (ℓ_q +ₗ 1) ↦ #ℓ_tail) ∗
      ("Hrepr"   ∷ hist_repr hist) ∗
      ("Hhist●"  ∷ γs.(γ_hist) ↪●ML hist) ∗
      ("Hhpos●"  ∷ γs.(γ_hpos) ↪●MN hpos) ∗
      ("%Hℓhpos" ∷ ⌜loc_at hist hpos = Some ℓ_head⌝) ∗
      ("%Hℓtpos" ∷ ⌜loc_at hist tpos = Some ℓ_tail⌝) ∗
      ("%Hvs"    ∷ ⌜vs = (drop (S hpos) hist).*2⌝).

  Definition queue_repr ℓ_q (vs : list val) : iProp Σ :=
    ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_repr_1 γs ℓ_q vs.

  #[global] Instance queue_repr_timeless ℓ_q vs : Timeless (queue_repr ℓ_q vs) := _.
  
  Lemma new_node_spec data :
    {{{ True }}}
      new_node data
    {{{ (ℓ : loc), RET #ℓ; node_repr ℓ data None }}}.
  Proof.
    iIntros "%Φ _ HΦ". iUnfold new_node. wp_lam.
    wp_alloc ℓ_node as "Hℓ_node"; first done.
    iDestruct (array_cons with "Hℓ_node") as "[Hℓ_node0 Hℓ_node1]".
    iDestruct (array_cons with "Hℓ_node1") as "[Hℓ_node1 _]".
    wp_let. do 2 wp_store.
    iMod (pointsto_persist with "Hℓ_node0") as "Hℓ_node0".
    iModIntro. iApply "HΦ". by iFrame.
  Qed.

  Lemma new_spec :
    {{{ True }}}
      new #()
    {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] }}}.
  Proof.
    iIntros "%Φ _ HΦ".  iUnfold new.
    wp_lam. wp_apply (new_node_spec with "[//]").
    iIntros (ℓ_node) "Hnode". wp_let.

    set ℓ_head := ℓ_node. set ℓ_tail := ℓ_node.
    set hpos := 0. set tpos := 0.
    set hist := [(ℓ_node, #())] : list (loc * val).
    iAssert (hist_repr hist) with "[$Hnode //]" as "Hrepr".

    iMod (mono_list_own_alloc hist) as "[%γ_hist [Hhist● _]]".
    iMod (mono_nat_own_alloc hpos) as "[%γ_hpos [Hhpos● _]]".
    set γs := {| γ_hist := γ_hist; γ_hpos := γ_hpos |}.

    iApply wp_fupd. iApply wp_allocN; [lia|done|].
    iIntros "!> %ℓ [Hℓ [Htok _]]".
    iDestruct (array_cons with "Hℓ") as "[Hℓ0 Hℓ1]".
    iDestruct (array_cons with "Hℓ1") as "[Hℓ1 _]".
    rewrite Loc.add_0.

    iMod (meta_set ⊤ ℓ γs nroot with "Htok") as "Hmeta"; first done.

    iApply "HΦ". iModIntro. iFrame. by iExists tpos.
  Qed.

  Lemma try_bump_tail_spec hist0 tpos ℓ_old ℓ_new ℓ_q γs :
    loc_at hist0 tpos = Some ℓ_old →
    loc_at hist0 (S tpos) = Some ℓ_new →
    γs.(γ_hist) ↪◯ML hist0 -∗
    <<{ ∀∀ vs, queue_repr_1 γs ℓ_q vs }>>
      CAS #(ℓ_q +ₗ 1) #ℓ_old #ℓ_new @ ∅
    <<{ ∃∃ (b : bool), queue_repr_1 γs ℓ_q vs | RET #b }>>.
  Proof.
    iIntros "%Hold %Hnew #Hhist◯ %Φ AU".
    wp_bind (CmpXchg _ _ _)%E.
    iMod "AU" as "(%vs & (%hist1 & %ℓ_head & %ℓ_tail & %hpos & %tpos' & @) & [_ Hclose])".
    iAssert ⌜hist0 `prefix_of` hist1⌝%I as %Hhist01.
    { by iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist◯") as "[_ ?]". }

    destruct (decide (ℓ_tail = ℓ_old)) as [->|].
    - (* The tail has not been updated yet *)
      wp_cmpxchg_suc.

      iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
      { iPureIntro.
        repeat split; try done || lia.
        exists (S tpos). repeat split; try done.
        by eapply loc_at_prefix. }
      iMod ("Hclose" with "[$Hq]") as "HΦ".
      iModIntro. wp_pures. iApply "HΦ".
    - (* The tail has been updated in the meantime *)
      wp_cmpxchg_fail.
      iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
      { iExists tpos'. by iFrameNamed. }
      iMod ("Hclose" with "[$Hq]") as "HΦ".
      iModIntro. wp_pures. iApply "HΦ".
  Qed.

  (* Given a history that is represented, after updating the [next]
     pointer of the current tail node to a new tail node, we obtain a
     new (extended) history (with the new tail node appended). *)
  Lemma hist_repr_snoc hist tpos (ℓ_tail ℓ_new : loc) data :
    length hist = S tpos →
    loc_at hist tpos = Some ℓ_tail →
    node_repr ℓ_new data None -∗
    hist_repr hist -∗
    (ℓ_tail +ₗ 1) ↦ loc_opt_hl None ∗
    ((ℓ_tail +ₗ 1) ↦ loc_opt_hl (Some ℓ_new) -∗ hist_repr (hist ++ [(ℓ_new, data)])).
  Proof.
    unfold loc_at.
    iIntros "%Hhistlen %Hloc @ Hhist".
    rewrite list_lookup_fmap in Hloc.
    destruct (hist !! tpos) as [[ℓ_tail' v_tail]|] eqn:Htpos; last done.
    injection Hloc as ->.
    apply list_elem_of_split_length in Htpos as (hist' & empty & -> & Htpos).
    rewrite length_app length_cons -Htpos in Hhistlen.
    assert (empty = []) as ->. { apply nil_length_inv. lia. }
    clear Hhistlen Htpos.

    iPoseProof (big_sepL_snoc with "Hhist") as "[Hinit Htail]".
    iNamedSuffix "Htail" "_tail".

    iSimplifyEq.
    assert (loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S (length hist')) = None) as ->.
    { apply lookup_ge_None_2. rewrite length_fmap length_app length_cons /=. lia. }
    iFrame "Hnnext_tail". iIntros "Hnnext_tail".
    iSimplifyEq. rewrite /hist_repr.
    iApply big_sepL_snoc.
    iSplitR "Hndata Hnnext".
    - iApply big_sepL_snoc. iSplitL "Hinit".
      + iApply (big_sepL_mono with "Hinit").
        iIntros (k [ℓ v] Hk) "Hrepr".
        assert (loc_at ((hist' ++ [(ℓ_tail, v_tail)]) ++ [(ℓ_new, data)]) (S k) = loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S k)) as ->.
        { rewrite /loc_at !list_lookup_fmap lookup_app_l // length_app /=.
          apply lookup_lt_Some in Hk. lia. }
        done.
      + iFrame.
        rewrite /loc_at list_lookup_fmap lookup_app_r; last first.
        { rewrite length_app /=. lia. }
        by rewrite length_app /= Nat.add_1_r Nat.sub_diag.
    - iFrame.
      rewrite /= /loc_at length_app /= Nat.add_1_r list_lookup_fmap lookup_app_r.
      * by rewrite !length_app /= !Nat.add_1_r Nat.sub_succ -Arith_base.minus_Sn_m_stt // Nat.sub_diag.
      * rewrite length_app /= Nat.add_1_r. lia.
  Qed.

  Lemma set_tail_spec (ℓ_q ℓ_node : loc) data :
    node_repr ℓ_node data None -∗
    <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
      set_tail #ℓ_q #ℓ_node @ ∅
    <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>.
  Proof.
    iIntros "@ %Φ AU". iLöb as "IH". wp_rec.

    wp_pures. wp_bind (! _)%E.
    iMod "AU" as "(%vs & (%γs & #Hγs & %hist0 & %ℓ_head & %ℓ_tail & %hpos & %tpos & @) & [Hclose _])".
    iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯".
    wp_load. iSimpl in "Hrepr".
    rename Hℓtpos into Hℓtpos0.
    iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
    { iExists tpos. by iFrameNamed. }
    iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos hpos vs ℓ_head.
    iModIntro. wp_let. wp_pure.

    wp_bind (! _)%E.
    iMod "AU" as "(%vs & (%γs' & Hγs' & %hist2 & %ℓ_head & %ℓ_tail'' & %hpos & %tpos'' & @) & [Hclose _])".
    iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
    iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist02.
    iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯".
    destruct Hhist02 as [_ Hhist02]. rename Hℓtpos into Hℓtpos2.
    assert (Hℓtpos0'' : loc_at hist2 tpos = Some ℓ_tail).
    { by eapply loc_at_prefix. } clear Hℓtpos0.
    wp_pures.
    iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w & Hnrepr & Hrepr)"; first done.
    iNamedSuffix "Hnrepr" "_tail".
    wp_load.
    iPoseProof ("Hrepr" with "[$]") as "Hrepr".
    iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
    { iExists tpos''. by iFrameNamed. }
    iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos Hℓtpos2 hpos vs ℓ_head ℓ_tail''.
    iModIntro.

    destruct (loc_at hist2 (S tpos)) as [ℓ_next|] eqn:Htpos2.
    + (* it is not the last node *)
      simpl. wp_pures. wp_bind (Snd (CmpXchg _ _ _))%E.
      awp_apply (try_bump_tail_spec with "[//]").
      { apply Hℓtpos0''. }
      { done. }
      rewrite /atomic_acc /=.
      iMod "AU" as "(%vs & (%γs' & Hγs' & Hrepr) & [Hclose _])".
      iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
      iModIntro. iExists vs. iFrame "Hrepr". iSplit.
      * iFrame. iIntros "Hrepr". by iApply ("Hclose" with "[$Hrepr]").
      * iIntros "%b Hrepr".
        iMod ("Hclose" with "[$Hrepr //]") as "AU".
        iModIntro. wp_pures.
        by iApply ("IH" with "[$] [$] [$]").
    + (* it is the last (non-final) node *)
      simpl. wp_pures. wp_bind (CmpXchg _ _ _)%E.

      iMod "AU" as "(%vs & (%γs' & Hγs' & %hist3 & %ℓ_head & %ℓ_tail''' & %hpos & %tpos''' & @) & Hclose)".
      iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
      iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23.
      destruct Hhist23 as [_ Hhist23]. rename Hℓtpos into Hℓtpos3.

      destruct (loc_at hist3 (S tpos)) as [ℓ_tail''''|] eqn:Hrace.
      * (* Another item has been enqueued in the meantime, so the CAS is poised to fail. *)
        iDestruct "Hclose" as "[Hclose _]".

        iDestruct (hist_repr_peek_3 with "[$Hrepr]") as "[Hℓ_tail1 Hrepr]".
        { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. }
        rewrite Hrace /=.
        wp_cmpxchg_fail.
        iSpecialize ("Hrepr" with "Hℓ_tail1").
        iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
        { iExists tpos'''. by iFrameNamed. }
        iMod ("Hclose" with "[$]") as "AU". iModIntro.
        wp_pures. iApply ("IH" with "Hndata Hnnext AU").
      * (* This node is still the tail, so the CAS will succeed. *)
        iDestruct "Hclose" as "[_ Hclose]".

        iAssert ⌜length hist3 = S tpos⌝%I as %Hhist3.
        { apply loc_at_length in Hrace as Hhist3.
          iPureIntro. apply loc_at_prefix with (xs':=hist3) in Hℓtpos0''; last done.
          apply lookup_lt_Some in Hℓtpos0''. rewrite length_fmap in Hℓtpos0''. lia. }

        iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w' & Hℓ_tail3 & Hrepr)".
        { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. }
        iNamedSuffix "Hℓ_tail3" "_tail3".
        iPoseProof ("Hrepr" with "[$]") as "Hrepr". clear w.
        
        iPoseProof (hist_repr_snoc with "[$Hndata $Hnnext] [$Hrepr]") as "[Htnode Henq]".
        { apply Hhist3. }
        { eapply prefix_lookup_Some. apply Hℓtpos0''. by apply prefix_of_fmap. }
        wp_cmpxchg_suc. iSpecialize ("Henq" with "Htnode").

        iMod (mono_list_auth_own_update_app [(ℓ_node, data)] with "Hhist●") as "[Hhist● _]".
        
        iAssert (queue_repr_1 γs ℓ_q (vs ++ [data])) with "[$Hhead $Htail $Hhist● $Hhpos● $Henq]" as "Hq".
        { iExists tpos'''. iPureIntro.
          repeat split; try done.
          - eapply loc_at_prefix; first done.
            by apply prefix_app_r.
          - eapply loc_at_prefix; first done.
            by apply prefix_app_r.
          - rewrite drop_app fmap_app -Hvs.
            f_equal.
            assert (Hhpos : hpos < length hist3).
            { apply lookup_lt_Some in Hℓhpos.
              by rewrite length_fmap in Hℓhpos. }
            by assert (S hpos - length hist3 = 0) as -> by lia. }
        iMod ("Hclose" with "[$]") as "HΦ".
        iModIntro. wp_pures. done.
  Qed.

  Lemma enqueue_spec (ℓ_q : loc) (data : val) :
    ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
        enqueue #ℓ_q data @ ∅
      <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>.
  Proof.
    iIntros "%Φ AU". wp_lam. wp_pures.
    wp_apply (new_node_spec with "[//]") as "%ℓ_node Hnode".
    awp_apply (set_tail_spec with "[$Hnode]").
    rewrite /atomic_acc /=. iMod "AU" as "(%vs & Hrepr & Hclose)".
    iModIntro. iFrame.
  Qed.

  Lemma try_dequeue_spec (ℓ_q : loc) :
    ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
        try_dequeue #ℓ_q @ ∅
      <<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>.
  Proof.
    iIntros "%Φ AU". iLöb as "IH". wp_rec.

    wp_bind (! _)%E.
    iMod "AU" as "(%vs0 & (%γs & #Hγs & %hist0 & %ℓ_head0 & %ℓ_tail0 & %hpos0 & %tpos0 & @) & [Hclose _])".
    iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯".
    iDestruct (mono_nat_lb_own_get with "Hhpos●") as "#Hhpos0◯".
    rename Hℓhpos into Hℓhpos0.
    wp_load.
    iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
    { iExists tpos0. by iFrameNamed. }
    iModIntro. clear vs0 Hvs tpos0 Hℓtpos ℓ_tail0.

    wp_pures. wp_bind (! _)%E.
    iMod "AU" as "(%vs1 & (%γs' & Hγs' & %hist1 & %ℓ_head1 & %ℓ_tail1 & %hpos1 & %tpos1 & @) & Hclose)".
    iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
    iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist1◯".
    iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos01.
    iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist01.
    destruct Hhpos01 as [_ Hhpos01]. destruct Hhist01 as [_ Hhist01].
    assert (Hℓhpos0' : loc_at hist1 hpos0 = Some ℓ_head0).
    { by eapply loc_at_prefix. } clear Hℓhpos0.
    iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%u & @ & Hrepr)"; first done.
    wp_load.
    iSpecialize ("Hrepr" with "[$]").

    destruct (loc_at hist1 (S hpos0)) as [ℓ_headS0|] eqn:Hℓ_headS0.
    - simpl. iDestruct "Hclose" as "[Hclose _]".
      iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
      { iExists tpos1. by iFrameNamed. }
      iModIntro. clear u vs1 Hvs tpos1 Hℓtpos ℓ_tail1.

      wp_pures. wp_bind (! _)%E.
      iMod "AU" as "(%vs2 & (%γs' & Hγs' & %hist2 & %ℓ_head2 & %ℓ_tail2 & %hpos2 & %tpos2 & @) & Hclose)".
      iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
      iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯".
      iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos02.
      iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist1◯") as %Hhist12.
      destruct Hhpos02 as [_ Hhpos02]. destruct Hhist12 as [_ Hhist12].
      assert (Hℓ_headS0' : loc_at hist2 (S hpos0) = Some ℓ_headS0).
      { by eapply loc_at_prefix. } clear Hℓ_headS0.
      apply loc_at_val_at_Some in Hℓ_headS0' as Hval_headS0'.
      destruct Hval_headS0' as [w Hval_headS0'].
      iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done.
      iDestruct "Hndata" as "#Hndata_head".
      wp_load.

      iDestruct "Hclose" as "[Hclose _]".

      iSpecialize ("Hrepr" with "[$]").
      iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
      { iExists tpos2. by iFrameNamed. }
      iModIntro.
      clear vs2 Hvs tpos2 Hℓtpos ℓ_tail2.

      wp_pures.

      wp_bind (CmpXchg _ _ _)%E.
      iMod "AU" as "(%vs3 & (%γs' & Hγs' & %hist3 & %ℓ_head3 & %ℓ_tail3 & %hpos3 & %tpos3 & @) & Hclose)".
      iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
      iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23.
      destruct Hhist23 as [_ Hhist23].
      assert (Hhist13 : hist1 `prefix_of` hist3).
      { by trans hist2. }

      destruct (decide (ℓ_head0 = ℓ_head3)) as [->|Hhead03].
      + iDestruct "Hclose" as "[_ Hclose]".

        wp_cmpxchg_suc.

        assert (Hℓhpos0'' : loc_at hist3 hpos0 = Some ℓ_head3).
        { by eapply loc_at_prefix. } clear Hℓhpos0'.
        iAssert ⌜hpos0 = hpos3⌝%I as %->.
        { by iApply (loc_at_inj with "Hrepr"). }

        simplify_eq/=.

        iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. }
        iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
        { iExists tpos3. iFrameNamed.
          iPureIntro. repeat split; try done.
          - by eapply loc_at_prefix.
          - by rewrite -[S (S _)]Nat.add_1_r -drop_drop [(drop 1 _).*2]fmap_drop. }

        iModIntro. wp_pures.

        assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w).
        { by eapply val_at_prefix. } clear Hval_headS0'.
        unfold val_at in Hval_headS0''.
        rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop /= -head_lookup in Hval_headS0''.
        by rewrite Hval_headS0'' /=.

      + iDestruct "Hclose" as "[Hclose _]".

        wp_cmpxchg_fail.

        iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
        { iExists tpos3. by iFrameNamed. }

        iModIntro. wp_pures. iApply ("IH" with "AU").
    - apply loc_at_length in Hℓ_headS0 as Hhistlen.
      rewrite drop_ge /= in Hvs; last lia. destruct vs1; try done.
      simplify_eq/=.

      iDestruct "Hclose" as "[_ Hclose]".
      iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
      { iExists tpos1. iFrameNamed. iPureIntro.
        rewrite drop_ge //=. lia. }

      iModIntro. wp_pures. iApply "HΦ".
  Qed.

End basic_queue.

Definition basic_queue `{!heapGS Σ, !basic_queueG Σ} : basic_queue_spec.basic_queue Σ.
Proof.
  refine {| basic_queue_spec.new_spec := new_spec;
            basic_queue_spec.enqueue_spec := enqueue_spec;
            basic_queue_spec.try_dequeue_spec := try_dequeue_spec |}.
Defined.

#[global] Typeclasses Opaque queue_repr.