From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode adequacy.
From iris.algebra Require Import list gmultiset.
From iris.algebra.lib Require Import excl_auth.
From iris.base_logic.lib Require Import invariants mono_list.
From iris_named_props Require Import custom_syntax.
From iris.heap_lang.lib Require Import assert par.

From lmpmc Require lmpmc_queue_spec lmpmc_queue_proof fin_queue_proof lmpmc_blocking_dequeue.
From lmpmc Require Import upstream.

Definition somes {A} (xs : list (option A)) : list A := xs ≫= option_list.
Definition option_le {A} (mx my : option A) := option_relation (=) (const False) (const True) mx my.
Definition option_nat (x : nat) : option nat := guard (x ≠ 0);; Some x.
Definition vals_of_nats : list nat → list val := fmap (LitV ∘ LitInt ∘ Z.of_nat).

Lemma option_le_None {A} (x : A) : option_le None (Some x).
Proof. done. Qed.
Lemma option_le_Some {A} (x : A) : option_le (Some x) (Some x).
Proof. done. Qed.
Lemma option_le_inv {A} (mx my : option A) : option_le mx my → mx = None ∨ mx = my.
Proof. induction mx, my; intros ?; simplify_eq/=; done || (by right) || by left. Qed.

#[global] Instance timeless_if_bool {PROP : bi} {b : bool} {Q R : PROP} : Timeless Q → Timeless R → Timeless (if b then Q else R).
Proof. by destruct b. Qed.

Section hl.
  Context (lq : lmpmc_queue_spec.lmpmc_queue_hl).
  Import lmpmc_blocking_dequeue lmpmc_queue_spec.

  Notation "'let2:' x1 , x2 := e1 'in' e2" :=
    (Lam (BNamed x2) (Lam (BNamed x1) (Lam (BNamed x2) e2 (Snd (Var x2))) (Fst (Var x2))) e1)%E
      (at level 200, x1, x2 at level 1, e1, e2 at level 200,
       format "'[' 'let2:'  x1 ',' x2  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.

  Definition simple_example_2_1 : expr :=
    let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
    let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
    lq.(enqueue) "ℓ_enq1" #10;;
    lq.(link) "ℓ_enq1" "ℓ_deq2";;
    lq.(enqueue) "ℓ_enq2" #20;;
    let: "x" := dequeue lq "ℓ_deq1" in
    let: "y" := dequeue lq "ℓ_deq1" in
    ("x", "y").

  Definition simple_example_2_2 : expr :=
    let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
    let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
    ((  lq.(enqueue) "ℓ_enq1" #10;;
        lq.(link) "ℓ_enq1" "ℓ_deq2")  (* thread A *)
    ||| lq.(enqueue) "ℓ_enq2" #20     (* thread B *)
    );;
    let: "x" := dequeue lq "ℓ_deq1" in
    let: "y" := dequeue lq "ℓ_deq1" in
    ("x", "y").

  Definition mt_example_1 : expr :=
    let: "ℓ_sum" := Alloc #0 in
    let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
    let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
    ((  lq.(enqueue) "ℓ_enq1" #1;;
        lq.(link) "ℓ_enq1" "ℓ_deq2")       (* thread A *)
    ||| lq.(enqueue) "ℓ_enq2" #2           (* thread B *)
    ||| lq.(enqueue) "ℓ_enq2" #3           (* thread C *)
    ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1")  (* thread D *)
    ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1")  (* thread E *)
    ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1")  (* thread F *)
    );;
    ! "ℓ_sum".

End hl.

Section proofs.
  Context `{!heapGS Σ, !spawnG Σ,
            !mono_listG natO Σ,
            !inG Σ (excl_authR (gmultisetO nat)),
            !inG Σ (excl_authR natO),
            !inG Σ (excl_authR boolO),
            !inG Σ (excl_authR (listO natO)),
            !inG Σ (excl_authR (optionO natO)),
            !inG Σ (exclR (listO natO))}.
  Context {lq : lmpmc_queue_spec.lmpmc_queue_hl}
          {lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq}.
  Import lmpmc_blocking_dequeue lmpmc_queue_spec.

  Lemma simple_example_2_1_safe :
    ⊢ WP simple_example_2_1 lq {{ v, ⌜v = (#10, #20)%V⌝ }}.
  Proof.
    iUnfold simple_example_2_1.
    wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
    wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
    awp_apply lqp.(enqueue_spec lq). iAaccIntro with "Hq1"; iIntros "Hq1"; first by iFrame.
    simpl. iModIntro. wp_pures.
    awp_apply lqp.(link_spec lq).
    rewrite /atomic_acc /=.
    iExists true. iFrame.
    iApply fupd_mask_intro; first done.
    iIntros "Hupd". iSplit. { iIntros "[? ?]". iFrame. }
    iIntros "Hq". simpl. iMod "Hupd" as "_". iModIntro.
    wp_pures. awp_apply lqp.(enqueue_spec lq).
    iAaccIntro with "Hq"; iIntros "Hq"; first by iFrame.
    simpl.

    iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp).
    iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame.
    iIntros (? ?) "[%Hvs Hq]". iSimplifyEq.
    iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp).
    iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame.
    iIntros (? ?) "[%Hvs Hq]". iSimplifyEq.

    iModIntro. by wp_pures.
  Qed.

  Record smp_gstate :=
    SmpGstate
      { γ1_linked : gname;  (* (●E) whether Q1 and Q2 have been linked already *)
        γ1_contA  : gname;  (* (●E) (list nat) contribution of thread A        *)
        γ1_contB  : gname;  (* (●E) (list nat) contribution of thread B        *)
      }.

  Definition smp_inv γs (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ :=
    ∃ (linked : bool) (contA contB : list nat),
      ("Hlinked●" ∷ own γs.(γ1_linked) (●E linked)) ∗
      ("HcontA●"  ∷ own γs.(γ1_contA) (●E contA)) ∗
      ("HcontB●"  ∷ own γs.(γ1_contB) (●E contB)) ∗
      ("Hq1"       ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats (if linked then contA ++ contB else contA))) ∗
      ("Hq2"       ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats contB)).

  Lemma simple_example_2_2_safe :
    ⊢ WP simple_example_2_2 lq {{ v, ⌜v = (#10, #20)%V⌝ }}.
  Proof.
    iUnfold simple_example_2_2.
    wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
    wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.

    iMod (own_alloc (●E false ⋅ ◯E false)) as (γ1_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contA') "[HcontA● HcontA◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contB') "[HcontB● HcontB◯]"; first apply excl_auth_valid.

    pose γs := SmpGstate γ1_linked' γ1_contA' γ1_contB'.
    replace γ1_linked' with γs.(γ1_linked) by done.
    replace γ1_contA' with γs.(γ1_contA) by done.
    replace γ1_contB' with γs.(γ1_contB) by done.
    clearbody γs. clear γ1_linked' γ1_contA' γ1_contB'.
    iAssert (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "[$]" as "Hinv".
    iMod (inv_alloc nroot _ (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv".

    wp_smart_apply (wp_par (λ _, own γs.(γ1_linked) (◯E true) ∗ own γs.(γ1_contA) (◯E [10]))%I
                           (λ _, own γs.(γ1_contB) (◯E [20]))
                    with "[Hlinked◯ HcontA◯] [HcontB◯]").
    { awp_apply lqp.(enqueue_spec lq).
      iInv "Hinv" as (linked contA contB) ">H".
      iNamedSuffix "H" "_1".
      iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L.
      iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L.
      iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
      iIntros "Hq1_1".
      iCombine "HcontA●_1 HcontA◯" as "HcontA".
      iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]".
      { apply (excl_auth_update _ _ [10]). }
      iIntros "!>".
      iSimplifyEq. replace ([ #10 ] : list val) with (vals_of_nats [10]) by done.
      iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". wp_pures. clear contB.

      awp_apply lqp.(link_spec lq).
      iInv "Hinv" as (linked contA contB) ">H".
      iNamedSuffix "H" "_2".
      iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L.
      iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L.
      rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
      iExists true. iFrame "Hq1_2 Hq2_2". iSplit.
      { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro. do 2 iFrame. }
      iIntros "Hq1". iMod "Hclose" as "_".
      iCombine "Hlinked●_2 Hlinked◯" as "Hlinked".
      iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]".
      { apply (excl_auth_update _ _ true). }
      iFrame "Hlinked●_2 HcontA●_2 HcontB●_2 Hq1". by iFrame. }
    { awp_apply lqp.(enqueue_spec lq).
      iInv "Hinv" as (linked contA contB) ">H".
      iNamedSuffix "H" "_1".
      iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L.
      destruct linked eqn:Hlinked.
      { iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
        iIntros "Hq1_1".
        iCombine "HcontB◯ HcontB●_1" as "HcontB".
        iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]".
        { apply (excl_auth_update _ _ [20]). }
        iIntros "!>".
        iSimplifyEq.
        replace [ #20 ] with (vals_of_nats [20]) by done.
        iEval (rewrite app_nil_r /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1_1".
        by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1". }
      { iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". by iFrame. }
        iIntros "Hq2_1".
        iCombine "HcontB◯ HcontB●_1" as "HcontB".
        iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]".
        { apply (excl_auth_update _ _ [20]). }
        iIntros "!>".
        iSimplifyEq.
        replace [ #20 ] with (vals_of_nats [20]) by done.
        by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". } }
    { iIntros (v1 v2) "[[Hlinked◯ HcontA◯] HcontB◯]".
      iModIntro. wp_pures. clear v1 v2.
      awp_apply (dequeue_spec lq lqp).
      iInv "Hinv" as (linked contA contB) ">H".
      iNamedSuffix "H" "_1".
      iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L.
      iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L.
      iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L.
      iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
      iIntros (v0 vs) "[%Hvs Hq1]".
      simpl in Hvs. injection Hvs as <- <-.
      replace [ #20%nat ] with (vals_of_nats [20]) by done.
      iCombine "HcontA●_1 HcontA◯" as "HcontA".
      iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]".
      { apply (excl_auth_update _ _ []). }
      iIntros "!>".
      iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1". wp_pures.

      awp_apply (dequeue_spec lq lqp).
      iInv "Hinv" as (linked contA contB) ">H".
      iNamedSuffix "H" "_2".
      iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L.
      iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L.
      iCombine "HcontB◯ HcontB●_2" gives %->%excl_auth_agree_L.
      iAaccIntro with "Hq1_2". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
      iIntros (v0 vs) "[%Hvs Hq1]".
      simpl in Hvs. injection Hvs as <- <-.
      replace [ #20%nat ] with (vals_of_nats [20]) by done.
      iCombine "HcontB●_2 HcontB◯" as "HcontB".
      iMod (own_update with "HcontB") as "[HcontB●_2 HcontB◯]".
      { apply (excl_auth_update _ _ []). }
      iIntros "!>".
      iFrame "Hlinked●_2 HcontB●_2 HcontA●_2 Hq1". wp_pures.
      done. }
  Qed.

  Record mt_gstate :=
    Gstate
      { γ2_hist1  : gname;  (* (●ML) (list nat) succesfully enqueued items (Q1)                   *)
        γ2_hist2  : gname;  (* (●E ) (list nat) sucessfully enqueued items (Q2)                   *)
        γ2_linked : gname;  (* (●E ) (bool) whether Q1 and Q2 have been linked                    *)
        γ2_venqA  : gname;  (* (●E ) (gmultiset nat) of items enqueued by thread A                *)
        γ2_venqB  : gname;  (* (●E ) (gmultiset nat) of items enqueued by thread B                *)
        γ2_venqC  : gname;  (* (●E ) (gmultiset nat) of items enqueued by thread C                *)
        γ2_vdeqD  : gname;  (* (●E ) (option nat) poised contribution of first dequeueing thread  *)
        γ2_vdeqE  : gname;  (* (●E ) (option nat) poised contribution of second dequeueing thread *)
        γ2_vdeqF  : gname;  (* (●E ) (option nat) poised contribution of third dequeueing thread  *)
        γ2_contD  : gname;  (* (●E ) (nat) as-is contribution of first dequeueing thread          *)
        γ2_contE  : gname;  (* (●E ) (nat) as-is contribution of second dequeueing thread         *)
        γ2_contF  : gname;  (* (●E ) (nat) as-is contribution of third dequeueing thread          *)
      }.

  Definition mt_inv γs ℓ_sum (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ :=
    ∃ (hist1 hist2 : list nat) (ndeq : nat) (linked : bool) (ecsA ecsB ecsC : gmultiset nat) (npD npE npF : option nat) (nD nE nF : nat) (vs1 : list nat),
      ("Hq1"       ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats vs1)) ∗
      ("Hq2"       ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats hist2)) ∗
      ("Hhist1●"   ∷ γs.(γ2_hist1)     ↪●ML hist1) ∗
      ("Hhist2E"   ∷ own γs.(γ2_hist2)  (Excl hist2)) ∗
      ("Hlinked●"  ∷ own γs.(γ2_linked) (●E linked)) ∗
      ("HvenqA●"   ∷ own γs.(γ2_venqA)  (●E ecsA)) ∗
      ("HvenqB●"   ∷ own γs.(γ2_venqB)  (●E ecsB)) ∗
      ("HvenqC●"   ∷ own γs.(γ2_venqC)  (●E ecsC)) ∗
      ("HvdeqD●"   ∷ own γs.(γ2_vdeqD)  (●E npD)) ∗
      ("HvdeqE●"   ∷ own γs.(γ2_vdeqE)  (●E npE)) ∗
      ("HvdeqF●"   ∷ own γs.(γ2_vdeqF)  (●E npF)) ∗
      ("HcontD●"   ∷ own γs.(γ2_contD)  (●E nD)) ∗
      ("HcontE●"   ∷ own γs.(γ2_contE)  (●E nE)) ∗
      ("HcontF●"   ∷ own γs.(γ2_contF)  (●E nF)) ∗
      ("Hsum"      ∷ ℓ_sum ↦ #(nD + nE + nF)) ∗
      ("%Hhist1"   ∷ ⌜list_to_set_disj hist1 ⊆ if linked then ecsA ⊎ ecsB ⊎ ecsC else ecsA⌝) ∗
      ("%Hhist2"   ∷ ⌜list_to_set_disj hist2 ⊆ ecsB ⊎ ecsC⌝) ∗
      ("%Hhist1n0" ∷ ⌜Forall (.≠ 0) hist1⌝) ∗
      ("%Hhist2n0" ∷ ⌜Forall (.≠ 0) hist2⌝) ∗
      ("%HnDEF"    ∷ ⌜somes [npD; npE; npF] ⊆+ take ndeq hist1⌝) ∗
      ("%HD"       ∷ ⌜option_le (option_nat nD) npD⌝) ∗
      ("%HE"       ∷ ⌜option_le (option_nat nE) npE⌝) ∗
      ("%HF"       ∷ ⌜option_le (option_nat nF) npF⌝) ∗
      ("%Hndeq"    ∷ ⌜ndeq ≤ length hist1⌝) ∗
      ("%Hhistvs"  ∷ ⌜drop ndeq hist1 = vs1⌝).

  (* Post, we expect:
       linked = true
       nD, nE, nF ≠ 0 (hence npD, npE, npF ≠ None and all are unique, adding up to 6) *)

  Lemma mt_example_1_safe :
    ⊢ WP mt_example_1 lq {{ v, ⌜v = #6⌝ }}.
  Proof.
    iUnfold mt_example_1.
    wp_alloc ℓ_sum as "Hsum". wp_pures.
    wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
    wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
    iEval (replace [] with (vals_of_nats [])) in "Hq1 Hq2".
    iMod (mono_list_own_alloc []) as "[%γ2_hist1 [Hhist1● _]]".
    iMod (own_alloc (Excl [])) as "[%γ2_hist2 Hhist2E]"; first done.
    iMod (own_alloc (●E false ⋅ ◯E false)) as (γ2_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqA') "[HvenqA● HvenqA◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqB') "[HvenqB● HvenqB◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqC') "[HvenqC● HvenqC◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqD' [HvdeqD● HvdeqD◯]]"; first apply excl_auth_valid.
    iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqE' [HvdeqE● HvdeqE◯]]"; first apply excl_auth_valid.
    iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqF' [HvdeqF● HvdeqF◯]]"; first apply excl_auth_valid.
    iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contD') "[HcontD● HcontD◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contE') "[HcontE● HcontE◯]"; first apply excl_auth_valid.
    iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contF') "[HcontF● HcontF◯]"; first apply excl_auth_valid.
    pose γs := Gstate γ2_hist1 γ2_hist2 γ2_linked' γ2_venqA' γ2_venqB' γ2_venqC' γ2_vdeqD' γ2_vdeqE' γ2_vdeqF' γ2_contD' γ2_contE' γ2_contF'.
    replace γ2_linked' with γs.(γ2_linked) by done.
    replace γ2_venqA' with γs.(γ2_venqA) by done.
    replace γ2_venqB' with γs.(γ2_venqB) by done.
    replace γ2_venqC' with γs.(γ2_venqC) by done.
    replace γ2_vdeqD' with γs.(γ2_vdeqD) by done.
    replace γ2_vdeqE' with γs.(γ2_vdeqE) by done.
    replace γ2_vdeqF' with γs.(γ2_vdeqF) by done.
    replace γ2_contD' with γs.(γ2_contD) by done.
    replace γ2_contE' with γs.(γ2_contE) by done.
    replace γ2_contF' with γs.(γ2_contF) by done.
    iAssert (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2)
      with "[$Hhist1● $Hhist2E $Hlinked● $HvenqA● $HvenqB● $HvenqC● $HvdeqD● $HvdeqE● $HvdeqF● $HcontD● $HcontE● $HcontF● $Hq1 $Hq2 $Hsum]"
      as "Hinv". 
    { iPureIntro. exists 0. split; try done. }
    clearbody γs.
    clear γ2_hist1 γ2_hist2 γ2_linked' γ2_venqA' γ2_venqB' γ2_venqC' γ2_vdeqD' γ2_vdeqE' γ2_vdeqF' γ2_contD' γ2_contE' γ2_contF'.
    iMod (inv_alloc nroot _ (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv".

    pose (P1 := (own (γ2_venqA γs) (◯E {[+ 1 +]}) ∗ own (γ2_linked γs) (◯E true))%I).
    pose (P2 := own (γ2_venqB γs) (◯E {[+ 2 +]})).
    pose (P3 := own (γ2_venqC γs) (◯E {[+ 3 +]})).
    pose (P4 := (∃ nD : nat, own γs.(γ2_contD) (◯E nD) ∗ ⌜nD ≠ 0⌝)%I).
    pose (P5 := (∃ nE : nat, own γs.(γ2_contE) (◯E nE) ∗ ⌜nE ≠ 0⌝)%I).
    pose (P6 := (∃ nF : nat, own γs.(γ2_contF) (◯E nF) ∗ ⌜nF ≠ 0⌝)%I).

    wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4 ∗ P5)%I (λ _, P6)%I with "[- HcontF◯ HvdeqF◯] [HcontF◯ HvdeqF◯]").
    { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4)%I (λ _, P5)%I with "[- HcontE◯ HvdeqE◯] [HcontE◯ HvdeqE◯]").
      { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3)%I (λ _, P4)%I with "[- HcontD◯ HvdeqD◯] [HcontD◯ HvdeqD◯]").
        { wp_smart_apply (wp_par (λ _, P1 ∗ P2)%I (λ _, P3)%I with "[- HvenqC◯] [HvenqC◯]").
          { wp_smart_apply (wp_par (λ _, P1) (λ _, P2) with "[- HvenqB◯] [HvenqB◯]").
            { awp_apply lqp.(enqueue_spec lq).
              iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
              iNamedSuffix "H" "_1". iCombine "HvenqA◯ HvenqA●_1" gives %->%excl_auth_agree_L.
              iCombine "Hlinked●_1 Hlinked◯" gives %->%excl_auth_agree_L.
              iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
              iIntros "Hq1".

              iMod (mono_list_auth_own_update (hist1 ++ [1]) with "Hhist1●_1") as "[Hhist1●_1 _]".
              { by apply prefix_app_r. }
              iCombine "HvenqA●_1 HvenqA◯" as "HvenqA".
              iMod (own_update with "HvenqA") as "[HvenqA●_1 HvenqA◯]".
              { apply (excl_auth_update _ _ {[+ 1 +]}). }
              replace (vals_of_nats vs1 ++ [ #1 ]) with (vals_of_nats (vs1 ++ [1]))
                by rewrite /vals_of_nats fmap_app //.
              iModIntro. iFrame "HvenqA◯". iFrame. iFrame "Hq1". iSplit.
              { iPureIntro. exists ndeq. repeat split; try done.
                + rewrite list_to_set_disj_app.
                  multiset_solver.
                + apply Forall_app. by split; last apply Forall_singleton.
                + etrans; first apply HnDEF_1.
                  apply prefix_submseteq, take_app_prefix.
                + rewrite ->!length_app in *. lia.
                + by rewrite drop_app_le // Hhistvs_1. }
              wp_pures.
              clear.

              awp_apply lqp.(link_spec lq).
              iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
              iNamedSuffix "H" "_2".
              iCombine "Hlinked●_2 Hlinked◯" gives %->%excl_auth_agree_L.
              rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
              iExists true. iFrame "Hq1_2 Hq2_2". iSplit.
              { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro.
                iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
              iIntros "Hq1". iMod "Hclose" as "_".

              iCombine "Hlinked●_2 Hlinked◯" as "Hlinked".
              iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]".
              { apply (excl_auth_update _ _ true). }
              iEval (rewrite /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1".
              iMod (mono_list_auth_own_update (hist1 ++ hist2) with "Hhist1●_2") as "[Hhist1●_2 _]"; first by apply prefix_app_r.
              iFrame. iModIntro. iModIntro. iPureIntro. exists ndeq. repeat split; try done.
              - rewrite list_to_set_disj_app. multiset_solver.
              - by rewrite Forall_app.
              - etrans; first apply HnDEF_2.
                apply prefix_submseteq, take_app_prefix.
              - rewrite length_app. lia.
              - by rewrite drop_app_le // Hhistvs_2.
            }
            { awp_apply lqp.(enqueue_spec lq).
              iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
              iNamedSuffix "H" "_1". iCombine "HvenqB◯ HvenqB●_1" gives %->%excl_auth_agree_L.

              destruct linked eqn:Hlinked.
              - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
                iIntros "Hq1".
                iCombine "HvenqB●_1 HvenqB◯" as "HvenqB".
                iMod (mono_list_auth_own_update (hist1 ++ [2]) with "Hhist1●_1") as "[Hhist1●_1 _]".
                { by apply prefix_app_r. }
                iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]".
                { apply (excl_auth_update _ _ {[+ 2 +]}). }
                replace (vals_of_nats vs1 ++ [ #2 ]) with (vals_of_nats (vs1 ++ [2]))
                  by rewrite /vals_of_nats fmap_app //.
                iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [2]). iFrame.
                iPureIntro. repeat split; try done.
                + rewrite list_to_set_disj_app.
                  multiset_solver
                + apply Forall_app.
                + multiset_solver.
                + apply Forall_app. by split; last apply Forall_singleton.
                + etrans; first apply HnDEF_1.
                  apply prefix_submseteq, take_app_prefix.
                + rewrite length_app. lia.
                + by rewrite drop_app_le // Hhistvs_1.
              - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. }
                iIntros "Hq1".
                iCombine "HvenqB●_1 HvenqB◯" as "HvenqB".
                iMod (own_update _ _ (Excl (hist2 ++ [2])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|].
                iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]".
                { apply (excl_auth_update _ _ {[+ 2 +]}). }
                replace (vals_of_nats hist2 ++ [ #2 ]) with (vals_of_nats (hist2 ++ [2]))
                  by rewrite /vals_of_nats fmap_app //.
                iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iFrame.
                iPureIntro. exists ndeq. repeat split; try done.
                + rewrite list_to_set_disj_app.
                  multiset_solver.
                + apply Forall_app. split; first done.
                  by apply Forall_singleton.
            }
            { by iIntros (_ _) "H !>". }
          }
          { awp_apply lqp.(enqueue_spec lq).
            iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
            iNamedSuffix "H" "_1". iCombine "HvenqC◯ HvenqC●_1" gives %->%excl_auth_agree_L.

            destruct linked eqn:Hlinked.
            - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
              iIntros "Hq1".
              iCombine "HvenqC●_1 HvenqC◯" as "HvenqC".
              iMod (mono_list_auth_own_update (hist1 ++ [3]) with "Hhist1●_1") as "[Hhist1●_1 _]".
              { by apply prefix_app_r. }
              iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]".
              { apply (excl_auth_update _ _ {[+ 3 +]}). }
              replace (vals_of_nats vs1 ++ [ #3 ]) with (vals_of_nats (vs1 ++ [3]))
                by rewrite /vals_of_nats fmap_app //.
              iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [3]). iFrame.
              iPureIntro. repeat split; try done.
              + rewrite list_to_set_disj_app.
                multiset_solver.
              + multiset_solver.
              + apply Forall_app. by split; last apply Forall_singleton.
              + etrans; first apply HnDEF_1.
                apply prefix_submseteq, take_app_prefix.
              + rewrite length_app. lia.
              + by rewrite drop_app_le // Hhistvs_1.
            - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. }
              iIntros "Hq1".
              iCombine "HvenqC●_1 HvenqC◯" as "HvenqC".
              iMod (own_update _ _ (Excl (hist2 ++ [3])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|].
              iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]".
              { apply (excl_auth_update _ _ {[+ 3 +]}). }
              replace (vals_of_nats hist2 ++ [ #3 ]) with (vals_of_nats (hist2 ++ [3]))
                by rewrite /vals_of_nats fmap_app //.
              iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iFrame.
              iPureIntro. exists ndeq. repeat split; try done.
              + rewrite list_to_set_disj_app.
                multiset_solver.
              + apply Forall_app. split; first done.
                by apply Forall_singleton.
          }
          { iIntros (_ _) "[H1 H2] !>". iFrame. }
        }
        { awp_apply (dequeue_spec lq lqp).
          iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
          iNamedSuffix "H" "_1".
          iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
          iIntros (v0 vs') "[%Hvs Hq1]".
          destruct vs1; simplify_eq/=.
          iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
          iCombine "HcontD◯ HcontD●_1" gives %->%excl_auth_agree_L.

          iCombine "HvdeqD●_1 HvdeqD◯" as "HvdeqD" gives %->%excl_auth_agree_L.
          iMod (own_update with "HvdeqD") as "[HvdeqD●_1 HvdeqD◯]".
          { apply (excl_auth_update _ _ (Some n)). }
          
          apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
          iModIntro. iFrame. iFrameNamed. iSplit.
          { iPureIntro. exists (S ndeq). repeat split; try done.
            - etrans; first done.
              simplify_eq/=. rewrite ->app_nil_r in *.
              etrans. { apply Permutation_submseteq, Permutation_cons_append. }
              rewrite (take_S_r _ _ n) //.
              by apply submseteq_skips_r.
            - by apply lookup_lt_Some in Hhistndeq_1. }
          
          clear - Hhistndeq_1 Hhistvs_1.
          iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
          iNamedSuffix "H" "_2".
          wp_faa.
          
          iCombine "HcontD●_2 HcontD◯" as "HcontD" gives %->%excl_auth_agree_L.
          iMod (own_update with "HcontD") as "[HcontD●_2 HcontD◯]".
          { apply (excl_auth_update _ _ n). }
          
          iEval (rewrite Z.add_0_l Z.add_comm Z.add_assoc) in "Hsum_2".

          iCombine "HvdeqD●_2 HvdeqD◯" gives %->%excl_auth_agree_L.

          iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
          assert (Hn : n ≠ 0).
          { eapply (Forall_lookup (.≠ 0)); last done.
            by eapply Forall_prefix. }
          
          iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
          iPureIntro. exists ndeq'. repeat split; try done.
          by rewrite /option_nat option_guard_True.
        }
        { iIntros (_ _) "[H1 H2] !>". iFrame. }
      }
      { awp_apply (dequeue_spec lq lqp).
        iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
        iNamedSuffix "H" "_1".
        iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
        iIntros (v0 vs') "[%Hvs Hq1]".
        destruct vs1; simplify_eq/=.
        iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
        iCombine "HcontE◯ HcontE●_1" gives %->%excl_auth_agree_L.

        iCombine "HvdeqE●_1 HvdeqE◯" as "HvdeqE" gives %->%excl_auth_agree_L.
        iMod (own_update with "HvdeqE") as "[HvdeqE●_1 HvdeqE◯]".
        { apply (excl_auth_update _ _ (Some n)). }

        apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
        iModIntro. iFrame. iFrameNamed. iSplit.
        { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done.
          - simplify_eq/=. rewrite app_nil_r in HnDEF_1.
            rewrite app_nil_r.
            etrans. { apply submseteq_skips_l, Permutation_submseteq, Permutation_cons_append. }
            rewrite (take_S_r _ _ n) // app_assoc.
            by apply submseteq_skips_r.
          - by apply lookup_lt_Some in Hhistndeq_1. }

        clear - Hhistndeq_1 Hhistvs_1.
        iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
        iNamedSuffix "H" "_2".
        wp_faa.
        
        iCombine "HcontE●_2 HcontE◯" as "HcontE" gives %->%excl_auth_agree_L.
        iMod (own_update with "HcontE") as "[HcontE●_2 HcontE◯]".
        { apply (excl_auth_update _ _ n). }
        
        iEval (rewrite Z.add_0_r -Z.add_assoc [(nF + n)%Z]Z.add_comm Z.add_assoc) in "Hsum_2".

        iCombine "HvdeqE●_2 HvdeqE◯" gives %->%excl_auth_agree_L.

        iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
        assert (Hn : n ≠ 0).
        { eapply (Forall_lookup (.≠ 0)); last done.
          by eapply Forall_prefix. }
        
        iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
        iPureIntro. exists ndeq'. repeat split; try done.
        by rewrite /option_nat option_guard_True.
      }
      { iIntros (_ _) "[H1 H2] !>". iFrame. }
    }
    { awp_apply (dequeue_spec lq lqp).
      iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
      iNamedSuffix "H" "_1".
      iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
      iIntros (v0 vs') "[%Hvs Hq1]".
      destruct vs1; simplify_eq/=.
      iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
      iCombine "HcontF◯ HcontF●_1" gives %->%excl_auth_agree_L.

      iCombine "HvdeqF●_1 HvdeqF◯" as "HvdeqF" gives %->%excl_auth_agree_L.
      iMod (own_update with "HvdeqF") as "[HvdeqF●_1 HvdeqF◯]".
      { apply (excl_auth_update _ _ (Some n)). }

      apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
      iModIntro. iFrame. iFrameNamed. iSplit.
      { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done.
        - simplify_eq/=. rewrite app_nil_r in HnDEF_1.
          rewrite (take_S_r _ _ n) // app_assoc.
          by apply submseteq_skips_r.
        - by apply lookup_lt_Some in Hhistndeq_1. }

      clear - Hhistndeq_1 Hhistvs_1.
      iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
      iNamedSuffix "H" "_2".
      wp_faa.

      iCombine "HcontF●_2 HcontF◯" as "HcontF" gives %->%excl_auth_agree_L.
      iMod (own_update with "HcontF") as "[HcontF●_2 HcontF◯]".
      { apply (excl_auth_update _ _ n). }

      iEval (rewrite Z.add_0_r) in "Hsum_2".

      iCombine "HvdeqF●_2 HvdeqF◯" gives %->%excl_auth_agree_L.

      iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
      assert (Hn : n ≠ 0).
      { eapply (Forall_lookup (.≠ 0)); last done.
        by eapply Forall_prefix. }

      iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
      iPureIntro. exists ndeq'. repeat split; try done.
      by rewrite /option_nat option_guard_True.
    }

    iIntros (v1 v2) "[(H1 & HvenqB◯ & HvenqC◯ & H4 & H5) H6]".
    unfold P1, P2, P3, P4, P5, P6. clear P1 P2 P3 P4 P5 P6.
    iDestruct "H1" as "[HvenqA◯ Hlinked◯]".
    iDestruct "H4" as "(%nD' & HnD'◯ & %HcontD)".
    iDestruct "H5" as "(%nE' & HnE'◯ & %HcontE)".
    iDestruct "H6" as "(%nF' & HnF'◯ & %HcontF)".
    iModIntro. wp_pures.

    iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">@".
    wp_load. iModIntro. iSplit; [by iFrame; iExists ndeq|].
    iCombine "HnD'◯ HcontD●" gives %<-%excl_auth_agree_L. iClear "HnD'◯ HcontD●".
    iCombine "HnE'◯ HcontE●" gives %<-%excl_auth_agree_L. iClear "HnE'◯ HcontE●".
    iCombine "HnF'◯ HcontF●" gives %<-%excl_auth_agree_L. iClear "HnF'◯ HcontF●".

    rewrite /option_nat !option_guard_True // in HD HE HF.
    apply option_le_inv in HD as [HD|<-]; first done.
    apply option_le_inv in HE as [HE|<-]; first done.
    apply option_le_inv in HF as [HF|<-]; first done.
    simplify_eq/=.

    iCombine "Hlinked● Hlinked◯" gives %->%excl_auth_agree_L.
    iClear "Hq2 Hlinked● Hlinked◯".

    iCombine "HvenqA● HvenqA◯" gives %->%excl_auth_agree_L. iClear "HvenqA◯ HvenqA●".
    iCombine "HvenqB● HvenqB◯" gives %->%excl_auth_agree_L. iClear "HvenqB◯ HvenqB●".
    iCombine "HvenqC● HvenqC◯" gives %->%excl_auth_agree_L. iClear "HvenqC◯ HvenqC●".
    iPureIntro. enough (nD + nE + nF = 6). { do 2 f_equal. lia. }

    assert (ndeq ≥ 3 ∧ length hist1 ≥ 3) as [Hndeq' Hhist1'].
    { apply submseteq_length in HnDEF as Hndeq'.
      rewrite /= length_take in Hndeq'. lia. }
    apply gmultiset_subseteq_size in Hhist1 as Hhist1''.
    rewrite list_to_set_disj_size !gmultiset_size_disj_union !gmultiset_size_singleton /= in Hhist1''.
    have {Hhist1''}Hhist1' : length hist1 = 3 by lia.
    apply gmultiset_subseteq_size_eq in Hhist1; last first.
    { rewrite !gmultiset_size_disj_union !gmultiset_size_singleton /= list_to_set_disj_size. lia. }

    assert (HnDEF' : [nD; nE; nF] ≡ₚ hist1).
    { apply submseteq_length_Permutation; last (simpl; lia).
      etrans; [apply HnDEF | apply submseteq_take]. }

    assert (Hhist1'' : hist1 ≡ₚ elements ({[+ 1; 2; 3 +]} : gmultiset nat)).
    { erewrite elements_list_to_set_disj_perm.
      by rewrite Hhist1. }

    assert (H123 : elements ({[+ 1; 2; 3 +]} : gmultiset nat) ≡ₚ [1; 2; 3]).
    { by rewrite !gmultiset_elements_disj_union !gmultiset_elements_singleton /=. }
    
    trans (foldr Nat.add 0 [nD; nE; nF]). { simpl. lia. }
    by rewrite HnDEF' Hhist1'' H123.
  Qed.

End proofs.

Definition fq := fin_queue_proof.fin_queue_hl.
Definition lq := lmpmc_queue_proof.lmpmc_queue_hl fq.

(** First example *)

Definition simple_clientΣ : gFunctors := #[ heapΣ; fin_queue_proof.fin_queueΣ ].
Lemma simple_client_adequate σ : adequate NotStuck (simple_example_2_1 lq) σ (λ v _, v = (#10, #20)%V).
Proof.
  eapply (heap_adequacy simple_clientΣ). iIntros (?) "_". iApply simple_example_2_1_safe.
  Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
Qed.

(** Second example *)

Definition simple_mt_clientΣ : gFunctors :=
  #[ heapΣ; spawnΣ;
     fin_queue_proof.fin_queueΣ;
     GFunctor (excl_authRF boolO);
     GFunctor (excl_authRF (listO natO)) ].

Instance smc_inG_excl_auth_bool Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR boolO).
Proof. solve_inG. Qed.
Instance smc_inG_excl_auth_nat_list Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR (listO natO)).
Proof. solve_inG. Qed.

Lemma simple_mt_client_adequate σ : adequate NotStuck (simple_example_2_2 lq) σ (λ v _, v = (#10, #20)%V).
Proof.
  eapply (heap_adequacy simple_mt_clientΣ). iIntros (?) "_". iApply simple_example_2_2_safe.
  Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
Qed.

(** Third example *)

Definition mt_example_1Σ : gFunctors :=
  #[ heapΣ; spawnΣ;
     fin_queue_proof.fin_queueΣ;
     mono_listΣ natO;
     GFunctor (excl_authRF (gmultisetO nat));
     GFunctor (excl_authRF natO);
     GFunctor (excl_authRF boolO);
     GFunctor (excl_authRF (optionO natO));
     GFunctor (exclR (listO natO)) ].

Instance me_inG_excl_auth_multiset Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (gmultisetO nat)).
Proof. solve_inG. Qed.
Instance me_inG_excl_auth_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR natO).
Proof. solve_inG. Qed.
Instance me_inG_excl_auth_bool Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR boolO).
Proof. solve_inG. Qed.
Instance me_inG_excl_auth_option_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (optionO natO)).
Proof. solve_inG. Qed.
Instance me_inG_excl_list_nat Σ : subG mt_example_1Σ Σ → inG Σ (exclR (listO natO)).
Proof. solve_inG. Qed.

Lemma mt_example_1_adequate σ : adequate NotStuck (mt_example_1 lq) σ (λ v _, v = #6%V).
Proof.
  eapply (heap_adequacy mt_example_1Σ). iIntros (?) "_". iApply mt_example_1_safe.
  Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
Qed.

Print Assumptions simple_client_adequate.
Print Assumptions simple_mt_client_adequate.
Print Assumptions mt_example_1_adequate.