1 files changed, 40 insertions, 0 deletions

diff --git a/theories/lmpmc_blocking_dequeue.v b/theories/lmpmc_blocking_dequeue.v
new file mode 100644
index 0000000..5051c6a
--- /dev/null
+++ b/theories/lmpmc_blocking_dequeue.v
@@ -0,0 +1,40 @@
+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.