1 files changed, 932 insertions, 0 deletions

diff --git a/theories/fin_queue_proof.v b/theories/fin_queue_proof.v
new file mode 100644
index 0000000..64646ae
--- /dev/null
+++ b/theories/fin_queue_proof.v
@@ -0,0 +1,932 @@
+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 fin_queue_spec upstream util.
+
+Definition new_node : val := λ: "data" "final",
+  let: "ℓ_node" := AllocN #3 #() in
+  "ℓ_node"       <- "data";;
+  "ℓ_node" +ₗ #1 <- NONE;;
+  "ℓ_node" +ₗ #2 <- "final";;
+  "ℓ_node".
+
+Definition new : val := λ: <>,
+  let: "ℓ_node" := new_node #() #false 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" #false).
+
+Definition finalize : val := λ: "ℓ_q" "data",
+  set_tail "ℓ_q" (new_node "data" #true).
+
+Definition try_dequeue : val := rec: "go" "ℓ_q" :=
+  let: "ℓ_head" := !"ℓ_q" in
+  match: !("ℓ_head" +ₗ #1) with
+    NONE => InjR NONE
+  | SOME "ℓ_next" =>
+      if: !("ℓ_next" +ₗ #2) then
+        (* The next node is the final node. We refuse to dequeue and
+           return the data of the final node. *)
+        InjR (SOME !"ℓ_next")
+      else (* [ℓ_next] node type = normal *)
+        let: "v" := !"ℓ_next" in
+        if: CAS "ℓ_q" "ℓ_head" "ℓ_next" then
+          InjL "v"
+        else
+          "go" "ℓ_q"
+  end.
+
+Class fin_queueG Σ := FinQueueG
+  { fin_queue_mono_natG  :: mono_natG Σ;
+    fin_queue_mono_listG :: mono_listG (prodO locO valO) Σ; }.
+
+Definition fin_queueΣ : gFunctors :=
+  #[ mono_natΣ; mono_listΣ (prodO locO valO) ].
+
+#[global] Instance subG_fin_queueΣ {Σ} : subG fin_queueΣ Σ → fin_queueG Σ.
+Proof. solve_inG. Qed.
+
+Section fin_queue.
+  Context `{!heapGS Σ, !fin_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.
+
+  Variant node_next :=
+    | Normal (mℓ_next : option loc)
+    | Final.
+  Instance node_next_eq_dec : EqDecision node_next.
+  Proof. solve_decision. Defined.
+  Definition node_final_hl (n : node_next) := #(bool_decide (n = Final)).
+  Definition node_next_hl (n : node_next) :=
+    match n with
+    | Normal mℓ_next => loc_opt_hl mℓ_next
+    | Final          => NONEV
+    end.
+  
+  Definition node_repr (ℓ : loc) (data : val) (n : node_next) : iProp Σ :=
+    ("Hndata"  ∷ ℓ        ↦□ data) ∗
+    ("Hnnext"  ∷ (ℓ +ₗ 1) ↦   node_next_hl n) ∗
+    ("Hnfinal" ∷ (ℓ +ₗ 2) ↦□ #(bool_decide (n = Final))).
+
+  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 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 next_from (hist : list (loc * val)) fin i :=
+    if fin && bool_decide (S i = length hist) then Final else Normal (loc_at hist (S i)).
+
+  Definition next_from_normal hist fin i v :
+    next_from hist fin i = Normal v →
+    (fin = false ∨ S i ≠ length hist) ∧ loc_at hist (S i) = v.
+  Proof.
+    rewrite /next_from. intros H.
+    destruct fin, (decide (S i = length hist)).
+    - rewrite bool_decide_true //= in H.
+    - rewrite bool_decide_false //= in H.
+      injection H as <-. split; last done. by right.
+    - injection H as <-. split; last done. by left.
+    - injection H as <-. split; last done. by left.
+  Qed.
+
+  Lemma next_from_S ℓv ℓvs fin n :
+    next_from (ℓv :: ℓvs) fin (S n) = next_from ℓvs fin n.
+  Proof.
+    rewrite /next_from /loc_at list_lookup_fmap /= -list_lookup_fmap.
+    erewrite bool_decide_ext; first done. lia.
+  Qed.
+
+  Lemma node_next_hl_next_from hist fin i :
+    node_next_hl (next_from hist fin i) = loc_opt_hl (loc_at hist (S i)).
+  Proof.
+    unfold node_next_hl, next_from.
+    destruct fin, (decide (S i = length hist)) as [Hhist|Hhist]; simpl; try done.
+    - by rewrite bool_decide_true // /loc_at list_lookup_fmap lookup_ge_None_2; last lia.
+    - by rewrite bool_decide_false.
+  Qed.
+
+  Definition hist_repr (hist : list (loc * val)) (fin : bool) : iProp Σ :=
+    [∗ list] i ↦ '(ℓ, data) ∈ hist, node_repr ℓ data (next_from hist fin i).
+
+  Lemma hist_repr_peek_1 hist fin i ℓ data :
+    loc_at hist i = Some ℓ →
+    val_at hist i = Some data → 
+    hist_repr hist fin -∗
+    node_repr ℓ data (next_from hist fin i) ∗
+    (node_repr ℓ data (next_from hist fin i) -∗ hist_repr hist fin).
+  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 fin i ℓ :
+    loc_at hist i = Some ℓ →
+    hist_repr hist fin -∗
+    ∃ data, node_repr ℓ data (next_from hist fin i) ∗
+            (node_repr ℓ data (next_from hist fin i) -∗ hist_repr hist fin).
+  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 fin i ℓ :
+    loc_at hist i = Some ℓ →
+    hist_repr hist fin -∗
+    (ℓ +ₗ 1) ↦ node_next_hl (next_from hist fin i) ∗
+    ((ℓ +ₗ 1) ↦ node_next_hl (next_from hist fin i) -∗ hist_repr hist fin).
+  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 next_from_drop ℓvs fin n i :
+    next_from ℓvs fin (n + i) = next_from (drop n ℓvs) fin i.
+  Proof.
+    rewrite /next_from /loc_at list_lookup_fmap /= -list_lookup_fmap.
+    erewrite bool_decide_ext with (Q:=S i = length (drop n ℓvs)); last first.
+    { rewrite length_drop. lia. }
+    by rewrite fmap_drop list_lookup_fmap lookup_drop -list_lookup_fmap plus_n_Sm.
+  Qed.
+  
+  Lemma hist_repr_proj hist i ℓ fin :
+    loc_at hist i = Some ℓ →
+    hist_repr hist fin -∗
+    (∃ v, (ℓ +ₗ 1) ↦ v) ∗ hist_repr (drop (S i) hist) fin.
+  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 Hnfinal Hclose".
+    
+    iAssert (hist_repr (drop (S i) hist) fin) with "[Hrepr2]" as "Hrepr2".
+    { unfold hist_repr. iApply (big_sepL_mono with "Hrepr2").
+      iIntros (k [ℓ' v'] Hk) "Hrepr".
+      rewrite -next_from_drop; first done. }
+    done.
+  Qed.
+
+  Lemma loc_at_inj_aux hist i j ℓ fin :
+    i < j →
+    loc_at hist i = Some ℓ →
+    loc_at hist j = Some ℓ →
+    hist_repr hist fin -∗
+    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 ℓ fin 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 ℓ fin Hlocj' with "Hrepr'") as "[[%nj Hℓj] _]".
+    by iCombine "Hℓi Hℓj" gives %[? _].
+  Qed.
+
+  Lemma loc_at_inj {hist i j ℓ fin} :
+    loc_at hist i = Some ℓ →
+    loc_at hist j = Some ℓ →
+    hist_repr hist fin -∗
+    ⌜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_γs_dq (hist : list (loc * val)) (hpos : nat) (mfin : option val) : dfrac :=
+    match mfin with
+    | None => DfracOwn 1
+    | Some _ =>
+        if decide (S (S hpos) = length hist)
+        then DfracDiscarded
+        else DfracOwn 1
+    end.
+
+  Lemma queue_γs_dq_cases hist hpos mfin :
+    queue_γs_dq hist hpos mfin = DfracOwn 1 ∨
+    queue_γs_dq hist hpos mfin = DfracDiscarded.
+  Proof.
+    unfold queue_γs_dq.
+    destruct mfin, (decide (S (S hpos) = length hist));
+      (by left) || by right.
+  Qed.
+
+  Definition queue_repr_1 (γs : gstate) ℓ_q (vs : list val) (mfin : option val) : iProp Σ :=
+    ∃ (hist : list (loc * val)) (ℓ_head ℓ_tail : loc) (hpos tpos : nat),
+      ("Hhead"   ∷ ℓ_q ↦ #ℓ_head) ∗
+      (* Not immediately clear whether this can be discarded when the queue is
+         finalized and otherwise emptied *)
+      ("Htail"   ∷ (ℓ_q +ₗ 1) ↦ #ℓ_tail) ∗
+      ("Hrepr"   ∷ hist_repr hist (bool_decide (is_Some mfin))) ∗
+      ("Hhist●"  ∷ γs.(γ_hist) ↪●ML{queue_γs_dq hist hpos mfin} hist) ∗
+      ("Hhpos●"  ∷ γs.(γ_hpos) ↪●MN{queue_γs_dq hist hpos mfin} hpos) ∗
+      ("%Hℓhpos" ∷ ⌜loc_at hist hpos = Some ℓ_head⌝) ∗
+      ("%Hℓtpos" ∷ ⌜loc_at hist tpos = Some ℓ_tail⌝) ∗
+      ("%Hvs"    ∷ ⌜vs ++ option_list mfin = (drop (S hpos) hist).*2⌝).
+
+  Definition queue_fin_1 (γs : gstate) (fin : val) : iProp Σ :=
+    ∃ (hist : list (loc * val)) (hpos : nat),
+      ("Hhist" ∷ γs.(γ_hist) ↪●ML□ hist) ∗
+      ("Hhpos" ∷ γs.(γ_hpos) ↪●MN□ hpos) ∗
+      ("%Hfin" ∷ ⌜val_at hist (S hpos) = Some fin⌝).
+
+  Definition queue_repr ℓ_q (vs : list val) (mfin : option val) : iProp Σ :=
+    ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_repr_1 γs ℓ_q vs mfin.
+
+  #[global] Instance queue_repr_timeless ℓ_q vs mfin : Timeless (queue_repr ℓ_q vs mfin) := _.
+
+  Definition queue_fin ℓ_q (fin : val) : iProp Σ :=
+    ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_fin_1 γs fin.
+
+  #[global] Instance queue_fin_persistent ℓ_q fin : Persistent (queue_fin ℓ_q fin) := _.
+  #[global] Instance queue_fin_timeless ℓ_q fin : Timeless (queue_fin ℓ_q fin) := _.
+
+  Lemma queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin.
+  Proof.
+    iIntros "(%γs & Hγs & @)". simplify_eq/=.
+    assert (Hlen : length (drop (S hpos) hist).*2 = 1) by rewrite -Hvs //.
+    rewrite fmap_drop length_drop length_fmap in Hlen.
+    case_decide; last lia. iFrame. iPureIntro.
+    by rewrite /val_at -[S hpos]Nat.add_0_r -lookup_drop -fmap_drop -Hvs.
+  Qed.
+
+  Lemma queue_fin_agree ℓ vs fin mfin :
+    queue_fin ℓ fin -∗
+    queue_repr ℓ vs mfin -∗
+    ⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝.
+  Proof.
+    iIntros "(%γs & Hγs & @) (%γs' & Hγs' & @)".
+    iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
+    iDestruct (mono_list_auth_own_agree with "Hhist Hhist●") as %[Hfracs <-].
+    iDestruct (mono_nat_auth_own_agree with "Hhpos Hhpos●") as %[_ <-].
+    iPureIntro.
+
+    unfold queue_γs_dq in Hfracs.
+    destruct mfin as [fin'|]; last done.
+    destruct (decide (S (S hpos) = length hist)); last done.
+
+    assert (Hlen : S (length vs) = 1).
+    { rewrite -Nat.add_1_r -(length_app _ [fin']) Hvs length_fmap length_drop -e. lia. }
+    destruct vs; last done. simplify_eq/=.
+
+    by rewrite -Hfin /val_at -[S hpos]Nat.add_0_r -lookup_drop -fmap_drop -Hvs.
+  Qed.
+
+  Lemma hist_weaken {γs} hist hpos mfin :
+    γs.(γ_hist) ↪●ML hist ==∗ γs.(γ_hist) ↪●ML{queue_γs_dq hist hpos mfin} hist.
+  Proof.
+    iIntros "Hhist".
+    destruct (queue_γs_dq_cases hist hpos mfin) as [-> | ->]; first done.
+    by iApply mono_list_auth_own_persist.
+  Qed.
+
+  Lemma hpos_weaken {γs hpos} hist mfin :
+    γs.(γ_hpos) ↪●MN hpos ==∗ γs.(γ_hpos) ↪●MN{queue_γs_dq hist hpos mfin} hpos.
+  Proof.
+    iIntros "Hhist".
+    destruct (queue_γs_dq_cases hist hpos mfin) as [-> | ->]; first done.
+    by iApply mono_nat_own_persist.
+  Qed.
+  
+  Variant new_node_next := NonFinalType | FinalType.
+  Definition new_node_next_red (n : new_node_next) :=
+    match n with
+    | NonFinalType => Normal None
+    | FinalType => Final
+    end.
+  Instance new_node_next_eq_dec : EqDecision new_node_next.
+  Proof. solve_decision. Defined.
+
+  Lemma new_node_spec data (final : bool) :
+    {{{ True }}}
+      new_node data #final
+    {{{ (ℓ : loc), RET #ℓ; node_repr ℓ data (new_node_next_red (if final then FinalType else NonFinalType)) }}}.
+  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ℓ_node12]".
+    iDestruct (array_cons with "Hℓ_node12") as "[Hℓ_node1 Hℓ_node2]".
+    iDestruct (array_cons with "Hℓ_node2") as "[Hℓ_node2 _]".
+    rewrite Loc.add_assoc.
+    wp_let. do 3 wp_store.
+    iMod (pointsto_persist with "Hℓ_node0") as "Hℓ_node0".
+    iMod (pointsto_persist with "Hℓ_node2") as "Hℓ_node2".
+    iModIntro. iApply "HΦ". destruct final; by iFrame.
+  Qed.
+
+  Lemma new_spec :
+    {{{ True }}}
+      new #()
+    {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] None }}}.
+  Proof.
+    iIntros "%Φ _ HΦ".  iUnfold new.
+    wp_lam. wp_apply (new_node_spec with "[//]") as (ℓ_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 false) 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 mfin, queue_repr_1 γs ℓ_q vs mfin }>>
+      CAS #(ℓ_q +ₗ 1) #ℓ_old #ℓ_new @ ∅
+    <<{ ∃∃ (b : bool), queue_repr_1 γs ℓ_q vs mfin | RET #b }>>.
+  Proof.
+    iIntros "%Hold %Hnew #Hhist◯ %Φ AU".
+    wp_bind (CmpXchg _ _ _)%E.
+    iMod "AU" as "(%vs & %fin & (%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 fin) 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 fin) 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 next :
+    length hist = S tpos →
+    loc_at hist tpos = Some ℓ_tail →
+    node_repr ℓ_new data (new_node_next_red next) -∗
+    hist_repr hist false -∗
+    (ℓ_tail +ₗ 1) ↦ node_next_hl (Normal None) ∗
+    ((ℓ_tail +ₗ 1) ↦ node_next_hl (Normal (Some ℓ_new)) -∗ hist_repr (hist ++ [(ℓ_new, data)]) (bool_decide (next = FinalType))).
+  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 Hnfinal Hnnext".
+    - iApply big_sepL_snoc. iSplitL "Hinit".
+      + iApply (big_sepL_mono with "Hinit").
+        iIntros (k [ℓ v] Hk) "Hrepr".
+        unfold next_from. simpl. rewrite [bool_decide (S k = _)]bool_decide_false; last first.
+        { apply lookup_lt_Some in Hk. rewrite !length_app /=. lia. }
+        rewrite andb_false_r /=.
+        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 /next_from /= [bool_decide (S (length hist') = _)]bool_decide_false; last first.
+        { rewrite !length_app /=. lia. }
+        rewrite andb_false_r /= /loc_at list_lookup_fmap lookup_app_r; last first.
+        { rewrite length_app /=. lia. }
+        rewrite length_app /= Nat.add_1_r Nat.sub_diag /=.
+        by iFrame.
+    - iFrame.
+      rewrite /next_from /= /loc_at length_app /= Nat.add_1_r list_lookup_fmap lookup_app_r.
+      * rewrite !length_app /= !Nat.add_1_r [bool_decide (S _ = S _)]bool_decide_true //
+          andb_true_r Nat.sub_succ -Arith_base.minus_Sn_m_stt // Nat.sub_diag /=.
+        destruct next; simpl; iFrame.
+      * rewrite length_app /= Nat.add_1_r. lia.
+  Qed.
+
+  Definition iffinal {A} (n : new_node_next) (a b : A) :=
+    match n with
+    | FinalType => a
+    | NonFinalType => b
+    end.
+  
+  Lemma set_tail_spec (ℓ_q ℓ_node : loc) data next :
+    node_repr ℓ_node data (new_node_next_red next) -∗
+    <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
+      set_tail #ℓ_q #ℓ_node @ ∅
+    <<{ queue_repr ℓ_q (vs ++ iffinal next [] [data]) (iffinal next (Some data) None) | 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 None) 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.
+    iDestruct "Hnfinal_tail" as "#Hnfinal_tail2".
+    iPoseProof ("Hrepr" with "[$]") as "Hrepr".
+    iAssert (queue_repr_1 γs ℓ_q vs None) 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.
+
+    destruct (next_from hist2 false tpos) as [[ℓ_next|]|] eqn:Htpos2; last done.
+    + (* it is not the last node *)
+      simpl. apply next_from_normal in Htpos2 as [Hnext HStpos2]. rewrite HStpos2 /=.
+      
+      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. apply next_from_normal in Htpos2 as [Hnext HStpos2]. rewrite HStpos2 /=.
+      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 /next_from [bool_decide (S _ = _)]bool_decide_false; last first.
+        { apply lookup_lt_Some in Hrace. rewrite length_fmap in Hrace. lia. }
+        rewrite andb_false_r Hrace /=.
+        wp_cmpxchg_fail.
+        iSpecialize ("Hrepr" with "Hℓ_tail1").
+        iAssert (queue_repr_1 γs ℓ_q vs None) 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 Hnfinal 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. }
+        rewrite /next_from [bool_decide (S _ = _)]bool_decide_true // andb_true_r Hrace /=.
+        iNamedSuffix "Hℓ_tail3" "_tail3".
+        iPoseProof ("Hrepr" with "[$]") as "Hrepr". clear w.
+        
+        iPoseProof (hist_repr_snoc with "[$Hndata $Hnfinal $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").
+
+        pose mfin := iffinal next (Some data) None.
+
+        iMod (mono_list_auth_own_update_app [(ℓ_node, data)] with "Hhist●") as "[Hhist● _]".
+        iMod (hpos_weaken (hist3 ++ [(ℓ_node, data)]) mfin with "Hhpos●") as "Hhpos●".
+        iMod (hist_weaken (hist3 ++ [(ℓ_node, data)]) hpos mfin with "Hhist●") as "Hhist●".
+        replace (bool_decide (next = FinalType)) with (bool_decide (is_Some mfin)); last first.
+        { apply bool_decide_ext. destruct next; by cbn. }
+        
+        iAssert (queue_repr_1 γs ℓ_q (vs ++ iffinal next [] [data]) mfin) 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. rewrite /= app_nil_r -app_assoc.
+            f_equal.
+            assert (Hhpos : hpos < length hist3).
+            { apply lookup_lt_Some in Hℓhpos.
+              by rewrite length_fmap in Hℓhpos. }
+            assert (S hpos - length hist3 = 0) as -> by lia.
+            simpl. by destruct next. }
+        iMod ("Hclose" with "[$]") as "HΦ".
+        iModIntro. wp_pures. done.
+  Qed.
+
+  Lemma enqueue_spec (ℓ_q : loc) (data : val) :
+    ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
+        enqueue #ℓ_q data @ ∅
+      <<{ queue_repr ℓ_q (vs ++ [data]) None | 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 finalize_spec (ℓ_q : loc) (data : val) :
+    ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
+        finalize #ℓ_q data @ ∅
+      <<{ queue_repr ℓ_q vs (Some 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. by rewrite app_nil_r.
+  Qed.
+
+  Lemma try_dequeue_spec (ℓ_q : loc) :
+    ⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>>
+        try_dequeue #ℓ_q @ ∅
+      <<{ queue_repr ℓ_q (tail vs) mfin
+        | RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>.
+  Proof.
+    iIntros "%Φ AU". iLöb as "IH". wp_rec.
+
+    wp_bind (! _)%E.
+    iMod "AU" as "(%vs0 & %fin0 & (%γ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 fin0 vs0 Hvs tpos0 Hℓtpos ℓ_tail0.
+
+    wp_pures. wp_bind (! _)%E.
+    iMod "AU" as "(%vs1 & %fin1 & (%γ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 "[$]").
+
+    rewrite node_next_hl_next_from.
+    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 fin1 vs1 Hvs tpos1 Hℓtpos ℓ_tail1.
+
+      wp_pures. wp_bind (! _)%E.
+      iMod "AU" as "(%vs2 & %fin2 & (%γ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.
+
+      destruct (next_from hist2 (bool_decide (is_Some fin2)) (S hpos0)) as [mℓ_next|] eqn:Hnext2.
+      + iDestruct "Hclose" as "[Hclose _]".
+        iEval (rewrite bool_decide_false //).
+
+        iDestruct "Hnfinal" as "#Hnfinal_head".
+        iEval (rewrite bool_decide_false //) in "Hnfinal_head".
+
+        iSpecialize ("Hrepr" with "[$]").
+        iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
+        { iExists tpos2. by iFrameNamed. }
+        iModIntro.
+        clear fin2 vs2 Hvs tpos2 Hℓtpos ℓ_tail2 Hnext2.
+
+        wp_pures. wp_load. wp_pures.
+
+        wp_bind (CmpXchg _ _ _)%E.
+        iMod "AU" as "(%vs3 & %fin3 & (%γ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"). }
+
+          destruct (decide (length (vs3 ++ option_list fin3) = 1)) as [Hvs3|Hvs3].
+          -- destruct fin3 eqn:Hfin3.
+             ++ assert (Hℓ_headS0'' : loc_at hist3 (S hpos3) = Some ℓ_headS0).
+                { by eapply loc_at_prefix. } clear Hℓ_headS0'.
+                assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w).
+                { by eapply val_at_prefix. } clear Hval_headS0'.
+
+                simplify_eq/=.
+                destruct vs3; last first.
+                { rewrite length_app /= Nat.add_1_r in Hvs3. lia. }
+
+                assert (length hist3 = S (S hpos3)).
+                { apply (f_equal length), symmetry in Hvs.
+                  rewrite /= length_fmap length_drop in Hvs. lia. }
+
+                iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done.
+                iClear "Hnnext".
+                rewrite /next_from !andb_true_l [bool_decide (S _ = _)]bool_decide_true //=.
+                by iCombine "Hnfinal_head Hnfinal" gives "[_ %contra]".
+             ++ simplify_eq/=. rewrite app_nil_r in Hvs Hvs3.
+
+                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 /= fmap_drop /= -Nat.add_1_r -drop_drop -fmap_drop -Hvs app_nil_r. }
+
+                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''.
+                destruct vs3; try done.
+                rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop -Hvs /= in Hval_headS0''.
+                by simplify_eq/=.
+          -- assert (S (S hpos3) ≠ length hist3).
+             { rewrite Hvs length_fmap length_drop in Hvs3. lia. }
+
+             assert (queue_γs_dq hist3 hpos3 fin3 = DfracOwn 1) as ->.
+             { unfold queue_γs_dq. by repeat case_match. }
+             iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. }
+             iMod (hpos_weaken hist3 fin3 with "Hhpos●") as "Hhpos●".
+             iMod (hist_weaken hist3 (S hpos3) fin3 with "Hhist●") as "Hhist●".
+
+             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.
+               - rewrite -Nat.add_1_r -drop_drop fmap_drop -Hvs.
+                 destruct fin3; last by rewrite /= !app_nil_r.
+                 by destruct vs3. }
+
+             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 -Hvs in Hval_headS0''.
+
+             destruct vs3; simplify_eq/=; last done.
+             by destruct fin3.
+
+        * 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").
+        
+      + iDestruct "Hclose" as "[_ Hclose]".
+
+        destruct fin2 as [fin2|]; last done. simplify_eq/=.
+        assert (Hhist2 : length hist2 = S (S hpos0)).
+        { destruct (decide (length hist2 = S (S hpos0))); first done.
+          by rewrite /next_from bool_decide_false in Hnext2. }
+        assert (S hpos2 < length hist2).
+        { rewrite -(length_fmap snd).
+          apply lookup_lt_is_Some_1.
+          rewrite -[S hpos2]Nat.add_0_r -lookup_drop -fmap_drop -Hvs.
+          by destruct vs2, fin2. }
+        assert (hpos0 = hpos2) as -> by lia.
+        assert (Hvs2 : length vs2 = 0).
+        { apply eq_add_S. rewrite -Nat.add_1_r -(length_app _ [fin2]) Hvs length_fmap length_drop Hhist2. lia. }
+        destruct vs2; last done. clear Hvs2.
+
+        iSpecialize ("Hrepr" with "[$]").
+        iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
+        { iExists tpos2. by iFrameNamed. }
+
+        iModIntro. clear tpos2 Hℓhpos Hℓtpos ℓ_tail2.
+        
+        wp_pures. wp_load.
+        rewrite /val_at in Hval_headS0'.
+        rewrite -[S hpos2]Nat.add_0_r -lookup_drop -fmap_drop -Hvs in Hval_headS0'.
+        simplify_eq/=. wp_pures. iApply "HΦ".
+    - apply loc_at_length in Hℓ_headS0 as Hhistlen.
+      rewrite drop_ge /= in Hvs; last lia. destruct vs1, fin1; 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 fin_queue.
+
+Definition fin_queue_hl :=
+  {| fin_queue_spec.new := new;
+     fin_queue_spec.enqueue := enqueue;
+     fin_queue_spec.finalize := finalize;
+     fin_queue_spec.try_dequeue := try_dequeue; |}.
+
+Definition fin_queue_iris `{!heapGS Σ, !fin_queueG Σ} : fin_queue_spec.fin_queue_iris Σ fin_queue_hl.
+Proof.
+  refine (FinQueueIris _ _
+            fin_queue_hl _ _ _ _ _
+            queue_fin_obtain
+            queue_fin_agree
+            new_spec
+            enqueue_spec
+            finalize_spec
+            try_dequeue_spec).
+Defined.
+
+#[global] Typeclasses Opaque queue_repr queue_fin.