1 files changed, 67 insertions, 0 deletions

diff --git a/theories/fin_queue_spec.v b/theories/fin_queue_spec.v
new file mode 100644
index 0000000..f7e0886
--- /dev/null
+++ b/theories/fin_queue_spec.v
@@ -0,0 +1,67 @@
+From iris.program_logic Require Import atomic.
+From iris.heap_lang Require Import notation proofmode.
+
+From lmpmc Require Import util.
+
+(* Doing this split because I don't know how to otherwise get a nice
+   closed proof. *)
+
+Record fin_queue_hl :=
+  FinQueueHl
+    { new : val;
+      enqueue : val;
+      finalize : val;
+      try_dequeue : val;}.
+Record fin_queue_iris {Σ} `{!heapGS Σ} (hl : fin_queue_hl) :=
+  FinQueueIris
+    { (** If [⊢ queue_repr ℓ vs mfin], then there is a queue at [ℓ]
+          which currently holds the values [vs], and possibly a final
+          value [mfin]. The dequeue and enqueue operations work in
+          FIFO fashion, with [head vs] (if any) representing the next
+          value that would be dequeued by a [try_dequeue ℓ] operation.
+
+          Only non-finalized queues can be enqueued in. Non-finalized queues
+          can be finalized using the [finalize ℓ v] operation, which sets
+          [mfin] to [v]. Subsequent [try_dequeue ℓ] operations then first
+          dequeue the remainder of [vs]; when [vs] is empty, they return [mfin]
+          (but, critically, do not unset it). *)
+      queue_repr : loc → list val → option val → iProp Σ;
+      #[global] queue_repr_timeless ℓ vs mfin :: Timeless (queue_repr ℓ vs mfin);
+
+      (** If [⊢ queue_fin ℓ v], then the queue at [ℓ] has been
+          finalized and all elements except for the final element [v]
+          have been dequeued.
+
+          Queues that enter this state never leave this state; this
+          allows [queue_fin ℓ v] to be a persistent proposition. *)
+      queue_fin : loc → val → iProp Σ;
+      #[global] queue_fin_persistent ℓ v :: Persistent (queue_fin ℓ v);
+      #[global] queue_fin_timeless ℓ v :: Timeless (queue_fin ℓ v);
+      queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin;
+      queue_fin_agree ℓ vs fin mfin :
+        queue_fin ℓ fin -∗
+        queue_repr ℓ vs mfin -∗
+        ⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝;
+
+      new_spec :
+        {{{ True }}}
+          hl.(new) #()
+        {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] None }}};
+
+      enqueue_spec (ℓ_q : loc) (data : val) :
+        ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
+            hl.(enqueue) #ℓ_q data @ ∅
+          <<{ queue_repr ℓ_q (vs ++ [data]) None | RET #() }>>;
+
+      finalize_spec (ℓ_q : loc) (data : val) :
+        ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
+            hl.(finalize) #ℓ_q data @ ∅
+          <<{ queue_repr ℓ_q vs (Some data) | RET #() }>>;
+
+      try_dequeue_spec (ℓ_q : loc) :
+        ⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>>
+            hl.(try_dequeue) #ℓ_q @ ∅
+          <<{ queue_repr ℓ_q (tail vs) mfin
+            | RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>;
+    }.
+#[global] Arguments fin_queue_iris _ {_} _ : assert.