1 files changed, 30 insertions, 0 deletions

diff --git a/theories/basic_queue_spec.v b/theories/basic_queue_spec.v
new file mode 100644
index 0000000..d7a38e1
--- /dev/null
+++ b/theories/basic_queue_spec.v
@@ -0,0 +1,30 @@
+From iris.program_logic Require Import atomic.
+From iris.heap_lang Require Import notation proofmode.
+
+From lmpmc Require Import util.
+
+Record basic_queue {Σ} `{!heapGS Σ} :=
+  BasicQueue
+    { new : val;
+      enqueue : val;
+      try_dequeue : val;
+
+      queue_repr : loc → list val → iProp Σ;
+      #[global] queue_repr_timeless ℓ vs :: Timeless (queue_repr ℓ vs);
+
+      new_spec :
+        {{{ True }}}
+          new #()
+        {{{ (ℓ_q : loc), RET #ℓ_q; queue_repr ℓ_q [] }}};
+
+      enqueue_spec (ℓ_q : loc) (data : val) :
+        ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
+            enqueue #ℓ_q data @ ∅
+          <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>;
+
+      try_dequeue_spec (ℓ_q : loc) :
+        ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
+            try_dequeue #ℓ_q @ ∅
+          <<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>;
+    }.
+#[global] Arguments basic_queue _ {_} : assert.