diff --git a/_CoqProject b/_CoqProject
index e1480b9266a8c4e48cf29d03bb5ab864962493bc..d2d1ae3b8afc100b271d11c425b4300b0291878c 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 0000000000000000000000000000000000000000..428c7b4a6cc611dba3237c85746e28f30c8598ed
--- /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 0000000000000000000000000000000000000000..3145fe85844851a73fae074decf73ab4c6a62bcb
--- /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.