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/lmpmc_queue_spec.v | 49 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 theories/lmpmc_queue_spec.v

(limited to 'theories/lmpmc_queue_spec.v')

diff --git a/theories/lmpmc_queue_spec.v b/theories/lmpmc_queue_spec.v
new file mode 100644
index 0000000..0ea3a4a
--- /dev/null
+++ b/theories/lmpmc_queue_spec.v
@@ -0,0 +1,49 @@
+From iris.program_logic Require Import atomic.
+From iris.heap_lang Require Import notation proofmode.
+
+From lmpmc Require Import util.
+
+Record lmpmc_queue_hl :=
+  LmpmcQueueHl
+    { new : val;
+      enqueue : val;
+      try_dequeue : val;
+      link : val;
+    }.
+
+Record lmpmc_queue_iris {Σ} `{!heapGS Σ} (hl : lmpmc_queue_hl) :=
+  LmpmcQueueIris
+    { queue_repr : loc → loc → list val → iProp Σ;
+      #[global] queue_repr_timeless ℓ_deq ℓ_enq vs :: Timeless (queue_repr ℓ_deq ℓ_enq vs);
+
+      new_spec :
+        {{{ True }}}
+          hl.(new) #()
+        {{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}};
+
+      enqueue_spec (ℓ_enq : loc) (data : val) :
+        ⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
+            hl.(enqueue) #ℓ_enq data @ ∅
+          <<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>;
+
+      try_dequeue_spec (ℓ_deq : loc) :
+        ⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
+            hl.(try_dequeue) #ℓ_deq @ ∅
+          <<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>;
+
+      (** Linking two queues:
+       *     _______________      _______________
+       *    /      Q1       \    /       Q2      \
+       *    ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2
+       *    \          \ link op args /          /
+       *     \          \____________/          /
+       *      \            Q1 <> Q2            /
+       *       \______________________________/
+       *)
+      link_spec (ℓ_enq1 ℓ_deq2 : loc) :
+        ⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗
+                            if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>>
+            hl.(link) #ℓ_enq1 #ℓ_deq2 @ ∅
+          <<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>;
+    }.
+#[global] Arguments lmpmc_queue_iris _ {_} _ : assert.
-- 
cgit v1.3