From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode.

From lmpmc Require Import lmpmc_queue_spec util.

Section lmpmc_blocking.
  Context (lq : lmpmc_queue_spec.lmpmc_queue_hl).

  (* https://types.pl/@pigworker/115629120124299549 *)
  Definition dequeue : val := rec: "go" "ℓ_deq" :=
    match: lq.(try_dequeue) "ℓ_deq" with
      NONE => "go" "ℓ_deq"
    | SOME "v" => "v"
    end.

  Section proofs.
    Context `{heapGS Σ} (lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq).

    Lemma dequeue_spec (ℓ_deq : loc) :
      ⊢ <<{ ∀∀ ℓ_enq cvs, lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs }>>
        dequeue #ℓ_deq @ ∅
        <<{ ∃∃ cv cvs', ⌜cvs = cv :: cvs'⌝ ∗ lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs' | RET cv }>>.
    Proof.
      iIntros (Φ) "AU". iLöb as "IH". wp_rec.
      awp_apply lqp.(try_dequeue_spec lq).
      rewrite /atomic_acc /=.
      iMod "AU" as "(%ℓ_enq & %cvs & Hcvs & Hclose)".
      iFrame. iModIntro. iSplit; iIntros "Hrepr".
      - by iMod ("Hclose" with "Hrepr") as "AU".
      - destruct cvs as [|cv cvs']; simplify_list_eq.
        + iMod ("Hclose" with "Hrepr") as "AU". iModIntro.
          wp_pures. by iApply "IH".
        + iDestruct "Hclose" as "[_ Hclose]".
          iMod ("Hclose" $! cv cvs' with "[$Hrepr //]") as "HΦ".
          iModIntro. by wp_pures.
    Qed.

  End proofs.

End lmpmc_blocking.