From 6454d3df4e812d51c1c7e0ebc56c27b836634da0 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre
Date: Fri, 5 Jul 2019 19:27:42 +0200
Subject: [PATCH] Herlihy-Wing queue example (involving prophecy variables)
---
_CoqProject | 2 +
theories/logatom/herlihy_wing_queue/hwq.v | 2869 ++++++++++++++++++++
theories/logatom/herlihy_wing_queue/spec.v | 42 +
3 files changed, 2913 insertions(+)
create mode 100644 theories/logatom/herlihy_wing_queue/hwq.v
create mode 100644 theories/logatom/herlihy_wing_queue/spec.v
diff --git a/_CoqProject b/_CoqProject
index e1480b9..d2d1ae3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -110,3 +110,5 @@ theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v
theories/logatom/proph_erasure.v
+theories/logatom/herlihy_wing_queue/spec.v
+theories/logatom/herlihy_wing_queue/hwq.v
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
new file mode 100644
index 0000000..428c7b4
--- /dev/null
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -0,0 +1,2869 @@
+From iris.algebra Require Import excl auth list gset gmap agree csum.
+From iris.heap_lang Require Export lifting notation.
+From iris.base_logic.lib Require Export invariants proph_map saved_prop.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation par.
+From iris.bi.lib Require Import fractional.
+From iris_examples.logatom.herlihy_wing_queue Require Import spec.
+Set Default Proof Using "Type".
+
+(** * Some library lemmas ***************************************************)
+
+Lemma replicate_S_end {A} (n : nat) (x : A) :
+ replicate (S n) x = replicate n x ++ [x].
+Proof. induction n as [|n IH]; [ done | by rewrite /= -IH ]. Qed.
+
+(* TODO move the following lemmas to std++. *)
+
+Lemma map_imap_id {A} (m : gmap nat A) :
+ map_imap (λ _ e, Some e) m = m.
+Proof.
+ apply map_eq. intros i. rewrite lookup_imap. by destruct (m !! i).
+Qed.
+
+Lemma map_imap_insert {A B} (f : nat → A → option B) (i : nat) (v : A) (m : gmap nat A) :
+ map_imap f (<[i:=v]> m) = match f i v with
+ | None => delete i (map_imap f m)
+ | Some w => <[i:=w]> (map_imap f m)
+ end.
+Proof.
+ destruct (f i v) as [w|] eqn:Hw.
+ - apply map_eq. intros k. rewrite lookup_imap.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ + by rewrite lookup_insert lookup_insert /=.
+ + rewrite lookup_insert_ne; last done.
+ rewrite lookup_insert_ne; last done.
+ by rewrite lookup_imap.
+ - apply map_eq. intros k. rewrite lookup_imap.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ + by rewrite lookup_insert lookup_delete /=.
+ + rewrite lookup_insert_ne; last done.
+ rewrite lookup_delete_ne; last done.
+ by rewrite lookup_imap.
+Qed.
+
+Lemma map_imap_ext {A B} (f1 f2 : nat → A → option B) (m1 m2 : gmap nat A) :
+ dom (gset nat) m2 ⊆ dom (gset nat) m1 →
+ (∀ k v, m1 !! k = Some v → Some (f1 k v) = f2 k <$> (m2 !! k)) →
+ map_imap f1 m1 = map_imap f2 m2.
+Proof.
+ intros Hdom HExt. apply map_eq. intros i.
+ rewrite lookup_imap lookup_imap.
+ destruct (m1 !! i) as [v1|] eqn:Hi1.
+ + specialize (HExt i v1 Hi1).
+ destruct (m2 !! i); by inversion HExt.
+ + destruct (m2 !! i) as [v2|] eqn:Hi2; [ exfalso | done ].
+ assert (i ∈ dom (gset nat) m2) as Hm2.
+ { apply elem_of_dom. by exists v2. }
+ assert (i ∉ dom (gset nat) m1) as Hm1.
+ { by apply not_elem_of_dom. }
+ set_solver.
+Qed.
+
+(** * Implementation and specification of a simple minimum function *********)
+
+Definition minimum : val :=
+ λ: "m" "n",
+ if: "m" < "n" then "m" else "n".
+
+Section minimum.
+
+Context `{!heapG Σ}.
+Notation iProp := (iProp Σ).
+
+Lemma min_spec (m n : nat) :
+ {{{ True }}} minimum #m #n {{{ RET #(m `min` n)%nat; True }}}.
+Proof.
+ iIntros (Φ) "_ HΦ". rewrite /minimum. wp_pures.
+ destruct (decide (m < n)) as [H | H].
+ - rewrite bool_decide_true; last done. wp_pures.
+ rewrite min_l; last omega. by iApply "HΦ".
+ - rewrite bool_decide_false; last done. wp_pures.
+ rewrite min_r; last omega. by iApply "HΦ".
+Qed.
+
+End minimum.
+
+(** * Implementation and specification of a diverging computation ***********)
+
+Definition loop : val :=
+ rec: "loop" "v" := "loop" "v".
+
+Section loop.
+
+Context `{!heapG Σ}.
+Notation iProp := (iProp Σ).
+
+Lemma loop_spec (P : iProp) (v : val) :
+ {{{ True }}} loop v {{{ RET #(); P }}}.
+Proof.
+ iIntros (Φ) "_ HΦ". rewrite /loop. iLöb as "IH". wp_pures.
+ iApply "IH". iApply "HΦ".
+Qed.
+
+Lemma wp_loop (Φ : val -> iProp) : (WP loop #() {{ v, Φ v }})%I.
+Proof.
+ iIntros "". iLöb as "IH". rewrite /loop. wp_pures. iApply "IH".
+Qed.
+
+End loop.
+
+(** * Some array-related notations ******************************************)
+
+Notation "new_array: sz" :=
+ (AllocN sz%E NONEV) (at level 80) : expr_scope.
+
+Notation "e1 <[[ e2 ]]>" :=
+ (BinOp OffsetOp e1%E e2%E) (at level 8) : expr_scope.
+
+(** * Implementation of the queue operations ********************************)
+
+(** new_queue(sz){
+ let ar := new_array sz None in
+ let back := ref 0 in
+ let p := new_proph () in
+ {sz, ar, back, p}
+ } *)
+Definition new_queue : val :=
+ λ: "sz",
+ let: "ar" := new_array: "sz" in
+ let: "back" := ref #0 in (* First free cell. *)
+ let: "p" := NewProph in
+ ("sz", "ar", "back", "p").
+
+(** enqueue(q : queue, x : item){
+ let i : int := FAA(q.back, 1) in
+ if(i < q.size){
+ q.items[i] := x
+ } else {
+ while true;
+ }
+ } *)
+Definition enqueue : val :=
+ λ: "q" "x",
+ let: "q_size" := Fst (Fst (Fst "q")) in
+ let: "q_ar" := Snd (Fst (Fst "q")) in
+ let: "q_back" := Snd (Fst "q") in
+ (* Get the next free index. *)
+ let: "i" := FAA "q_back" #1 in
+ (* Check not full, and actually insert. *)
+ if: "i" < "q_size" then "q_ar"<[["i"]]> <- SOME "x" ;; Skip
+ else loop #().
+
+(** dequeue(q : queue){
+ let range = min(!q.back, q.size) in
+ let rec dequeue_aux(i) =
+ if i = 0 {
+ dequeue(q)
+ } else {
+ let j = range - i in
+ let x = ! q.ar[j] in
+ if x == null {
+ dequeue_aux(i-1)
+ } else {
+ if resolve (CAS q.ar[j] x null) q.p (j, x) {
+ v
+ } else {
+ dequeue_aux(i-1)
+ }
+ }
+ }
+ in
+ dequeue_aux(range)
+ } *)
+Definition dequeue_aux : val :=
+ rec: "loop" "dequeue" "q" "range" "i" :=
+ if: "i" = #0 then "dequeue" "q" else
+ let: "q_ar" := Snd (Fst (Fst "q")) in
+ let: "q_p" := Snd "q" in
+ let: "j" := "range" - "i" in
+ let: "x" := ! "q_ar"<[["j"]]> in
+ match: "x" with
+ NONE => "loop" "dequeue" "q" "range" ("i" - #1)
+ | SOME "v" =>
+ let: "c" := Resolve (CmpXchg ("q_ar"<[["j"]]>) "x" NONE) "q_p" "j" in
+ if: Snd "c" then "v" else "loop" "dequeue" "q" "range" ("i" - #1)
+ end.
+Definition dequeue : val :=
+ rec: "dequeue" "q" :=
+ let: "q_size" := Fst (Fst (Fst "q")) in
+ let: "q_back" := Snd (Fst "q") in
+ let: "range" := minimum !"q_back" "q_size" in
+ dequeue_aux "dequeue" "q" "range" "range".
+
+(** * Definition of the cameras we need for queues **************************)
+
+Definition prod4R A B C D E :=
+ prodR (prodR (prodR (prodR A B) C) D) E.
+
+Definition oneshotUR := optionUR $ csumR (exclR unitR) (agreeR unitR).
+Definition shot : oneshotUR := Some $ Cinr $ to_agree ().
+Definition not_shot : oneshotUR := Some $ Cinl $ Excl ().
+
+Definition per_slot :=
+ prod4R
+ (* Unique token for the index. *)
+ (optionUR $ exclR unitR)
+ (* The location stored at our index, which always remains the same. *)
+ (optionUR $ agreeR locO)
+ (* Possible unique name for the index, only if being helped. *)
+ (optionUR $ exclR gnameO)
+ (* One shot witnessing the transition from pending to helped. *)
+ oneshotUR
+ (* One shot witnessing the physical writing of the value in the slot. *)
+ oneshotUR.
+
+Definition eltsUR := authR $ optionUR $ exclR $ listO locO.
+Definition contUR := csumR (exclR unitR) (agreeR (prodO natO natO)).
+Definition slotUR := authR $ gmapUR nat per_slot.
+Definition backUR := authR mnatUR.
+
+Class hwqG Σ :=
+ HwqG {
+ hwq_arG :> inG Σ eltsUR; (** Logical contents of the queue. *)
+ hwq_contG :> inG Σ contUR; (** One-shot for contradiction states. *)
+ hwq_slotG :> inG Σ slotUR; (** State data for used array slots. *)
+ hwq_back :> inG Σ backUR; (** Used to show that back only increases. *)
+ }.
+
+Definition hwqΣ : gFunctors :=
+ #[GFunctor eltsUR; GFunctor contUR; GFunctor slotUR; GFunctor backUR].
+
+Instance subG_hwqΣ {Σ} : subG hwqΣ Σ → hwqG Σ.
+Proof. solve_inG. Qed.
+
+(** * The specifiaction... **************************************************)
+
+Section herlihy_wing_queue.
+
+Context `{!heapG Σ, !savedPropG Σ, !hwqG Σ}.
+Context (N : namespace).
+Notation iProp := (iProp Σ).
+Implicit Types γe γc γs : gname.
+Implicit Types sz : nat.
+Implicit Types ℓ_ar ℓ_back : loc.
+Implicit Types p : proph_id.
+Implicit Types v : val.
+Implicit Types pvs : list nat.
+
+(** Operations for the CMRA representing the logical contents of the queue. *)
+
+Lemma new_elts l : (|==> ∃ γe, own γe (● Excl' l) ∗ own γe (◯ Excl' l))%I.
+Proof.
+ iMod (own_alloc (● Excl' l ⋅ ◯ Excl' l)) as (γe) "[H● H◯]".
+ - by apply auth_both_valid.
+ - iModIntro. iExists γe. iFrame.
+Qed.
+
+Lemma sync_elts γe (l1 l2 : list loc) :
+ own γe (● Excl' l1) -∗ own γe (◯ Excl' l2) -∗ ⌜l1 = l2⌝.
+Proof.
+ iIntros "H● H◯". iCombine "H●" "H◯" as "H".
+ iDestruct (own_valid with "H") as "H".
+ by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
+Qed.
+
+Lemma update_elts γe (l1 l2 l : list loc) :
+ own γe (● Excl' l1) -∗ own γe (◯ Excl' l2) ==∗
+ own γe (● Excl' l) ∗ own γe (◯ Excl' l).
+Proof.
+ iIntros "H● H◯". iCombine "H●" "H◯" as "H". rewrite -own_op.
+ iApply (own_update with "H").
+ by apply auth_update, option_local_update, exclusive_local_update.
+Qed.
+
+(* Fragmental part, made available during atomic updates. *)
+Definition hwq_cont γe (elts : list loc) : iProp :=
+ own γe (◯ Excl' elts).
+
+Lemma hwq_cont_exclusive γe elts1 elts2 :
+ hwq_cont γe elts1 -∗ hwq_cont γe elts2 -∗ False.
+Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
+
+(** Operations for the CMRA used to show that back only increases. *)
+
+Definition back_value γb n := own γb (● (n : mnatUR) : backUR).
+Definition back_lower_bound γb n := own γb (◯ (n : mnatUR) : backUR).
+
+Lemma new_back : (|==> ∃ γb, back_value γb 0%nat)%I.
+Proof.
+ iMod (own_alloc (● (0%nat : mnatUR) : backUR)) as (γb) "H●".
+ - by rewrite auth_auth_valid.
+ - by iExists γb.
+Qed.
+
+Lemma back_incr γb n :
+ (back_value γb n ==∗ back_value γb (S n)%nat)%I.
+Proof.
+ iIntros "H●". iMod (own_update with "H●") as "[$ _]"; last done.
+ apply auth_update_alloc, (mnat_local_update _ _ (S n)). by lia.
+Qed.
+
+Lemma back_snapshot γb n :
+ (back_value γb n ==∗ back_value γb n ∗ back_lower_bound γb n)%I.
+Proof.
+ iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
+ by apply auth_update_alloc, mnat_local_update.
+Qed.
+
+Lemma back_le γb n1 n2 :
+ (back_value γb n1 -∗ back_lower_bound γb n2 -∗ ⌜n2 ≤ n1⌝%nat)%I.
+Proof.
+ iIntros "H1 H2". iCombine "H1 H2" as "H".
+ iDestruct (own_valid with "H") as %Hvalid. iPureIntro.
+ apply auth_both_valid in Hvalid as [H1 H2].
+ by apply mnat_included.
+Qed.
+
+(* Stores a lower bound on the [i2] part of any contradiction that
+ has arised or may arise in the future. *)
+Definition i2_lower_bound γi n := back_value γi n.
+
+(* Witness that the [i2] part of any (future or not) contradicton is
+ greater than [n]. *)
+Definition no_contra_wit γi n := back_lower_bound γi n.
+
+Lemma i2_lower_bound_update γi n m :
+ (n ≤ m)%nat →
+ (i2_lower_bound γi n ==∗ i2_lower_bound γi m)%I.
+Proof.
+ iIntros (H) "H●". iMod (own_update with "H●") as "[$ _]"; last done.
+ apply auth_update_alloc, (mnat_local_update _ _ m). by lia.
+Qed.
+
+Lemma i2_lower_bound_snapshot γi n :
+ (i2_lower_bound γi n ==∗ i2_lower_bound γi n ∗ no_contra_wit γi n)%I.
+Proof.
+ iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
+ by apply auth_update_alloc, mnat_local_update.
+Qed.
+
+(** Operations for the one-shot CMRA used for contradiction states. *)
+
+(** Element for "no contradiction yet". *)
+Definition no_contra γc :=
+ own γc (Cinl (Excl ())).
+
+(** Element witnessing a contradiction [(i1, i2)]. *)
+Definition contra γc (i1 i2 : nat) :=
+ own γc (Cinr (to_agree (i1, i2))).
+
+Lemma new_no_contra : (|==> ∃ γc, no_contra γc)%I.
+Proof. by apply own_alloc. Qed.
+
+Lemma to_contra i1 i2 γc : no_contra γc ==∗ contra γc i1 i2.
+Proof. apply own_update. by apply cmra_update_exclusive. Qed.
+
+Lemma contra_not_no_contra i1 i2 γc :
+ (no_contra γc -∗ contra γc i1 i2 -∗ False)%I.
+Proof. iIntros "HnoC HC". iDestruct (own_valid_2 with "HnoC HC") as %[]. Qed.
+
+Lemma contra_agree i1 i2 i1' i2' γc :
+ (contra γc i1 i2 -∗ contra γc i1' i2' -∗ ⌜i1' = i1 ∧ i2' = i2⌝)%I.
+Proof.
+ iIntros "HC HC'". iDestruct (own_valid_2 with "HC HC'") as %H.
+ iPureIntro. apply agree_op_invL' in H. by inversion H.
+Qed.
+
+Global Instance contra_persistent γc i1 i2 : Persistent (contra γc i1 i2).
+Proof. apply own_core_persistent. by rewrite /CoreId. Qed.
+
+(** Operations for the state data. *)
+
+Inductive state :=
+ (** Help was requested (element not committed). *)
+ | Pend : gname → state
+ (** Help has been provided (element committed). *)
+ | Help : gname → state
+ (** The enqueue operation known it has been committed. *)
+ | Done : state.
+
+Instance state_inhabited : Inhabited state.
+Proof. constructor. refine Done. Qed.
+
+(** Data associated to each slot. The four components are:
+ - the location that is being written in the slot,
+ - a possible name for a stored proposition containing the postcondition
+ of the atomic update of the enqueue happening for the slot (used only
+ in case of helping),
+ - state of the slot,
+ - [true] if a value was physically written in the slot. *)
+Definition slot_data : Type := loc * state * bool.
+
+Implicit Types slots : gmap nat slot_data.
+
+Definition update_slot i f slots :=
+ match slots !! i with
+ | Some d => <[i := f d]> (delete i slots)
+ | None => slots
+ end.
+
+Definition val_of (data : slot_data) : loc :=
+ match data with (l, _, _) => l end.
+
+Definition state_of (data : slot_data) : state :=
+ match data with (_, s, _) => s end.
+
+Definition name_of (data : slot_data) : option gname :=
+ match state_of data with Pend γ => Some γ | Help γ => Some γ | _ => None end.
+
+Definition was_written (data : slot_data) : bool :=
+ match data with (_, _, b) => b end.
+
+Definition was_committed (data : slot_data) : bool :=
+ match state_of data with Pend _ => false | _ => true end.
+
+Definition set_written (data : slot_data) : slot_data :=
+ match data with (l, s, _) => (l, s, true) end.
+
+Definition set_written_and_done (data : slot_data) : slot_data :=
+ match data with (l, _, _) => (l, Done, true) end.
+
+Definition to_helped (γ : gname) (data : slot_data) : slot_data :=
+ match data with (l, _, w) => (l, Help γ, w) end.
+
+Definition to_done (data : slot_data) : slot_data :=
+ match data with (l, _, w) => (l, Done, w) end.
+
+Definition physical_value (data : slot_data) : val :=
+ match data with (l, _, w) => if w then SOMEV #l else NONEV end.
+
+Lemma val_of_set_written d : val_of (set_written d) = val_of d.
+Proof. by destruct d as [[l s] w]. Qed.
+
+Lemma was_written_set_written d : was_written (set_written d) = true.
+Proof. by destruct d as [[l s] w]. Qed.
+
+Lemma state_of_set_written d : state_of (set_written d) = state_of d.
+Proof. by destruct d as [[l s] w]. Qed.
+
+Definition of_slot_data (data : slot_data) : per_slot :=
+ match data with
+ | (l, s, w) =>
+ let name := match s with Pend γ => Excl' γ | Help γ => Excl' γ | Done => None end in
+ let comm := if was_committed data then shot else not_shot in
+ let wr := if w then shot else not_shot in
+ (Excl' (), Some (to_agree l), name, comm, wr)
+ end.
+
+Lemma of_slot_data_valid d : ✓ of_slot_data d.
+Proof. by destruct d as [[l []] []]. Qed.
+
+(* The (unique) token for slot [i]. *)
+Definition slot_token γs i :=
+ own γs (◯ {[i := (Excl' (), None, None, None, None)]} : slotUR).
+
+(* A witness that the location enqueued in slot [i] is [l]. *)
+Definition slot_val_wit γs i l :=
+ own γs (◯ {[i := (None, Some (to_agree l), None, None, None)]} : slotUR).
+
+(* A witness that the element inserted at slot [i] has been committed. *)
+Definition slot_committed_wit γs i :=
+ own γs (◯ {[i := (None, None, None, shot, None)]} : slotUR).
+
+Definition slot_name_tok γs i γ :=
+ own γs (◯ {[i := (None, None, Excl' γ, None, None)]} : slotUR).
+
+(* A witness that the element inserted at slot [i] has been written. *)
+Definition slot_written_wit γs i :=
+ own γs (◯ {[i := (None, None, None, None, shot)]} : slotUR).
+
+(* A token proving that the enqueue in slot [i] has not been commited. *)
+Definition slot_pending_tok γs i :=
+ own γs (◯ {[i := (None, None, None, not_shot, None)]} : slotUR).
+
+(* A token proving that no value has been written in slot [i]. *)
+Definition slot_writing_tok γs i :=
+ own γs (◯ {[i := (None, None, None, None, not_shot)]} : slotUR).
+
+(* Initial slot data, with not allocated slots. *)
+Lemma new_slots : (|==> ∃ γs, own γs (● ∅))%I.
+Proof.
+ iMod (own_alloc (● ∅ ⋅ ◯ ∅)) as (γs) "[H● _]".
+ - by apply auth_both_valid.
+ - iModIntro. iExists γs. iFrame.
+Qed.
+
+(* Allocate a new slot with data [d] at the fresh index [i]. *)
+Lemma alloc_slot γs slots (i : nat) (d : slot_data) :
+ slots !! i = None →
+ own γs (● (of_slot_data <$> slots) : slotUR) ==∗
+ own γs (● (of_slot_data <$> (<[i := d]> slots)) : slotUR) ∗
+ own γs (◯ {[i := of_slot_data d]} : slotUR).
+Proof.
+ iIntros (Hi) "H". rewrite -own_op fmap_insert.
+ iApply (own_update with "H"). apply auth_update_alloc.
+ apply alloc_singleton_local_update.
+ - by rewrite lookup_fmap Hi.
+ - apply of_slot_data_valid.
+Qed.
+
+Lemma alloc_done_slot γs slots i l :
+ slots !! i = None →
+ own γs (● (of_slot_data <$> slots) : slotUR) ==∗
+ own γs (● (of_slot_data <$> (<[i := (l, Done, false)]> slots)) : slotUR) ∗
+ slot_token γs i ∗
+ slot_val_wit γs i l ∗
+ slot_committed_wit γs i ∗
+ slot_writing_tok γs i.
+Proof.
+ iIntros (Hi) "H". iMod (alloc_slot _ _ _ _ Hi with "H") as "[$ Hi]".
+ repeat rewrite -own_op. repeat rewrite -auth_frag_op.
+ repeat rewrite -insert_op. repeat rewrite left_id.
+ by rewrite insert_empty.
+Qed.
+
+Lemma alloc_pend_slot γs slots i l γ :
+ slots !! i = None →
+ own γs (● (of_slot_data <$> slots) : slotUR) ==∗
+ own γs (● (of_slot_data <$> (<[i := (l, Pend γ, false)]> slots)) : slotUR) ∗
+ slot_token γs i ∗
+ slot_val_wit γs i l ∗
+ slot_pending_tok γs i ∗
+ slot_name_tok γs i γ ∗
+ slot_writing_tok γs i.
+Proof.
+ iIntros (Hi) "H". iMod (alloc_slot _ _ _ _ Hi with "H") as "[$ Hi]".
+ repeat rewrite -own_op. repeat rewrite -auth_frag_op.
+ repeat rewrite -insert_op. repeat rewrite left_id.
+ by rewrite insert_empty.
+Qed.
+
+Lemma use_val_wit γs slots i l :
+ (own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_val_wit γs i l -∗
+ ⌜val_of <$> slots !! i = Some l⌝)%I.
+Proof.
+ iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+ destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
+ destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
+ inversion_clear H1; rename H into H1.
+ destruct H2 as [H2|[a [b (H21 & H22 & H23)]]]; first done. simplify_eq.
+ simpl. destruct b as [[[[b1 b2] b3] b4] b5].
+ destruct d as [[dl ds] dw].
+ destruct H1 as [[[[_ H1] _] _] _]; simpl in H1. simpl. f_equal.
+ destruct H23 as [H2|H2].
+ - destruct H2 as [[[[_ H2] _] _] _]; simpl in H2.
+ assert (Some (to_agree l) ≡ Some (to_agree dl)) as H by by transitivity b2.
+ apply Some_equiv_inj, to_agree_inj in H. done.
+ - apply prod_included in H2 as [H2 _]; simpl in H2.
+ apply prod_included in H2 as [H2 _]; simpl in H2.
+ apply prod_included in H2 as [H2 _]; simpl in H2.
+ apply prod_included in H2 as [_ H2]; simpl in H2.
+ assert (Some (to_agree l) ≼ Some (to_agree dl)) as H by set_solver.
+ apply option_included in H.
+ destruct H as [H|[a [b (H11 & H12 & H13)]]]; first done.
+ simplify_eq. destruct H13 as [H|H].
+ + by apply to_agree_inj in H.
+ + by apply to_agree_included in H.
+Qed.
+
+Lemma use_name_tok γs slots i γ :
+ (own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_name_tok γs i γ -∗
+ ⌜name_of <$> slots !! i = Some (Some γ)⌝)%I.
+Proof.
+ iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+ destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
+ destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
+ inversion_clear H1; rename H into H1.
+ destruct H2 as [H2|[a [b (H21 & H22 & H23)]]]; first done. simplify_eq.
+ simpl. destruct b as [[[[b1 b2] b3] b4] b5].
+ destruct d as [[dl ds] dw].
+ destruct H1 as [[[[_ _] H1] _] _]; simpl in H1. simpl. f_equal.
+ destruct H23 as [H2|H2].
+ - destruct H2 as [[[[_ _] H2] _] _]; simpl in H2.
+ destruct ds as [γ'|γ'|]; rewrite /name_of /=; try f_equal.
+ + assert (Excl' γ ≡ Excl' γ') as H by by transitivity b3.
+ inversion H as [x y HH|]. by inversion HH.
+ + assert (Excl' γ ≡ Excl' γ') as H by by transitivity b3.
+ inversion H as [x y HH|]. by inversion HH.
+ + assert (Excl' γ ≡ None) as H by by transitivity b3.
+ inversion H.
+ - apply prod_included in H2 as [H2 _]; simpl in H2.
+ apply prod_included in H2 as [H2 _]; simpl in H2.
+ apply prod_included in H2 as [_ H2]; simpl in H2.
+ destruct ds as [γ'|γ'|]; rewrite /name_of /=; try f_equal.
+ + assert (Excl' γ ≼ Excl' γ') as H by set_solver.
+ by apply Excl_included in H.
+ + assert (Excl' γ ≼ Excl' γ') as H by set_solver.
+ by apply Excl_included in H.
+ + assert (Excl' γ ≼ None) as H by set_solver.
+ exfalso. apply option_included in H as [H|H]; first done.
+ destruct H as [a [b (H11 & H12 & H13)]]. by simplify_eq.
+Qed.
+
+Lemma shot_not_equiv_not_shot : shot ≢ not_shot.
+Proof.
+ intros H. rewrite /shot /not_shot in H.
+ inversion H as [x y HAbsurd|]. inversion HAbsurd.
+Qed.
+
+Lemma shot_not_equiv_not_shot' e : shot ≢ not_shot ⋅ e.
+Proof.
+ intros H. rewrite /shot /not_shot in H.
+ destruct e as [e|]; first destruct e.
+ - rewrite -Some_op Cinl_op in H.
+ inversion H as [x y Habsurd|]; inversion Habsurd.
+ - rewrite -Some_op in H. compute in H.
+ inversion H as [x y HAbsurd|]. inversion HAbsurd.
+ - inversion H as [x y HAbsurd|]. inversion HAbsurd.
+ - inversion H as [x y HAbsurd|]. inversion HAbsurd.
+Qed.
+
+Lemma shot_not_included_not_shot : ¬ shot ≼ not_shot.
+Proof.
+ intros H. rewrite /shot /not_shot in H.
+ apply option_included in H. destruct H as [H|H]; first done.
+ destruct H as [a [b (H1 & H2 & [H3|H3])]].
+ - simplify_eq. by inversion H3.
+ - simplify_eq. apply csum_included in H3.
+ destruct H3 as [H3|H3]; first done. destruct H3 as [H3|H3].
+ + destruct H3 as [a [b (H1 & H2 & H3)]]. by inversion H1.
+ + destruct H3 as [a [b (H1 & H2 & H3)]]. by inversion H1.
+Qed.
+
+Lemma use_committed_wit γs slots i :
+ (own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_committed_wit γs i -∗
+ ⌜was_committed <$> slots !! i = Some true⌝)%I.
+Proof.
+ iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+ destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
+ destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
+ inversion_clear H1; rename H into H1.
+ destruct H2 as [H2|[a [b (H21 & H22 & H23)]]]; first done. simplify_eq.
+ simpl. destruct b as [[[[b1 b2] b3] b4] b5].
+ destruct d as [[dl ds] dw].
+ destruct H1 as [[[[_ _] _] H1]]; simpl in H1. f_equal.
+ destruct (was_committed (dl, ds, dw)); first done. exfalso.
+ destruct H23 as [H2|H2].
+ - destruct H2 as [[[[_ _] _] H2] _]; simpl in H2.
+ apply shot_not_equiv_not_shot. set_solver.
+ - apply prod_included in H2 as [H2 _]; simpl in H2.
+ apply prod_included in H2 as [_ H2]; simpl in H2.
+ apply shot_not_included_not_shot. set_solver.
+Qed.
+
+Lemma use_written_wit γs slots i :
+ (own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_written_wit γs i -∗
+ ⌜was_written <$> slots !! i = Some true⌝)%I.
+Proof.
+ iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+ destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
+ destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
+ inversion_clear H1; rename H into H1.
+ destruct H2 as [H2|[a [b (H21 & H22 & H23)]]]; first done. simplify_eq.
+ simpl. destruct b as [[[[b1 b2] b3] b4] b5]. destruct d as [[dl ds] dw].
+ destruct H1 as [[[[_ _] _] _] H1]; simpl in H1. f_equal.
+ destruct dw; first done. exfalso.
+ destruct H23 as [H2|H2].
+ - destruct H2 as [[[[_ _] _] _] H2]; simpl in H2.
+ exfalso. apply shot_not_equiv_not_shot. set_solver.
+ - apply prod_included in H2 as [_ H2]; simpl in H2.
+ exfalso. apply shot_not_included_not_shot. set_solver.
+Qed.
+
+Lemma use_writing_tok γs i slots :
+ own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_writing_tok γs i ==∗
+ own γs (● (of_slot_data <$> update_slot i set_written slots) : slotUR) ∗
+ slot_written_wit γs i.
+Proof.
+ iIntros "Hs● Htok". iCombine "Hs● Htok" as "H". rewrite -own_op.
+ iDestruct (own_valid with "H") as %Hvalid.
+ iApply (own_update with "H").
+ apply auth_both_valid in Hvalid as [H1 H2].
+ apply singleton_included in H1 as [e (H1_1 & H1_2)].
+ rewrite lookup_fmap in H1_1.
+ destruct (slots !! i) as [[[l s] w]|] eqn:Hi; last by inversion H1_1.
+ apply Some_equiv_inj in H1_1.
+ assert (w = false) as ->.
+ { destruct w; [ exfalso | done ].
+ apply Some_included in H1_2 as [H1_2|H1_2].
+ - assert ((None, None, None, None, not_shot)
+ ≡ of_slot_data (l, s, true)) as Hequiv by by transitivity e.
+ destruct Hequiv as [[[[_ _] _] _] Hequiv]; simpl in Hequiv.
+ by apply shot_not_equiv_not_shot.
+ - destruct H1_2 as [f H1_2].
+ assert ((None, None, None, None, not_shot) ⋅ f
+ ≡ of_slot_data (l, s, true)) as Hequiv by by transitivity e.
+ destruct Hequiv as [[[[_ _] _] _] Hequiv]; simpl in Hequiv.
+ by eapply shot_not_equiv_not_shot'. }
+ rewrite /update_slot Hi insert_delete fmap_insert.
+ apply auth_update. eapply (singleton_local_update _ i).
+ { by rewrite lookup_fmap Hi. }
+ rewrite /set_written. apply prod_local_update; first done. simpl.
+ by apply option_local_update, exclusive_local_update.
+Qed.
+
+Lemma writing_tok_not_written γs slots i :
+ own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_writing_tok γs i -∗
+ ⌜was_written <$> slots !! i = Some false⌝.
+Proof.
+ iIntros "Hs● Htok". iCombine "Hs● Htok" as "H".
+ iDestruct (own_valid with "H") as %Hvalid%auth_both_valid.
+ iPureIntro. destruct Hvalid as [H1 H2].
+ apply singleton_included in H1 as [e (H1_1 & H1_2)].
+ rewrite lookup_fmap in H1_1.
+ destruct (slots !! i) as [[[l s] w]|]; last by inversion H1_1.
+ apply Some_equiv_inj in H1_1. simpl. f_equal. destruct w; last done.
+ exfalso. apply Some_included in H1_2 as [H1_2|H1_2].
+ - assert ((None, None, None, None, not_shot)
+ ≡ of_slot_data (l, s, true)) as Hequiv by by transitivity e.
+ destruct Hequiv as [[[[_ _] _] _] Hequiv]; simpl in Hequiv.
+ by apply shot_not_equiv_not_shot.
+ - destruct H1_2 as [f H1_2].
+ assert ((None, None, None, None, not_shot) ⋅ f
+ ≡ of_slot_data (l, s, true)) as Hequiv by by transitivity e.
+ destruct Hequiv as [[[[_ _] _] _] Hequiv]; simpl in Hequiv.
+ by eapply shot_not_equiv_not_shot'.
+Qed.
+
+Lemma None_op {A : cmraT} : (None : optionUR A) ⋅ None = None.
+Proof. done. Qed.
+
+Lemma use_pending_tok γs i γ slots :
+ state_of <$> slots !! i = Some (Pend γ) →
+ own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_pending_tok γs i ==∗
+ own γs (● (of_slot_data <$> update_slot i (to_helped γ) slots) : slotUR) ∗
+ slot_committed_wit γs i.
+Proof.
+ iIntros (Hlookup) "Hs● Htok". iCombine "Hs● Htok" as "H".
+ rewrite -own_op. iDestruct (own_valid with "H") as %Hvalid.
+ iApply (own_update with "H").
+ apply auth_both_valid in Hvalid as [H1 H2].
+ apply singleton_included in H1 as [e (H1_1 & H1_2)].
+ rewrite lookup_fmap in H1_1.
+ destruct (slots !! i) as [[[l s] w]|] eqn:Hi; last by inversion H1_1.
+ simpl in Hlookup. inversion Hlookup; subst s.
+ rewrite /update_slot Hi insert_delete fmap_insert.
+ apply auth_update. repeat rewrite pair_op.
+ eapply (singleton_local_update _ i). { by rewrite lookup_fmap Hi. }
+ rewrite /to_helped. repeat rewrite None_op.
+ repeat apply prod_local_update; try done.
+ by apply option_local_update, exclusive_local_update.
+Qed.
+
+Lemma slot_token_exclusive γs i :
+ slot_token γs i -∗ slot_token γs i -∗ False.
+Proof.
+ iIntros "H1 H2". iCombine "H1 H2" as "H".
+ iDestruct (own_valid with "H") as %H. iPureIntro.
+ move:H =>/auth_frag_valid H. apply singleton_valid in H.
+ by repeat apply pair_valid in H as [H _]; simpl in H.
+Qed.
+
+Lemma helped_to_done_aux γs i γ slots :
+ state_of <$> slots !! i = Some (Help γ) →
+ own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_name_tok γs i γ ==∗
+ own γs (● (of_slot_data <$> update_slot i to_done slots) : slotUR) ∗
+ own γs (◯ {[i := (None, None, None, None, None)]} : slotUR).
+Proof.
+ iIntros (H) "H1 H2". iCombine "H1 H2" as "H".
+ iDestruct (own_valid with "H") as %Hvalid. rewrite -own_op.
+ iApply (own_update with "H"). apply auth_update. rewrite /update_slot.
+ destruct (slots !! i) as [d|] eqn:Hd; last by inversion H.
+ rewrite insert_delete fmap_insert. eapply singleton_local_update.
+ { by rewrite lookup_fmap Hd /=. }
+ destruct d as [[dl ds] dw]. inversion H; subst ds; simpl.
+ repeat apply prod_local_update; try done. simpl.
+ apply delete_option_local_update. apply _.
+Qed.
+
+Lemma helped_to_done γs i γ slots :
+ state_of <$> slots !! i = Some (Help γ) →
+ own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_name_tok γs i γ ==∗
+ own γs (● (of_slot_data <$> update_slot i to_done slots) : slotUR).
+Proof.
+ iIntros (H) "H1 H2". by iMod (helped_to_done_aux with "H1 H2") as "[H _]".
+Qed.
+
+Lemma val_wit_from_auth γs i l slots :
+ val_of <$> slots !! i = Some l →
+ own γs (● (of_slot_data <$> slots) : slotUR) ==∗
+ own γs (● (of_slot_data <$> slots) : slotUR) ∗
+ slot_val_wit γs i l.
+Proof.
+ iIntros (H) "H". rewrite -own_op. iApply (own_update with "H").
+ apply auth_update_core_id; first apply _.
+ assert (∃ d, slots !! i = Some d) as [d Hlookup].
+ { destruct (slots !! i) as [d|]; inversion H. by exists d. }
+ apply singleton_included. rewrite lookup_fmap. rewrite Hlookup /=.
+ exists (of_slot_data d). split; first done.
+ apply Some_included. right. destruct d as [[dl ds] dw]. simpl.
+ repeat (apply prod_included; split; simpl);
+ try by (apply option_included; left).
+ apply option_included; right. exists (to_agree l), (to_agree dl).
+ repeat (split; first done). left.
+ rewrite Hlookup /= in H. by inversion H.
+Qed.
+
+(** * Prophecy abstractions *************************************************)
+
+Fixpoint proph_data sz (deq : gset nat) (rs : list (val * val)) : list nat :=
+ match rs with
+ | (PairV _ #true , LitV (LitInt i)) :: rs =>
+ if decide (0 ≤ i < sz) then
+ let i := Z.to_nat i in
+ if decide (i ∈ deq) then
+ []
+ else
+ i :: proph_data sz ({[i]} ∪ deq) rs
+ else []
+ | (PairV _ #false, LitV (LitInt i)) :: rs =>
+ if decide (0 ≤ i < sz) then
+ proph_data sz deq rs
+ else
+ []
+ | _ => []
+ end.
+
+(* Wrapper for the Iris [proph] proposition, using our data abstraction. *)
+Definition hwq_proph p sz deq pvs :=
+ (∃ rs, proph p rs ∗ ⌜pvs = proph_data sz deq rs⌝)%I.
+
+Lemma proph_data_deq sz deq rs : ∀ i, i ∈ deq → i ∉ proph_data sz deq rs.
+Proof.
+ revert deq. induction rs as [|[b k] rs IH]; intros deq i Hi.
+ - apply not_elem_of_nil.
+ - destruct b; simpl; try by apply not_elem_of_nil.
+ destruct b2; simpl; try by apply not_elem_of_nil.
+ destruct l; simpl; try by apply not_elem_of_nil.
+ destruct b.
+ + destruct k; simpl; try by apply not_elem_of_nil.
+ destruct l; simpl; try by apply not_elem_of_nil.
+ destruct (decide (0 ≤ n < sz)); last by apply not_elem_of_nil.
+ destruct (decide (Z.to_nat n ∈ deq)); first by apply not_elem_of_nil.
+ apply not_elem_of_cons. split; first by set_solver.
+ apply IH. set_solver.
+ + destruct k; simpl; try by apply not_elem_of_nil.
+ destruct l; simpl; try by apply not_elem_of_nil.
+ destruct (decide (0 ≤ n < sz)); last by apply not_elem_of_nil.
+ apply IH. done.
+Qed.
+
+Lemma proph_data_sz sz deq rs : ∀ i, i ∈ proph_data sz deq rs → (i < sz)%nat.
+Proof.
+ revert deq. induction rs as [|[b k] rs IH]; intros deq i Hi.
+ - set_solver.
+ - destruct b; simpl; try by set_solver.
+ destruct b2; simpl; try by set_solver.
+ destruct l; simpl; try by set_solver.
+ destruct b.
+ + destruct k; simpl; try by set_solver.
+ destruct l; simpl; try by set_solver.
+ simpl in Hi.
+ destruct (decide (0 ≤ n < sz)) as [Hn|Hn]; last by set_solver.
+ destruct (decide (Z.to_nat n ∈ deq)) as [H|H]; first by set_solver.
+ apply elem_of_cons in Hi. destruct Hi as [->|Hi].
+ * apply Nat2Z.inj_lt. destruct Hn as [Hn1 Hn2]. by rewrite Z2Nat.id.
+ * by apply (IH _ _ Hi).
+ + destruct k; simpl; try by set_solver.
+ destruct l; simpl; try by set_solver.
+ simpl in Hi.
+ destruct (decide (0 ≤ n < sz)); last by set_solver.
+ apply (IH _ _ Hi).
+Qed.
+
+Lemma proph_data_NoDup sz deq rs :
+ NoDup (proph_data sz deq rs ++ elements deq).
+Proof.
+ revert deq. induction rs as [|[b k] rs IH]; intros deq.
+ - apply NoDup_elements.
+ - destruct b; simpl; try by apply NoDup_elements.
+ destruct b2; simpl; try by apply NoDup_elements.
+ destruct l; simpl; try by apply NoDup_elements.
+ destruct b.
+ + destruct k; simpl; try by apply NoDup_elements.
+ destruct l; simpl; try by apply NoDup_elements.
+ destruct (decide (0 ≤ n < sz))
+ as [Hn|Hn]; last by apply NoDup_elements.
+ destruct (decide (Z.to_nat n ∈ deq))
+ as [Hn_in_deq|Hn_not_in_deq]; first by apply NoDup_elements.
+ specialize (IH ({[Z.to_nat n]} ∪ deq)) as H1.
+ assert (Z.to_nat n ∉ proph_data sz ({[Z.to_nat n]} ∪ deq) rs) as H2.
+ { apply proph_data_deq. by set_solver. }
+ apply NoDup_app in H1 as (H1_1 & H1_2 & H1_3).
+ apply NoDup_app. repeat split_and.
+ * by apply NoDup_cons.
+ * intros i Hi. apply elem_of_cons in Hi as [Hi|Hi]; first by set_solver.
+ intros H_elements%elem_of_elements.
+ eapply (proph_data_deq sz ({[Z.to_nat n]} ∪ deq) rs i); by set_solver.
+ * by apply NoDup_elements.
+ + destruct k; simpl; try by apply NoDup_elements.
+ destruct l; simpl; try by apply NoDup_elements.
+ destruct (decide (0 ≤ n < sz)); [ by apply IH | by apply NoDup_elements ].
+Qed.
+
+Definition block : Type := nat * list nat.
+Definition blocks : Type := list block.
+
+(* A block is valid if it follows the structure described above. *)
+Definition block_valid slots (b : block) :=
+ slots !! b.1 = None ∧
+ ∀ i, i ∈ b.2 → was_committed <$> (slots !! i) = Some false.
+
+Fixpoint glue_blocks (b : block) (i : nat) (bs : blocks) : blocks :=
+ match bs with
+ | [] => [b]
+ | (j, pends) :: bs => if decide (i = j) then (b.1, b.2 ++ i :: pends) :: bs
+ else b :: glue_blocks (j, pends) i bs
+ end.
+
+Fixpoint flatten_blocks bs : list nat :=
+ match bs with
+ | [] => []
+ | (i, pends) :: bs => i :: pends ++ flatten_blocks bs
+ end.
+
+Lemma blocks_elem1 b blocks :
+ b ∈ blocks → b.1 ∈ flatten_blocks blocks.
+Proof.
+ intros H. induction blocks as [|b' blocks IH]; first by inversion H.
+ destruct (decide (b' = b)) as [->|Hb_not_b'].
+ - destruct b as [b_u b_ps]. by apply elem_of_list_here.
+ - destruct b' as [b'_u b'_bs]. simpl.
+ apply elem_of_list_further. apply elem_of_app; right.
+ apply IH. apply elem_of_cons in H as [H|H]; last done.
+ by rewrite H in Hb_not_b'.
+Qed.
+
+Lemma blocks_elem2 b blocks :
+ b ∈ blocks → ∀ i, i ∈ b.2 → i ∈ flatten_blocks blocks.
+Proof.
+ intros H. induction blocks as [|b' blocks IH]; first by inversion H.
+ destruct (decide (b' = b)) as [->|Hb_not_b'].
+ - destruct b as [b_u b_ps]. intros i Hi. simpl in *.
+ apply elem_of_list_further. apply elem_of_app. by left.
+ - destruct b' as [b'_u b'_bs]. simpl. intros i Hi.
+ apply elem_of_list_further. apply elem_of_app; right.
+ apply IH; last done. apply elem_of_cons in H as [H|H]; last done.
+ by rewrite H in Hb_not_b'.
+Qed.
+
+Lemma glue_blocks_valid slots i b_unused b_pendings blocks l γ :
+ slots !! i = None →
+ b_unused ≠ i →
+ NoDup (b_unused :: b_pendings ++ flatten_blocks blocks) →
+ (∀ b : block, b ∈ (b_unused, b_pendings) :: blocks → block_valid slots b) →
+ ∀ b, b ∈ glue_blocks (b_unused, b_pendings) i blocks → block_valid (<[i:=(l, Pend γ, false)]> slots) b.
+Proof using N heapG0 hwqG0 savedPropG0 Σ.
+ intros Hi. revert b_unused b_pendings.
+ induction blocks as [|[b_u b_ps] blocks IH];
+ intros b_unused b_pendings Hb_unused_not_i HND Hblocks_valid [b_u' b_ps'] Hb.
+ - apply Hblocks_valid in Hb as Hvalid.
+ apply elem_of_list_singleton in Hb. simplify_eq.
+ destruct Hvalid as (Hvalid1 & Hvalid2). split.
+ + by rewrite lookup_insert_ne.
+ + simpl in *. intros k Hk. specialize (Hvalid2 _ Hk) as Hvalid_k.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ * by rewrite lookup_insert.
+ * by rewrite lookup_insert_ne.
+ - simpl in Hb. destruct (decide (i = b_u)) as [->|Hi_not_b_u].
+ + apply elem_of_cons in Hb as [Hb|Hb].
+ * simplify_eq.
+ assert ((b_unused, b_pendings) ∈ (b_unused, b_pendings) :: (b_u, b_ps) :: blocks)
+ as Hvalid%Hblocks_valid by set_solver.
+ destruct Hvalid as (Hvalid1 & Hvalid2).
+ assert ((b_u, b_ps) ∈ (b_unused, b_pendings) :: (b_u, b_ps) :: blocks)
+ as Hvalid'%Hblocks_valid by set_solver.
+ destruct Hvalid' as (Hvalid1' & Hvalid2').
+ split; simpl.
+ ** by rewrite lookup_insert_ne.
+ ** intros k Hk. apply elem_of_app in Hk as [Hk|Hk].
+ *** assert (k ≠ b_u) as HNEq2.
+ { apply NoDup_cons in HND as (_ & HND).
+ apply NoDup_app in HND as (_ & HND & _). apply HND in Hk.
+ simpl in Hk. by apply not_elem_of_cons in Hk as (Hk & _). }
+ rewrite lookup_insert_ne; last done. by apply Hvalid2.
+ *** apply elem_of_cons in Hk as [->|Hk]; first by rewrite lookup_insert.
+ assert (b_u ≠ k) as HNEq2.
+ { apply NoDup_cons in HND as (_ & HND).
+ apply NoDup_app in HND as (_ & _ & HND). simpl in HND.
+ apply NoDup_cons in HND as (HND & _).
+ apply not_elem_of_app in HND as (HND & _).
+ intros ->. apply HND, Hk. }
+ rewrite lookup_insert_ne; last done. by apply Hvalid2'.
+ * assert ((b_u', b_ps') ∈ (b_unused, b_pendings) :: (b_u, b_ps) :: blocks)
+ as Hvalid%Hblocks_valid by set_solver.
+ destruct Hvalid as (Hvalid1 & Hvalid2). rewrite /block_valid.
+ assert (b_u ≠ b_u') as HNeq1.
+ { apply NoDup_cons in HND as (_ & HND).
+ apply NoDup_app in HND as (_ & _ & HND). simpl in HND.
+ apply NoDup_cons in HND as (HND & _). intros <-.
+ apply not_elem_of_app in HND as (_ & HND). apply HND.
+ by apply blocks_elem1 in Hb. }
+ rewrite lookup_insert_ne; last done. split; first done.
+ intros k Hk. simpl in Hk.
+ assert (b_u ≠ k) as HNeq2.
+ { apply NoDup_cons in HND as (_ & HND).
+ apply NoDup_app in HND as (_ & _ & HND). simpl in HND.
+ apply NoDup_cons in HND as (HND & _). intros <-.
+ apply not_elem_of_app in HND as (_ & HND). apply HND.
+ by eapply blocks_elem2 in Hb. }
+ rewrite lookup_insert_ne; last done. by apply Hvalid2.
+ + apply elem_of_cons in Hb as [Hb|Hb].
+ * simplify_eq.
+ assert ((b_unused, b_pendings) ∈ (b_unused, b_pendings) :: (b_u, b_ps) :: blocks)
+ as Hvalid%Hblocks_valid by set_solver.
+ destruct Hvalid as (Hvalid1 & Hvalid2). split.
+ ** by rewrite lookup_insert_ne.
+ ** intros k Hk. simpl in *.
+ assert (k ≠ i) as HNEq.
+ { intros ->. apply Hvalid2 in Hk. rewrite Hi in Hk. by inversion Hk. }
+ rewrite lookup_insert_ne; last done. by apply Hvalid2.
+ * eapply IH; last done. done.
+ { apply NoDup_cons in HND as (_ & HND).
+ by apply NoDup_app in HND as (_ & _ & HND). }
+ intros b' Hb'.
+ assert (b' ∈ (b_unused, b_pendings) :: (b_u, b_ps) :: blocks)
+ as Hb'_valid%Hblocks_valid by set_solver. done.
+Qed.
+
+(* Contradiction status: either there is a contradiction going on with
+ the given indices, or there is no contradiction. In the latter case
+ the prophecy has well-formed pending blocks as a suffix. *)
+Inductive cont_status :=
+ | WithCont : nat → nat → cont_status
+ | NoCont : blocks → cont_status.
+
+Global
+Instance cont_status_inhabited : Inhabited cont_status.
+Proof. constructor. refine (NoCont []). Qed.
+
+Lemma initial_block_valid b pvs :
+ b ∈ map (λ i : nat, (i, [])) pvs → block_valid ∅ b.
+Proof.
+ intros H. induction pvs as [|i pvs IH].
+ - by inversion H.
+ - simpl in H. apply elem_of_cons in H as [->|H].
+ + split; first by apply lookup_empty. intros k Hk. by inversion Hk.
+ + apply IH, H.
+Qed.
+
+Lemma flatten_blocks_initial pvs :
+ pvs = flatten_blocks (map (λ i : nat, (i, [])) pvs).
+Proof.
+ induction pvs as [|i pvs IH]; first done.
+ simpl. f_equal. by apply IH.
+Qed.
+
+Lemma flatten_blocks_glue b bs i :
+ flatten_blocks (b :: bs) = flatten_blocks (glue_blocks b i bs).
+Proof.
+ revert b.
+ induction bs as [|[b_u' b_ps'] bs IH]; intros [b_u b_ps]; first done.
+ simpl. destruct (decide (i = b_u')) as [->|HNEq]; simpl.
+ - by rewrite -app_assoc.
+ - by rewrite -IH.
+Qed.
+
+Lemma flatten_blocks_mem1 blocks :
+ ∀b, b ∈ blocks → b.1 ∈ flatten_blocks blocks.
+Proof.
+ intros b Hb. induction blocks as [|[i ps] bs IH]; first by inversion Hb.
+ apply elem_of_cons in Hb as [->|Hb]; first by apply elem_of_list_here.
+ simpl. apply elem_of_list_further. apply elem_of_app. right. by apply IH.
+Qed.
+
+Lemma flatten_blocks_mem2 blocks :
+ ∀b, b ∈ blocks → ∀i, i ∈ b.2 → i ∈ flatten_blocks blocks.
+Proof.
+ intros b Hb. induction blocks as [|[i ps] bs IH]; first by inversion Hb.
+ intros k Hk. apply elem_of_cons in Hb as [->|Hb]; simpl.
+ - apply elem_of_list_further. apply elem_of_app. by left.
+ - apply elem_of_list_further. apply elem_of_app. right. by apply IH.
+Qed.
+
+(** * Some definitions and lemmas about array content manipulation **********)
+
+Definition array_get slots (deqs : gset nat) i :=
+ match slots !! i with
+ | None => NONEV
+ | Some d => if decide (i ∈ deqs) then NONEV
+ else physical_value d
+ end.
+
+Fixpoint array_content n slots deqs :=
+ match n with
+ | 0%nat => []
+ | S n => array_content n slots deqs ++ [array_get slots deqs n]
+ end.
+
+Lemma length_array_content sz slots deqs :
+ length (array_content sz slots deqs) = sz.
+Proof.
+ induction sz as [|sz IH]; first done.
+ by rewrite /= app_length plus_comm /= IH.
+Qed.
+
+Lemma array_content_lookup sz slots deqs i :
+ (i < sz)%nat →
+ array_content sz slots deqs !! i = Some (array_get slots deqs i).
+Proof.
+ intros H. induction sz as [|sz IH]; first lia.
+ destruct (decide (i = sz)) as [->|Hi_not_sz]; simpl.
+ - rewrite lookup_app_r length_array_content; last done.
+ by rewrite Nat.sub_diag /=.
+ - rewrite lookup_app_l; first (apply IH; by lia).
+ rewrite length_array_content. lia.
+Qed.
+
+Lemma array_content_empty sz :
+ array_content sz ∅ ∅ = replicate sz NONEV.
+Proof.
+ induction sz as [|sz IH]; first done.
+ rewrite replicate_S_end /= IH. done.
+Qed.
+
+Lemma array_content_NONEV sz i d slots deqs :
+ physical_value d = NONEV → slots !! i = None → i ∉ deqs →
+ array_content sz (<[i:=d]> slots) deqs = array_content sz slots deqs.
+Proof.
+ intros H1 H2 H3. induction sz as [|sz IH]; first done.
+ rewrite /= /array_get. destruct (decide (i = sz)) as [->|Hi_not_sz].
+ - rewrite lookup_insert H2 decide_False; last done. by rewrite IH H1.
+ - rewrite lookup_insert_ne; last done. by rewrite IH.
+Qed.
+
+Lemma array_content_is_Some sz i slots deqs :
+ (i < sz)%nat →
+ is_Some (array_content sz slots deqs !! i).
+Proof.
+ intros H. apply lookup_lt_is_Some. by rewrite length_array_content.
+Qed.
+
+Lemma array_content_ext sz slots1 slots2 deqs :
+ (∀ i, (i < sz)%nat → array_get slots1 deqs i = array_get slots2 deqs i) →
+ array_content sz slots1 deqs = array_content sz slots2 deqs.
+Proof.
+ induction sz as [|sz IH]; intros H; first done.
+ simpl. rewrite H; last by lia. f_equal. apply IH.
+ intros i Hi. apply H. by lia.
+Qed.
+
+Lemma array_content_more_deqs sz slots deqs i :
+ (sz ≤ i)%nat →
+ array_content sz slots ({[i]} ∪ deqs) = array_content sz slots deqs.
+Proof.
+ intros H. induction sz as [|sz IH]; first done.
+ rewrite /= IH; last by lia. f_equal.
+ rewrite /array_get. destruct (slots !! sz) as [d|]; last done.
+ destruct (decide (sz ∈ deqs)) as [Helem|Hnot_elem].
+ - rewrite decide_True; [ done | by set_solver ].
+ - rewrite decide_False; [ done | .. ].
+ apply not_elem_of_union. split; last done.
+ apply not_elem_of_singleton. by lia.
+Qed.
+
+Lemma array_content_update_slot_ge sz slots deqs f i :
+ (sz ≤ i)%nat →
+ array_content sz slots deqs = array_content sz (update_slot i f slots) deqs.
+Proof.
+ intros H. induction sz as [|sz IH]; first done.
+ rewrite /= IH; last by lia. f_equal.
+ rewrite /array_get /update_slot.
+ destruct (slots !! i) as [d|]; last done.
+ rewrite insert_delete. rewrite lookup_insert_ne; [ done | by lia ].
+Qed.
+
+Lemma array_content_dequeue sz i slots deqs :
+ (i < sz)%nat →
+ i ∉ deqs →
+ array_content sz slots ({[i]} ∪ deqs) = <[i:=NONEV]> (array_content sz slots deqs).
+Proof using N heapG0 hwqG0 savedPropG0 Σ.
+ revert i. induction sz as [|sz IH]; intros i H1 H2; first done.
+ destruct (decide (sz = i)) as [->|Hsz_not_i]; simpl.
+ - assert (i = length (array_content i slots deqs) + 0)%nat as HEq.
+ { rewrite length_array_content. by lia. }
+ rewrite [X in <[X:=_]> _]HEq.
+ rewrite (insert_app_r (array_content i slots deqs) _ 0 NONEV).
+ rewrite /= /array_get. destruct (slots !! i) as [d|].
+ + rewrite decide_True; last by set_solver. f_equal.
+ rewrite array_content_more_deqs; [ done | by lia ].
+ + f_equal. rewrite array_content_more_deqs; [ done | by lia ].
+ - rewrite insert_app_l; last (rewrite length_array_content; by lia).
+ rewrite IH; [ .. | by lia | done ]. f_equal.
+ rewrite /array_get. destruct (slots !! sz) as [d|]; last done.
+ destruct (decide (sz ∈ deqs)) as [H|H].
+ * rewrite decide_True; [ done | by set_solver ].
+ * rewrite decide_False; [ done | by set_solver ].
+Qed.
+
+Lemma array_content_set_written sz i (l : loc) slots deqs :
+ (i < sz)%nat →
+ val_of <$> slots !! i = Some l →
+ ¬ i ∈ deqs →
+ <[i:=InjRV #l]> (array_content sz slots deqs) = array_content sz (update_slot i set_written slots) deqs.
+Proof using N heapG0 hwqG0 savedPropG0 Σ.
+ revert i. induction sz as [|sz IH]; intros i H1 H2 H3; first done.
+ destruct (decide (sz = i)) as [->|Hsz_not_i]; simpl.
+ - assert (i = length (array_content i slots deqs) + 0)%nat as HEq.
+ { rewrite length_array_content. by lia. }
+ rewrite [X in <[X:=_]> _]HEq.
+ rewrite (insert_app_r (array_content i slots deqs) _ 0).
+ erewrite array_content_update_slot_ge; [ f_equal | by lia ].
+ rewrite /= /array_get /update_slot. destruct (slots !! i) as [d|].
+ + rewrite lookup_insert decide_False; last done.
+ destruct d as [[ld sd] wd]. inversion H2; subst ld. done.
+ + inversion H2.
+ - rewrite insert_app_l; last (rewrite length_array_content; by lia).
+ rewrite IH; [ .. | by lia | done | done ]. f_equal.
+ rewrite /array_get /update_slot. destruct (slots !! i) as [d|]; last done.
+ by rewrite insert_delete lookup_insert_ne.
+Qed.
+
+(* FIXME similar to previous lemma. Share stuff? *)
+Lemma array_content_set_written_and_done sz i (l : loc) slots deqs :
+ (i < sz)%nat →
+ val_of <$> slots !! i = Some l →
+ ¬ i ∈ deqs →
+ <[i:=InjRV #l]> (array_content sz slots deqs) = array_content sz (update_slot i set_written_and_done slots) deqs.
+Proof.
+ revert i. induction sz as [|sz IH]; intros i H1 H2 H3; first done.
+ destruct (decide (sz = i)) as [->|Hsz_not_i]; simpl.
+ - assert (i = length (array_content i slots deqs) + 0)%nat as HEq.
+ { rewrite length_array_content. by lia. }
+ rewrite [X in <[X:=_]> _]HEq.
+ rewrite (insert_app_r (array_content i slots deqs) _ 0).
+ erewrite array_content_update_slot_ge; [ f_equal | by lia ].
+ rewrite /= /array_get /update_slot. destruct (slots !! i) as [d|].
+ + rewrite lookup_insert decide_False; last done.
+ destruct d as [[ld sd] wd]. inversion H2; subst ld. done.
+ + inversion H2.
+ - rewrite insert_app_l; last (rewrite length_array_content; by lia).
+ rewrite IH; [ .. | by lia | done | done ]. f_equal.
+ rewrite /array_get /update_slot. destruct (slots !! i) as [d|]; last done.
+ by rewrite insert_delete lookup_insert_ne.
+Qed.
+
+Lemma update_slot_lookup i f slots :
+ update_slot i f slots !! i = f <$> slots !! i.
+Proof.
+ rewrite /update_slot.
+ destruct (slots !! i) as [d|] eqn:HEq; last done.
+ by rewrite lookup_insert.
+Qed.
+
+Lemma update_slot_lookup_ne i k f slots :
+ i ≠ k →
+ update_slot i f slots !! k = slots !! k.
+Proof.
+ intros H. rewrite /update_slot.
+ destruct (slots !! i) as [d|] eqn:HEq; last done.
+ rewrite lookup_insert_ne; last done.
+ by rewrite lookup_delete_ne.
+Qed.
+
+Lemma update_slot_update_slot i f g slots :
+ update_slot i f (update_slot i g slots) = update_slot i (f ∘ g) slots.
+Proof.
+ rewrite /update_slot.
+ destruct (slots !! i) as [d|] eqn:HEq.
+ - rewrite lookup_insert. repeat rewrite insert_delete.
+ rewrite insert_insert. done.
+ - rewrite HEq. done.
+Qed.
+
+Definition get_value slots (deqs : gset nat) i :=
+ match slots !! i with
+ | None => Build_loc 0
+ | Some d => val_of d
+ end.
+
+Definition map_get_value_not_in_pref i d pref slots deqs :
+ was_written d = false →
+ i ∉ pref →
+ map (get_value (<[i:=d]> slots) deqs) pref = map (get_value slots deqs) pref.
+Proof.
+ intros Hd. induction pref as [|k pref IH]; intros Hi; first done.
+ rewrite /= IH; last by set_solver. f_equal. rewrite /get_value.
+ rewrite lookup_insert_ne; first done. set_solver.
+Qed.
+
+(** * Definition of the main ************************************************)
+
+(** Atomic update for the insertion of [l], with post-condition [Q]. *)
+Definition enqueue_AU γe l Q :=
+ (AU << ∀ ls : list loc, hwq_cont γe ls >> @ ⊤ ∖ ↑N, ∅
+ << hwq_cont γe (ls ++ [l]), COMM Q >>)%I.
+
+(*
+When a contradiction is going on, we have [cont = WithCont i1 i2] where:
+ - [i1] is the index reserved by the enqueue operation the initiated the
+ contradiction,
+ - [i2] is the first index in the prophecy that was not yet reserved for
+ an enqueue operation (when the contradiction was initiated).
+*)
+
+Definition per_slot_own γe γs i d :=
+ (slot_val_wit γs i (val_of d) ∗
+ (if was_written d then slot_written_wit γs i else True) ∗
+ match state_of d with
+ | Pend γ => slot_pending_tok γs i ∗
+ ∃ Q, saved_prop_own γ Q ∗ enqueue_AU γe (val_of d) Q
+ | Help γ => slot_committed_wit γs i ∗ ∃ Q, saved_prop_own γ Q ∗ ▷ Q
+ | Done => slot_committed_wit γs i ∗ slot_token γs i
+ end)%I.
+
+Definition inv_hwq sz γb γi γe γc γs ℓ_ar ℓ_back p : iProp :=
+ (∃ (back : nat) (** Physical value of [q.back]. *)
+ (pvs : list nat) (** Full contents of the prophecy. *)
+ (pref : list nat) (** Commit prefix of the prophecy *)
+ (rest : list loc) (** Logical queue after commit prefix. *)
+ (cont : cont_status) (** Contradiction or prophecy suffix. *)
+ (slots : gmap nat slot_data) (** Per-slot data for used indices. *)
+ (deqs : gset nat), (** Dequeued indices. *)
+ (** Physical data. *)
+ ℓ_back ↦ #back ∗ ℓ_ar ↦∗ (array_content sz slots deqs) ∗
+ (** Logical contents of the queue and prophecy contents. *)
+ back_value γb back ∗
+ i2_lower_bound γi (match cont with WithCont _ i2 => i2 | NoCont _ => back `min` sz end)%nat ∗
+ own γe (● (Excl' (map (get_value slots deqs) pref ++ rest))) ∗
+ own γs (● (of_slot_data <$> slots : gmap nat per_slot)) ∗
+ hwq_proph p sz deqs pvs ∗
+ (** Per-slot ownership. *)
+ ([∗ map] i ↦ d ∈ slots, per_slot_own γe γs i d) ∗
+ (** Contradiction status. *)
+ match cont with NoCont _ => no_contra γc | WithCont i1 i2 => contra γc i1 i2 end ∗
+ (** Tying the logical and physical data and some other pure stuff. *)
+ ⌜(∀ i, (i < back `min` sz)%nat ↔ is_Some (slots !! i)) ∧
+ (∀ i, (was_committed <$> slots !! i = Some false → was_written <$> slots !! i = Some false) ∧
+ (was_written <$> slots !! i = Some false → i ∉ deqs)) ∧
+ (∀ i, i ∈ pref → was_committed <$> slots !! i = Some true ∧ i ∉ deqs ∧
+ match cont with WithCont i1 _ => i ≠ i1 | _ => True end) ∧
+ (∀ i, i ∈ deqs → was_written <$> slots !! i = Some true ∧
+ was_committed <$> slots !! i = Some true ∧
+ array_get slots deqs i = NONEV) ∧
+ (NoDup (pvs ++ elements deqs) ∧ ∀ i, i ∈ pvs → (i < sz)%nat) ∧
+ match cont with
+ | NoCont bs =>
+ (∀ b, b ∈ bs → block_valid slots b) ∧
+ (bs ≠ [] → rest = []) ∧
+ pvs = pref ++ flatten_blocks bs
+ | WithCont i1 i2 =>
+ (i1 < i2 < sz ∧ i1 < back)%nat ∧
+ was_committed <$> slots !! i1 = Some true ∧
+ was_written <$> slots !! i1 = Some true ∧ ¬ i1 ∈ deqs ∧
+ array_get slots deqs i1 ≠ NONEV ∧
+ pref ++ [i2] `prefix_of` pvs
+ end⌝)%I.
+
+Definition is_hwq sz γe v : iProp :=
+ (∃ γb γi γc γs ℓ_ar ℓ_back p,
+ ⌜v = (#sz, #ℓ_ar, #ℓ_back, #p)%V⌝ ∗
+ inv N (inv_hwq sz γb γi γe γc γs ℓ_ar ℓ_back p))%I.
+
+(** * Some useful instances *************************************************)
+
+Instance blocks_match_persistent (bs : blocks) γc i1 :
+ Persistent (match bs with
+ | [] => True
+ | (i2, _) :: _ => contra γc i1 i2
+ end)%I.
+Proof. destruct bs as [|[i2 _] _]; apply _. Qed.
+
+Instance cont_match_persistent cont γc :
+ Persistent (match cont with
+ | NoCont _ => True
+ | WithCont i1 i2 => contra γc i1 i2
+ end)%I.
+Proof. destruct cont as [i1 i2|_]; apply _. Qed.
+
+Instance contra_timeless cont γc :
+ Timeless (match cont with
+ | NoCont _ => no_contra γc
+ | WithCont i1 i2 => contra γc i1 i2
+ end).
+Proof. destruct cont as [i1 i2|_]; apply _. Qed.
+
+(** * Some important lemmas for the specification of [enqueue] **************)
+
+Definition get_values (slots : gmap nat slot_data) (p : list nat) :=
+ fold_right (λ i acc, match val_of <$> slots !! i with
+ | None => acc
+ | Some l => l :: acc end) [] p.
+
+Definition get_values_not_in n ps d s :
+ n ∉ ps → get_values (<[n:=d]> s) ps = get_values s ps.
+Proof.
+ intros H. induction ps as [|p ps IH]; first done. simpl.
+ assert (n ≠ p) as Hn_not_p by set_solver.
+ rewrite lookup_insert_ne; last done.
+ rewrite IH; first done. set_solver.
+Qed.
+
+Definition helped (p : list nat) (i : nat) d :=
+ match state_of d with
+ | Pend γ => if decide (i ∈ p) then
+ Some (val_of d, Help γ, was_written d)
+ else
+ Some d
+ | _ => Some d
+ end.
+
+Lemma is_Some_helped (p : list nat) i d : is_Some (helped p i d).
+Proof.
+ rewrite /helped. destruct (state_of d); try by eexists.
+ destruct (decide (i ∈ p)); by eexists.
+Qed.
+
+Lemma map_imap_helped_nil slots : map_imap (helped []) slots = slots.
+Proof.
+ apply map_eq. intros i. rewrite lookup_imap.
+ destruct (slots !! i) as [d|] eqn:HEq.
+ - rewrite /helped /= HEq. by destruct (state_of d).
+ - by rewrite /= HEq.
+Qed.
+
+Lemma annoying_lemma_1 slots deqs pref i l b_pendings :
+ (∀ k, k ∈ pref → was_committed <$> slots !! k = Some true ∧ k ∉ deqs) →
+ NoDup (pref ++ i :: b_pendings) →
+ map (get_value (map_imap (helped b_pendings) (<[i:=(l, Done, false)]> slots)) deqs) pref =
+ map (get_value slots deqs) pref.
+Proof.
+ intros Hpref HND.
+ induction pref as [|pref_hd pref IH]; first done.
+ assert (NoDup (pref ++ i :: b_pendings)) as HND_IH.
+ { simpl in HND. apply NoDup_cons in HND as [_ HND]. done. }
+ assert (∀ k, k ∈ pref → was_committed <$> slots !! k = Some true ∧
+ k ∉ deqs) as Hpref_IH.
+ { intros k Hk. by apply Hpref, elem_of_list_further, Hk. }
+ rewrite /= IH; try done. clear IH HND_IH Hpref_IH. f_equal.
+ assert (i ≠ pref_hd) as Hi_not_pref_hd.
+ { simpl in HND. apply NoDup_cons in HND as (HND & _).
+ apply not_elem_of_app in HND as (_ & HND).
+ by apply not_elem_of_cons in HND as (HND & _). }
+ rewrite /get_value lookup_imap lookup_insert_ne; last done.
+ destruct (slots !! pref_hd) as [[[lp sp] wp]|]; last done.
+ destruct sp; try done. rewrite /= /helped /=.
+ rewrite decide_False; first done.
+ simpl in HND. apply NoDup_cons in HND as (HND & _).
+ apply not_elem_of_app in HND as (_ & HND).
+ by apply not_elem_of_cons in HND as (_ & HND).
+Qed.
+
+Lemma annoying_lemma_2 slots deqs pref i l b_pendings :
+ block_valid slots (i, b_pendings) →
+ NoDup (pref ++ i :: b_pendings) →
+ map (get_value (map_imap (helped b_pendings) (<[i:=(l, Done, false)]> slots)) deqs) b_pendings =
+ get_values (<[i:=(l, Done, false)]> slots) b_pendings.
+Proof.
+ intros (Hvalid_1 & Hvalid_2) HND.
+ induction b_pendings as [|p ps IH]; first done. simpl in *.
+ assert (i ≠ p) as Hi_not_p.
+ { intros ->. apply NoDup_app in HND as (_ & _ & HND).
+ apply NoDup_cons in HND as (HND & _). by set_solver +HND. }
+ rewrite lookup_insert_ne; last done.
+ assert (p ∈ p :: ps) as Hcomm%Hvalid_2 by set_solver.
+ destruct (slots !! p)
+ as [[[lp sp] wp]|] eqn:Hslots_p; [ f_equal | by inversion Hcomm ].
+ - rewrite /= map_imap_insert /helped /= /get_value.
+ rewrite lookup_insert_ne; last done. rewrite lookup_imap Hslots_p /=.
+ destruct sp; try done. rewrite decide_True; [ done | by set_solver ].
+ - rewrite -IH; first last; try done.
+ { apply NoDup_app in HND as (HND1 & HND2 & HND3).
+ apply NoDup_app. split; first done. split.
+ - intros e He. apply HND2 in He. apply not_elem_of_cons.
+ split; by set_solver +He.
+ - apply NoDup_cons in HND3 as (HND3_1 & HND3_2).
+ apply NoDup_cons. split; first by set_solver +HND3_1.
+ apply NoDup_cons in HND3_2 as (HND3_2_1 & HND3_2_2). done. }
+ { intros k Hk. by apply Hvalid_2, elem_of_list_further, Hk. }
+ apply map_ext_in. intros k Hk.
+ rewrite /get_value lookup_imap lookup_imap.
+ assert (i ≠ k) as Hi_not_k.
+ { intros ->. apply NoDup_app in HND as (_ & _ & HND).
+ apply NoDup_cons in HND as (HND & _).
+ apply not_elem_of_cons in HND as (_ & HND).
+ by apply HND, elem_of_list_In, Hk. }
+ rewrite lookup_insert_ne; last done.
+ assert (k ∈ p :: ps) as Hk_p_ps
+ by by apply elem_of_list_further, elem_of_list_In.
+ specialize (Hvalid_2 _ Hk_p_ps) as Hcomm_k.
+ destruct (slots !! k) as [[[lk sk] wk]|]; last by inversion Hcomm_k.
+ destruct sk; try done. rewrite /= /helped /=.
+ rewrite decide_True; last done.
+ rewrite decide_True; [ done | by apply elem_of_list_In ].
+Qed.
+
+Lemma big_lemma γe γs (ls : list loc) slots (p : list nat) :
+ NoDup p →
+ (∀ i, i ∈ p → was_committed <$> slots !! i = Some false) →
+ (own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ ([∗ map] i ↦ d ∈ slots, per_slot_own γe γs i d) -∗
+ own γe (● (Excl' ls)) ={⊤ ∖ ↑N}=∗
+ own γs (● (of_slot_data <$> map_imap (helped p) slots) : slotUR) ∗
+ ([∗ map] i ↦ d ∈ map_imap (helped p) slots, per_slot_own γe γs i d) ∗
+ own γe (● (Excl' (ls ++ get_values slots p))))%I.
+Proof.
+ revert p. iIntros (p).
+ iInduction p as [|n ps] "IH" forall (slots ls); iIntros (HNoDup H) "Hs● Hbig He●".
+ - iModIntro. rewrite /= -app_nil_end map_imap_helped_nil. iFrame.
+ - assert (∀ i : nat, i ∈ ps → was_committed <$> slots !! i = Some false) as H1.
+ { intros i Hi. apply H. apply elem_of_list_further, Hi. }
+ assert (was_committed <$> slots !! n = Some false) as H2.
+ { apply H. apply elem_of_list_here. }
+ assert (∃ ln γn wn, slots !! n = Some (ln, Pend γn, wn)) as Hn.
+ { destruct (slots !! n) as [[[ln sn] wn]|]; last by inversion H2.
+ (destruct sn as [γn|γn|]; last by inversion H2); by exists ln, γn, wn. }
+ apply NoDup_cons in HNoDup. destruct HNoDup as [Hn_not_in_ps HNoDup].
+ destruct Hn as [l [γ [w Hn]]].
+ assert (slots = <[n:=(l, Pend γ, w)]> (delete n slots)) as Hs.
+ { by rewrite insert_delete insert_id. }
+ rewrite [in ([∗ map] _ ↦ _ ∈ slots, _)%I]Hs.
+ iDestruct (big_sepM_insert with "Hbig")
+ as "[Hbig_n Hbig]"; first by apply lookup_delete.
+ iDestruct "Hbig_n" as "[Hval_wit_n [Hwritten_n [Hpending_tok_n H]]]".
+ iDestruct "H" as (Q) "[Hsaved AU]".
+ iMod "AU" as (elts_AU) "[He◯ [_ Hclose]]".
+ iDestruct (sync_elts with "He● He◯") as %<-.
+ iMod (update_elts _ _ _ (ls ++ [l]) with "He● He◯") as "[He● He◯]".
+ iMod ("Hclose" with "[$He◯]") as "HPost".
+ iMod (use_pending_tok with "Hs● Hpending_tok_n")
+ as "[Hs● Hcommitted_wit_n]"; first by rewrite Hn.
+ iCombine "Hsaved HPost" as "Hn".
+ iDestruct (big_sepM_insert _ (delete n slots) n (l, Help γ, w)
+ with "[Hn Hval_wit_n Hwritten_n Hcommitted_wit_n Hbig]")
+ as "Hbig"; first by apply lookup_delete.
+ { iClear "IH". iFrame "Hbig". rewrite /per_slot_own /=. iFrame.
+ iExists Q. iDestruct "Hn" as "[$ HPost]". iNext. done. }
+ rewrite insert_delete /update_slot Hn insert_delete.
+ assert (∀ i : nat, i ∈ ps → was_committed <$> <[n:=(l, Help γ, w)]> slots !! i = Some false) as HHH.
+ { intros i Hi. rewrite lookup_insert_ne; [ by apply H1 | by set_solver ]. }
+ iMod ("IH" $! (<[n:=(l, Help γ, w)]> slots) (ls ++ [l]) HNoDup HHH
+ with "Hs● Hbig He●") as "[Hs● [Hbig He●]]"; iClear "IH".
+ assert (map_imap (helped ps) (<[n:=(l, Help γ, w)]> slots)
+ = map_imap (helped (n :: ps)) slots) as ->.
+ { apply map_eq. intros i. destruct (decide (i = n)) as [->|Hi_not_n].
+ - rewrite lookup_imap lookup_imap /= lookup_insert Hn /=.
+ rewrite /helped /=. rewrite decide_True; first done. set_solver.
+ - rewrite lookup_imap lookup_imap /= lookup_insert_ne; last done.
+ destruct (slots !! i) as [[[li si] wi]|]; last done. simpl.
+ rewrite /helped /=. destruct si; try done.
+ destruct (decide (i ∈ n :: ps)).
+ + rewrite decide_True; first done. set_solver.
+ + rewrite decide_False; first done. set_solver. }
+ iModIntro. iFrame.
+ by rewrite /= Hn -app_assoc /= get_values_not_in.
+Qed.
+
+Lemma array_contents_cases γs slots deqs i li :
+ own γs (● (of_slot_data <$> slots) : slotUR) -∗
+ slot_val_wit γs i li -∗
+ ⌜array_get slots deqs i = SOMEV #li ∨ array_get slots deqs i = NONEV⌝.
+Proof.
+ iIntros "Hs● Hval_wit_i".
+ iDestruct (use_val_wit with "Hs● Hval_wit_i") as %Hslots_i.
+ destruct (slots !! i) as [d|] eqn:HEq; last by inversion Hslots_i.
+ destruct d as [[li' si] wi]. inversion Hslots_i as [H]; subst li'.
+ rewrite /array_get HEq. simpl. iPureIntro.
+ destruct (decide (i ∈ deqs)); first by right.
+ destruct wi; by [ left | right ].
+Qed.
+
+(** * Specification of the queue operations *********************************)
+
+Lemma new_queue_spec sz :
+ 0 < sz →
+ {{{ True }}}
+ new_queue #sz
+ {{{ v γ, RET v; is_hwq sz γ v ∗ hwq_cont γ [] }}}.
+Proof.
+ iIntros (Hsz Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
+ (** Allocate [q.ar], [q.back] and [q.p]. *)
+ wp_apply wp_allocN; [ lia | done | iIntros (ℓa) "[Hℓa _]" ].
+ wp_alloc ℓb as "Hℓb".
+ wp_apply wp_new_proph; [ done | iIntros (rs p) "Hp" ].
+ wp_pures.
+ (* Allocate the remaining ghost state. *)
+ iMod new_back as (γb) "Hb●".
+ iMod new_back as (γi) "Hi●". (* FIXME not about back. *)
+ iMod (new_elts []) as (γe) "[He● He◯]".
+ iMod new_no_contra as (γc) "HC".
+ iMod new_slots as (γs) "Hs●".
+ (* Allocate the invariant. *)
+ iMod (inv_alloc N _ (inv_hwq sz γb γi γe γc γs ℓa ℓb p)
+ with "[Hℓa Hℓb Hp Hb● Hi● He● HC Hs●]") as "#InvN".
+ { pose (pvs := proph_data sz ∅ rs).
+ pose (cont := NoCont (map (λ i, (i, [])) pvs)).
+ iNext. iExists 0%nat, pvs, [], [], cont, ∅, ∅.
+ rewrite array_content_empty Nat2Z.id fmap_empty /=.
+ iFrame. iSplitL. { iExists rs. by iFrame. }
+ repeat (iSplit; first done). iPureIntro.
+ repeat split_and; try done.
+ - intros i. split; intros Hi; [ by lia | by inversion Hi].
+ - intros e He. set_solver.
+ - apply proph_data_NoDup.
+ - intros i. apply proph_data_sz.
+ - intros b. apply initial_block_valid.
+ - simpl. apply flatten_blocks_initial. }
+ (* Wrap things up. *)
+ iModIntro. iApply "HΦ". iFrame.
+ iExists γb, γi, γc, γs, ℓa, ℓb, p. by iSplit.
+Qed.
+
+Lemma enqueue_spec sz γe (q : val) (l : loc) :
+ is_hwq sz γe q -∗
+ <<< ∀ (ls : list loc), hwq_cont γe ls >>>
+ enqueue q #l @ ⊤ ∖ ↑N
+ <<< hwq_cont γe (ls ++ [l]), RET #() >>>.
+Proof.
+ iIntros "Hq" (Φ) "AU".
+ iDestruct "Hq" as (γb γi γc γs ℓ_ar ℓ_back p ->) "#Inv".
+ rewrite /enqueue. wp_pures. wp_bind (FAA _ _)%E.
+ (* Open the invariant to perform the increment. *)
+ iInv "Inv" as (back pvs pref rest cont slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [Hb● [Hi● [He● [Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[Hproph [Hbig [Hcont >Hpures]]]".
+ iDestruct "Hpures" as %(Hslots & Hstate & Hpref & Hdeqs & Hpvs_OK & Hcont).
+ destruct Hpvs_OK as (Hpvs_ND & Hpvs_sz).
+ wp_faa. assert (back + 1 = S back) as -> by lia.
+ iMod (back_incr with "Hb●") as "Hb●".
+ iAssert (i2_lower_bound γi match cont with
+ | WithCont _ i2 => i2
+ | NoCont _ => (back `min` sz)%nat
+ end -∗ |==>
+ i2_lower_bound γi match cont with
+ | WithCont _ i2 => i2
+ | NoCont _ => ((S back) `min` sz)%nat
+ end)%I as "Hup".
+ { destruct cont as [i1 i2|bs]; iIntros "Hi●"; first done.
+ iMod (i2_lower_bound_update with "Hi●") as "$"; [ lia | done ]. }
+ iMod ("Hup" with "Hi●") as "Hi●".
+ (* We first handle the case where there is no more space in the queue. *)
+ destruct (decide (back < sz)) as [Hback_sz|Hback_sz]; last first.
+ { iModIntro. iClear "AU". iSplitL.
+ - iNext. iExists (S back), pvs, pref, rest, cont, slots, deqs.
+ assert (S back `min` sz = back `min` sz)%nat as -> by lia.
+ iFrame. iPureIntro. repeat split_and; try done.
+ destruct cont as [i1 i2|bs]; last done.
+ destruct Hcont as ((H1 & H2) & H3 & H4).
+ by repeat (split; first lia).
+ - wp_pures. rewrite (bool_decide_false _ Hback_sz).
+ wp_pures. wp_apply (wp_loop Φ). }
+ (* We now have a reserved slot [i], which is still free. *)
+ pose (i := back). pose (elts := map (get_value slots deqs) pref ++ rest).
+ assert (slots !! back = None) as Hi_free.
+ { destruct (Hslots i) as [H1 H2]. rewrite min_l in H1; last by lia.
+ assert (¬ is_Some (slots !! back)). { intro H. apply H2 in H. lia. }
+ apply eq_None_not_Some, H. }
+ (* Useful fact: our index was not yet dequeued. *)
+ assert (i ∉ deqs) as Hi_not_in_deq.
+ { intros H. apply Hdeqs in H as (H & _). rewrite Hi_free in H. inversion H. }
+ (* We then handle the case where there is a contradiction going on. *)
+ destruct cont as [i1 i2|bs].
+ { (* We access the atomic update and commit the element. *)
+ iMod "AU" as (elts_AU) "[He◯ [_ Hclose]]".
+ iDestruct (sync_elts with "He● He◯") as %<-.
+ iMod (update_elts _ _ _ (elts ++ [l]) with "He● He◯") as "[He● He◯]".
+ iMod ("Hclose" with "[$He◯]") as "HΦ".
+ (* We allocate the new slot. *)
+ iMod (alloc_done_slot γs slots i l Hi_free with "Hs●")
+ as "[Hs [Htok_i [#val_wit_i [#commit_wit_i Hwriting_tok_i]]]]".
+ (* We also remember that we had contradiciton states. *)
+ iDestruct "Hcont" as "#cont_wit".
+ (* And we can close the invariant. *)
+ iModIntro. iSplitR "HΦ Hwriting_tok_i".
+ { iNext. iExists (S back), pvs, pref, (rest ++ [l]), (WithCont i1 i2).
+ iExists (<[i := (l, Done, false)]> slots), deqs.
+ rewrite fmap_insert /= array_content_NONEV; try done. iFrame.
+ iFrame. iSplitL "He●".
+ { rewrite /elts app_assoc map_get_value_not_in_pref; try done.
+ intros Hi%Hpref. rewrite Hi_free in Hi. destruct Hi; done. }
+ iSplitL "Hbig Htok_i".
+ { iApply big_sepM_insert.
+ + apply eq_None_not_Some. intros H. apply Hslots in H. lia.
+ + iFrame "Hbig". repeat (iSplit; first done). done. }
+ iFrame "cont_wit".
+ destruct Hcont as (((HC1 & HC2) & HC3) & HC4 & HC5 & HC6 & HC7 & HC8).
+ iPureIntro. repeat split_and; try done; try by lia.
+ - intros k. destruct sz; first by lia.
+ split; intros Hk.
+ + destruct (decide (k = i)) as [->|k_not_i].
+ * rewrite lookup_insert. by eexists.
+ * rewrite lookup_insert_ne; last done. apply Hslots. by lia.
+ + destruct (decide (k = i)) as [->|k_not_i].
+ * destruct sz; by lia.
+ * rewrite lookup_insert_ne in Hk; last done.
+ apply Hslots in Hk. by lia.
+ - intros k. destruct (decide (k = i)) as [->|k_not_i].
+ + by rewrite lookup_insert.
+ + rewrite lookup_insert_ne; last done. apply Hstate.
+ - intros k Hk. destruct (decide (k = i)) as [->|HNeq].
+ + split; first by rewrite lookup_insert. split; first done.
+ intros ->. apply Hpref in Hk as (_ & _ & H). done.
+ + rewrite lookup_insert_ne; last done. apply Hpref, Hk.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + by rewrite lookup_insert.
+ + rewrite /array_get. rewrite lookup_insert_ne; last done.
+ apply Hdeqs in Hk as (H1 & H2 & H3). repeat (split; first done).
+ rewrite /array_get in H3.
+ destruct (slots !! k) as [[[dl ds] dw]|]; last done. done.
+ - destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ + by rewrite lookup_insert.
+ + by rewrite lookup_insert_ne.
+ - rewrite /array_get lookup_insert_ne; first done. lia.
+ - rewrite /array_get lookup_insert_ne; last by lia.
+ destruct (slots !! i1) as [[[li1 si1] wi2]|]; last by inversion HC4.
+ rewrite decide_False; last done. inversion HC5; subst wi2. done. }
+ (* Let's clean up the context a bit. *)
+ clear Hslots Hstate Hpref Hdeqs Hcont Hi_not_in_deq Hi_free Hpvs_ND Hpvs_sz.
+ clear elts pvs pref rest slots deqs. subst i. rename back into i.
+ (* We can now move to the store. *)
+ wp_pures. rewrite (bool_decide_true _ Hback_sz).
+ wp_pures. wp_bind (_ <- _)%E.
+ (* We open the invariant again for the store. *)
+ iInv "Inv" as (back pvs pref rest cont slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [Hb● [Hi● [He● [>Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[Hproph [Hbig [>Hcont >Hpures]]]".
+ iDestruct "Hpures" as %(Hslots & Hstate & Hpref & Hdeqs & Hpvs_OK & Hcont).
+ destruct Hpvs_OK as (Hpvs_ND & Hpvs_sz).
+ (* Using witnesses, we show that our value and state have not changed. *)
+ iDestruct (use_val_wit with "Hs● val_wit_i") as %Hval_wit_i.
+ iDestruct (use_committed_wit with "Hs● commit_wit_i") as %Hval_commit_i.
+ iDestruct (writing_tok_not_written with "Hs● Hwriting_tok_i") as %Hnot_written_i.
+ (* We also show that the same contradiction ist still going on. *)
+ destruct cont as [i1' i2'|bs]; last first.
+ { by iDestruct (contra_not_no_contra with "Hcont cont_wit") as %Absurd. }
+ iDestruct (contra_agree with "cont_wit Hcont") as %[-> ->].
+ destruct Hcont as (((HC1 & HC2) & HC3) & HC4 & HC5 & HC6 & HC7 & HC8).
+ (* Our slot is mapped. *)
+ assert (is_Some (slots !! i)) as Hslots_i.
+ { destruct (slots !! i) as [d|]; first by exists d. inversion Hval_wit_i. }
+ (* Our index is in the array. *)
+ assert (i < back `min` sz)%nat as Hi_le_back by by apply Hslots.
+ (* An we perform the store. *)
+ wp_apply (wp_store_offset _ _ ℓ_ar i (array_content sz slots deqs) with "Hℓ_ar").
+ { apply array_content_is_Some. by lia. }
+ iIntros "Hℓ_ar".
+ (* We perform some updates. *)
+ iMod (use_writing_tok with "Hs● Hwriting_tok_i") as "[Hs● #written_wit_i]".
+ iModIntro. iSplitR "HΦ"; last by wp_pures. iNext.
+ (* It remains to re-establish the invariant. *)
+ pose (new_slots := update_slot i set_written slots).
+ iExists back, pvs, pref, rest, (WithCont i1 i2), new_slots, deqs.
+ subst new_slots. iFrame. iSplitL "Hℓ_ar".
+ { rewrite array_content_set_written;
+ [ by iFrame | by lia | done | by apply Hstate ]. }
+ iSplitL "He●".
+ { erewrite map_ext; first by iFrame. rewrite /get_value. intros k.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ - rewrite update_slot_lookup. destruct Hslots_i as [d Hslots_i].
+ destruct d as [[ld sd] wd]. rewrite Hslots_i in Hnot_written_i.
+ inversion Hnot_written_i; subst wd. rewrite Hslots_i /=. done.
+ - rewrite update_slot_lookup_ne; last done. done. }
+ iSplitL "Hbig".
+ { rewrite /update_slot. destruct (slots !! i) as [d|] eqn:HEq; last done.
+ iApply big_sepM_insert; first by rewrite lookup_delete.
+ assert (slots = <[i:=d]> (delete i slots)) as HEq_slots.
+ { rewrite insert_delete. by rewrite insert_id. }
+ rewrite [X in ([∗ map] _ ↦ _ ∈ X, _)%I] HEq_slots.
+ iDestruct (big_sepM_insert with "Hbig")
+ as "[[H1 [H2 H3]] $]"; first by rewrite lookup_delete.
+ rewrite /per_slot_own val_of_set_written state_of_set_written.
+ iFrame. by rewrite was_written_set_written. }
+ iPureIntro.
+ destruct Hslots_i as [[[li si] wi] Hslots_i].
+ repeat split_and; try done.
+ - intros k. destruct (decide (k = i)) as [->|k_not_i].
+ + rewrite update_slot_lookup. split; intros H; last done.
+ rewrite Hslots_i. by eexists.
+ + rewrite update_slot_lookup_ne; last done. by apply Hslots.
+ - intros k. destruct (decide (k = i)) as [->|k_not_i].
+ + rewrite update_slot_lookup Hslots_i /=. split; intros H.
+ * exfalso. rewrite Hslots_i in Hval_commit_i.
+ destruct si as [γ|γ|]; try by inversion Hval_commit_i.
+ * by inversion H.
+ + rewrite update_slot_lookup_ne; last done. apply Hstate.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hslots_i /=. repeat split.
+ * rewrite Hslots_i in Hval_commit_i.
+ destruct si; try by inversion Hval_commit_i.
+ * intros Hi%Hdeqs. destruct Hi as [H _].
+ rewrite Hnot_written_i in H. inversion H.
+ * by apply Hpref in Hk as (_ & _ & H).
+ + rewrite update_slot_lookup_ne; last done. apply Hpref, Hk.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hslots_i /update_slot /=.
+ rewrite Hslots_i /= insert_delete /array_get lookup_insert.
+ rewrite decide_True; last done. repeat split; try done.
+ destruct si; try done. rewrite Hslots_i in Hval_commit_i. done.
+ + rewrite /array_get update_slot_lookup_ne; last done.
+ apply Hdeqs in Hk. rewrite /array_get in Hk. done.
+ - destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ + rewrite update_slot_lookup Hslots_i /=.
+ rewrite Hslots_i in HC4. by inversion HC4.
+ + by rewrite update_slot_lookup_ne.
+ - destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ + rewrite /array_get update_slot_lookup Hslots_i /=.
+ destruct (decide (i ∈ deqs)) as [H|H]; last done.
+ exfalso. apply Hdeqs in H as (H1 & H2 & H3).
+ rewrite Hnot_written_i in H1. inversion H1.
+ + by rewrite /array_get update_slot_lookup_ne.
+ - destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ + rewrite /array_get update_slot_lookup Hslots_i /=.
+ rewrite Hslots_i in HC5. inversion HC5; subst wi.
+ by rewrite decide_False.
+ + rewrite /array_get update_slot_lookup_ne; last done.
+ destruct (slots !! i1) as [[[li1 si1] wi1]|]; last by inversion HC4.
+ rewrite decide_False; last done. inversion HC5; subst wi1. done. }
+ (* There is no [Contra1]/[Contra2], first assume the prophecy is trivial. *)
+ destruct bs as [|b blocks].
+ { (* We access the atomic update and commit the element. *)
+ iMod "AU" as (elts_AU) "[He◯ [_ Hclose]]".
+ iDestruct (sync_elts with "He● He◯") as %<-.
+ iMod (update_elts _ _ _ (elts ++ [l]) with "He● He◯") as "[He● He◯]".
+ iMod ("Hclose" with "[$He◯]") as "HΦ".
+ (* We allocate the new slot. *)
+ iMod (alloc_done_slot γs slots i l Hi_free with "Hs●")
+ as "[Hs [Htok_i [#val_wit_i [#commit_wit_i Hwriting_tok_i]]]]".
+ (* And we can close the invariant. *)
+ iModIntro. iSplitR "HΦ Hwriting_tok_i".
+ { iNext. iExists (S back), pvs, pref, (rest ++ [l]), (NoCont []).
+ iExists (<[i := (l, Done, false)]> slots), deqs.
+ rewrite array_content_NONEV. iFrame.
+ iFrame. iSplitL "He●".
+ { rewrite /elts app_assoc map_get_value_not_in_pref; try done.
+ intros Hi%Hpref. rewrite Hi_free in Hi. destruct Hi; done. }
+ iSplitL "Hbig Htok_i".
+ { iApply big_sepM_insert.
+ + apply eq_None_not_Some. intros H. apply Hslots in H. lia.
+ + iFrame "Hbig". repeat (iSplit; first done). done. }
+ destruct Hcont as (HC1 & HC2 & HC3).
+ iPureIntro. repeat split_and; try done; try by lia.
+ - intros k. destruct sz; first by lia.
+ split; intros Hk.
+ + destruct (decide (k = i)) as [->|k_not_i].
+ * rewrite lookup_insert. by eexists.
+ * rewrite lookup_insert_ne; last done. apply Hslots. by lia.
+ + destruct (decide (k = i)) as [->|k_not_i].
+ * destruct sz; by lia.
+ * rewrite lookup_insert_ne in Hk; last done.
+ apply Hslots in Hk. by lia.
+ - intros k. destruct (decide (k = i)) as [->|k_not_i].
+ + by rewrite lookup_insert.
+ + rewrite lookup_insert_ne; last done. apply Hstate.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + by rewrite lookup_insert.
+ + rewrite lookup_insert_ne; last done. apply Hpref, Hk.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + by rewrite lookup_insert.
+ + rewrite /array_get. rewrite lookup_insert_ne; last done.
+ apply Hdeqs in Hk as (H1 & H2 & H3). repeat (split; first done).
+ rewrite /array_get in H3.
+ destruct (slots !! k) as [[[dl ds] dw]|]; last done. done.
+ - intros b Hb. by inversion Hb.
+ - done.
+ - done.
+ - done. }
+ (* Let's clean up the context a bit. *)
+ clear Hslots Hstate Hpref Hdeqs Hcont Hi_not_in_deq Hi_free Hpvs_ND Hpvs_sz.
+ clear pvs pref rest slots deqs elts. subst i. rename back into i.
+ (* We can now move to the store. *)
+ wp_pures. rewrite (bool_decide_true _ Hback_sz).
+ wp_pures. wp_bind (_ <- _)%E.
+ (* We open the invariant again for the store. *)
+ iInv "Inv" as (back pvs pref rest cont slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [Hb● [Hi● [He● [>Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[Hproph [Hbig [>Hcont >Hpures]]]".
+ iDestruct "Hpures" as %(Hslots & Hstate & Hpref & Hdeqs & Hpvs_OK & Hcont).
+ destruct Hpvs_OK as (Hpvs_ND & Hpvs_sz).
+ (* Using witnesses, we show that our value and state have not changed. *)
+ iDestruct (use_val_wit with "Hs● val_wit_i") as %Hval_wit_i.
+ iDestruct (use_committed_wit with "Hs● commit_wit_i") as %Hval_commit_i.
+ iDestruct (writing_tok_not_written with "Hs● Hwriting_tok_i") as %Hnot_written_i.
+ (* Our slot is mapped. *)
+ assert (is_Some (slots !! i)) as Hslots_i.
+ { destruct (slots !! i) as [d|]; first by exists d. inversion Hval_wit_i. }
+ (* Our index is in the array. *)
+ assert (i < back `min` sz)%nat as Hi_le_back by by apply Hslots.
+ (* An we perform the store. *)
+ wp_apply (wp_store_offset _ _ ℓ_ar i (array_content sz slots deqs) with "Hℓ_ar").
+ { apply array_content_is_Some. by lia. }
+ iIntros "Hℓ_ar".
+ (* We perform some updates. *)
+ iMod (use_writing_tok with "Hs● Hwriting_tok_i") as "[Hs● #written_wit_i]".
+ iModIntro. iSplitR "HΦ"; last by wp_pures. iNext.
+ (* It remains to re-establish the invariant. *)
+ pose (new_slots := update_slot i set_written slots).
+ iExists back, pvs, pref, rest, cont, new_slots, deqs.
+ subst new_slots. iFrame. iSplitL "Hℓ_ar".
+ { rewrite array_content_set_written;
+ [ by iFrame | by lia | done | by apply Hstate ]. }
+ iSplitL "He●".
+ { erewrite map_ext; first by iFrame. rewrite /get_value. intros k.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ - rewrite update_slot_lookup. destruct Hslots_i as [d Hslots_i].
+ destruct d as [[ld sd] wd]. rewrite Hslots_i in Hnot_written_i.
+ inversion Hnot_written_i; subst wd. rewrite Hslots_i /=. done.
+ - rewrite update_slot_lookup_ne; last done. done. }
+ iSplitL "Hbig".
+ { rewrite /update_slot. destruct (slots !! i) as [d|] eqn:HEq; last done.
+ iApply big_sepM_insert; first by rewrite lookup_delete.
+ assert (slots = <[i:=d]> (delete i slots)) as HEq_slots.
+ { rewrite insert_delete. by rewrite insert_id. }
+ rewrite [X in ([∗ map] _ ↦ _ ∈ X, _)%I] HEq_slots.
+ iDestruct (big_sepM_insert with "Hbig")
+ as "[[H1 [H2 H3]] $]"; first by rewrite lookup_delete.
+ rewrite /per_slot_own val_of_set_written state_of_set_written.
+ iFrame. by rewrite was_written_set_written. }
+ iPureIntro.
+ destruct Hslots_i as [[[li si] wi] Hslots_i].
+ repeat split_and; try done.
+ - intros k. destruct (decide (k = i)) as [->|k_not_i].
+ + rewrite update_slot_lookup. split; intros H; last done.
+ rewrite Hslots_i. by eexists.
+ + rewrite update_slot_lookup_ne; last done. by apply Hslots.
+ - intros k. destruct (decide (k = i)) as [->|k_not_i].
+ + rewrite update_slot_lookup Hslots_i /=. split; intros H.
+ * exfalso. rewrite Hslots_i in Hval_commit_i.
+ destruct si as [γ|γ|]; try by inversion Hval_commit_i.
+ * by inversion H.
+ + rewrite update_slot_lookup_ne; last done. apply Hstate.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hslots_i /=. repeat split.
+ * rewrite Hslots_i in Hval_commit_i.
+ destruct si; try by inversion Hval_commit_i.
+ * by intros Hi%Hpref.
+ * by apply Hpref in Hk as (_ & _ & H).
+ + rewrite update_slot_lookup_ne; last done. apply Hpref, Hk.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hslots_i /update_slot /=.
+ rewrite Hslots_i /= insert_delete /array_get lookup_insert.
+ rewrite decide_True; last done. repeat split; try done.
+ destruct si; try done. rewrite Hslots_i in Hval_commit_i. done.
+ + rewrite /array_get update_slot_lookup_ne; last done.
+ apply Hdeqs in Hk. rewrite /array_get in Hk. done.
+ - destruct cont as [i1 i2|bs].
+ + destruct Hcont as (HC1 & HC2 & HC3 & HC4 & HC5 & HC6). split; first done.
+ destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ * rewrite /array_get update_slot_lookup Hslots_i /=.
+ repeat split_and; try done.
+ ** rewrite Hslots_i in Hval_commit_i. destruct si; try done.
+ ** rewrite decide_False; first done. apply Hstate. done.
+ * rewrite /array_get update_slot_lookup_ne; last done.
+ rewrite /array_get in HC3. done.
+ + destruct Hcont as (HC1 & HC2 & HC3). repeat split_and; try done.
+ intros b Hb. apply HC1 in Hb as (Hb1 & Hb2). split.
+ * destruct (decide (b.1 = i)) as [Hb1_is_i|Hb1_not_i].
+ ** rewrite -Hb1_is_i in Hslots_i. by rewrite Hslots_i in Hb1.
+ ** rewrite /update_slot Hslots_i insert_delete.
+ by rewrite lookup_insert_ne.
+ * intros k Hk. destruct (decide (k = i)) as [Hk_is_i|Hk_not_i].
+ ** rewrite /update_slot Hslots_i insert_delete. subst k.
+ rewrite lookup_insert /=. rewrite Hslots_i in Hval_commit_i.
+ destruct (was_committed (li, si, true)) eqn:H; last done.
+ exfalso. apply Hb2 in Hk. rewrite Hslots_i in Hk. inversion Hk.
+ destruct si; try done.
+ ** rewrite /update_slot Hslots_i insert_delete.
+ rewrite lookup_insert_ne; last done. apply Hb2, Hk. }
+ (* There is no [Contra1]/[Contra2], and the prophecy is non-trivial. *)
+ destruct Hcont as (Hblocks & Hrest & Hpvs).
+ assert (rest = []) as -> by by apply Hrest.
+ rewrite -app_nil_end in elts. rewrite -app_nil_end.
+ destruct b as [b_unused b_pendings].
+ (* We compare our index with the unused element of the prophecy. *)
+ destruct (decide (b_unused = i)) as [->|b_unused_not_i].
+ + (* We are the non-committed element of the prophecy: commit the block. *)
+ (* We allocate the new slot. *)
+ iMod (alloc_done_slot γs slots i l Hi_free with "Hs●")
+ as "[Hs● [Htok_i [#val_wit_i [#commit_wit_i Hwriting_tok_i]]]]".
+ (* We then commit at our index. *)
+ iMod "AU" as (elts_AU) "[He◯ [_ Hclose]]".
+ iDestruct (sync_elts with "He● He◯") as %<-.
+ iMod (update_elts _ _ _ (elts ++ [l]) with "He● He◯") as "[He● He◯]".
+ iMod ("Hclose" with "[$He◯]") as "HΦ".
+ (* Our prophecy block must be valid. *)
+ assert (block_valid slots (i, b_pendings))
+ as Hb_valid by apply Hblocks, elem_of_list_here.
+ rewrite /block_valid /= in Hb_valid.
+ destruct Hb_valid as [Hb_valid1 Hb_valid2].
+ (* We also need to commit for all indices in in [p_pendings] *)
+ assert (NoDup (i :: b_pendings)) as Hblock_ND.
+ { apply NoDup_app in Hpvs_ND as (H & _ & _). subst pvs.
+ apply NoDup_app in H as (_ & _ & H). simpl in H.
+ rewrite app_comm_cons in H. by apply NoDup_app in H as (H & _ & _). }
+ apply NoDup_cons in Hblock_ND as (Hi & HNoDup).
+ iAssert (per_slot_own γe γs i (l, Done, false)) with "[Htok_i]" as "Hi".
+ { rewrite /per_slot_own /=. eauto with iFrame. }
+ iDestruct (big_sepM_insert (per_slot_own γe γs) slots i (l, Done, false)
+ with "[Hi Hbig]") as "Hbig"; [ done | by iFrame | .. ].
+ iMod (big_lemma _ _ _ _ b_pendings HNoDup with "Hs● Hbig He●") as "[Hs● [Hbig He●]]".
+ { intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + exfalso. apply Hi, Hk.
+ + rewrite lookup_insert_ne; last done. apply Hb_valid2, Hk. }
+ (* And then we can close the invariant. *)
+ iModIntro. iSplitR "HΦ Hwriting_tok_i".
+ { pose (new_pref := pref ++ i :: b_pendings).
+ pose (new_slots := map_imap (helped b_pendings) (<[i:=(l, Done, false)]> slots)).
+ iNext. iExists (S back), pvs, new_pref, [], (NoCont blocks), new_slots, deqs.
+ iFrame. iSplitL "Hℓ_ar".
+ { assert (array_content sz slots deqs = array_content sz new_slots deqs) as ->; last done.
+ apply array_content_ext. intros k Hk. rewrite /new_slots /array_get.
+ rewrite lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i].
+ - by rewrite lookup_insert Hb_valid1 /helped /= decide_False.
+ - rewrite lookup_insert_ne; last done.
+ destruct (slots !! k) as [[[dl ds] dw]|]; last done.
+ rewrite /helped /=. destruct ds as [dγ|dγ|].
+ + destruct dw; try done; by destruct (decide (k ∈ b_pendings)).
+ + by destruct dw.
+ + by destruct dw. }
+ iSplitL "He●".
+ { rewrite -app_nil_end /new_pref /elts map_app map_cons.
+ rewrite [in get_value new_slots deqs i]/get_value.
+ rewrite [in new_slots !! i]/new_slots.
+ rewrite lookup_imap lookup_insert /= -app_assoc cons_middle.
+ assert (NoDup (pref ++ i :: b_pendings)) as HND.
+ { apply NoDup_app in Hpvs_ND as (HND & _ & _).
+ rewrite cons_middle app_assoc.
+ rewrite Hpvs /= in HND. rewrite cons_middle in HND.
+ rewrite app_assoc app_assoc in HND.
+ by apply NoDup_app in HND as (HND & _ & _). }
+ rewrite annoying_lemma_1; try done.
+ assert (map (get_value new_slots deqs) b_pendings
+ = get_values (<[i:=(l, Done, false)]> slots) b_pendings) as ->.
+ - rewrite /new_slots. by eapply annoying_lemma_2.
+ - done.
+ - intros k Hk. by apply Hpref in Hk as (H1 & H2 & _). }
+ iPureIntro. repeat split_and; try done.
+ - intros k. rewrite /new_slots lookup_imap. split; intros Hk.
+ + destruct (decide (k = i)) as [->|Hk_not_i].
+ * rewrite lookup_insert /helped /=. by eexists.
+ * rewrite lookup_insert_ne; last done.
+ assert (is_Some (slots !! k)) as [d ->] by (apply Hslots; lia).
+ by apply is_Some_helped.
+ + destruct (decide (k = i)) as [->|Hk_not_i]; first by lia.
+ rewrite lookup_insert_ne in Hk; last done.
+ assert (k < back `min` sz)%nat as H; last by lia.
+ apply Hslots. destruct (slots !! k) as [d|]; first by exists d.
+ by inversion Hk.
+ - intros k. rewrite /new_slots lookup_imap.
+ destruct (decide (k = i)) as [->|Hk_not_i];
+ first by rewrite lookup_insert /helped /=.
+ rewrite lookup_insert_ne; last done. split; intros Hk.
+ + destruct (slots !! k) as [d|] eqn:HEq; last done.
+ assert (was_committed <$> Some d ≫= helped b_pendings k = was_committed <$> Some d) as HEq1.
+ { destruct d as [[dl []] dw]; simpl; simpl in Hk; by rewrite Hk. }
+ rewrite HEq1 -HEq in Hk. apply Hstate in Hk. rewrite HEq in Hk.
+ assert (was_written <$> Some d ≫= helped b_pendings k = was_written <$> Some d) as HEq2.
+ { destruct d as [[dl []] []]; simpl; simpl in Hk; try by inversion Hk.
+ rewrite /helped /=. destruct (decide (k ∈ b_pendings)); done. }
+ rewrite HEq2. by inversion Hk.
+ + destruct (slots !! k) as [d|] eqn:HEq; last done.
+ assert (was_written <$> Some d ≫= helped b_pendings k = was_written <$> Some d) as HEq1.
+ { by destruct d as [[dl []] dw]; rewrite /helped; destruct (decide (k ∈ b_pendings)). }
+ rewrite HEq1 -HEq in Hk. apply Hstate in Hk. done.
+ - intros k Hk. subst new_pref new_slots. apply elem_of_app in Hk as [Hk|Hk].
+ { apply Hpref in Hk as (H1 & H2). split; last done.
+ rewrite map_imap_insert /=. destruct (decide (k = i)) as [->|Hk_not_i].
+ - by rewrite lookup_insert.
+ - rewrite lookup_insert_ne; last done. rewrite lookup_imap.
+ destruct (slots !! k) as [[[dl ds] dw]|]; last by inversion H1.
+ rewrite /= /helped. destruct ds as [dγ|dγ|]; try done. }
+ apply elem_of_cons in Hk as [Hk|Hk].
+ { subst k. split; last done. by rewrite map_imap_insert /= lookup_insert. }
+ apply Hb_valid2 in Hk as Hb_valid2_k. split.
+ + rewrite lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i].
+ * by rewrite lookup_insert /=.
+ * rewrite lookup_insert_ne; last done.
+ destruct (slots !! k) as [[[kl ks] kw]|]; last by inversion Hb_valid2_k.
+ rewrite /= /helped. destruct ks; try done. by rewrite /= decide_True.
+ + apply Hstate in Hb_valid2_k. apply Hstate in Hb_valid2_k. done.
+ - intros k Hk. subst new_slots. rewrite /array_get lookup_imap.
+ assert (k ≠ i) as Hk_not_i. { intros ->. apply Hi_not_in_deq, Hk. }
+ rewrite lookup_insert_ne; last done. apply Hdeqs in Hk as (H1 & H2 & H3).
+ destruct (slots !! k) as [[[lk sk] wk]|] eqn:HEq; last by inversion H1.
+ inversion H1; subst wk. rewrite /=. repeat split_and; try by destruct sk.
+ destruct sk; try done; simpl.
+ + rewrite decide_True; first done.
+ rewrite /array_get HEq in H3. simpl in H3.
+ destruct (decide (k ∈ deqs)); first done. by inversion H3.
+ + rewrite decide_True; first done.
+ rewrite /array_get HEq in H3. simpl in H3.
+ destruct (decide (k ∈ deqs)); first done. by inversion H3.
+ - intros b Hk. subst new_slots. rewrite map_imap_insert /=.
+ assert (b ∈ (i, b_pendings) :: blocks) as H by set_solver +Hk.
+ assert (NoDup (i :: b_pendings ++ flatten_blocks blocks)) as HND.
+ { subst pvs. apply NoDup_app in Hpvs_ND as (HND & _ & _).
+ apply NoDup_app in HND as (_ & _ & HND). done. }
+ apply flatten_blocks_mem1 in Hk as Hk1.
+ apply Hblocks in H as (H1 & H2). split.
+ + assert (b.1 ≠ i) as Hb1_not_i.
+ { intros HEq. apply NoDup_cons in HND as [HND1 HND2]. apply HND1.
+ rewrite -HEq. apply elem_of_app. by right. }
+ rewrite lookup_insert_ne; last done. by rewrite lookup_imap H1.
+ + intros j Hj. assert (j ≠ i) as Hj_not_i.
+ { intros HEq. apply NoDup_cons in HND as [HND1 HND2]. apply HND1.
+ rewrite -HEq. apply elem_of_app. right.
+ apply (flatten_blocks_mem2 _ _ Hk _ Hj). }
+ rewrite lookup_insert_ne; last done. rewrite lookup_imap.
+ apply H2 in Hj as Hcomm.
+ destruct (slots !! j) as [[[lj sj] wj]|]; last by inversion Hj.
+ rewrite /= /helped. destruct sj; try done. simpl.
+ assert (j ∉ b_pendings); last by rewrite decide_False.
+ intros Hj_contra. apply NoDup_cons in HND as [_ HND].
+ apply NoDup_app in HND. destruct HND as (HND1 & HND2 & HND3).
+ apply (HND2 _ Hj_contra). apply (flatten_blocks_mem2 _ _ Hk _ Hj).
+ - by rewrite Hpvs /= /new_pref app_comm_cons app_assoc. }
+ clear Hslots Hstate Hpref Hdeqs Hpvs Hrest Hblocks Hi_free Hi_not_in_deq.
+ clear Hpvs_ND Hpvs_sz Hb_valid1 Hb_valid2 HNoDup Hi elts pvs pref slots deqs.
+ clear blocks b_pendings. subst i. rename back into i.
+ wp_pures. rewrite bool_decide_true; last done. wp_pures.
+ wp_bind (_ <- _)%E.
+ (* We open the invariant again for the store. *)
+ iInv "Inv" as (back pvs pref rest cont slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [Hb● [Hi● [He● [>Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[Hproph [Hbig [>Hcont >Hpures]]]".
+ iDestruct "Hpures" as %(Hslots & Hstate & Hpref & Hdeqs & Hpvs_OK & Hcont).
+ destruct Hpvs_OK as (Hpvs_ND & Hpvs_sz).
+ (* Using witnesses, we show that our value and state have not changed. *)
+ iDestruct (use_val_wit with "Hs● val_wit_i") as %Hval_wit_i.
+ iDestruct (use_committed_wit with "Hs● commit_wit_i") as %Hval_commit_i.
+ iDestruct (writing_tok_not_written with "Hs● Hwriting_tok_i") as %Hnot_written_i.
+ (* Our slot is mapped. *)
+ assert (is_Some (slots !! i)) as Hslots_i.
+ { destruct (slots !! i) as [d|]; first by exists d. inversion Hval_wit_i. }
+ (* Our index is in the array. *)
+ assert (i < back `min` sz)%nat as Hi_le_back by by apply Hslots.
+ (* An we perform the store. *)
+ wp_apply (wp_store_offset _ _ ℓ_ar i (array_content sz slots deqs) with "Hℓ_ar").
+ { apply array_content_is_Some. by lia. }
+ iIntros "Hℓ_ar".
+ (* We perform some updates. *)
+ iMod (use_writing_tok with "Hs● Hwriting_tok_i") as "[Hs● #written_wit_i]".
+ iModIntro. iSplitR "HΦ"; last by wp_pures. iNext.
+ (* It remains to re-establish the invariant. *)
+ { pose (new_slots := update_slot i set_written slots).
+ iExists back, pvs, pref, rest, cont, new_slots, deqs.
+ subst new_slots. iFrame. iSplitL "Hℓ_ar".
+ { rewrite array_content_set_written;
+ [ by iFrame | by lia | done | by apply Hstate ]. }
+ iSplitL "He●".
+ { erewrite map_ext; first by iFrame. rewrite /get_value. intros k.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ - rewrite update_slot_lookup. destruct Hslots_i as [d Hslots_i].
+ destruct d as [[ld sd] wd]. rewrite Hslots_i in Hnot_written_i.
+ inversion Hnot_written_i; subst wd. rewrite Hslots_i /=. done.
+ - rewrite update_slot_lookup_ne; last done. done. }
+ iSplitL "Hbig".
+ { rewrite /update_slot. destruct (slots !! i) as [d|] eqn:HEq; last done.
+ iApply big_sepM_insert; first by rewrite lookup_delete.
+ assert (slots = <[i:=d]> (delete i slots)) as HEq_slots.
+ { rewrite insert_delete. by rewrite insert_id. }
+ rewrite [X in ([∗ map] _ ↦ _ ∈ X, _)%I] HEq_slots.
+ iDestruct (big_sepM_insert with "Hbig")
+ as "[[H1 [H2 H3]] $]"; first by rewrite lookup_delete.
+ rewrite /per_slot_own val_of_set_written state_of_set_written.
+ iFrame. by rewrite was_written_set_written. }
+ iPureIntro.
+ repeat split_and; try done.
+ - intros k. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup. split; intros Hk; last by lia.
+ by apply fmap_is_Some.
+ + rewrite update_slot_lookup_ne; last done. apply Hslots.
+ - intros k. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup. split; intros Hk; exfalso.
+ * destruct (slots !! i) as [[[li si] wi]|]; last by inversion Hk.
+ inversion_clear Hnot_written_i. destruct si; inversion Hk.
+ inversion Hval_commit_i.
+ * destruct (slots !! i) as [[[li si] wi]|]; by inversion Hk.
+ + rewrite update_slot_lookup_ne; last done. by apply Hstate.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup /=. split.
+ * destruct (slots !! i) as [[[li si] wi]|]; first done.
+ by inversion Hval_wit_i.
+ * apply Hpref, Hk.
+ + rewrite update_slot_lookup_ne; last done. by apply Hpref.
+ - intros k Hk. assert (k ≠ i) as Hk_not_i.
+ { intros ->. apply Hdeqs in Hk as (H1 & H2 & H3).
+ apply Hstate in Hnot_written_i. rewrite /array_get in H3.
+ destruct Hslots_i as [[[li si] wi] Hslots_i].
+ rewrite Hslots_i decide_False in H3; last done.
+ rewrite Hslots_i in H1. inversion H1; subst wi. inversion H3. }
+ rewrite /array_get update_slot_lookup_ne; last done.
+ apply Hdeqs in Hk. rewrite /array_get in Hk. done.
+ - destruct cont as [i1 i2|bs].
+ + destruct Hcont as (HC1 & HC2 & HC3 & HC4 & HC5 & HC6).
+ split; first done. repeat split_and; try done.
+ * destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ ** rewrite update_slot_lookup.
+ destruct (slots !! i) as [[[li si] wi]|]; first done.
+ by inversion Hval_wit_i.
+ ** by rewrite update_slot_lookup_ne.
+ * destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ ** rewrite /array_get update_slot_lookup.
+ destruct (slots !! i) as [[[li si] wi]|] eqn:HEq; try done.
+ ** by rewrite /array_get update_slot_lookup_ne.
+ * destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ ** rewrite /array_get update_slot_lookup.
+ destruct (slots !! i) as [[[li si] wi]|] eqn:HEq; try done.
+ inversion HC3; subst wi. done.
+ ** rewrite /array_get update_slot_lookup_ne; last done.
+ destruct (slots !! i1) as [[[li1 si1] wi1]|] eqn:HEq; try done.
+ rewrite decide_False; last done. inversion HC3; subst wi1. done.
+ + destruct Hcont as (HC1 & HC2 & HC3). repeat split_and; try done.
+ destruct Hslots_i as [[[li si] wi] Hslots_i].
+ intros b Hb. apply HC1 in Hb as (Hb1 & Hb2). split.
+ * destruct (decide (b.1 = i)) as [Hb1_is_i|Hb1_not_i].
+ ** rewrite -Hb1_is_i in Hslots_i. rewrite Hb1 in Hslots_i.
+ by inversion Hslots_i.
+ ** by rewrite /update_slot Hslots_i insert_delete lookup_insert_ne.
+ * intros k Hk. destruct (decide (k = i)) as [Hk_is_i|Hk_not_i].
+ ** rewrite /update_slot Hslots_i insert_delete. subst k.
+ rewrite lookup_insert /=. rewrite Hslots_i in Hval_commit_i.
+ destruct (was_committed (li, si, true)) eqn:H; last done.
+ exfalso. apply Hb2 in Hk. rewrite Hslots_i in Hk. inversion Hk.
+ destruct si; try done.
+ ** rewrite /update_slot Hslots_i insert_delete.
+ rewrite lookup_insert_ne; last done. apply Hb2, Hk. }
+ + (* We are not the first non-done element, we will give away our AU. *)
+ iMod (saved_prop_alloc (Φ #())) as (γs_i) "#Hγs_i".
+ iMod (alloc_pend_slot γs slots i l γs_i Hi_free with "Hs●")
+ as "[Hs● [Htok_i [#val_wit_i [Hpend_tok_i [Hname_tok_i Hwriting_tok_i]]]]]".
+ (* We close the invariant, storing our AU. *)
+ iModIntro. iSplitR "Htok_i Hname_tok_i Hwriting_tok_i".
+ { pose (new_bs := glue_blocks (b_unused, b_pendings) i blocks).
+ pose (new_slots := <[i:=(l, Pend γs_i, false)]> slots).
+ iNext. iExists (S back), pvs, pref, [], (NoCont new_bs), new_slots, deqs.
+ rewrite -app_nil_end. iFrame. iSplitL "Hℓ_ar".
+ { assert (array_content sz slots deqs = array_content sz new_slots deqs) as ->; last done.
+ apply array_content_ext. intros k Hk. rewrite /new_slots /array_get.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ - by rewrite Hi_free lookup_insert decide_False.
+ - rewrite lookup_insert_ne; last done. destruct (slots !! k) as [d|]; last done.
+ destruct d as [[dl ds] dw]. rewrite /helped /=.
+ destruct ds as [dγ|dγ|]; destruct dw; try done. }
+ iSplitL "He●".
+ { erewrite map_ext_in; first done. subst new_slots.
+ intros k Hk%elem_of_list_In. rewrite /get_value.
+ assert (k ≠ i); last by rewrite lookup_insert_ne.
+ intros ->. apply Hpref in Hk as (H1 & H2).
+ rewrite Hi_free in H1. inversion H1. }
+ iSplitL "Hbig Hpend_tok_i AU".
+ { iApply big_sepM_insert; first done. iFrame. iSplit; first done.
+ iExists (Φ #()). iFrame. done. }
+ iPureIntro. subst new_slots. repeat split_and; try done.
+ - intros k. destruct sz; first by lia.
+ split; intros Hk.
+ + destruct (decide (k = i)) as [->|k_not_i].
+ * rewrite lookup_insert. by eexists.
+ * rewrite lookup_insert_ne; last done. apply Hslots. by lia.
+ + destruct (decide (k = i)) as [->|k_not_i].
+ * destruct sz; by lia.
+ * rewrite lookup_insert_ne in Hk; last done.
+ apply Hslots in Hk. by lia.
+ - intros k. destruct (decide (k = i)) as [->|Hk_not_i].
+ + by rewrite lookup_insert.
+ + rewrite lookup_insert_ne; last done. apply Hstate.
+ - intros k Hk. rewrite lookup_insert_ne; first by apply Hpref, Hk.
+ intros HEq. subst k. apply Hpref in Hk as [H _].
+ rewrite Hi_free in H. inversion H.
+ - intros k Hk. rewrite /array_get lookup_insert_ne.
+ + apply Hdeqs in Hk. by rewrite /array_get in Hk.
+ + intros <-. apply Hdeqs in Hk as [Hk _]. rewrite Hi_free in Hk. done.
+ - intros b Hb. subst new_bs. rewrite Hpvs in Hpvs_ND.
+ apply NoDup_app in Hpvs_ND as (HND & _ & _).
+ apply NoDup_app in HND as (_ & _ & HND). simpl in HND.
+ by eapply glue_blocks_valid.
+ - subst pvs new_bs. f_equal. apply flatten_blocks_glue. }
+ clear Hslots Hstate Hpref Hdeqs Hblocks Hrest Hpvs Hi_free Hi_not_in_deq.
+ clear Hpvs_ND Hpvs_sz b_unused b_unused_not_i elts blocks pvs pref slots.
+ clear deqs b_pendings. subst i. rename back into i.
+ wp_pures. rewrite bool_decide_true; last done.
+ wp_pures. wp_bind (_ <- _)%E.
+ (* We open the invariant again for the store. *)
+ iInv "Inv" as (back pvs pref rest cont slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [Hb● [Hi● [He● [>Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[Hproph [Hbig [>Hcont >Hpures]]]".
+ iDestruct "Hpures" as %(Hslots & Hstate & Hpref & Hdeqs & Hpvs_OK & Hcont).
+ destruct Hpvs_OK as (Hpvs_ND & Hpvs_sz).
+ (* Using witnesses, we show that our value and state have not changed. *)
+ iDestruct (use_val_wit with "Hs● val_wit_i") as %Hval_wit_i.
+ iDestruct (writing_tok_not_written with "Hs● Hwriting_tok_i") as %Hnot_written_i.
+ (* Our slot is mapped. *)
+ assert (is_Some (slots !! i)) as Hslots_i.
+ { destruct (slots !! i) as [d|]; first by exists d. inversion Hval_wit_i. }
+ (* Our index is in the array. *)
+ assert (i < back `min` sz)%nat as Hi_le_back by by apply Hslots.
+ (* An we perform the store. *)
+ wp_apply (wp_store_offset _ _ ℓ_ar i (array_content sz slots deqs) with "Hℓ_ar").
+ { apply array_content_is_Some. by lia. }
+ iIntros "Hℓ_ar".
+ (* We now look at the state of our cell. *)
+ destruct Hslots_i as [[[l' s] w] Hi].
+ rewrite Hi in Hval_wit_i. simpl in Hval_wit_i.
+ inversion Hval_wit_i; subst l'.
+ destruct s as [γs_i'|γs_i'|].
+ - (* We are still in the pending state: contradiction. *)
+ (* We need to run our atomic update ourselves, we recover it. *)
+ rewrite -[in X in ([∗ map] _ ↦ _ ∈ X, _)%I](insert_id _ _ _ Hi).
+ rewrite -insert_delete.
+ iDestruct (big_sepM_insert with "Hbig")
+ as "[Hbig_i Hbig]"; first by apply lookup_delete.
+ iDestruct "Hbig_i" as "[_ [_ [Hcommit_tok_i HAU]]]".
+ iDestruct "HAU" as (Q) "[Hsaved AU]".
+ (* We use the name token to show that γs_i and γs_i' are equal. *)
+ iDestruct (use_name_tok with "Hs● Hname_tok_i") as %Hname_tok_i.
+ assert (γs_i' = γs_i) as Hγs_i; last subst γs_i'.
+ { rewrite Hi /= in Hname_tok_i. by inversion Hname_tok_i. }
+ iDestruct (saved_prop_agree with "Hγs_i Hsaved") as "HQ_is_Φ".
+ (* We run our atomic update ourself. *)
+ pose (elts := map (get_value slots deqs) pref ++ rest).
+ iMod "AU" as (elts_AU) "[He◯ [_ Hclose]]".
+ iDestruct (sync_elts with "He● He◯") as %<-.
+ iMod (update_elts _ _ _ (elts ++ [l]) with "He● He◯") as "[He● He◯]".
+ iMod ("Hclose" with "[$He◯]") as "HΦ".
+ iMod (use_writing_tok with "Hs● Hwriting_tok_i") as "[Hs● #written_wit_i]".
+ iMod (use_pending_tok with "Hs● Hcommit_tok_i") as "[Hs● #commit_wit_i]".
+ { by rewrite update_slot_lookup Hi /=. }
+ iMod (helped_to_done with "Hs● Hname_tok_i") as "Hs●".
+ { by rewrite update_slot_lookup update_slot_lookup Hi. }
+ (* We now act according ot the contradiction status. *)
+ destruct cont as [i1 i2|bs].
+ * (* A contradiction has arised from somewhere else, we keep it. *)
+ iModIntro. iSplitR "HQ_is_Φ HΦ".
+ { iNext. iExists back, pvs, pref, (rest ++ [l]), (WithCont i1 i2).
+ iExists (update_slot i set_written_and_done slots), deqs.
+ subst elts. rewrite app_assoc. iFrame. iSplitL "Hℓ_ar".
+ { rewrite array_content_set_written_and_done;
+ [ by iFrame | by lia | by rewrite Hi | by apply Hstate ]. }
+ iSplitL "He●".
+ { erewrite map_ext_in; first done. intros k Hk%elem_of_list_In.
+ rewrite /get_value /update_slot Hi insert_delete.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ - by rewrite lookup_insert Hi.
+ - by rewrite lookup_insert_ne. }
+ iSplitL "Hs●".
+ { repeat rewrite update_slot_update_slot. by rewrite /update_slot Hi. }
+ iSplitL.
+ { rewrite /update_slot Hi.
+ iApply big_sepM_insert; first by rewrite lookup_delete.
+ iFrame "Hbig". rewrite /per_slot_own /=. iFrame.
+ iSplit; first done. iSplit; done. }
+ iPureIntro.
+ destruct Hcont as (((HC1 & HC2) & HC3) & HC4 & HC5 & HC6 & HC7 & HC8).
+ repeat split_and; try lia; try done.
+ - intros k. destruct (decide (i = k)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hi. split; [ by eexists | lia ].
+ + rewrite update_slot_lookup_ne; last done. apply Hslots.
+ - intros k. split; intros Hk.
+ + assert (k ≠ i) as Hk_not_i.
+ { intros ->. by rewrite update_slot_lookup Hi in Hk. }
+ rewrite update_slot_lookup_ne; last done.
+ rewrite update_slot_lookup_ne in Hk; last done.
+ by apply Hstate.
+ + assert (k ≠ i) as Hk_not_i.
+ { intros ->. by rewrite update_slot_lookup Hi in Hk. }
+ rewrite update_slot_lookup_ne in Hk; last done. by apply Hstate.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hi /=. split; [ done | by apply Hpref, Hk ].
+ + rewrite update_slot_lookup_ne; last done. apply Hpref, Hk.
+ - intros k Hk. assert (k ≠ i) as Hk_not_i.
+ { intros ->. apply Hdeqs in Hk as (H1 & H2 & H3).
+ apply Hstate in Hnot_written_i. rewrite /array_get in H3.
+ rewrite Hi decide_False in H3; last done.
+ rewrite Hi in H1. inversion H1; subst w. inversion H3. }
+ rewrite /array_get update_slot_lookup_ne; last done.
+ apply Hdeqs in Hk. rewrite /array_get in Hk. done.
+ - destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ + by rewrite update_slot_lookup Hi.
+ + by rewrite update_slot_lookup_ne.
+ - destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ + by rewrite update_slot_lookup Hi /=.
+ + rewrite update_slot_lookup_ne; last done.
+ destruct (slots !! i1) as [[[li1 si1] wi1]|]; last by inversion HC4.
+ inversion HC5; subst wi1. done.
+ - destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ + by rewrite /array_get update_slot_lookup Hi /= decide_False.
+ + rewrite /array_get update_slot_lookup_ne; last done.
+ destruct (slots !! i1) as [[[li1 si1] wi1]|]; last by inversion HC4.
+ rewrite decide_False; last done. inversion HC5; subst wi1. done. }
+ wp_pures. iRewrite "HQ_is_Φ". done.
+ * (* No contradiction yet, make it ours if the prophecy is non-trivial. *)
+ iAssert (match bs with
+ | [] => i2_lower_bound γi (back `min` sz)%nat
+ | _ => no_contra γc ∗ i2_lower_bound γi (back `min` sz)%nat
+ end -∗ |==>
+ match bs with
+ | [] => True
+ | (i2, _) :: _ => contra γc i i2
+ end ∗
+ match bs with
+ | [] => i2_lower_bound γi (back `min` sz)%nat
+ | (i2, _) :: _ => i2_lower_bound γi i2
+ end)%I as "Hup".
+ { destruct bs as [|[i2 ps] bs]; first (iIntros "Hi●"; by iFrame).
+ iIntros "[Hcont Hi●]". iMod (to_contra i i2 with "Hcont") as "$".
+ iMod (i2_lower_bound_update _ _ i2 with "Hi●") as "$"; last done.
+ assert (block_valid slots (i2, ps)) as [Hvalid _].
+ { destruct Hcont as (Hblocks & _ & _). apply Hblocks, elem_of_list_here. }
+ assert (¬ (i2 < back `min` sz)%nat) as H%not_lt; last by lia.
+ eapply iffRLn. apply Hslots. intros H. rewrite Hvalid in H. by inversion H. }
+ iAssert (match bs with
+ | [] => i2_lower_bound γi (back `min` sz)%nat
+ | _ => no_contra γc ∗ i2_lower_bound γi (back `min` sz)%nat
+ end ∗
+ match bs with
+ | [] => no_contra γc
+ | _ => True
+ end)%I with "[Hcont Hi●]" as "[HNC_triv HNC_non_triv]".
+ { destruct bs; by iFrame. }
+ iMod ("Hup" with "HNC_triv") as "[#HC_triv Hi●]".
+ (* We can now close the invariant. *)
+ iModIntro. iSplitR "HQ_is_Φ HΦ".
+ { pose (new_slots := update_slot i set_written_and_done slots).
+ pose (cont := match bs with [] => NoCont [] | (i2, _) :: _ => WithCont i i2 end).
+ iNext. iExists back, pvs, pref, (rest ++ [l]), cont, new_slots, deqs.
+ subst new_slots elts cont. rewrite app_assoc. iFrame. iSplitL "Hℓ_ar".
+ { rewrite array_content_set_written_and_done;
+ [ by iFrame | by lia | by rewrite Hi | by apply Hstate ]. }
+ iSplitL "Hi●".
+ { destruct bs as [|[b_u b_ps] bs]; by iFrame. }
+ iSplitL "He●".
+ { erewrite map_ext_in; first done. intros k Hk%elem_of_list_In.
+ rewrite /get_value /update_slot Hi insert_delete.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ - by rewrite lookup_insert Hi.
+ - by rewrite lookup_insert_ne. }
+ iSplitL "Hs●".
+ { repeat rewrite update_slot_update_slot. by rewrite /update_slot Hi. }
+ iSplitR "HNC_non_triv".
+ { rewrite /update_slot Hi.
+ iApply big_sepM_insert; first by rewrite lookup_delete.
+ iFrame "Hbig". rewrite /per_slot_own /=. iFrame.
+ iSplit; first done. iSplit; done. }
+ iSplitL "HNC_non_triv"; first by destruct bs as [|[i2 ps] bs].
+ iPureIntro. repeat split_and.
+ - intros k. destruct (decide (i = k)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hi. split; [ by eexists | lia ].
+ + rewrite update_slot_lookup_ne; last done. apply Hslots.
+ - intros k. split; intros Hk.
+ + assert (k ≠ i) as Hk_not_i.
+ { intros ->. by rewrite update_slot_lookup Hi in Hk. }
+ rewrite update_slot_lookup_ne; last done.
+ rewrite update_slot_lookup_ne in Hk; last done.
+ by apply Hstate.
+ + assert (k ≠ i) as Hk_not_i.
+ { intros ->. by rewrite update_slot_lookup Hi in Hk. }
+ rewrite update_slot_lookup_ne in Hk; last done. by apply Hstate.
+ - intros k Hk. apply Hpref in Hk as (H1 & H2 & _). repeat split; try done.
+ + destruct (decide (k = i)) as [->|Hk_not_i].
+ * by rewrite update_slot_lookup Hi.
+ * by rewrite update_slot_lookup_ne.
+ + destruct bs as [|[b_u b_ps] bs]; first done.
+ intros ->. rewrite Hi in H1. by inversion H1.
+ - intros k Hk. assert (k ≠ i) as Hk_not_i.
+ { intros ->. apply Hdeqs in Hk as (H1 & H2 & H3).
+ apply Hstate in Hnot_written_i. rewrite /array_get in H3.
+ rewrite Hi decide_False in H3; last done.
+ rewrite Hi in H1. inversion H1; subst w. inversion H3. }
+ rewrite /array_get update_slot_lookup_ne; last done.
+ apply Hdeqs in Hk. rewrite /array_get in Hk. done.
+ - done.
+ - done.
+ - destruct Hcont as (HC1 & HC2 & HC3).
+ destruct bs as [|[i2 ps] bs].
+ + repeat split_and; try done. intros. by set_solver.
+ + repeat split_and; try lia.
+ * assert (i < back `min` sz)%nat
+ as Hi_lt by (apply Hslots; by eexists).
+ assert (block_valid slots (i2, ps))
+ as Hvalid by apply HC1, elem_of_list_here.
+ assert (slots !! i2 = None)
+ as Hi2_None by by destruct Hvalid as (H & _).
+ assert (¬ i2 < back `min` sz)%nat as Hi2_ge; last by lia.
+ intros H%Hslots. rewrite Hi2_None in H. by inversion H.
+ * apply Hpvs_sz. subst pvs. apply elem_of_app. right. simpl.
+ by apply elem_of_list_here.
+ * by rewrite update_slot_lookup Hi /=.
+ * by rewrite update_slot_lookup Hi /=.
+ * by apply Hstate.
+ * rewrite /array_get update_slot_lookup Hi /=.
+ rewrite decide_False; first done. apply Hstate. done.
+ * rewrite HC3 /=. exists (ps ++ flatten_blocks bs).
+ by rewrite cons_middle app_assoc. }
+ wp_pures. iRewrite "HQ_is_Φ". done.
+ - (* We have moved to the helped state. *)
+ assert (slots = <[i := (l, Help γs_i', w)]> (delete i slots))
+ as Hslots_i by by rewrite insert_delete insert_id.
+ rewrite [X in ([∗ map] _ ↦ _ ∈ X, _)%I]Hslots_i.
+ (* We recover our postcondition. *)
+ iDestruct (big_sepM_insert with "Hbig")
+ as "[Hbig_i Hbig]"; first by apply lookup_delete.
+ iDestruct "Hbig_i" as "[_ [_ [Hcommit_wit_i Hpost]]]".
+ iDestruct "Hpost" as (Q) "[Hsaved Hpost]".
+ (* We use the name token to show that γs_i and γs_i' are equal. *)
+ iDestruct (use_name_tok with "Hs● Hname_tok_i") as %Hname_tok_i.
+ assert (γs_i' = γs_i) as Hγs_i; last subst γs_i'.
+ { rewrite Hi /= in Hname_tok_i. by inversion Hname_tok_i. }
+ iDestruct (saved_prop_agree with "Hγs_i Hsaved") as "HQ_is_Φ".
+ (* We need to move from helped to done. *)
+ iMod (helped_to_done with "Hs● Hname_tok_i") as "Hs●". { by rewrite Hi. }
+ (* We perform some updates. *)
+ iMod (use_writing_tok with "Hs● Hwriting_tok_i") as "[Hs● #written_wit_i]".
+ iModIntro. iSplitR "HQ_is_Φ Hpost".
+ { pose (new_slots := update_slot i set_written_and_done slots).
+ iNext. iExists back, pvs, pref, rest, cont, new_slots, deqs.
+ subst new_slots. iFrame. iSplitL "Hℓ_ar".
+ { rewrite array_content_set_written_and_done;
+ [ by iFrame | by lia | by rewrite Hi | by apply Hstate ]. }
+ iSplitL "He●".
+ { erewrite map_ext_in; first done. intros k Hk%elem_of_list_In.
+ rewrite /get_value /update_slot Hi insert_delete.
+ destruct (decide (k = i)) as [->|Hk_not_i].
+ - by rewrite lookup_insert Hi.
+ - by rewrite lookup_insert_ne. }
+ iSplitL "Hs●".
+ { repeat rewrite update_slot_update_slot. by rewrite /update_slot Hi. }
+ iSplitL.
+ { rewrite /update_slot Hi.
+ iApply big_sepM_insert; first by rewrite lookup_delete.
+ iFrame "Hbig". rewrite /per_slot_own /=. iFrame. iSplit; done. }
+ iPureIntro. repeat split_and; try done.
+ - intros k. destruct (decide (i = k)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hi. split; [ by eexists | lia ].
+ + rewrite update_slot_lookup_ne; last done. apply Hslots.
+ - intros k. split; intros Hk.
+ + assert (k ≠ i) as Hk_not_i.
+ { intros ->. by rewrite update_slot_lookup Hi in Hk. }
+ rewrite update_slot_lookup_ne; last done.
+ rewrite update_slot_lookup_ne in Hk; last done.
+ by apply Hstate.
+ + assert (k ≠ i) as Hk_not_i.
+ { intros ->. by rewrite update_slot_lookup Hi in Hk. }
+ rewrite update_slot_lookup_ne in Hk; last done. by apply Hstate.
+ - intros k Hk. destruct (decide (k = i)) as [->|Hk_not_i].
+ + rewrite update_slot_lookup Hi. split; first done. apply Hpref, Hk.
+ + rewrite update_slot_lookup_ne; last done. apply Hpref, Hk.
+ - intros k Hk. assert (k ≠ i) as Hk_not_i.
+ { intros ->. apply Hdeqs in Hk as (H1 & H2 & H3).
+ apply Hstate in Hnot_written_i. rewrite /array_get in H3.
+ rewrite Hi decide_False in H3; last done.
+ rewrite Hi in H1. inversion H1; subst w. inversion H3. }
+ rewrite /array_get update_slot_lookup_ne; last done.
+ apply Hdeqs in Hk. rewrite /array_get in Hk. done.
+ - destruct cont as [i1 i2|bs].
+ + destruct Hcont as (HC1 & HC2 & HC3 & HC4 & HC5 & HC6).
+ split; first done. repeat split_and; try done.
+ * destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ ** by rewrite update_slot_lookup Hi.
+ ** by rewrite update_slot_lookup_ne.
+ * destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ ** by rewrite /array_get update_slot_lookup Hi /=.
+ ** rewrite /array_get update_slot_lookup_ne; last done.
+ rewrite /array_get in HC3. done.
+ * destruct (decide (i1 = i)) as [->|Hi1_not_i].
+ ** by rewrite /array_get update_slot_lookup Hi decide_False.
+ ** rewrite /array_get update_slot_lookup_ne; last done.
+ rewrite /array_get in HC3. done.
+ + destruct Hcont as (HC1 & HC2 & HC3). repeat split_and; try done.
+ intros b Hb. apply HC1 in Hb as (H1 & H2). split.
+ ** assert (b.1 ≠ i) as Hb1_not_i.
+ { intros H. rewrite H in H1. by rewrite Hi in H1. }
+ by rewrite update_slot_lookup_ne.
+ ** intros k Hk. assert (k ≠ i) as Hb1_not_i.
+ { intros H. subst k. apply H2 in Hk. rewrite Hi in Hk.
+ by inversion Hk. }
+ rewrite update_slot_lookup_ne; last done. by apply H2. }
+ wp_pures. iRewrite "HQ_is_Φ". done.
+ - (* We are in the done state: contradiction. *)
+ iDestruct (big_sepM_lookup _ _ i with "Hbig")
+ as "[_ [_ H]]"; first done; simpl.
+ iDestruct "H" as "[_ Htok_i']".
+ by iDestruct (slot_token_exclusive with "Htok_i Htok_i'") as "H".
+Qed.
+
+Lemma dequeue_spec sz γe (q : val) :
+ is_hwq sz γe q -∗
+ <<< ∀ (ls : list loc), hwq_cont γe ls >>>
+ dequeue q @ ⊤ ∖ ↑N
+ <<< ∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_cont γe ls', RET #l >>>.
+Proof.
+ iIntros "Hq" (Φ) "AU". iLöb as "IH".
+ iDestruct "Hq" as (γb γi γc γs ℓ_ar ℓ_back p ->) "#Inv".
+ wp_lam. wp_pures. wp_bind (! _)%E.
+ (* We need to open the invariant to read [q.back]. *)
+ iInv "Inv" as (back pvs pref rest cont slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [>Hb● [Hi● [He● [Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[Hproph [Hbig [>Hcont Hpures]]]". wp_load.
+ (* If there is a contradiction, remember that. *)
+ iAssert (match cont with
+ | NoCont _ => True
+ | WithCont i1 i2 => contra γc i1 i2
+ end)%I with "[Hcont]" as "#Hinit_cont".
+ { destruct cont as [i1 i2|bs]; [ by iDestruct "Hcont" as "#C" | done ]. }
+ (* We remember the current back value. *)
+ iMod (back_snapshot with "Hb●") as "[Hb● Hback_snap]".
+ iMod (i2_lower_bound_snapshot with "Hi●") as "[Hi● Hi2_lower_bound]".
+ (* We close the invariant again. *)
+ iModIntro. iSplitR "AU Hback_snap Hi2_lower_bound".
+ { iNext. repeat iExists _. eauto with iFrame. }
+ clear pref rest slots deqs pvs.
+ (* The range is the min between [q.back - 1] and [q.size - 1]. *)
+ wp_bind (minimum _ _)%E.
+ wp_apply min_spec; [done | iIntros "_"]. wp_pures.
+ (* We now prove the inner loop part by induction in the index. *)
+ assert (back `min` sz ≤ back `min` sz)%nat as Hn by done.
+ assert (match cont with
+ | NoCont _ => True
+ | WithCont i1 _ => (back `min` sz - back `min` sz ≤ i1)%nat
+ end) as Hcont_i1 by (destruct cont as [i1 _|_]; lia).
+ revert Hn Hcont_i1. generalize (back `min` sz)%nat at 1 4 7 as n.
+ intros n Hn Hcont_i1.
+ iInduction n as [|n] "IH_loop" forall (Hn Hcont_i1).
+ (* The bas case is trivial. *)
+ { wp_lam. wp_pures. iApply "IH"; last done.
+ iExists _, _, _, _, _, _, _. iSplitR; done. }
+ (* Now the induction case: we need to open the invariant for the load. *)
+ wp_lam. wp_pures. wp_bind (! _)%E.
+ iInv "Inv" as (back' pvs pref rest cont' slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [>Hb● [Hi● [He● [Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[Hproph [Hbig [Hcont >Hpures]]]".
+ iDestruct "Hpures" as %(Hslots & Hstate & Hpref & Hdeqs & Hpvs_OK & Hcont).
+ destruct Hpvs_OK as (Hpvs_ND & Hpvs_sz).
+ (* We use our snapshot to show that back is smaller that back'. *)
+ iDestruct (back_le with "Hb● Hback_snap") as %Hback.
+ (* We define the loop index as [i]. *)
+ pose (i := ((back `min` sz) - S n)%nat).
+ assert ((back `min` sz)%nat - S n = i) as -> by by rewrite Nat2Z.inj_sub.
+ (* We can now load. *)
+ wp_apply (wp_load_offset _ _ ℓ_ar i _ (array_get slots deqs i) with "Hℓ_ar");
+ [ apply array_content_lookup; lia | iIntros "Hℓa" ].
+ (* If there was an initial contradiction, it is still here. *)
+ iAssert ⌜match cont with
+ | NoCont _ => True
+ | WithCont i1 i2 => cont' = cont ∧ (back `min` sz - S n ≤ i1)%nat
+ end⌝%I as %Hinitial_cont.
+ { destruct cont as [i1 i2|bs]; destruct cont' as [i1' i2'|bs']; try done.
+ - iDestruct (contra_agree with "Hinit_cont Hcont") as %[-> ->].
+ iPureIntro. split; first done.
+ destruct Hcont as (((H1 & H2) & H3) & _). lia.
+ - by iDestruct (contra_not_no_contra with "Hcont Hinit_cont") as "False". }
+ (* We then reason by cas on the physical contents of slot [i]. *)
+ destruct (decide (array_get slots deqs i = NONEV)) as [Hi_NULL|Hi_not_NULL].
+ { rewrite Hi_NULL. iModIntro.
+ iSplitR "AU Hback_snap Hi2_lower_bound".
+ { iNext. repeat iExists _. iFrame. iSplit; done. }
+ wp_pures. assert (S n - 1 = n%nat) as -> by lia.
+ iApply ("IH_loop" with "[] [] AU Hback_snap").
+ - iPureIntro. lia.
+ - iPureIntro. destruct cont as [i1 i2|bs]; last done.
+ destruct Hinitial_cont as [-> Hi1].
+ destruct Hcont as (HC1 & HC2 & HC3 & HC4 & HC5 & HC6).
+ apply le_lt_or_eq in Hcont_i1 as [H|H]; rewrite -/i in H; first by lia.
+ exfalso. subst i1.
+ assert (is_Some (slots !! i)) as [d Hslots_i] by (apply Hslots; lia).
+ destruct d as [[li si] wi]. rewrite /array_get Hslots_i /= in Hi_NULL.
+ rewrite /array_get Hslots_i in HC3. rewrite decide_False in Hi_NULL; last done.
+ inversion HC3; subst wi. by inversion Hi_NULL.
+ - by iFrame. }
+ (* We know that a non-null value [li] at index [i], we get a witness. *)
+ assert (is_Some (slots !! i)) as [[[li si] wi] Hslots_i].
+ { rewrite /array_get in Hi_not_NULL.
+ destruct (slots !! i) as [d|]; last done. by eexists. }
+ assert (array_get slots deqs i = SOMEV #li) as ->.
+ { rewrite /array_get Hslots_i /=. rewrite /array_get Hslots_i in Hi_not_NULL.
+ revert Hi_not_NULL. destruct (decide (i ∈ deqs)); intros H; first done.
+ by destruct wi. }
+ iMod (val_wit_from_auth γs i li with "Hs●")
+ as "[Hs● #Hval_wit_i]"; first by rewrite Hslots_i.
+ (* Close the invariant and clean up the context. *)
+ iModIntro. iSplitR "AU Hback_snap Hi2_lower_bound".
+ { iNext. repeat iExists _. iFrame. iSplit; done. }
+ clear Hslots Hstate Hpref Hdeqs Hcont Hinitial_cont Hback back' Hpvs_ND.
+ clear Hpvs_sz pvs pref rest cont' Hslots_i si wi Hi_not_NULL slots deqs.
+ (* Finally, the interesting where the cell was non-NULL on the load. *)
+ wp_pures. wp_bind (Resolve _ _ _)%E.
+ iInv "Inv" as (back' pvs pref rest cont' slots deqs) "HInv".
+ iDestruct "HInv" as "[Hℓ_back [Hℓ_ar [>Hb● [>Hi● [He● [>Hs● HInv]]]]]]".
+ iDestruct "HInv" as "[>Hproph [Hbig [>Hcont >Hpures]]]".
+ iDestruct "Hpures" as %(Hslots & Hstate & Hpref & Hdeqs & Hpvs_OK & Hcont).
+ destruct Hpvs_OK as (Hpvs_ND & Hpvs_sz).
+ (* If there was an initial contradiction, it is still here. *)
+ iAssert ⌜match cont with
+ | NoCont _ => True
+ | WithCont i1 i2 => cont' = cont ∧ (back `min` sz - S n ≤ i1)%nat
+ end⌝%I as %Hinitial_cont.
+ { destruct cont as [i1 i2|bs]; destruct cont' as [i1' i2'|bs']; try done.
+ - iDestruct (contra_agree with "Hinit_cont Hcont") as %[-> ->].
+ iPureIntro. split; first done. destruct Hcont as (((H1 & H2) & H3) & _). done.
+ - by iDestruct (contra_not_no_contra with "Hcont Hinit_cont") as "False". }
+ SearchAbout "snap".
+ (* We resolve. *)
+ iDestruct "Hproph" as (rs) "[Hp Hpvs]". iDestruct "Hpvs" as %Hpvs.
+ wp_apply (wp_resolve with "Hp"); first done.
+ (* We reason by case on the success of the CAS. *)
+ iDestruct (array_contents_cases γs slots deqs with "Hs● Hval_wit_i") as %[Hi|Hi].
+ * (* The CmpXchg succeeded. *) iClear "IH_loop IH".
+ assert (array_content sz slots deqs !! i = Some (SOMEV #li)).
+ { rewrite array_content_lookup; last by lia. by rewrite Hi. }
+ wp_apply (wp_cmpxchg_suc_offset with "Hℓ_ar");
+ [ done | done | by right | iIntros "Hℓ_ar" (rs' ->) "Hp" ].
+ (* Note that [i] is used (otherwise the CmpXchg would have failed). *)
+ iDestruct (use_val_wit with "Hs● Hval_wit_i") as %Hval_wit_i.
+ iDestruct (back_le with "Hi● Hi2_lower_bound") as %Hi2.
+ assert (is_Some (slots !! i)) as [[[dl ds] dw] Hslots_i].
+ { destruct (slots !! i) as [d|]; [ by exists d | by inversion Hval_wit_i ]. }
+ assert (dl = li) as Hdl_li; last subst dl.
+ { rewrite Hslots_i in Hval_wit_i. by inversion Hval_wit_i. }
+ (* We now reason by case on whether the enqueue at [i] was committed. *)
+ destruct (was_committed (li, ds, dw)) eqn:Hcommitted.
+ { (* We first consider the case where it was committed. *)
+ (* If [i] has been dequeued alread: contradiction. *)
+ assert (i ∉ deqs) as Hi_not_deq.
+ { intros Hi_deq. specialize (Hdeqs i Hi_deq) as (H1 & H2 & H3).
+ rewrite Hslots_i /= in H1. inversion H1; subst dw.
+ rewrite /array_get Hslots_i in Hi. rewrite decide_True in Hi; last done.
+ inversion Hi. }
+ (* We clean up the prophecy. *)
+ rewrite /= decide_True in Hpvs; last lia. rewrite Nat2Z.id in Hpvs.
+ rewrite decide_False in Hpvs; last done.
+ (* We then show that the commit prefix cannot be empty. *)
+ destruct pref as [|i' new_pref].
+ { exfalso. destruct cont as [i1 i2|_].
+ - destruct Hinitial_cont as [-> Hi1].
+ destruct Hcont as (((HC1 & HC2) & HC3) & HC4 & HC5 & HC6 & HC7 & HC8).
+ rewrite Hpvs /= in HC8. destruct HC8 as [junk HEq].
+ inversion HEq as [[HEq1 HEq2]]. lia.
+ - destruct cont' as [i1' i2'|bs].
+ + destruct Hcont as (((HC1 & HC2) & HC3) & HC4 & HC5 & HC6 & HC7 & HC8).
+ rewrite Hpvs /= in HC8. destruct HC8 as [junk HEq].
+ inversion HEq as [[HEq1 HEq2]].
+ assert (back < i2')%nat; last by lia. lia.
+ + destruct Hcont as (HC1 & HC2 & HC3). rewrite Hpvs /= in HC3.
+ destruct bs as [|[b_u b_ps] bs]; first by inversion HC3.
+ simpl in HC3. inversion HC3 as [[HEq1 HEq2]].
+ assert (block_valid slots (b_u, b_ps))
+ as [Hvalid _] by apply HC1, elem_of_list_here.
+ rewrite /= -HEq1 Hslots_i in Hvalid. inversion Hvalid. }
+ assert (i' = i) as ->.
+ { destruct cont' as [i1' i2'|bs].
+ - destruct Hcont as (_ & _ & _ & _ & _ & HC).
+ rewrite Hpvs in HC. destruct HC as [junk HC]. by inversion HC.
+ - destruct Hcont as (_ & _ & HC).
+ rewrite Hpvs in HC. by inversion HC. }
+ (* We commit. *)
+ pose (new_elts := map (get_value slots ({[i]} ∪ deqs)) new_pref ++ rest).
+ pose (new_pvs := proph_data sz ({[i]} ∪ deqs) rs').
+ iMod "AU" as (elts_AU) "[He◯ [_ Hclose]]".
+ iDestruct (sync_elts with "He● He◯") as %<-.
+ iMod (update_elts _ _ _ new_elts with "He● He◯") as "[He● He◯]".
+ iMod ("Hclose" $! li new_elts with "[$He◯]") as "HΦ".
+ { iPureIntro. rewrite /new_elts /=. by rewrite /get_value Hslots_i. }
+ iModIntro. iSplitR "HΦ Hback_snap".
+ { pose (new_deqs := {[i]} ∪ deqs).
+ iNext. iExists back', new_pvs, new_pref, rest, cont', slots, new_deqs.
+ subst new_deqs. iFrame. iSplitL "Hℓ_ar".
+ { rewrite array_content_dequeue; [ done | by lia | done ]. }
+ iSplitL "Hp".
+ { iExists rs'. by iFrame "Hp". }
+ iPureIntro. repeat split_and; try done.
+ - intros k. split; intros Hk; first by apply Hstate.
+ intros Hk_in_deqs. apply elem_of_union in Hk_in_deqs.
+ destruct Hk_in_deqs as [Hk_is_i|Hk_in_deqs].
+ + apply elem_of_singleton in Hk_is_i. subst k.
+ rewrite /array_get Hslots_i decide_False in Hi; last done.
+ rewrite /physical_value in Hi. rewrite Hslots_i in Hk.
+ inversion Hk; subst dw. inversion Hi.
+ + apply Hdeqs in Hk_in_deqs as (HContra & _).
+ rewrite HContra in Hk. inversion Hk.
+ - intros k Hk.
+ assert (k ∈ i :: new_pref) as HH%Hpref by set_solver +Hk.
+ destruct HH as (H1 & H2 & H3). repeat split; try done.
+ apply not_elem_of_union. split; last done.
+ apply not_elem_of_singleton. intros ->.
+ destruct cont' as [i1' i2'|bs].
+ + destruct Hcont as (HC1 & HC2 & HC3 & HC4 & HC5 & [junk HC6]).
+ rewrite HC6 in Hpvs_ND.
+ apply NoDup_app in Hpvs_ND as (HND & _ & _).
+ apply NoDup_app in HND as (HND & _ & _).
+ apply NoDup_app in HND as (HND & _ & _).
+ apply NoDup_cons in HND as (HND & _). apply HND, Hk.
+ + destruct Hcont as (HC1 & HC2 & HC3). rewrite HC3 in Hpvs_ND.
+ apply NoDup_app in Hpvs_ND as (HND & _ & _).
+ apply NoDup_app in HND as (HND & _ & _).
+ apply NoDup_cons in HND as (HND & _). apply HND, Hk.
+ - intros k Hk. apply elem_of_union in Hk as [Hk%elem_of_singleton|Hk].
+ + subst k. rewrite Hslots_i /=.
+ assert (dw = true) as ->.
+ { rewrite /array_get Hslots_i decide_False in Hi; last done.
+ rewrite /physical_value in Hi. destruct dw; first done. by inversion Hi. }
+ repeat split_and; [ done | by f_equal | .. ].
+ rewrite /array_get Hslots_i decide_True; [ done | by set_solver ].
+ + destruct (Hdeqs k Hk) as (H1 & H2 & H3). repeat split_and; try done.
+ rewrite /array_get. destruct (slots !! k) as [[[lk sk] wk]|]; last done.
+ rewrite decide_True; first done. by set_solver +Hk.
+ - by apply proph_data_NoDup.
+ - intros k Hk. by eapply (proph_data_sz sz _ _ _ Hk).
+ - destruct cont' as [i1' i2'|bs].
+ + destruct Hcont as (((HC1 & HC2) & HC3) & HC4 & HC5 & HC6 & HC7 & HC8).
+ assert (i1' ≠ i) as Hi1'_not_i.
+ { intros ->. assert (i ∈ i :: new_pref) as Hpref_i%Hpref by set_solver.
+ by destruct Hpref_i as (_ & _ & Hpref_i). }
+ repeat split_and; try done.
+ * apply not_elem_of_union. split; last done. by apply not_elem_of_singleton.
+ * rewrite /array_get. destruct (slots !! i1') as [di1'|]; last by inversion HC2.
+ destruct di1' as [[li1' si1'] wi1']. rewrite decide_False; last by set_solver.
+ inversion HC5; subst wi1'. done.
+ * rewrite Hpvs /= in HC8. rewrite /new_pvs. by eapply prefix_cons_inv_2.
+ + destruct Hcont as (HC1 & HC2 & HC3).
+ repeat split_and; try done. rewrite Hpvs /= in HC3. by inversion HC3. }
+ wp_pures. done. }
+ (* If the enqueue at index [i] was not committed: contradiction. *)
+ exfalso.
+ assert (was_committed <$> slots !! i = Some false) as Hcom_i.
+ { rewrite Hslots_i. simpl. by f_equal. }
+ apply Hstate in Hcom_i. rewrite Hslots_i in Hcom_i.
+ inversion Hcom_i; subst dw. rewrite /array_get Hslots_i /= in Hi.
+ destruct (decide (i ∈ deqs)); by inversion Hi.
+ * (* The CmpXchg failed, we continue looping. *)
+ assert (array_content sz slots deqs !! i = Some NONEV).
+ { rewrite array_content_lookup; last by lia. by rewrite Hi. }
+ wp_apply (wp_cmpxchg_fail_offset _ _ _ _ _ (array_get slots deqs i) with "Hℓ_ar");
+ [ by rewrite Hi | by rewrite Hi | by right | iIntros "Hℓa" (rs' ->) "Hp"].
+ (* We can close the invariant. *)
+ iModIntro. iSplitR "AU Hback_snap Hi2_lower_bound".
+ { iNext. iExists _, _, _, _, cont', _, _. iFrame. iSplit; last done.
+ iExists rs'. rewrite Hpvs /= decide_True; last by lia. by iFrame. }
+ (* And conclude using the loop induction hypothesis. *)
+ wp_pures. assert (S n - 1 = n%nat) as -> by lia. iClear "Hval_wit_i".
+ iApply ("IH_loop" with "[] [] AU Hback_snap").
+ - iPureIntro. lia.
+ - iPureIntro. destruct cont as [i1 i2|bs]; last done.
+ apply le_lt_or_eq in Hcont_i1. destruct Hcont_i1 as [Hi1|Hi1]; first lia.
+ exfalso. destruct Hinitial_cont as [-> Hinitial_cont].
+ destruct Hcont as (HC1 & HC2 & HC3 & HC4 & HC5 & HC6 & HC7).
+ assert (is_Some (slots !! i1)) as Hslots_i1. { apply Hslots. lia. }
+ destruct Hslots_i1 as [[[li1 si1] wi1] Hslots_i1].
+ rewrite /array_get Hslots_i1 decide_False in HC5; last done.
+ simpl in HC5. destruct wi1; last done. clear HC5.
+ rewrite array_content_lookup in H; last by lia.
+ rewrite /array_get in H. subst i i1. rewrite Hslots_i1 in H.
+ rewrite decide_False in H; last done. inversion H.
+ - by iFrame.
+Qed.
+
+End herlihy_wing_queue.
+
+(** * Instantiation of the specification ***********************************)
+
+Definition atomic_cinc `{!heapG Σ, !savedPropG Σ, !hwqG Σ} :
+ spec.atomic_hwq Σ :=
+ {| spec.new_queue_spec := new_queue_spec;
+ spec.enqueue_spec := enqueue_spec;
+ spec.dequeue_spec := dequeue_spec;
+ spec.hwq_content_exclusive := hwq_cont_exclusive |}.
+
+Typeclasses Opaque hwq_content is_hwq.
diff --git a/theories/logatom/herlihy_wing_queue/spec.v b/theories/logatom/herlihy_wing_queue/spec.v
new file mode 100644
index 0000000..3145fe8
--- /dev/null
+++ b/theories/logatom/herlihy_wing_queue/spec.v
@@ -0,0 +1,42 @@
+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+Set Default Proof Using "Type".
+
+(** A general logically atomic interface for Herlihy-Wing queues. *)
+Record atomic_hwq {Σ} `{!heapG Σ} := AtomicHWQ {
+ (* -- operations -- *)
+ new_queue : val;
+ enqueue : val;
+ dequeue : val;
+ (* -- other data -- *)
+ name : Type;
+ name_eqdec : EqDecision name;
+ name_countable : Countable name;
+ (* -- predicates -- *)
+ is_hwq (N : namespace) (sz : nat) (γ : name) (v : val) : iProp Σ;
+ hwq_content (γ : name) (ls : list loc) : iProp Σ;
+ (* -- predicate properties -- *)
+ is_hwq_persistent N sz γ v : Persistent (is_hwq N sz γ v);
+ hwq_content_timeless γ ls : Timeless (hwq_content γ ls);
+ hwq_content_exclusive γ ls1 ls2 :
+ hwq_content γ ls1 -∗ hwq_content γ ls2 -∗ False;
+ (* -- operation specs -- *)
+ new_queue_spec N (sz : nat) :
+ 0 < sz →
+ {{{ True }}}
+ new_queue #sz
+ {{{ v γ, RET v; is_hwq N sz γ v ∗ hwq_content γ [] }}};
+ enqueue_spec N (sz : nat) (γ : name) (q : val) (l : loc) :
+ is_hwq N sz γ q -∗
+ <<< ∀ (ls : list loc), hwq_content γ ls >>>
+ enqueue q #l @ ⊤ ∖ ↑N
+ <<< hwq_content γ (ls ++ [l]), RET #() >>>;
+ dequeue_spec N (sz : nat) (γ : name) (q : val) :
+ is_hwq N sz γ q -∗
+ <<< ∀ (ls : list loc), hwq_content γ ls >>>
+ dequeue q @ ⊤ ∖ ↑N
+ <<< ∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_content γ ls', RET #l >>>;
+}.
+Arguments atomic_hwq _ {_}.
+
+Existing Instances is_hwq_persistent hwq_content_timeless.
--
GitLab