From e2681e43cc7849d66425d5bc93565e9e177d229a Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 24 Jun 2026 19:29:28 +0200 Subject: Initial commit --- theories/fin_queue_proof.v | 932 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 932 insertions(+) create mode 100644 theories/fin_queue_proof.v (limited to 'theories/fin_queue_proof.v') 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. -- cgit v1.3