diff --git a/_CoqProject b/_CoqProject
index b4749740542cd68c1cf71c14c2df947590c0e760..2f2296ecfbec8a1a36c4da856df837076ad21649 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,6 +10,7 @@ theories/prelude/properness.v
 theories/prelude/asubst.v
 theories/prelude/bijections.v
 theories/prelude/lang_facts.v
+theories/prelude/arith.v
 
 theories/logic/spec_ra.v
 theories/logic/spec_rules.v
@@ -53,6 +54,15 @@ theories/examples/stack/refinement.v
 theories/examples/various.v
 theories/examples/lateearlychoice.v
 theories/examples/coinflip.v
+theories/examples/red_blue_flag.v
+
+theories/examples/folly_queue/set.v
+theories/examples/folly_queue/CG_queue.v
+theories/examples/folly_queue/turnSequencer.v
+theories/examples/folly_queue/singleElementQueue.v
+theories/examples/folly_queue/mpmcqueue.v
+theories/examples/folly_queue/refinement.v
+theories/examples/folly_queue/ticketLock.v
 
 theories/examples/par.v
 theories/experimental/cka.v
diff --git a/theories/examples/folly_queue/CG_queue.v b/theories/examples/folly_queue/CG_queue.v
new file mode 100644
index 0000000000000000000000000000000000000000..4df3f84728117f2e262754c46639d9dc13a30998
--- /dev/null
+++ b/theories/examples/folly_queue/CG_queue.v
@@ -0,0 +1,120 @@
+From reloc Require Import reloc lib.lock lib.list.
+
+(* The course-grained queue is implemented as a linked list guarded by a
+   lock. *)
+
+Definition CG_dequeue_go : val := λ: "head",
+  match: !"head" with
+    NONE => #() #() (* Stuck. *)
+  | SOME "p" => "head" <- (Snd "p");; Fst "p"
+  end.
+
+Definition CG_dequeue : val := λ: "lock" "head" <>,
+  acquire "lock" ;;
+  let: "v" := CG_dequeue_go "head" in
+  release "lock" ;;
+  "v".
+
+Definition CG_enqueue_go : val := rec: "enqueue" "x" "head" :=
+  match: "head" with
+    NONE => CONS "x" NIL
+  | SOME "p" => CONS (Fst "p") ("enqueue" "x" (Snd "p"))
+  end.
+
+Definition CG_enqueue : val := λ: "lock" "head" "x",
+  acquire "lock" ;;
+  "head" <- CG_enqueue_go "x" (! "head") ;;
+  release "lock".
+
+Definition CG_queue : val := Λ:
+  let: "head" := ref NIL in
+  let: "lock" := newlock #() in
+  ((λ: "x", CG_enqueue "lock" "head" "x"),
+   (λ: "x", CG_dequeue "lock" "head" "x")).
+
+Section CG_queue.
+  Context `{relocG Σ}.
+
+  (* Representation predicate for the course grained queue. *)
+  Fixpoint isCGQueue_go (xs : list val) : val :=
+    match xs with
+    | nil => NILV
+    | x :: xs' => (CONSV x (isCGQueue_go xs'))
+    end.
+
+  Definition cgQueueInv (ℓ : loc) lk (xs : list val) : iProp Σ :=
+    ℓ ↦ₛ (isCGQueue_go xs) ∗ is_locked_r lk false.
+
+  Lemma refines_CG_enqueue_body_r E t (K : Datatypes.list (ectxi_language.ectx_item heap_ectxi_lang)) A x xs :
+    nclose relocN ⊆ E →
+    (REL t << fill K (isCGQueue_go (xs ++ [x])) @ E : A) -∗
+    (REL t << fill K (CG_enqueue_go x (isCGQueue_go xs)) @ E : A).
+  Proof.
+    iIntros (HNE) "H".
+    iInduction xs as [|x' xs'] "IH" forall (K). simpl.
+    - rel_rec_r. rel_pures_r. rel_pures_r.
+      iApply "H".
+    - simpl.
+      rel_rec_r. rel_pures_r. rel_pures_r. rel_apply_r ("IH").
+      rel_pures_r. done.
+  Qed.
+
+  Lemma refines_CG_enqueue_r list lk E t A x xs :
+    nclose relocN ⊆ E →
+    cgQueueInv list lk xs -∗
+    (cgQueueInv list lk (xs ++ [x]) -∗ REL t << #() @ E : A) -∗
+    REL t << (CG_enqueue lk #list x) @ E : A.
+  Proof.
+    iIntros (HNE) "[pts lofal] H".
+    rewrite /CG_enqueue.
+    rel_pures_r.
+    rel_apply_r (refines_acquire_r with "lofal"). iIntros "lotru".
+    rel_pures_r.
+    rel_load_r.
+    rel_apply_r (refines_CG_enqueue_body_r).
+    rel_pures_r.
+    rel_store_r.
+    rel_pures_r.
+    rel_apply_r (refines_release_r with "lotru"). iIntros "lofal".
+    iApply "H".
+    iFrame.
+  Qed.
+
+  Lemma refines_right_CG_dequeue E k lk list x xs :
+    nclose relocN ⊆ E →
+    cgQueueInv list lk (x :: xs) -∗
+    refines_right k (CG_dequeue lk #list #()) ={E}=∗
+    cgQueueInv list lk (xs) ∗ refines_right k (of_val x).
+  Proof.
+    iIntros (HNE) "[pts lofal] H". simpl.
+    rewrite /CG_dequeue /CG_dequeue_go /is_locked_r.
+    iDestruct "lofal" as (â„“k ->)  "Hlk".
+    tp_pures k.
+    tp_rec k.
+    tp_cmpxchg_suc k.
+    tp_pures k.
+    tp_load k.
+    tp_pures k.
+    tp_store k.
+    tp_pures k.
+    tp_rec k.
+    tp_store k.
+    tp_pures k.
+    iModIntro. iFrame "H". rewrite /cgQueueInv. iFrame "pts".
+    iExists _. by iFrame.
+  Qed.
+
+  Lemma refines_CG_dequeue_cons_r E t A lk list x xs :
+    nclose relocN ⊆ E →
+    cgQueueInv list lk (x :: xs) -∗
+    (cgQueueInv list lk xs -∗ REL t << x @ E : A) -∗
+    REL t << (CG_dequeue lk #list #()) @ E : A.
+  Proof.
+    iIntros (HNE) "H1 H2".
+    iApply refines_split. iIntros (k) "Hk".
+    iMod (refines_right_CG_dequeue with "H1 Hk") as "[H1 Hk]"; first done.
+    iSpecialize ("H2" with "H1").
+    iApply (refines_combine with "H2 Hk").
+  Qed.
+
+End CG_queue.
diff --git a/theories/examples/folly_queue/README.md b/theories/examples/folly_queue/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..1b315f70a2cb38bfae3e013bebedbcc9c86f188a
--- /dev/null
+++ b/theories/examples/folly_queue/README.md
@@ -0,0 +1,5 @@
+# MPMC queue from the Folly library
+
+In this case study we prove linearizability of the MPMC queue algorithm from the Folly library:
+
+- https://github.com/facebook/folly/blob/master/folly/MPMCQueue.h
diff --git a/theories/examples/folly_queue/mpmcqueue.v b/theories/examples/folly_queue/mpmcqueue.v
new file mode 100644
index 0000000000000000000000000000000000000000..3fcdb53738c94510a968727f6347b8f8bee790e2
--- /dev/null
+++ b/theories/examples/folly_queue/mpmcqueue.v
@@ -0,0 +1,27 @@
+From iris.heap_lang.lib Require Export array.
+From reloc Require Export reloc.
+From reloc.examples.folly_queue Require Export singleElementQueue.
+
+Definition enqueue : val := λ: "slots" "cap" "ticket_" "v",
+  let: "ticket" := FAA "ticket_" #1 in
+  let: "turn" := "ticket" `quot` "cap" in
+  let: "idx" := "ticket" `rem` "cap" in
+  enqueueWithTicket (!("slots" +â‚— "idx")) "turn" "v".
+
+Definition dequeue : val := λ: "slots" "cap" "ticket_",
+  let: "ticket" := FAA "ticket_" #1 in
+  let: "turn" := "ticket" `quot` "cap" in
+  let: "idx" := "ticket" `rem` "cap" in
+  dequeueWithTicket (!("slots" +â‚— "idx")) "turn".
+
+Definition newSQueue : val := λ: <>,
+  let: "r" := ref NONE in
+  let: "t" := newTS #() in
+  ("t", "r").
+
+Definition newQueue : val := λ: "q", Λ:
+  let: "slots" := array_init "q" newSQueue in
+  let: "pushTicket" := ref #0 in
+  let: "popTicket"  := ref #0 in
+  (λ: "v", enqueue "slots" "q" "pushTicket" "v",
+   λ: <>, dequeue "slots" "q" "popTicket").
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
new file mode 100644
index 0000000000000000000000000000000000000000..e083cf80ed2c0a6f1c6ea9faa0186befb9cddc4b
--- /dev/null
+++ b/theories/examples/folly_queue/refinement.v
@@ -0,0 +1,1029 @@
+From reloc Require Import reloc lib.lock.
+From iris.algebra Require Import numbers csum excl auth list gmap gset.
+From iris.bi.lib Require Export fixpoint.
+
+From reloc.examples.folly_queue Require Import
+    set turnSequencer singleElementQueue CG_queue mpmcqueue.
+
+Definition queueN : namespace := nroot .@ "queue".
+
+(* Setup the cameras. *)
+
+(* We use a finite map from nats to represent a list. *)
+Definition listUR := authUR (gmapUR nat (agreeR valO)).
+
+(* LP stepping requests. *)
+Definition requestReg := gmap nat ref_id.
+Definition requestRegR := authR $ gmapUR nat (agreeR ref_idO).
+
+Class queueG Σ := {
+  queue_listUR :> inG Σ listUR;
+  queue_requestUR :> inG Σ requestRegR;
+}.
+
+(* For the [lia] tactic. *)
+(* To support Z.div, Z.modulo, Z.quot, and Z.rem: *)
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+
+(* Begin hooks to make `lia` work with Nat.modulo and Nat.div *)
+Require Import Arith ZArith ZifyClasses ZifyInst Lia.
+
+Program Instance Op_Nat_mod : BinOp Nat.modulo :=
+  {| TBOp := Z.modulo ; TBOpInj := Nat2Z_inj_mod |}.
+Add Zify BinOp Op_Nat_mod.
+
+Program Instance Op_Nat_div : BinOp Nat.div :=
+  {| TBOp := Z.div ; TBOpInj := Nat2Z_inj_div |}.
+Add Zify BinOp Op_Nat_div.
+
+(* lia now works with Nat.modulo nad Nat.div. *)
+
+Section queue_refinement.
+  Context `{!relocG Σ, !TSG Σ, !queueG Σ}.
+
+  (* A few lemmas and definitions related to the ghost list.
+
+     The ghost list keeps track of _all_ elements that have been enqueued in the
+     queue. Including those that are no longer in the queue (they have been
+     dequeued). *)
+
+  Lemma list_to_map_snoc {B : Type} l i x :
+    i ∉ l.*1 →
+    list_to_map (l ++ [(i, x)]) = <[i:=x]> (list_to_map l : gmap nat B).
+  Proof.
+    intros Hnd.
+    induction l as [|[i' x'] l' IH].
+    - done.
+    - apply not_elem_of_cons in Hnd.
+      simpl in *. rewrite IH. 2: { apply Hnd. }
+      rewrite insert_commute; first done.
+      rewrite comm.
+      apply Hnd.
+  Qed.
+
+  Definition list_idx_to_map {A : Type} (l : list A) : gmap nat A :=
+    list_to_map (zip (seq 0 (length l)) l).
+
+  Lemma list_idx_to_map_append {B : Type} xs (x : B) :
+    list_idx_to_map (xs ++ [x]) = <[length xs := x]>(list_idx_to_map xs).
+  Proof.
+    rewrite /list_idx_to_map.
+    rewrite app_length /= Nat.add_1_r.
+    rewrite seq_S /=.
+    rewrite zip_with_app /=.
+    2: { by rewrite seq_length. }
+    rewrite list_to_map_snoc; first done.
+    rewrite fst_zip. 2: { rewrite seq_length. done. }
+    intros [i Hl]%elem_of_list_lookup_1.
+    apply lookup_seq in Hl as Hlm.
+    simpl in Hlm.
+    destruct Hlm as [-> Hlm].
+    lia.
+  Qed.
+
+  Definition make_map (m : gmap nat val) : gmapUR nat (agreeR valO) :=
+    to_agree <$> m.
+
+  Lemma dom_make_map (m : gmap nat val) : dom (gset nat) (make_map m) = dom _ m.
+  Proof.
+    rewrite /make_map. rewrite dom_fmap_L. done.
+  Qed.
+
+  Lemma make_map_empty : make_map ∅ = ∅.
+  Proof. rewrite /make_map. apply: fmap_empty. Qed.
+
+  Definition ghost_list γl (xs : list val) := own γl (● make_map (list_idx_to_map xs)).
+
+  Definition ghost_list_mapsto γl i (x : val) := own γl (◯ {[i := to_agree x]}).
+
+  Lemma ghost_list_alloc : ⊢ |==> ∃ γl, ghost_list γl [].
+    iMod (own_alloc (● ∅ : listUR)) as (γl) "Hauth"; first by apply auth_auth_valid.
+    rewrite /ghost_list. rewrite make_map_empty.
+    iModIntro. iExists _. done.
+  Qed.
+
+  Lemma ghost_list_append γl xs (x : val) :
+    ghost_list γl xs ==∗ ghost_list γl (xs ++ [x]) ∗ ghost_list_mapsto γl (length xs) x.
+  Proof.
+    iIntros "HL".
+    rewrite /ghost_list /ghost_list_mapsto.
+    rewrite -(own_op γl).
+    iApply (own_update with "HL").
+    apply auth_update_alloc.
+    rewrite list_idx_to_map_append.
+    rewrite /make_map fmap_insert.
+    apply alloc_singleton_local_update; last done.
+    rewrite /list_idx_to_map.
+    rewrite lookup_fmap.
+    rewrite not_elem_of_list_to_map_1; first done.
+    rewrite fst_zip. 2: { rewrite seq_length. done. }
+    rewrite elem_of_list_In.
+    rewrite in_seq. lia.
+  Qed.
+
+  Lemma dom_list_to_map {B : Type} (l : list (nat * B)) :
+    dom (gset nat) (list_to_map l : gmap nat B) = list_to_set l.*1.
+  Proof.
+    induction l as [|?? IH].
+    - rewrite dom_empty_L. done.
+    - rewrite dom_insert_L. rewrite IH. done.
+  Qed.
+
+  Lemma ghost_list_le γl xs i x :
+    ghost_list γl xs -∗ ghost_list_mapsto γl i x -∗ ⌜i < length xs⌝.
+  Proof.
+    rewrite /ghost_list /ghost_list_mapsto /list_idx_to_map.
+    iIntros "Ha Hb".
+    iDestruct (own_valid_2 with "Ha Hb") as %[Hincl _]%auth_both_valid_discrete.
+    apply dom_included in Hincl.
+    rewrite dom_singleton_L in Hincl.
+    rewrite dom_make_map in Hincl.
+    rewrite dom_list_to_map in Hincl.
+    rewrite fst_zip in Hincl. 2: { rewrite seq_length. done. }
+    rewrite list_to_set_seq in Hincl.
+    iPureIntro. set_solver.
+  Qed.
+
+  Lemma ghost_list_lookup (γl : gname) xs (i : nat) (x : val) :
+    xs !! i = Some x →
+    ghost_list γl xs ==∗ ghost_list γl xs ∗ ghost_list_mapsto γl i x.
+  Proof.
+    iIntros (Hs) "Hlist".
+    rewrite /ghost_list /ghost_list_mapsto /list_idx_to_map.
+    rewrite -own_op.
+    iApply (own_update with "Hlist").
+    apply: auth_update_dfrac_alloc.
+    apply singleton_included_l.
+    exists (to_agree x).
+    split; last done.
+    rewrite lookup_fmap.
+    erewrite elem_of_list_to_map_1.
+    - simpl. reflexivity.
+    - rewrite fst_zip. 2: { rewrite seq_length. done. }
+      apply NoDup_seq.
+    - apply elem_of_lookup_zip_with.
+      exists i, i, x.
+      apply lookup_lt_Some in Hs as Lt.
+      repeat split; last done.
+      apply lookup_seq.
+      lia.
+  Qed.
+
+  Lemma map_list_snoc γl xs pushTicket popTicket (xn : val) :
+    popTicket ≤ pushTicket →
+    length xs = pushTicket - popTicket →
+    own γl (◯ {[pushTicket := to_agree xn ]}) -∗
+    ([∗ list] i↦x ∈ xs, own γl (◯ {[popTicket + i := to_agree x]})) -∗
+    [∗ list] i↦x ∈ xs ++ [xn], own γl (◯ {[popTicket + i := to_agree x]}).
+  Proof.
+    iIntros (Hle Hlen) "Hf Hl".
+    rewrite big_sepL_app.
+    iFrame.
+    simpl.
+    replace (popTicket + (length xs + 0)) with (pushTicket) by lia.
+    iFrame.
+  Qed.
+
+  (* Fragments of the list agree. *)
+  Lemma map_list_agree γl i (x x' : val) :
+    own γl (◯ {[i := to_agree x]}) -∗
+    own γl (◯ {[i := to_agree x']}) -∗
+    ⌜x = x'⌝.
+  Proof.
+    iIntros "A B". iCombine "A B" as "A".
+    by iDestruct (own_valid with "A")
+      as %Hv%auth_frag_valid%singleton_valid%to_agree_op_inv_L.
+    (* by iDestruct (own_valid with "A")
+      as %Hv%auth_frag_valid_1%singleton_valid%to_agree_op_inv_L. *)
+  Qed.
+
+  Lemma decide_agree γl i (id id' : ref_id) :
+    own γl (◯ {[i := to_agree (id : ref_idO)]}) -∗
+    own γl (◯ {[i := to_agree (id' : ref_idO)]}) -∗
+    ⌜id = id'⌝.
+  Proof.
+    iIntros "A B". iCombine "A B" as "A".
+    by iDestruct (own_valid with "A")
+      as %HI%auth_frag_valid%singleton_valid%to_agree_op_inv_L.
+  Qed.
+
+  Lemma map_list_elem_of γl m (pushTicket popTicket : nat) (v : val) :
+    dom (gset nat) m = set_seq 0 pushTicket →
+    own γl (● make_map m) -∗
+    own γl (◯ {[popTicket := to_agree v]}) -∗
+    ⌜popTicket ∈ set_seq (C:=gset nat) 0 pushTicket⌝.
+  Proof.
+    iIntros (Hsub) "Ha Hf".
+    iDestruct (own_valid_2 with "Ha Hf") as %[H%dom_included _]%auth_both_valid_discrete.
+    rewrite dom_make_map in H.
+    rewrite Hsub in H.
+    rewrite dom_singleton_L in H.
+    iPureIntro. set_solver.
+  Qed.
+
+  (* A few lemmas related to the tokens. *)
+
+  Definition tokens_from γt n := own γt (set_above n).
+  Definition token γt (n : nat) := own γt (set_singleton n).
+  Lemma tokens_take γ m : tokens_from γ m -∗ tokens_from γ (m + 1) ∗ token γ m.
+  Proof. rewrite /tokens_from /token -own_op comm -take_first. done. Qed.
+
+  (* A single element queue contains: TS, location, gname for ghost state. *)
+  Record seq : Type := MkSeq {
+    seq_gname : gname;
+    seq_val : val;
+  }.
+
+  (* Definition seq_to_val (s : seq) := PairV #s.(seq_ts) #s.(seq_loc). *)
+
+  (* The resource that the i'th SEQ protects in a queue of capacity q.
+     Note, j is the the index of the enqueue/dequeue operation we're
+     at at the SEQ (a local index). From this we have to "count
+     backwards" to compute the index of the enqueue/dequeue operation
+     we're at at the queue in total (global index n). *)
+  Definition R γl q i (j : nat) (v : val) : iProp Σ :=
+    let n := j * q + i
+    in ghost_list_mapsto γl n v.
+
+  (* Turn management. *)
+
+  (* Given the total number of push or pop operations that has been carried out,
+  ops, returns the number of operations that has affected the i'th SEQ/TS. *)
+  Definition nr_of_affecting_ops (q i ops : nat) :=
+    (ops / q) + (if i <? ops `mod` q then 1 else 0).
+
+  (* Helper lemmas *)
+  Lemma mod_S_le a b :
+    0 < b →
+    (a + 1) `mod` b ≤ a `mod` b →
+    (a + 1) `mod` b = 0 ∧ a `mod` b = b - 1.
+  Proof.
+    intros Hob Hab.
+    assert (Z.of_nat a = (b * (a `div` b)%Z + (a `mod` b)%Z)%Z)%Z as Ha.
+    { lia. }
+    destruct (decide ((a `mod` b) < b - 1)) as [Hb|Hb].
+    - exfalso.
+      cut ((a + 1) `mod` b = a `mod` b + 1)%Z; first lia.
+      symmetry. eapply (Zmod_unique _ _ (a `div` b)); lia.
+    - assert (a `mod` b = b - 1)%Z as Hamodb by lia.
+      split; last lia.
+      cut (0 = (a + 1) `mod` b)%Z; first by lia.
+      eapply (Zmod_unique _ _ (a `div` b + 1)). lia.
+      rewrite {1}Ha Hamodb. lia.
+  Qed.
+
+  Lemma mod_S_gt a b :
+    0 < b →
+    (a + 1) `mod` b > a `mod` b →
+    (a + 1) `mod` b = a `mod` b + 1.
+  Proof.
+    intros Hob Hab.
+    assert (Z.of_nat a = (b * (a `div` b)%Z + (a `mod` b)%Z)%Z)%Z as Ha.
+    { lia. }
+    cut (a `mod` b + 1 = (a + 1) `mod` b)%Z; first lia.
+    destruct (decide ((a `mod` b) < b - 1)) as [Hb|Hb].
+    - eapply (Zmod_unique _ _ (a `div` b)). lia.
+      rewrite {1}Ha. lia.
+    - assert (a `mod` b = b - 1)%Z as Hamodb by lia.
+      exfalso. lia.
+  Qed.
+
+  Lemma nr_of_affecting_ops_0 q i :
+    nr_of_affecting_ops q i 0 = 0.
+  Proof.
+    unfold nr_of_affecting_ops.
+    rewrite div0 mod0.
+    assert (i <? 0 = false) as ->.
+    { apply Nat.ltb_nlt. lia. }
+    done.
+  Qed.
+
+  Lemma nr_of_affecting_ops_incr q i ops :
+    0 < q →
+    i < q →
+    ops `mod` q ≠ i →
+    nr_of_affecting_ops q i (ops + 1) = nr_of_affecting_ops q i ops.
+  Proof.
+    intros Hgt Hiq Hneq. symmetry.
+    rewrite /nr_of_affecting_ops.
+    assert (Z.of_nat ops = (q * (ops `div` q)%Z + (ops `mod` q)%Z)%Z)%Z as Hops2.
+    { lia. }
+    destruct (decide (i < ops `mod` q)) as [Hops|Hops].
+    - rewrite ltb_lt_1 //.
+      destruct (decide (i < (ops + 1) `mod` q)) as [Hops3|Hops3].
+      + rewrite ltb_lt_1 //.
+        destruct (decide (ops `mod` q < (ops + 1) `mod` q)) as [Hsucc|Hsucc];
+          last first.
+        { cut ((ops + 1) `mod` q = 0); first lia.
+          eapply mod_S_le; lia. }
+        cut (ops `div` q = (ops + 1) `div` q)%Z; first lia.
+        eapply (Zdiv_unique _ _ _ (ops `mod` q + 1)); first lia.
+        rewrite {1}Hops2. lia.
+      + assert (i <? (ops + 1) `mod` q = false) as ->.
+        { by apply Nat.ltb_nlt. }
+        rewrite Nat.add_0_r.
+        destruct (decide ((ops + 1) `mod` q ≤ ops `mod` q)) as [Hsucc|Hsucc]; last lia.
+        assert (((ops + 1) `mod` q = 0) ∧ ops `mod` q = q - 1) as [HSmodq Hmodq].
+        { eapply mod_S_le; lia. }
+        assert (ops + 1 = q * ((ops + 1) `div` q))%Z as Hops4.
+        { lia. }
+        cut (ops `div` q + 1 = (ops + 1) `div` q)%Z ; first lia.
+        eapply (Zdiv_unique _ _ _ 0); lia.
+    - assert (i <? ops `mod` q = false) as ->.
+      { by apply Nat.ltb_nlt. }
+      rewrite Nat.add_0_r.
+      destruct (decide (i < (ops + 1) `mod` q)) as [Hops3|Hops3].
+      + rewrite ltb_lt_1 //.
+        assert (ops `mod` q < (ops + 1) `mod` q) as Hsucc by lia.
+        cut (ops `div` q = (ops + 1) `div` q)%Z; first lia.
+        eapply (Zdiv_unique _ _ _ (ops `mod` q + 1)); first lia.
+        rewrite {1}Hops2. lia.
+      + assert (i <? (ops+1) `mod` q = false) as ->.
+        { by apply Nat.ltb_nlt. }
+        rewrite Nat.add_0_r.
+        cut (ops `div` q = (ops + 1) `div` q)%Z; first lia.
+        destruct (decide (ops `mod` q < (ops + 1) `mod` q)) as [Hsucc|Hsucc].
+        { eapply (Zdiv_unique _ _ _ (ops `mod` q + 1)); first lia.
+          rewrite {1}Hops2. lia. }
+        exfalso.
+        assert ((ops + 1) `mod` q = 0 ∧ ops `mod` q = q - 1) as [HSmod Hmod].
+        { eapply mod_S_le; lia. }
+        lia.
+  Qed.
+
+  Lemma nr_of_affecting_ops_incr_eq q i ops :
+    0 < q →
+    ops `mod` q = i →
+    nr_of_affecting_ops q i (ops + 1) = nr_of_affecting_ops q i ops + 1.
+  Proof.
+    intros Hgt Heq. symmetry.
+    rewrite /nr_of_affecting_ops.
+    assert (i <? ops `mod` q = false) as ->.
+    { apply Nat.ltb_ge. lia. }
+    rewrite Nat.add_0_r.
+    assert (Z.of_nat ops = (q * (ops `div` q)%Z + i%Z)%Z)%Z as Hops2.
+    { rewrite -Heq. lia. }
+    destruct (decide (i < (ops + 1) `mod` q)) as [Hops|Hops].
+    - rewrite ltb_lt_1 //.
+      assert ((ops + 1) `mod` q = i + 1).
+      { rewrite -Heq. eapply mod_S_gt; lia. }
+      cut (ops `div` q = (ops + 1) `div` q)%Z; first lia.
+      eapply (Zdiv_unique _ _ _ (i+1)); first lia.
+      rewrite {1}Hops2. lia.
+    - assert ((ops + 1) `mod` q ≤ i) by lia.
+      assert (i <? (ops + 1) `mod` q = false) as ->.
+      { by apply Nat.ltb_ge. }
+      rewrite Nat.add_0_r.
+      cut (((ops `div` q) + 1) = (ops + 1) `div` q)%Z; first lia.
+      assert (((ops + 1) `mod` q = 0) ∧ ops `mod` q = q - 1) as [HSmodq Hmodq].
+      { eapply mod_S_le; lia. }
+      assert (ops + 1 = q * ((ops + 1) `div` q))%Z as Hops3.
+      { lia. }
+      eapply (Zdiv_unique _ _ _ 0); lia.
+  Qed.
+
+  (* How many turns have been allocated for a SEQ/TS that has been affected by
+  nrPush push operations and nrPop pop operations. NOTE: Since the first turn is
+  for a `push` operation for equal values of nrPush and nrPop it is nrPop that
+  "dominates" how many tickets have been allocated.
+   *)
+  (* Definition allocated_turns nrPush nrPop :=
+    if decide (nrPush ≤ nrPop) then 2 * nrPop else (2 * nrPush) - 1. *)
+
+  (* Ticket management for the i'th SEQ. *)
+  Definition turn_ctx γ q i popTicket pushTicket : iProp Σ :=
+    let nrPop := nr_of_affecting_ops q i popTicket in
+    let nrPush := nr_of_affecting_ops q i pushTicket in
+    enqueue_turns γ nrPush ∗
+    dequeue_turns γ nrPop.
+
+  Lemma turn_ctx_initial γ q i : turn_ctx γ q i 0 0 = (enqueue_turns γ 0 ∗ dequeue_turns γ 0)%I.
+  Proof.
+    rewrite /turn_ctx /nr_of_affecting_ops. autorewrite with natb. done.
+  Qed.
+
+  (* If popTicket is advanced in a way that don't affect the i'th TSer then the
+  turn_ctx for it does not change. *)
+  Lemma turn_ctx_incr_pop γ q i popT pushT :
+    0 < q →
+    i < q →
+    (popT `mod` q ≠ i) →
+    turn_ctx γ q i popT pushT -∗
+    turn_ctx γ q i (popT + 1) pushT.
+  Proof.
+    iIntros (Hgt Hiq Hneq) "Hctx".
+    rewrite /turn_ctx (nr_of_affecting_ops_incr q i popT); done.
+  Qed.
+
+  Lemma turn_ctx_incr_push γ q i popT pushT :
+    0 < q →
+    i < q →
+    (pushT `mod` q ≠ i) →
+    turn_ctx γ q i popT pushT -∗
+    turn_ctx γ q i popT (pushT+1).
+  Proof.
+    iIntros (Hgt Hiq Hneq) "Hctx".
+    rewrite /turn_ctx (nr_of_affecting_ops_incr q i pushT); done.
+  Qed.
+
+  Lemma turn_ctx_incr_pop_eq γ q popT pushT :
+    0 < q →
+    turn_ctx γ q (popT `mod` q) popT pushT -∗
+    turn_ctx γ q (popT `mod` q) (popT + 1) pushT ∗
+    dequeue_turn γ (popT `div` q).
+  Proof.
+    iIntros (Hgt) "[He Hd]".
+    rewrite /turn_ctx. iFrame "He".
+    rewrite (nr_of_affecting_ops_incr_eq q _ popT); [|lia|lia].
+    rewrite /nr_of_affecting_ops.
+    assert (_ <? _ = false) as ->.
+    { apply Nat.ltb_ge. lia. }
+    autorewrite with natb.
+    by rewrite dequeue_turns_take.
+  Qed.
+
+  Lemma turn_ctx_incr_push_eq γ q popT pushT :
+    0 < q →
+    turn_ctx γ q (pushT `mod` q) popT pushT -∗
+    turn_ctx γ q (pushT `mod` q) popT (pushT+1) ∗
+    enqueue_turn γ (pushT `div` q).
+  Proof.
+    iIntros (Hgt) "[He Hd]".
+    rewrite /turn_ctx. iFrame "Hd".
+    rewrite (nr_of_affecting_ops_incr_eq q _ pushT); try lia.
+    rewrite /nr_of_affecting_ops.
+    assert (_ <? _ = false) as ->.
+    { apply Nat.ltb_ge. lia. }
+    autorewrite with natb.
+    by rewrite enqueue_turns_take.
+  Qed.
+
+  (* The invariants. *)
+
+  (* The resources we have for each TSer. *)
+  Definition SEQinv γl (q i : nat) (s : seq) popTicket pushTicket :=
+    (let (γ, v) := s
+     in isSEQ γ (R γl q i) v ∗ turn_ctx γ q i popTicket pushTicket)%I.
+
+  (* The invariant for all SEQs/TSes. *)
+  Definition SEQsinv γl q SEQs popTicket pushTicket : iProp Σ :=
+    ⌜length SEQs = q⌝ ∧
+      [∗ list] i ↦ s ∈ SEQs, SEQinv γl q i s popTicket pushTicket.
+
+  Lemma SEQs_inc_prop_go γl q SEQs popTicket pushTicket v γ :
+    0 < q →
+    SEQs !! (popTicket `mod` q) = Some (MkSeq γ v) →
+    SEQsinv γl q SEQs popTicket pushTicket -∗
+    isSEQ γ (R γl q (popTicket `mod` q)) v ∗
+    SEQsinv γl q SEQs (popTicket + 1) pushTicket ∗ dequeue_turn γ (popTicket `div` q).
+  Proof.
+    rewrite /SEQsinv.
+    iIntros (Hgt Hlook) "[%Hlen Hs]".
+    rewrite (big_sepL_delete' _ _ (popTicket `mod` q)); last done.
+    iDestruct "Hs" as "[H Hs]".
+    iAssert (
+      [∗ list] k↦y ∈ SEQs, ⌜k ≠ popTicket `mod` q⌝ → SEQinv γl q k y (popTicket + 1) pushTicket
+    )%I with "[Hs]" as "Hs".
+    { iApply (big_sepL_impl with "Hs []").
+      iModIntro. iIntros (k x Hlook') "Himpl %Hneq".
+      destruct x as [v' γ'].
+      iDestruct ("Himpl" $! Hneq) as "[Himpl ho]".
+      rewrite /SEQinv. iFrame.
+      assert (k < q).
+      { rewrite -Hlen. eapply lookup_lt_is_Some_1. eauto. }
+      rewrite turn_ctx_incr_pop; done. }
+    simpl.
+    iDestruct "H" as "[#Hi Hctx]".
+    iDestruct (turn_ctx_incr_pop_eq with "Hctx") as "[Hctx Hturn]"; first done.
+    iAssert (SEQinv γl q (popTicket `mod` q) (MkSeq γ v) (popTicket + 1) pushTicket)%I with "[Hi Hctx]" as "Hsingl".
+    { iFrame "#∗". }
+    iCombine "Hsingl Hs" as "Hs".
+    iDestruct (big_sepL_delete' _ SEQs (popTicket `mod` q)) as "HI"; first done.
+    iDestruct ("HI" with "Hs") as "HOHO".
+    by iFrame "#∗".
+  Qed.
+
+  Lemma SEQs_incr_pop γl q SEQs popTicket pushTicket :
+    0 < q →
+    SEQsinv γl q SEQs popTicket pushTicket ==∗
+    ∃ (γ : gname) v,
+      let i := (popTicket `mod` q) in
+      ⌜SEQs !! i = Some (MkSeq γ v)⌝ ∗
+      isSEQ γ (R γl q i) v ∗
+      SEQsinv γl q SEQs (popTicket + 1) pushTicket ∗
+      dequeue_turn γ (popTicket / q).
+  Proof.
+    iIntros (Hlt) "Hinv".
+    iAssert (⌜length SEQs = q⌝%I) as %Hlen.
+    { by iDestruct "Hinv" as "[$ _]". }
+    set (i := popTicket `mod` q).
+    assert (i < length SEQs) as Hlt'; first lia.
+    destruct (lookup_lt_is_Some_2 _ _ Hlt') as [[γ v] Hlook].
+    iExists γ, v.
+    iModIntro.
+    iSplit; first done.
+    rewrite /SEQsinv.
+    by iDestruct (SEQs_inc_prop_go with "Hinv") as "Hinv".
+  Qed.
+
+  (* If you increment pushTicket you get a turn. You also get the persistent
+  predicate for the SEQer b.c. otherwise the turn is not useful. *)
+  Lemma SEQs_incr_push γl q SEQs popTicket pushTicket :
+    0 < q →
+    SEQsinv γl q SEQs popTicket pushTicket ==∗
+    ∃ (γ : gname) v,
+      let i := (pushTicket `mod` q) in
+      ⌜SEQs !! i = Some (MkSeq γ v)⌝ ∗
+      isSEQ γ (R γl q i) v ∗
+      SEQsinv γl q SEQs popTicket (pushTicket + 1) ∗
+      enqueue_turn γ (pushTicket / q).
+  Proof.
+    iIntros (H0q) "[%Hlen HInv]".
+    pose (i := pushTicket `mod` q).
+    assert (i < length SEQs) as Hi by lia.
+    apply lookup_lt_is_Some_2 in Hi. destruct Hi as [[γ v] Hi].
+    iExists γ,v.
+    rewrite (big_sepL_delete _ _ i); last done.
+    iDestruct "HInv" as "[Hi HInv]".
+    (* First, update the queues that are *not* affected, i.e. all the non-i queues *)
+    rewrite (big_sepL_mono _ (fun j sq => ⌜j ≠ i⌝ → SEQinv γl q j sq popTicket (pushTicket+1))%I); last first.
+    { iIntros (k [v' γ'] Hk) "Hq".
+      iIntros (Hki). destruct (decide (k = i)); first (simplify_eq/=); [].
+      unfold SEQinv.
+      destruct (decide (k < i)).
+      + iDestruct "Hq" as "[$ Hq]".
+        rewrite turn_ctx_incr_push; eauto. lia.
+      + assert (i < k) by lia.
+        iDestruct "Hq" as "[$ Hq]".
+        assert (k < q).
+        { rewrite -Hlen. apply lookup_lt_is_Some_1. eauto. }
+        rewrite turn_ctx_incr_push; eauto. }
+    (* Update the resources for the i-th queue and obtain the ticket *)
+    iAssert (|==> SEQinv γl q i {| seq_val := v; seq_gname := γ |} popTicket (pushTicket+1) ∗ enqueue_turn γ (pushTicket `div` q))%I with "[Hi]" as ">[Hi $]".
+    { iDestruct "Hi" as "[#Hinv Htctx]".
+      rewrite /SEQinv. iFrame "Hinv".
+      rewrite turn_ctx_incr_push_eq; eauto. }
+    iModIntro. repeat (iSplitR; first done).
+    iDestruct "Hi" as "[#$ H2]".
+    rewrite /SEQsinv. iSplit; first done.
+    iApply big_sepL_delete'; eauto. rewrite /SEQinv. by iFrame.
+  Qed.
+
+  (* The i'th enqueue/push must add this to the invariant. *)
+  Definition push_i A γl γt γm i : iProp Σ :=
+    token γt i ∨
+    (∃ id v vₛ, own γm (◯ {[ i := to_agree id ]}) ∗
+                (refines_right id (of_val vₛ)) ∗
+                A v vₛ ∗
+                ghost_list_mapsto γl i v).
+
+  Definition mpmcInv A γt γm γl q (ℓpop ℓpush ℓarr : loc) (SEQs : list seq)
+    (xsᵢ : list val) (ℓs : loc) (lk : val) : iProp Σ :=
+    ∃ (popTicket pushTicket : nat) (m : list val) (p : Qp) threads,
+
+      (* The physical state. *)
+      ℓpop ↦ #popTicket ∗
+      ℓpush ↦ #pushTicket ∗
+      ℓarr ↦∗{#p} (seq_val <$> SEQs) ∗ (* FIXME: Use persistent points-to predicate here. *)
+
+      (* Ghost list *)
+      (ghost_list γl m ∗
+      ⌜length m = pushTicket⌝ ∗
+      ⌜drop popTicket m = xsᵢ⌝) ∗
+
+      (* Knowledge about each SEQ. *)
+      SEQsinv γl q SEQs popTicket pushTicket ∗
+
+      (* Handling of external LP. *)
+      (* The 'I-came-first' token *)
+      tokens_from γt (popTicket `max` pushTicket) ∗ (* Keeps track of which tokens we own. *)
+      (* Some pop operations has decided on a [j] and a [K]. *)
+      own γm (● threads) ∗
+      ⌜dom (gset _) threads ⊆ set_seq 0 popTicket⌝ ∗
+      (* Every push operation must show this for i. *)
+      ([∗ set] i ∈ (set_seq 0 pushTicket), push_i A γl γt γm i) ∗
+      (* When popTicket is greater than pushTicket the pop operation has left a
+        spec thread resource. *)
+      ([∗ set] i ∈ (set_seq pushTicket (popTicket - pushTicket)),
+        ∃ id, own γm (◯ {[ i := to_agree id ]}) ∗ (refines_right id (CG_dequeue lk #ℓs #()))).
+
+  Definition I A γt γm γl q ℓpop ℓpush ℓarr SEQs ℓs lk : iProp Σ :=
+    (∃ xsᵢ xsₛ,
+      mpmcInv A γt γm γl q ℓpop ℓpush ℓarr SEQs xsᵢ ℓs lk ∗
+      cgQueueInv ℓs lk xsₛ ∗
+      [∗ list] xᵢ ; xₛ ∈ xsᵢ ; xsₛ, A xᵢ xₛ)%I.
+
+  (* Decide j and K. *)
+  Lemma thread_alloc (γm : gname) mt popTicket (id : ref_id) :
+    dom (gset nat) mt ⊆ set_seq 0 popTicket →
+    own γm (● mt) ==∗
+    ⌜dom (gset nat) (<[ popTicket := to_agree id ]>mt) ⊆ set_seq 0 (popTicket + 1)⌝ ∗
+    own γm (● (<[ popTicket := to_agree id ]>mt)) ∗
+    own γm (◯ ({[ popTicket := to_agree id ]})).
+  Proof.
+    iIntros (Hsub) "Hown".
+    iMod (own_update with "Hown") as "[Hown Hfrag]".
+    { apply auth_update_alloc.
+      eapply (alloc_local_update _ _ popTicket (to_agree (id : ref_idO))); last done.
+      apply not_elem_of_dom.
+      set_solver by lia. }
+    iModIntro. iFrame.
+    iPureIntro. rewrite dom_insert. set_solver by lia.
+  Qed.
+
+  Lemma push_i_add A γl γt γm n :
+    ([∗ set] i ∈ set_seq 0 n, push_i A γl γt γm i)
+    -∗ push_i A γl γt γm n
+    -∗ ([∗ set] i ∈ set_seq 0 (n + 1), push_i A γl γt γm i).
+  Proof.
+    iIntros "Ho Htok".
+    rewrite Nat.add_1_r.
+    rewrite set_seq_S_end_union_L. simpl.
+    iApply big_sepS_insert; first set_solver by lia.
+    iSplitL "Htok"; iFrame.
+  Qed.
+
+
+  Lemma makeArray_newSQueue (γl : gname) (q : nat) :
+    {{{ ⌜q > 0⌝ }}}
+      array_init #q newSQueue
+    {{{ â„“arr SEQs, RET #â„“arr;
+      ⌜length SEQs = q⌝ ∗
+      ℓarr ↦∗ (seq_val <$> SEQs) ∗
+      ([∗ list] i ↦ s ∈ SEQs, SEQinv γl q i s 0 0)
+    }}}.
+  Proof.
+    iIntros (Ï•) "%Hqgt HÏ•".
+    iApply (wp_array_init_fmap seq_val (λ i s, SEQinv γl q i s 0 0)); first lia.
+    { iApply big_sepL_intro. iModIntro.
+      iIntros (k i Hi).
+      wp_apply newSEQ_spec; first done.
+      iIntros (γ v) "(isSEQ & Ht1 & Ht2)".
+      iExists (MkSeq γ v). iSplit; first done.
+      rewrite /SEQinv.
+      rewrite (turn_ctx_initial _ q). by iFrame. }
+    iNext.
+    iIntros (â„“arr SEQs) "(%Hlen & arrPts & Hlist)".
+    iApply "HÏ•".
+    iFrame. iPureIntro. by simplify_eq/=.
+  Qed.
+
+
+  Lemma big_sepS_take_first (n m : nat) (Φ : nat → iProp Σ) :
+    0 < m → ([∗ set] i ∈ set_seq n m, Φ i) -∗ Φ n ∗ ([∗ set] i ∈ set_seq (n + 1) (m - 1), Φ i).
+  Proof.
+    intros Hlt.
+    rewrite (set_seq_take_start_L n m 1); last lia.
+    rewrite big_sepS_union; last set_solver by lia.
+    simpl.
+    assert ({[n]} ∪ ∅ = {[n]}) as ->; first by set_solver.
+    rewrite big_sepS_singleton.
+    done.
+  Qed.
+
+  Lemma enqueue_refinement (A : lrel Σ) (q : nat) γt γm γl ℓpop ℓpush ℓarr SEQs list l x x' :
+    q > 0 →
+    inv queueN (I A γt γm γl q ℓpop ℓpush ℓarr SEQs list l) -∗
+    A x x' -∗
+    REL enqueue #â„“arr #q #â„“push x << CG_enqueue l #list x' : ().
+  Proof.
+    iIntros (?) "#Hinv #HA".
+    rel_rec_l.
+    rel_pures_l.
+
+    (* This is the linearization points for enqueue. *)
+    rel_apply_l refines_faa_l.
+    iInv queueN as (xs xsâ‚›) "(Hmpmc & Hsq & Hlink)" "Hcl".
+    iDestruct "Hmpmc" as (popTicket pushTicket m p mt)
+                           "(>popPts & >pushPts & >[arrPts arrPts'] & >(Hlist & %Hlen & %Hlisteq) & Hseqs & HAtok & Ha & Hb & Hpush & Hmore)".
+    iModIntro. iExists _. iFrame "pushPts". iNext. iIntros "pushPts".
+
+    (* We need to get a ticket out for the SEQ. *)
+    iMod (SEQs_incr_push with "Hseqs") as (γ v) "(%Hattss & #HisSEq & Hseqs & Hturn)"; first lia.
+
+    (* This is the linearization point for enqueue. *)
+    rel_apply_r (refines_CG_enqueue_r with "Hsq"). iIntros "Hsq".
+
+    (* We insert the enqueued element into the logical list. *)
+    iMod (ghost_list_append _ _ x with "Hlist") as "[Hlist #Helem]".
+
+    (* Did we came first or did a pop come before us? *)
+    destruct (le_lt_dec popTicket pushTicket) as [Hle|Hgt].
+
+    * (* We came first *)
+
+      (* In this case handling the LP/token infrastructure is fiarly
+        straightforward. Since [popTicket ≤ pushTicket] we can take a ticket. *)
+      rewrite (max_r _ _ Hle).
+      iDestruct (tokens_take with "HAtok") as "[HAtok Htok]".
+      iDestruct (push_i_add with "Hpush [$]") as "Hpush".
+
+      iMod ("Hcl" with "[-arrPts Hturn]") as "_".
+      { iNext. iExists (xs ++ [x]), (xsâ‚› ++ [x']).
+        iFrame. iFrame "HA".
+        rewrite big_sepL2_nil.
+        iSplitL; last done.
+        iExists popTicket, (pushTicket + 1), _, _, _.
+        assert ((pushTicket + 1)%Z = (pushTicket + 1)%nat) as -> by lia.
+        assert (popTicket `max` (pushTicket + 1) = pushTicket + 1) as -> by lia.
+        assert (popTicket - (pushTicket + 1) = 0) as -> by lia.
+        iFrame. simpl.
+        rewrite big_sepS_empty.
+        iPureIntro. split; last done. split.
+        { rewrite app_length. simpl. lia. }
+        rewrite drop_app_le; last lia.
+        rewrite Hlisteq. done. }
+      rel_pures_l.
+      rel_bind_l (! _)%E.
+      rel_apply_l refines_wp_l.
+      assert ((Z.of_nat pushTicket `rem` Z.of_nat q)%Z = Z.of_nat (pushTicket `mod` q)) as ->.
+      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      wp_apply (wp_load_offset with "arrPts").
+      { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
+      iIntros "arrPts".
+      rewrite Z.quot_div_nonneg; [|lia|lia].
+      rewrite -Nat2Z_inj_div.
+      rel_apply_l refines_wp_l.
+      wp_apply (enqueueWithTicket_spec' _ (R _ q (pushTicket `mod` q)) with "[-]").
+      2: { iIntros. rel_values. }
+      iFrame "Hturn".
+      rewrite /R.
+      rewrite div_mod'; last lia.
+      rewrite Hlen.
+      iFrame "#".
+
+    * (* We came _last_ and we must step forward a dequeue. *)
+
+      (* The queue is empty. *)
+      assert (length xs = 0) as Hlen'.
+      { rewrite -Hlisteq. rewrite drop_ge; [done|lia]. }
+      destruct xs as [|? ?]; last done.
+      iDestruct (big_sepL2_nil_inv_l with "Hlink") as %->.
+
+      iDestruct (big_sepS_take_first with "Hmore") as "[Hobl Hmore]"; first lia.
+      iDestruct "Hobl" as (id) "[#Hagree Hj]".
+      simpl.
+
+      (* We already carried out the LP for enqueue, we now also perform the LP
+           for the dequeue. *)
+      iMod (refines_right_CG_dequeue with "Hsq Hj") as "[Hsq Hj]".
+      { solve_ndisj. }
+
+      (* We have now carried out our obligation to the dequeue and can prove that. *)
+      rewrite Hlen.
+      iDestruct (push_i_add with "Hpush [Hj]") as "Hpush".
+      { iRight. iExists id, _, _. iFrame "#∗". }
+
+      iMod ("Hcl" with "[-arrPts Hturn]") as "_".
+      { iNext. iExists [], []. iFrame "Hsq".
+        simpl. iSplitL; last done.
+        iExists popTicket, (pushTicket + 1), _, _, _.
+        assert ((pushTicket + 1)%Z = (pushTicket + 1)%nat) as -> by lia.
+        assert (popTicket - (pushTicket + 1) = popTicket - pushTicket - 1) as -> by lia.
+        assert (popTicket `max` (pushTicket + 1) = popTicket `max` pushTicket) as -> by lia.
+        simpl. iFrame.
+        iPureIntro. split.
+        - rewrite app_length. simpl. lia.
+        - apply drop_ge. rewrite app_length. simpl. lia. }
+
+      rel_pures_l.
+      rel_bind_l (! _)%E.
+      rel_apply_l refines_wp_l.
+      assert ((Z.of_nat pushTicket `rem` Z.of_nat q)%Z = Z.of_nat (pushTicket `mod` q)) as ->.
+      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      wp_apply (wp_load_offset with "arrPts").
+      { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
+      iIntros "arrPts".
+      rewrite Z.quot_div_nonneg; [|lia|lia].
+      rewrite -Nat2Z_inj_div.
+      rel_apply_l refines_wp_l.
+      wp_apply (enqueueWithTicket_spec' _ (R _ q (pushTicket `mod` q)) with "[-]").
+      2: { iIntros. rel_values. }
+      iFrame "Hturn".
+      rewrite /R.
+      rewrite div_mod'; last lia.
+      iFrame "#".
+  Qed.
+
+  Lemma dequeue_refinement (A : lrel Σ) (q : nat) γt γm γl ℓpop ℓpush ℓarr SEQs list l :
+    q > 0 →
+    inv queueN (I A γt γm γl q ℓpop ℓpush ℓarr SEQs list l) -∗
+    REL dequeue #â„“arr #q #â„“pop << CG_dequeue l #list #() : A.
+  Proof.
+    iIntros (?) "#Hinv".
+    rel_rec_l.
+    rel_pures_l.
+
+    (* We get to the FAA which increments the popTicket. *)
+    rel_apply_l refines_faa_l.
+    iInv queueN as (xs xsâ‚›) "(Hmpmc & Hsq & Hlink)" "Hcl".
+    iDestruct "Hmpmc" as (popTicket pushTicket m p mt)
+      "(>popPts & >pushPts & >[arrPts arrPts'] & >(Hlist & %Hlen & %Hlisteq) & Hseqs & HAtok & Ha & >%Hb & Hpush & Hmore)".
+    iModIntro. iExists _. iFrame "popPts". iNext. iIntros "popPts".
+
+    (* We need to get a ticket out for the SEQ. *)
+    iMod (SEQs_incr_pop with "Hseqs") as (γ v) "(%Hattss & #HisSEq & Hseqs & Hturn)"; first done.
+
+    (* Did we came first or did a push come before us? *)
+    destruct (le_lt_dec pushTicket popTicket) as [Hle|Hgt].
+
+    * (* We came first and there is currently no element for us. *)
+
+      (* We can take the I-came-first-token. *)
+      iDestruct (tokens_take with "HAtok") as "[HAtok Htok]".
+      replace (popTicket `max` pushTicket) with popTicket by lia.
+      iApply refines_split.
+      iIntros (id) "Hright".
+      (* We now allocate the [id] agreement. *)
+      iMod (thread_alloc _ _ _ id with "Ha") as "(%Sub & Ha & #Hdec)"; first done.
+
+      assert (length xs = 0) as Hlen'.
+      { rewrite -Hlisteq. rewrite drop_ge; [done|lia]. }
+      destruct xs as [|? ?]; last done.
+      iDestruct (big_sepL2_nil_inv_l with "Hlink") as %->.
+      simpl.
+
+      iMod ("Hcl" with "[-arrPts Hturn Htok]") as "_".
+      { iNext. iExists [], []. simpl. iFrame.
+        iExists (popTicket + 1), pushTicket, _, _, _.
+        simpl.
+        assert ((popTicket + 1)%Z = (popTicket + 1)%nat) as ->; first lia.
+        replace ((popTicket + 1) `max` pushTicket) with (popTicket + 1) by lia.
+        (* assert (popTicket `max` pushTicket + 1 = (popTicket + 1) `max` pushTicket) as ->; first lia. *)
+        iFrame.
+        repeat iSplit; eauto with lia.
+        { iPureIntro. apply drop_ge. lia. }
+        replace (popTicket + 1 - pushTicket) with (S (popTicket - pushTicket)) by lia.
+        rewrite set_seq_S_end_union_L.
+        rewrite big_sepS_union; last set_solver by lia.
+        iFrame.
+        rewrite big_sepS_singleton.
+        iExists id. iFrame.
+        replace (pushTicket + (popTicket - pushTicket)) with popTicket by lia.
+        iFrame "#". }
+      (* FIXME: The the iModIntro here unfolds [refines_left]. *)
+      (* iModIntro. *)
+      rel_pures_l.
+
+      assert ((Z.of_nat popTicket `rem` Z.of_nat q)%Z = Z.of_nat (popTicket `mod` q)) as ->.
+      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      rel_apply_l refines_wp_l.
+      wp_apply (wp_load_offset with "arrPts").
+      { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
+      iIntros "arrPts".
+
+      rewrite Z.quot_div_nonneg; [|lia|lia].
+      rewrite -Nat2Z_inj_div.
+      iApply wp_fupd.
+      simpl.
+      wp_apply (dequeueWithTicket_spec2 _ (R _ q (popTicket `mod` q)) with "[-Htok]").
+      { iFrame "#∗". }
+      iIntros (?).
+      rewrite /R.
+      rewrite div_mod'; last lia.
+      iIntros "#Hag".
+
+      clear.
+      (* We now open the invariant again. It this point we can be sure that a
+           enqueue operation has stepped our specification forward. *)
+      iInv queueN as (xs xsâ‚›) "(Hmpmc & Hsq & Hlink)" "Hcl".
+      iDestruct "Hmpmc" as (popTicket' pushTicket m p mt)
+                             "(>popPts & >pushPts & >[arrPts arrPts'] & (>Hlist & >%Hlen & Hlisteq) & Hseqs & HAtok & Ha & Hb & Hpush & Hmore)".
+      (* We now "flip" the disjunction for one of the popTickets. *)
+      iDestruct (ghost_list_le with "Hlist Hag") as %popLePush.
+      rewrite (big_sepS_delete _ _ popTicket). 2: { rewrite elem_of_set_seq. lia. }
+      iDestruct "Hpush" as "[[>Htok'|Hright] Hpush]".
+      { by iDestruct (own_valid_2 with "Htok Htok'") as %Hv%set_singleton_invalid. }
+      iDestruct "Hright" as (id' v' vâ‚›) "(>#Hdec' & Hright & #Hrel & >#Hag')".
+      iAssert (push_i A γl γt γm popTicket) with "[Htok]" as "Hi".
+      { iLeft. iFrame. }
+
+      iMod ("Hcl" with "[-Hright]") as "_".
+      { iNext. iExists xs, xsâ‚›. iFrame.
+        iCombine "Hi Hpush" as "Hpush".
+        rewrite -big_sepS_insert; last set_solver by lia.
+        (* rewrite difference_union_distr_l_L. *)
+        replace ({[popTicket]} ∪ set_seq 0 pushTicket ∖ {[popTicket]}) with (set_seq (C:=gset nat) 0 pushTicket) by set_solver by lia.
+        iExists _, _, _, _, _. by iFrame. }
+
+      iModIntro. iNext. iModIntro.
+      iDestruct (map_list_agree with "Hag Hag'") as %->.
+      iDestruct (decide_agree with "Hdec Hdec'") as %->.
+      iApply refines_combine; last iApply "Hright".
+      rel_values.
+
+    * (* An enqueue has been here. *)
+      (* We can take a logical value from the list. *)
+      (* The list must be non-empty. *)
+      assert (is_Some (m !! popTicket)) as [x' Hlk].
+      { apply lookup_lt_is_Some_2. lia. }
+      destruct xs as [|x xs]. {
+        erewrite drop_S in Hlisteq; last apply Hlk.
+        discriminate. }
+      clear x' Hlk.
+      epose proof (drop_nth _ _ _ _ Hlisteq) as HMlook.
+      iMod (ghost_list_lookup with "Hlist") as "[Hlist #Hlistelem]".
+      { done. }
+      iDestruct (big_sepL2_cons_inv_l with "Hlink") as (xâ‚› xsâ‚›' ->) "[#Hrel Hlink]".
+
+      (* In this case handling the LP/token infrastructure is fiarly
+        straightforward. The tickets don't change. *)
+      assert (popTicket `max` pushTicket = (popTicket + 1) `max` pushTicket) as -> by lia.
+
+      (* Step specification forward. *)
+      rel_apply_r (refines_CG_dequeue_cons_r with "Hsq"). iIntros "Hsq".
+
+      (* Close the invariant. *)
+      iMod ("Hcl" with "[-arrPts Hturn]") as "_".
+      { iNext. iExists xs, xsâ‚›'. iFrame.
+        iExists (popTicket + 1), pushTicket, _, _, _.
+        assert ((popTicket + 1)%Z = (popTicket + 1)%nat) as -> by lia.
+        assert (popTicket + 1 - pushTicket = 0) as -> by lia.
+        iFrame.
+        rewrite big_sepS_empty.
+        repeat iSplit; try by (iPureIntro; set_solver by lia).
+        iPureIntro.
+        rewrite Nat.add_1_r .
+        pose proof (drop_S _ _ _ HMlook) as T.
+        rewrite T in Hlisteq.
+        pose proof Hlisteq as [= ?].
+        done. }
+      rel_pures_l.
+
+      rel_bind_l (! _)%E.
+      rel_apply_l refines_wp_l.
+      assert ((Z.of_nat popTicket `rem` Z.of_nat q)%Z = Z.of_nat (popTicket `mod` q)) as ->.
+      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      wp_apply (wp_load_offset with "arrPts").
+      { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
+      iIntros "arrPts".
+
+      rewrite Z.quot_div_nonneg; [|lia|lia].
+      rewrite -Nat2Z_inj_div.
+      rel_apply_l refines_wp_l.
+      wp_apply (dequeueWithTicket_spec' _ (R _ q (popTicket `mod` q)) with "[-]").
+      { iFrame "#∗". }
+      iIntros (?).
+      rewrite /R.
+      rewrite Nat.mul_comm.
+      rewrite <- (Nat.div_mod _ q); last lia.
+      iIntros "Hlistelem'".
+      iDestruct (map_list_agree with "Hlistelem Hlistelem'") as %<-.
+      rel_values.
+  Qed.
+
+  Lemma queue_refinement (q : nat) :
+    q > 0 →
+    ⊢ REL newQueue #q << CG_queue : ∀ A, (A → ()) * (() → A).
+  Proof.
+    intros Hqgt.
+
+    rel_rec_l. rel_pure_l.
+    iApply refines_forall.
+    iModIntro.
+    iIntros (A).
+
+    iMod ghost_list_alloc as (γl) "Hlist".
+
+    (* Step through implementation. *)
+    rel_bind_l (array_init _ _).
+    rel_apply_l refines_wp_l.
+    wp_apply (makeArray_newSQueue γl); first done.
+    iIntros (â„“arr SEQs) "(%Htsslen & arrPts & Hseqs)".
+    rel_alloc_l â„“push as "pushts".
+    rel_alloc_l â„“pop as "popPts".
+    do 2 rel_pure_l.
+
+    (* Step through specification. *)
+    rel_alloc_r list as "listPts".
+    rel_pure_r.
+    rel_pure_r.
+    rel_apply_r refines_newlock_r. iIntros (l) "lofal".
+    do 2 rel_pure_r.
+
+    (* Establish the invariant. *)
+    iMod (own_alloc (set_above 0)) as (γt) "Htok"; first done.
+    iMod (own_alloc (● ∅ : requestRegR)) as (γm) "Hdec"; first by apply auth_auth_valid.
+    iMod (inv_alloc queueN _ (I A γt γm γl q ℓpop ℓpush ℓarr SEQs _ _) with "[-]") as "#Hinv".
+    { iNext. iExists [], []. simpl. iFrame. iExists 0, 0, ∅, 1%Qp, ∅. cbn. iFrame.
+      rewrite !dom_empty_L !big_sepS_empty. iFrame. done. }
+
+    iApply refines_pair.
+    - (* enqueue *)
+      rel_pures_l.
+      rel_pures_r.
+      iApply refines_arrow_val. iModIntro.
+      iIntros (x x') "#Hrel".
+      rel_pures_l. rel_rec_r.
+      by iApply enqueue_refinement.
+    - (* dequeue *)
+      rel_pures_l.
+      rel_pures_r.
+      iApply refines_arrow_val. iModIntro.
+      iIntros (?? [-> ->]).
+      rel_pures_l.
+      rel_pures_r.
+      by iApply dequeue_refinement.
+  Qed.
+
+End queue_refinement.
diff --git a/theories/examples/folly_queue/set.v b/theories/examples/folly_queue/set.v
new file mode 100644
index 0000000000000000000000000000000000000000..bfdd78735f1b9f02c63b3106075f751bed4f1c5f
--- /dev/null
+++ b/theories/examples/folly_queue/set.v
@@ -0,0 +1,209 @@
+From stdpp Require Import base decidable.
+From iris.algebra Require Import numbers cmra excl.
+From reloc.prelude Require Import arith.
+
+(* A camera of, potentially, infinite sets. Most of the lemmas are about sets of
+   natural numbers. *)
+
+Definition setUR (A : Type) := discrete_funUR (λ (a : A), optionUR (exclR unitO)).
+
+(* Sets of natural numbers. *)
+
+(* Create a set from a characteristic function. *)
+Definition set_cf {A : Type} (f : A → bool) : setUR A :=
+  λ a, if f a then Some (Excl ()) else None.
+
+Definition set_of (A : Type) := @set_cf A (const true).
+
+Definition set_singleton `{!EqDecision A} (a : A) :=
+  set_cf (λ a', if decide (a = a') then true else false).
+
+Definition set_nat := set_of nat.
+Definition set_even := set_cf even.
+Definition set_odd := set_cf odd.
+
+Lemma split_even_odd : set_nat ≡ set_even ⋅ set_odd.
+Proof.
+  intros n. rewrite /set_even /set_odd /set_cf. simpl.
+  rewrite discrete_fun_lookup_op.
+  destruct (even_odd_spec n) as [[-> ->]|[-> ->]]; done.
+Qed.
+
+(* Set of nats including and above n. *)
+Definition set_above n := set_cf (λ n', n <=? n').
+
+Definition set_upto n := set_cf (λ n', n' <? n).
+
+Lemma set_above_lookup n m : n ≤ m → set_above n m = Excl' ().
+Proof. rewrite /set_above /set_cf. by intros ->%leb_le. Qed.
+
+Lemma set_above_lookup_none n m : m < n → (set_above n) m = None.
+Proof. rewrite /set_above /set_cf. by intros ->%Nat.leb_gt. Qed.
+
+Lemma set_upto_lookup n m : m < n → (set_upto n) m = Excl' ().
+Proof. rewrite /set_upto /set_cf. by intros ->%Nat.ltb_lt. Qed.
+
+Lemma set_upto_lookup_none n m : n ≤ m → (set_upto n) m = None.
+Proof. rewrite /set_upto /set_cf. by intros ->%Nat.ltb_ge. Qed.
+
+Lemma set_above_zero : set_above 0 ≡ set_nat.
+Proof. intros n. rewrite set_above_lookup; [done | lia]. Qed.
+
+Lemma set_upto_zero : set_upto 0 ≡ ε.
+Proof.
+  intros n. rewrite /set_upto /set_cf.
+  assert (n <? 0 = false) as ->; last done.
+  apply leb_correct_conv. lia.
+Qed.
+
+Lemma discrete_fun_valid' (s : setUR nat) (n : nat) : ✓ s → ✓ (s n).
+Proof. done. Qed.
+
+Lemma set_singleton_lookup (n : nat) : set_singleton n n = Excl' ().
+Proof. rewrite /set_singleton /set_cf. rewrite decide_True; done. Qed.
+
+Lemma set_singleton_lookup_none (n m : nat) : n ≠ m → set_singleton n m = None.
+Proof.
+  intros H. rewrite /set_singleton /set_cf. rewrite decide_False; done.
+Qed.
+
+Lemma set_singleton_invalid (n : nat) : ¬ ✓ (set_singleton n ⋅ set_singleton n).
+Proof.
+  rewrite /set_singleton /set_cf.
+  intros Hv.
+  pose proof (Hv n) as Hv.
+  rewrite discrete_fun_lookup_op in Hv.
+  rewrite decide_True in Hv; done.
+Qed.
+
+Lemma set_singletons_valid (n m : nat) : ✓ (set_singleton n ⋅ set_singleton m) → n ≠ m.
+Proof.
+  intros Hv ->.
+  by apply set_singleton_invalid in Hv.
+Qed.
+
+(* Rewrite n <? m when true *)
+Hint Rewrite ltb_lt_1 using lia : natb.
+Hint Rewrite leb_correct_conv using lia : natb.
+Hint Rewrite leb_correct using lia : natb.
+Hint Rewrite set_above_lookup using lia : natb.
+Hint Rewrite @decide_False using lia : natb.
+Hint Rewrite @decide_True using lia : natb.
+Hint Rewrite set_above_lookup_none using lia : natb.
+Hint Rewrite set_upto_lookup_none using lia : natb.
+Hint Rewrite set_upto_lookup using lia : natb.
+Hint Rewrite set_singleton_lookup_none using lia : natb.
+Hint Rewrite set_singleton_lookup using lia : natb.
+Hint Rewrite div_mod' : natb.
+Hint Rewrite mod0 : natb.
+Hint Rewrite div0 : natb.
+Hint Rewrite Nat.add_0_r : natb.
+Hint Rewrite Nat.add_0_l : natb.
+Hint Rewrite Nat.ltb_irrefl : natb.
+Hint Rewrite Nat.max_0_r : natb.
+Hint Rewrite Nat.max_0_l : natb.
+
+Lemma set_upto_singleton_valid n m : ✓ (set_upto n ⋅ set_singleton m) → n ≤ m.
+Proof.
+  destruct (le_gt_dec n m); first done.
+  intros Hv.
+  pose proof (Hv m).
+  rewrite discrete_fun_lookup_op in H.
+  rewrite /set_singleton /set_cf in H.
+  autorewrite with natb in H.
+  done.
+Qed.
+
+Lemma take_first n : set_above n ≡ set_singleton n ⋅ set_above (n + 1).
+Proof.
+  intros n'.
+  rewrite /set_singleton. rewrite /set_cf.
+  rewrite discrete_fun_lookup_op.
+  destruct (le_lt_dec n n').
+  - autorewrite with natb.
+    destruct (le_lt_or_eq n n' l); autorewrite with natb; done.
+  - autorewrite with natb. done.
+Qed.
+
+Lemma set_upto_singleton n : set_singleton n ⋅ set_upto n ≡ set_upto (n + 1).
+Proof.
+  intros m.
+  rewrite discrete_fun_lookup_op.
+  destruct (le_gt_dec m n).
+  - rewrite (set_upto_lookup (n + 1)); last lia.
+    destruct (le_lt_or_eq m n l).
+    * autorewrite with natb. done.
+    * subst. autorewrite with natb. done.
+  - autorewrite with natb. done.
+Qed.
+
+(* Create a set from a decidable predicate. *)
+Definition set_prop {A : Type} (f : A → Prop) `{!∀ a, Decision (f a)} : setUR A :=
+  λ a, if decide (f a) then Some (Excl ()) else None.
+
+(* All even numbers except for the first n. *)
+Definition set_even_drop n := set_cf (λ n', (even n') && (2 * n <=? n')).
+
+(* All odd numbers except for the first n. *)
+Definition set_odd_drop n := set_cf (λ n', (odd n') && (2 * n + 1 <=? n')).
+
+Lemma set_even_drop_lookup n m : Even m → 2 * n ≤ m → set_even_drop n m = Excl' ().
+Proof.
+  intros He Hle.
+  rewrite /set_even_drop /set_cf.
+  assert (Nat.even m = true) as -> by by apply Nat.even_spec.
+  rewrite leb_correct; last done.
+  done.
+Qed.
+
+Lemma set_even_drop_zero : set_even_drop 0 ≡ set_even.
+Proof.
+  intros n.
+  rewrite /set_even_drop /set_even /set_cf.
+  destruct (Nat.even n); done.
+Qed.
+
+Lemma set_odd_drop_zero : set_odd_drop 0 ≡ set_odd.
+Proof.
+  intros n.
+  rewrite /set_odd_drop /set_odd /set_cf.
+  destruct n; first done.
+  destruct (Nat.odd (S n)); done.
+Qed.
+
+Lemma set_even_drop_singleton n : set_even_drop n ≡ set_even_drop (n + 1) ⋅ set_singleton (2 * n).
+Proof.
+  intros m.
+  rewrite /set_even_drop /set_singleton /set_cf /=.
+  autorewrite with natb.
+  rewrite discrete_fun_lookup_op.
+  destruct (Nat.Even_or_Odd m) as [[a b]|[a b]].
+  - replace (Nat.even m) with true.
+    + destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He]; autorewrite with natb; eauto.
+    + symmetry. apply Nat.even_spec. by econstructor.
+  - replace (Nat.even m) with false.
+    + by autorewrite with natb.
+    + rewrite -Nat.negb_odd.
+      cut (Nat.odd m = true); first by intros ->.
+      eapply Nat.odd_spec. by econstructor.
+Qed.
+
+Lemma set_odd_drop_singleton n : set_odd_drop n ≡ set_odd_drop (n + 1) ⋅ set_singleton (2 * n + 1).
+Proof.
+  intros m.
+  rewrite /set_odd_drop /set_singleton /set_cf /=.
+  autorewrite with natb.
+  rewrite discrete_fun_lookup_op.
+  destruct (Nat.Even_or_Odd m) as [[a b]|[a b]].
+  - replace (Nat.odd m) with false.
+    + destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He]; autorewrite with natb; eauto.
+    + rewrite -Nat.negb_even.
+      cut (Nat.even m = true); first by intros ->.
+      eapply Nat.even_spec. by econstructor.
+  - replace (Nat.odd m) with true.
+    + destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He];
+        autorewrite with natb; try lia; eauto.
+      destruct (gt_eq_gt_dec m ((n+1) + (n+1))) as [[He1|He1]|He1];
+        autorewrite with natb; try lia; eauto.
+    + symmetry. apply Nat.odd_spec. by econstructor.
+Qed.
diff --git a/theories/examples/folly_queue/singleElementQueue.v b/theories/examples/folly_queue/singleElementQueue.v
new file mode 100644
index 0000000000000000000000000000000000000000..ad60984448a683a811d23e6d6446494330241ec4
--- /dev/null
+++ b/theories/examples/folly_queue/singleElementQueue.v
@@ -0,0 +1,216 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl auth gset.
+From reloc Require Import reloc.
+From reloc.prelude Require Export arith.
+From reloc.examples.folly_queue Require Export set turnSequencer.
+
+Definition enqueueWithTicket : val := λ: "this" "ticket" "v",
+  let: "t" := Fst "this" in
+  let: "r" := Snd "this" in
+  let: "turn" := "ticket" * #2 in
+  waitForTurn "t" "turn";;
+  "r" <- SOME "v";;
+  completeTurn "t" "turn".
+
+Definition getSome : val := λ: "r",
+  match: !"r" with
+    NONE => errorE (* Error *)
+  | SOME "x" => "r" <- NONE;; "x"
+  end.
+
+Definition dequeueWithTicket : val := λ: "this" "ticket",
+  let: "t" := Fst "this" in
+  let: "r" := Snd "this" in
+  let: "turn" := ("ticket" * #2) + #1 in
+  waitForTurn "t" "turn";;
+  let: "v" := getSome "r" in
+  completeTurn "t" "turn";;
+  "v".
+
+(* The single-element queue used by the MPMC queue. *)
+Definition newSEQ : val := λ: <>,
+  let: "r" := ref NONE in
+  let: "t" := newTS #() in
+  ("t", "r").
+
+(* Code for a single element queue that manages tickets itself. *)
+Definition enqueue : val := rec: "enqueue" "t" "r" "ticket_" "v" :=
+  let: "ticket" := FAA "ticket_" #1 in
+  enqueueWithTicket ("t", "r") "ticket" "v".
+
+Definition dequeue : val := rec: "dequeue" "t" "r" "ticket_" <> :=
+  let: "ticket" := FAA "ticket_" #1 in
+  dequeueWithTicket ("t","r") "ticket".
+
+Definition newQueue : val := λ: <>,
+  let: "popTicket" := ref #0 in
+  let: "pushTicket" := ref #0 in
+  let: "r" := ref NONE in
+  let: "t" := newTS #() in
+  (λ: "v", enqueue "t" "r" "pushTicket" "v", λ: <>, dequeue "t" "r" "popTicket" #()).
+
+(* Alternative spec for the TS. *)
+Section spec.
+  Context `{!relocG Σ, !TSG Σ}.
+
+  Definition Nseq : namespace := nroot .@ "SEQ".
+
+  (* R is the resource that the single element queue protects. The i'th dequeue
+     is sure to get a value, v, that satisfies R i v. *)
+  Implicit Type R : nat → val → iProp Σ.
+
+  (* The resource for the turn sequencer. *)
+  Definition TSR R (ℓ : loc) (n : nat) : iProp Σ :=
+    (if even n
+     then ℓ ↦ NONEV
+     else ∃ v, ℓ ↦ SOMEV v ∗ R ((n - 1) / 2) v)%I.
+
+  Definition isSEQ (γ : gname) R (v : val) : iProp Σ :=
+    ∃ ts (ℓ : loc), ⌜v = (ts, #ℓ)%V⌝ ∗ isTS γ (TSR R ℓ) ts.
+
+  Definition enqueue_turns γ n := own γ (set_even_drop n).
+  Definition dequeue_turns γ n := own γ (set_odd_drop n).
+  Definition enqueue_turn γ n := own γ (set_singleton (2 * n)).
+  Definition dequeue_turn γ n := own γ (set_singleton (2 * n + 1)).
+
+  Lemma enqueue_turns_take γ n :
+    enqueue_turns γ n ⊣⊢ enqueue_turns γ (n + 1) ∗ enqueue_turn γ n.
+  Proof. by rewrite -own_op -set_even_drop_singleton. Qed.
+
+  Lemma dequeue_turns_take γ n :
+    dequeue_turns γ n ⊣⊢ dequeue_turns γ (n + 1) ∗ dequeue_turn γ n.
+  Proof. by rewrite -own_op -set_odd_drop_singleton. Qed.
+
+  Lemma newSEQ_spec (v : val) R :
+    {{{ True }}} newSEQ v {{{ γ v, RET v; isSEQ γ R v ∗ enqueue_turns γ 0 ∗ dequeue_turns γ 0 }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ".
+    wp_rec.
+    wp_alloc â„“ as "pts". wp_pures.
+    wp_apply (ts_mk_spec (TSR R â„“) with "pts").
+    iIntros (γ ts) "[Hts turns]".
+    wp_pures.
+    iApply ("HΦ" $! γ).
+    iSplitL "Hts". { iExists _, _. iFrame. done. }
+    rewrite /turns_from /enqueue_turns /dequeue_turns.
+    rewrite set_above_zero.
+    rewrite split_even_odd.
+    rewrite set_even_drop_zero.
+    rewrite set_odd_drop_zero.
+    rewrite own_op.
+    by iFrame.
+  Qed.
+
+  (* For the [lia] tactic. *)
+  (* To support Z.div, Z.modulo, Z.quot, and Z.rem: *)
+  Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+
+  Lemma enqueueWithTicket_spec' γ R v x n :
+  {{{ isSEQ γ R v ∗ enqueue_turn γ n ∗ R n x }}}
+    enqueueWithTicket v #n x
+  {{{ RET #(); True }}}.
+  Proof. 
+    iIntros (Φ) "(isSEQ & Hturn & HR) HΦ".
+    iDestruct "isSEQ" as (ts â„“) "[-> #Hts]".
+    wp_rec.
+    wp_pures.
+    assert ((n * 2)%Z = (2 * n)%nat) as ->. { lia. }
+    wp_apply (wait_spec with "[$Hts Hturn]"); first done.
+    iIntros "[Htsr Hclose]".
+    iEval (rewrite /TSR) in "Htsr".
+    wp_pures.
+    assert (Nat.even (2 * n) = true) as ->.
+    { apply Nat.even_spec, Even_mul2. }
+    wp_store.
+    wp_apply (complete_spec with "[Hclose HR Htsr]").
+    { simpl. iFrame "#∗".
+      rewrite /TSR.
+      assert (Nat.even (n + (n + 0) + 1) = false) as ->.
+      { replace (n + (n + 0) + 1) with (S (2 * n)) by lia.
+        rewrite Nat.even_succ. rewrite -Nat.negb_even.
+        assert (Nat.even (2 * n) = true) as ->; last done.
+        apply Nat.even_spec. apply Even_mul2. }
+      iExists _. iFrame.
+      replace (n + (n + 0) + 1 - 1) with (n * 2) by lia.
+      rewrite Nat.div_mul; last done.
+      done. }
+    iAssumption.
+  Qed.
+ 
+  Lemma dequeueWithTicket_spec' γ R v n :
+  {{{ isSEQ γ R v ∗ dequeue_turn γ n }}}
+    dequeueWithTicket v #n
+  {{{ v, RET v; R n v }}}.
+  Proof.
+    iIntros (Φ) "(isSEQ & Hturn) HΦ".
+    iDestruct "isSEQ" as (ts â„“) "[-> #Hts]".
+    wp_rec. wp_pures.
+    assert ((n * 2 + 1)%Z = (2 * n + 1)%nat) as -> by lia.
+    wp_apply (wait_spec with "[$Hts Hturn]"); first done.
+    iIntros "[Htsr Hclose]".
+    rewrite /getSome. wp_pures.
+    iEval (rewrite /TSR) in "Htsr".
+    rewrite Nat.add_0_r.
+    assert (Nat.even (2 * n + 1) = false) as ->.
+    { replace (2 * n + 1) with (S (2 * n)) by lia.
+      rewrite Nat.even_succ. rewrite -Nat.negb_even.
+      assert (Nat.even (2 * n) = true) as ->; last done.
+      apply Nat.even_spec. apply Even_mul2. }
+    iDestruct "Htsr" as (v) "[pts HR]".
+    wp_load.
+    wp_store. wp_pures.
+    wp_apply (complete_spec with "[Hclose pts]").
+    { iFrame "#∗".
+      replace (n + n + 1 + 1) with (2 * (n + 1)) by lia.
+      replace (n + n + 1) with (2 * n + 1) by lia.
+      rewrite /TSR.
+      assert (Nat.even _ = true) as ->.
+      { apply Nat.even_spec. apply Even_mul2. }
+      by iFrame. }
+    iIntros "_".
+    wp_pures.
+    iApply "HΦ".
+    replace (2 * n + 1 - 1) with (n * 2) by lia.
+    rewrite Nat.div_mul; last done.
+    by iFrame.
+  Qed.
+
+  Lemma dequeueWithTicket_spec2 (γ : gname) R (v : val) (n : nat) (Φ : val → iPropI Σ) :
+    isSEQ γ R v ∗ dequeue_turn γ n
+    -∗ ▷ (∀ v0 : val, R n v0 ={⊤}=∗ ▷ Φ v0 )
+      -∗ WP dequeueWithTicket v #n {{ v, Φ v }}.
+  Proof.
+    iIntros "(isSEQ & Hturn) HΦ".
+    iDestruct "isSEQ" as (ts â„“) "[-> #Hts]".
+    wp_rec. wp_pures.
+    assert ((n * 2 + 1)%Z = (2 * n + 1)%nat) as -> by lia.
+    wp_apply (wait_spec with "[$Hts Hturn]"); first done.
+    iIntros "[Htsr Hclose]".
+    rewrite /getSome. wp_pures.
+    iEval (rewrite /TSR) in "Htsr".
+    rewrite Nat.add_0_r.
+    assert (Nat.even (2 * n + 1) = false) as ->.
+    { replace (2 * n + 1) with (S (2 * n)) by lia.
+      rewrite Nat.even_succ. rewrite -Nat.negb_even.
+      assert (Nat.even (2 * n) = true) as ->; last done.
+      apply Nat.even_spec. apply Even_mul2. }
+    iDestruct "Htsr" as (v) "[pts HR]".
+    wp_load.
+    wp_store. wp_pures.
+    wp_apply (complete_spec with "[Hclose pts]").
+    { iFrame "#∗".
+      replace (n + n + 1 + 1) with (2 * (n + 1)) by lia.
+      replace (n + n + 1) with (2 * n + 1) by lia.
+      rewrite /TSR.
+      assert (Nat.even _ = true) as ->.
+      { apply Nat.even_spec. apply Even_mul2. }
+      by iFrame. }
+    iIntros "_".
+    replace (2 * n + 1 - 1) with (n * 2) by lia.
+    rewrite Nat.div_mul; last done.
+    iMod ("HΦ" $! v with "HR") as "HI".
+    wp_pures.
+    by iFrame.
+  Qed.
+
+End spec.
diff --git a/theories/examples/folly_queue/ticketLock.v b/theories/examples/folly_queue/ticketLock.v
new file mode 100644
index 0000000000000000000000000000000000000000..80e367618a56fd7bf291eca5fa6b2540d885ee1d
--- /dev/null
+++ b/theories/examples/folly_queue/ticketLock.v
@@ -0,0 +1,103 @@
+(* A ticket lock using a turn sequencer *)
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth excl cmra agree frac gset.
+From reloc Require Import reloc.
+From reloc.examples.folly_queue Require Import set turnSequencer.
+
+Definition newlock : val := λ: <>,
+  let: "turn" := ref #0 in
+  let: "t" := newTS #() in
+  ("t", "turn").
+Definition acquire : val := rec: "acquire" "l" :=
+  let: "t" := Fst "l" in
+  let: "turn" := Snd "l" in
+  let: "ct" := !"turn" in
+  if: CAS "turn" "ct" ("ct" + #1)
+  then waitForTurn "t" "ct";; "ct"
+  else "acquire" "l".
+Definition release : val := λ: "l" "ct",
+  let: "t" := Fst "l" in
+  completeTurn "t" "ct".
+
+Section contents.
+  Context `{!relocG Σ, !TSG Σ}.
+
+  Context (N' : namespace).
+  Context (R : iProp Σ).
+
+  Definition N := N'.@"N".
+  Definition LN := N'.@"ticketLock".
+
+  Definition lock_inv_body (γTS : gname) turn : iProp Σ :=
+    (∃ (n : nat), turn ↦ #n ∗ turns_from γTS n)%I.
+  Definition lock_inv (γTS : gname) (ts : val) (turn : loc) : iProp Σ :=
+    (isTS γTS (fun _ => R) ts ∗
+           inv LN (lock_inv_body γTS turn))%I.
+  Definition locked ts n := complete ts n.
+
+  Lemma newlock_spec :
+    {{{ R }}}
+      newlock #()
+    {{{ ts turn γTS, RET (ts, #turn); lock_inv γTS ts turn }}}.
+  Proof.
+    iIntros (Φ) "HR HΦ".
+    unlock newlock. wp_rec.
+    wp_alloc turn as "Hturn". wp_let.
+    (* iMod (own_alloc ((● Excl' 0) ⋅ (◯ Excl' 0))) as (γ) "[Hγ HP]". *)
+    (* { by apply auth_both_valid_discrete. } *)
+    wp_bind (newTS #()).
+    iApply (ts_mk_spec (fun _ => R)%I with "HR").
+    iNext. iIntros (γTS ts) "[#Hts Hturns]".
+    iMod (inv_alloc LN _ (lock_inv_body γTS turn) with "[Hturn Hturns]") as "#Hinv".
+    { iNext. iExists 0. by iFrame. }
+    wp_pures.
+    iApply "HΦ". rewrite /lock_inv. by iFrame "Hts Hinv".
+  Qed.
+
+  Lemma turns_take γ m : turns_from γ m -∗ turns_from γ (m + 1) ∗ turn γ m.
+  Proof. by rewrite /turns_from /turn -own_op comm -take_first. Qed.
+
+  Lemma acquire_spec γTS ts (turn : loc) :
+    {{{ lock_inv γTS ts turn }}}
+      acquire (ts, #turn)
+    {{{ n, RET #n; locked ts n ∗ R }}}.
+  Proof.
+    iIntros (Φ) "#[Hts Hlinv] HΦ".
+    wp_pures. iLöb as "IH". wp_rec. wp_pures.
+    wp_bind (! #turn)%E.
+    iInv LN as (n) "(Hturn & Htickets)" "Hcl".
+    wp_load.
+    iMod ("Hcl" with "[Hturn Htickets]") as "_".
+    { iNext. iExists _; iFrame. }
+    iModIntro. wp_pures.
+    wp_bind (CmpXchg _ _ _).
+    iInv LN as (n') "(Hturn & Htickets)" "Hcl".
+    destruct (decide (n = n')); subst.
+    - wp_cmpxchg_suc.
+      rewrite turns_take. iDestruct "Htickets" as "[Htickets Hticket]".
+      iMod ("Hcl" with "[Hturn Htickets]") as "_".
+      { iNext. iExists _.
+        rewrite -(Nat2Z.inj_add n' 1).
+        assert (n' + 1 = S n') as -> by lia.
+        by iFrame. }
+      iModIntro. wp_pures.
+      wp_apply (wait_spec with "[$Hts $Hticket]").
+      iIntros "[HR Hcompl]". wp_pures. iApply "HΦ".
+      by iFrame.
+    - wp_cmpxchg_fail. naive_solver.
+      iMod ("Hcl" with "[-HΦ]") as "_".
+      { iNext. iExists _. by iFrame. }
+      iModIntro. wp_pures.
+      by iApply "IH".
+  Qed.
+
+  Lemma release_spec γTS ts (turn : loc) n :
+    {{{ lock_inv γTS ts turn ∗ locked ts n ∗ R }}}
+      release (ts, #turn) #n
+    {{{ RET #(); True }}}.
+  Proof.
+    iIntros (Φ) "[#[Hts Hlinv] [Hlk HR]] HΦ".
+    wp_pures. wp_rec. wp_pures.
+    by iApply (complete_spec with "[$Hts $Hlk $HR]").
+  Qed.
+End contents.
diff --git a/theories/examples/folly_queue/turnSequencer.v b/theories/examples/folly_queue/turnSequencer.v
new file mode 100644
index 0000000000000000000000000000000000000000..7a4c87da42bc837dc79367dd1f8814aa8f74aa4a
--- /dev/null
+++ b/theories/examples/folly_queue/turnSequencer.v
@@ -0,0 +1,153 @@
+From iris.algebra Require Import auth excl cmra agree frac gset.
+From reloc Require Import reloc.
+From reloc.lib Require Import lock.
+From reloc.examples.folly_queue Require Import set.
+
+(** * Implementation *)
+
+Notation errorE := (#0 #1). (* This gets stuck *)
+
+(* Turn Sequencer with simple spinning. Ignoring arithmetic, shifter turns and use of futex. *)
+
+Definition newTS : val := λ: <>, ref #0.
+
+Definition completeTurn : val :=
+  rec: "complete" "state_" "turn" :=
+    let: "state" := !"state_" in
+    if: ("state" ≠ "turn")
+    then errorE
+    else "state_" <- ("turn" + #1).
+
+Definition waitForTurn : val :=
+  rec: "wait" "state_" "turn" :=
+    let: "state" := !"state_" in
+    if: ("state" = "turn") then #()
+    else if: ("turn" < "state") then errorE
+         else "wait" "state_" "turn".
+
+Definition turnSequencer : val :=
+  (newTS, completeTurn, waitForTurn).
+
+Class TSG Σ := { TSG_tickets :> inG Σ (setUR nat) }.
+
+(* Alternative spec for the TS. *)
+Section spec.
+  Context `{!relocG Σ, !TSG Σ}.
+
+  Implicit Types R : nat → iProp Σ.
+
+  Definition N : namespace := nroot .@ "TS".
+
+
+  Definition turn γ n := own γ (set_singleton n).
+
+  Definition turns_from γ n := own γ (set_above n).
+
+  Definition turns γ n := own γ (set_upto n).
+
+  Lemma turns_add γ m : turns γ m -∗ turn γ m -∗ turns γ (m + 1).
+  Proof.
+    iIntros "T S". iCombine "S T" as "T". by rewrite set_upto_singleton.
+  Qed.
+
+  Definition complete v (n : nat) : iProp Σ :=
+    (∃ ℓ : loc, ⌜v = #ℓ⌝ ∗ ℓ ↦{#1/2} #n)%I.
+
+  Definition TS_inv γ R ℓ : iProp Σ :=
+    ∃ (n : nat), ℓ ↦{#1/2} #n ∗ turns γ n ∗ (R n ∗ complete #ℓ n ∨ turn γ n).
+
+  Definition isTS (γ : gname) R v := (∃ ℓ : loc, ⌜v = #ℓ⌝ ∗ inv N (TS_inv γ R ℓ))%I.
+
+  Lemma ts_mk_spec R :
+   {{{ R 0 }}} newTS #() {{{ γ v, RET v; isTS γ R v ∗ turns_from γ 0 }}}.
+  Proof.
+    iIntros (Ï•) "Hr HÏ•".
+    wp_rec.
+    iApply wp_fupd.
+    wp_alloc â„“ as "[â„“Pts â„“Pts']".
+    iMod (own_alloc (set_above 0)) as (γ) "Hturns"; first done.
+    iMod (own_unit (setUR nat)) as "H".
+    iMod (inv_alloc N _ (TS_inv γ R ℓ)%I with "[-Hϕ Hturns] ") as "HI".
+    { iNext. iExists 0. unfold turns.
+      rewrite -set_upto_zero.
+      iFrame "â„“Pts H". iLeft. iFrame "Hr". iExists _; eauto with iFrame. }
+    iApply "HÏ•".
+    iModIntro. iFrame "Hturns". iExists _. iSplit; eauto with iFrame.
+  Qed.
+
+  Lemma wait_spec γ R v n :
+   {{{ isTS γ R v ∗ turn γ n }}} waitForTurn v #n {{{ RET #(); R n ∗ complete v n }}}.
+  Proof.
+    iLöb as "IH".
+    iIntros (Ï•) "[#Hts Ht] HÏ•".
+    iDestruct "Hts" as (â„“ ->) "#Hinv".
+    wp_rec.
+    wp_pures.
+    wp_bind (! _)%E.
+    iInv N as (m) "(>â„“Pts & Hturns & Hdisj)" "Hcl".
+    wp_load.
+    destruct (lt_eq_lt_dec n m) as [[Hle|<-]|Hho].
+    - iDestruct (own_valid_2 with "Hturns Ht") as %HI%set_upto_singleton_valid.
+      exfalso. lia.
+    - iDestruct "Hdisj" as "[[Hr â„“Pts'] | Ht']"; last first.
+      { by iDestruct (own_valid_2 with "Ht Ht'") as %?%set_singleton_invalid. }
+      iMod ("Hcl" with "[Ht â„“Pts Hturns]") as "_".
+      { iNext. iExists _. iFrame. }
+      iModIntro. wp_pures.
+      rewrite bool_decide_true //. wp_pures.
+      iApply "HÏ•". by iFrame.
+    - iMod ("Hcl" with "[-HÏ• Ht]") as "_".
+      { iNext. iExists _. iFrame. }
+      iModIntro. wp_pures.
+      case_bool_decide; simplify_eq; first lia.
+      wp_pures.
+      rewrite bool_decide_false; last lia.
+      wp_pures.
+      iApply ("IH" with "[$Ht]"); last done.
+      { iExists _. eauto with iFrame. }
+  Qed.
+
+  Lemma complete_spec γ R v n :
+    {{{ isTS γ R v ∗ R (n + 1) ∗ complete v n }}} completeTurn v #n {{{ RET #(); True }}}.
+  Proof.
+    iIntros (Ï•) "(#Hts & Hr & Hc) HÏ•".
+    wp_rec.
+    wp_pures.
+    wp_bind (! _)%E.
+    iDestruct "Hts" as (â„“ ->) "#Hinv".
+    iDestruct "Hc" as (â„“1 ?) "Hc".
+    simplify_eq/=.
+    iInv N as (m) "(>â„“Pts & >Hturns & [(_ & >Hc')|Ht])" "Hcl".
+    { rewrite /complete.
+      iDestruct "Hc'" as (â„“1' ?) "Hc'".
+      simplify_eq/=.
+      iCombine "â„“Pts Hc'" as "â„“Pts".
+      iDestruct (mapsto_valid_2 with "â„“Pts Hc") as %[?%Qp_not_add_le_l _].
+      done. }
+    wp_load.
+    iDestruct (mapsto_agree with "â„“Pts Hc") as %[= Heq].
+    iMod ("Hcl" with "[Ht â„“Pts Hturns]") as "_".
+    { iNext. iExists m. iFrame. }
+    iModIntro. wp_pures. simplify_eq/=.
+    rewrite bool_decide_true //.
+    wp_pures.
+    iInv N as (m) "(>â„“Pts & >Hturns & [(_ & >Hc')|>Ht])" "Hcl".
+    { rewrite /complete.
+      iDestruct "Hc'" as (â„“1' ?) "Hc'".
+      simplify_eq/=.
+      iCombine "â„“Pts Hc'" as "â„“Pts".
+      iDestruct (mapsto_valid_2 with "â„“Pts Hc") as %[?%Qp_not_add_le_l _].
+      done. }
+    iDestruct (mapsto_combine with "â„“Pts Hc") as "[â„“Pts %Heq]".
+    simplify_eq/=.
+    rewrite dfrac_op_own Qp_half_half.
+    wp_store.
+    assert ((n + 1)%Z = (n + 1)%nat) as ->. { lia. }
+    iDestruct "â„“Pts" as "[â„“Pts â„“Pts']".
+    iDestruct (turns_add with "Hturns Ht") as "Hturns".
+    iMod ("Hcl" with "[-HÏ•]") as "_".
+    { iNext. iExists (n + 1). iFrame. iLeft. iFrame. iExists _; eauto with iFrame. }
+    iModIntro. by iApply "HÏ•".
+  Qed.
+
+End spec.
diff --git a/theories/examples/red_blue_flag.v b/theories/examples/red_blue_flag.v
new file mode 100644
index 0000000000000000000000000000000000000000..076ff67eda1d6a6ef4dd53f05cb3b9ea3f869c1f
--- /dev/null
+++ b/theories/examples/red_blue_flag.v
@@ -0,0 +1,437 @@
+(* This example considers two implementations of a concurrent flag. That is, a
+   single "bit" with a flip operation and a read operation.
+
+   The example demonstrates how to handle an _external_ linearization points in
+   ReLoC.
+
+   The specification uses a lock to guard the critical section in flip.
+
+   This example is from "Logical Relations for Fine-Grained Concurrency". *)
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth excl cmra agree frac gset csum.
+From reloc Require Import reloc lib.lock.
+
+(* blueFlag - the specification *)
+
+Definition blueFlip : val := λ: "flag" "lock",
+  acquire "lock" ;;
+  "flag" <- ~ !"flag" ;;
+  release "lock".
+
+Definition blueRead : val := λ: "flag", !"flag".
+
+Definition blueFlag : val :=  λ: <>,
+  let: "flag" := ref #true in
+  let: "lock" := newlock #() in
+  (λ: <>, blueRead "flag",
+   λ: <>, blueFlip "flag" "lock").
+
+(* redFlag - the implementation *)
+
+(* The value of the side channel represents:
+   0 - No one is using the side channel.
+   1 - An offer is made on the side channel.
+   2 - An offer was accepted. *)
+
+Definition redFlip : val := λ: "flag" "chan",
+  rec: "try" <> :=
+    if: CAS "chan" #1 #2 then #() else (* Take an offer. *)
+    if: CAS "flag" #true #false then #() else (* LP if this succeeds. *)
+    if: CAS "flag" #false #true then #() else (* LP if this succeeds. *)
+    if: CAS "chan" #0 #1 (* Make an offer. This is _not_ LP but when someone takes the offer our LP is during the execution of "someone". *)
+    then (if: CAS "chan" #1 #0 then "try" #() else "chan" <- #0;; #()) (* Did someone take our offer? *)
+    else "try" #().
+
+Definition redRead : val :=
+  λ: "flag" <>, ! "flag".
+
+Definition redFlag : val :=  λ: <>,
+  let: "flag" := ref #true in
+  let: "chan" := ref #0 in
+  (redRead "flag", redFlip "flag" "chan").
+
+
+Definition offer : Type := Qp * gname * (list ectx_item).
+Definition offerR :=
+  csumR (exclR unitR)
+        (prodR fracR (agreeR ref_idO)).
+
+Class offerPreG Σ := OfferPreG {
+  offer_inG :> inG Σ offerR;
+  offer_token_inG :> inG Σ fracR;
+}.
+
+Section offer_theory.
+  Context `{!relocG Σ, !lockG Σ, !offerPreG Σ}.
+
+  Definition no_offer γ := own γ (Cinl (Excl ())).
+
+  Definition offer_elm (q : Qp) k : offerR := Cinr (q, to_agree k).
+
+  Definition own_offer γ q k := own γ (offer_elm q k).
+
+  Definition half_offer γ k := own_offer γ (1/2) k.
+
+  Definition quarter_offer γ k := own_offer γ (1/4) k.
+
+  (* Global Instance no_offer_exclusive' : Exclusive (Cinl (Excl ()) : offerR).
+  Proof. apply _. Qed.  *)
+
+  Lemma no_offer_alloc : ⊢ |==> ∃ γ, no_offer γ.
+  Proof. by iApply own_alloc. Qed.
+
+  Lemma own_offer_valid γ q k : (own_offer γ q k -∗ ⌜(q ≤ 1)%Qp⌝).
+  Proof.
+    iIntros "Hown".
+    rewrite /own_offer /offer_elm.
+    iDestruct (own_valid with "Hown") as %[Hown _].
+    done.
+  Qed.
+
+  Lemma no_offer_exclusive γ q k : no_offer γ -∗ own_offer γ q k -∗ False.
+  Proof. iIntros "O P". by iDestruct (own_valid_2 with "O P") as %?. Qed.
+
+  Lemma no_offer_to_offer γ k : no_offer γ ==∗ own_offer γ 1 k.
+  Proof.
+    iIntros "O".
+    iMod (own_update with "O") as "$"; last done.
+    by apply cmra_update_exclusive.
+  Qed.
+
+  Lemma offer_to_no_offer γ k : own_offer γ 1 k ==∗ no_offer γ.
+  Proof.
+    iIntros "O".
+    iMod (own_update with "O") as "$"; last done.
+    by apply cmra_update_exclusive.
+  Qed.
+
+  Lemma offer_agree γ q q' k k' :
+    own_offer γ q k -∗ own_offer γ q' k' -∗ ⌜k = k'⌝.
+  Proof.
+    iIntros "O P".
+    iDestruct (own_valid_2 with "O P") as %[_ ?%to_agree_op_inv]%pair_valid.
+    by unfold_leibniz.
+  Qed.
+
+  (** TODO: Implement Fractional and AsFractional instances *)
+  Lemma offer_split γ q q' k :
+    own_offer γ (q + q') k ⊣⊢ own_offer γ q k ∗ own_offer γ q' k.
+  Proof.
+    rewrite -own_op /own_offer.
+    rewrite /offer_elm.
+    rewrite -Cinr_op -pair_op.
+    rewrite frac_op.
+    by rewrite agree_idemp.
+  Qed.
+
+  Lemma offer_combine γ q q' k k' :
+    own_offer γ q k -∗ own_offer γ q' k' -∗ ⌜k = k'⌝ ∗ own_offer γ (q + q') k.
+  Proof.
+    iIntros "O P".
+    iDestruct (offer_agree with "O P") as %<-.
+    repeat iSplit; first done.
+    iCombine "O P" as "O".
+    rewrite -Cinr_op -pair_op frac_op.
+    by rewrite agree_idemp.
+  Qed.
+
+  Lemma half_offer_combine γ k k' :
+    half_offer γ k -∗ half_offer γ k' ==∗ ⌜k = k'⌝ ∗ no_offer γ.
+  Proof.
+    iIntros "O P".
+    iDestruct (offer_agree with "O P") as %<-.
+    iMod (own_update_2 _ _ _  (Cinl (Excl ())) with "O P") as "O".
+    { rewrite -Cinr_op -pair_op frac_op Qp_half_half.
+      apply cmra_update_exclusive. done. }
+    iModIntro. iFrame. done.
+  Qed.
+
+  Lemma no_offer_to_offers γ k : no_offer γ ==∗ own_offer γ (3/4) k ∗ quarter_offer γ k.
+  Proof.
+    iIntros "O".
+    iMod (no_offer_to_offer with "O") as "O".
+    rewrite -{1}Qp_three_quarter_quarter.
+    iDestruct (offer_split with "O") as "[Hhalf Hhalf']".
+    iModIntro. iFrame.
+  Qed.
+
+End offer_theory.
+
+Section proofs.
+  Context `{!relocG Σ, !lockG Σ, !offerPreG Σ}.
+
+  Definition offer_token γ q := own γ (q : frac).
+
+  Lemma offer_token_split γ : own γ 1%Qp ⊣⊢ own γ (1/2)%Qp ∗ own γ (1/2)%Qp.
+  Proof. rewrite -{1}Qp_half_half. rewrite -own_op. done. Qed.
+
+  (* The specification thread `k` is about to run a flip. *)
+  Definition tp_flip k bf lk := (refines_right k (blueFlip #bf lk))%I.
+
+  (* The specification thread `k` is done flipping. *)
+  Definition tp_flip_done k := (refines_right k (of_val #()))%I.
+
+  (** The offer invariant *)
+  Definition I_offer γ γ' (l : loc) bf lk : iProp Σ := ∃ (n : nat),
+    l ↦ #n ∗
+    (⌜n = 0⌝ ∗ offer_token γ' 1 ∗ no_offer γ (* No offer, everyone is free to make one. *)
+    ∨ (∃ k, (* The side channel is being used. *)
+          ⌜n = 1⌝ ∗ own_offer γ (1/2) k ∗ (refines_right k (blueFlip #bf lk)) (* An offer is made. *)
+        ∨ ⌜n = 2⌝ ∗ (own_offer γ (1/2) k ∗ (refines_right k #()) ∨ offer_token γ' (1/2)))). (* An offer is accepted. *)
+
+  Definition I γ γ' (rf bf chan : loc) lk : iProp Σ :=
+    ∃ (b : bool),
+      is_locked_r lk false ∗
+      rf ↦ #b ∗ bf ↦ₛ #b ∗
+      I_offer γ γ' chan bf lk.
+
+  Definition iN := nroot .@ "invariant".
+
+  (* When you take an offer you have to step whoever made the offer's
+     specification thread forward. *)
+  Lemma take_offer_l γ γ' l bf lk E t A K :
+    (|={⊤, E}=> ▷ I_offer γ γ' l bf lk ∗
+      ▷ ((I_offer γ γ' l bf lk -∗ REL fill K (of_val #false) << t @ E : A)
+        ∧ (∀ k, tp_flip k bf lk -∗ (tp_flip_done k -∗ I_offer γ γ' l bf lk) -∗
+            REL fill K (of_val #true) << t @ E : A))) -∗
+    REL fill K (CAS #l #1 #2) << t : A.
+  Proof.
+    iIntros "Hlog".
+    rel_cmpxchg_l_atomic.
+    iMod "Hlog" as "(Hoff & Hcont)".
+    iDestruct "Hoff" as (n) "[lPts Hdisj]".
+    iModIntro. iExists _. iFrame "lPts". iSplit.
+    - iIntros (Hneq).
+      iNext. iIntros "lPts".
+      rel_pures_l.
+      iDestruct "Hcont" as "[Hcont _]".
+      iApply "Hcont".
+      iExists _. iFrame.
+    - iIntros ([= Heq]).
+      iNext. iIntros "lPts".
+      iDestruct "Hdisj" as "[[% _] | Hdisj]"; first by subst.
+      iDestruct "Hdisj" as (k) "[(_ & Hoff & Hs) | [% _]]"; last by subst.
+      iDestruct "Hcont" as "[_ Hcont]".
+      rel_pures_l.
+      iApply ("Hcont" with "Hs").
+      iIntros "HI". iExists 2. iFrame "lPts".
+      iRight. iExists _. iRight. iFrame. iSplit; first done. iLeft. iFrame.
+  Qed.
+
+  Lemma blue_refines_red :
+    ⊢ REL redFlag << blueFlag : () → (() → lrel_bool) * (() → ()).
+  Proof.
+    rewrite /redFlag /blueFlag.
+    rel_arrow_val. iIntros (?? [-> ->]).
+    rel_pures_l.
+    rel_pures_r.
+    (* Implementation initialization. *)
+    rel_alloc_l rf as "rfPts".
+    rel_alloc_l chan as "chanPts".
+    rel_pures_l.
+    (* Specification initialization. *)
+    rel_alloc_r bf as "bfPts".
+    rel_pures_r.
+    rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
+    do 2 rel_pure_r.
+    (* Allocate the invariant. *)
+    iMod no_offer_alloc as (γ) "Hno".
+    iMod (own_alloc (1%Qp)) as (γ') "Htok"; first done.
+    iMod (inv_alloc iN _ (I γ γ' rf bf chan lk) with "[-]") as "#Hinv".
+    { iNext. iFrame. iExists _. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
+    iApply refines_pair.
+
+    (* Refines read. *)
+    - rel_rec_l.
+      rel_arrow_val. iIntros (?? [-> ->]).
+      rel_pures_l.
+      rel_pures_r.
+      rel_load_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & chanPts)" "Hclose".
+      iExists _. iFrame "rfPts". iModIntro. iNext. iIntros "rfPts".
+      rel_rec_r.
+      rel_load_r.
+      iMod ("Hclose" with "[-]") as "_".
+      { iNext. iExists _. iFrame. }
+      rel_values.
+
+    (* Refines flip. *)
+    - rel_rec_l.
+      rel_pures_l.
+      rel_pures_r.
+      rel_arrow_val. iIntros (?? [-> ->]).
+      fold blueFlip.
+      rel_pures_r.
+      iLöb as "IH".
+      rel_pures_l.
+
+      (* The first CAS. *)
+      rel_apply_l take_offer_l.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iModIntro. iFrame "Hchan". iNext. iSplit.
+      (* Taking the offer succeeded. *)
+      2: {
+        iIntros (j) "Hj Hrest".
+
+        (* Step our specification forward for our LP. *)
+        rewrite /blueFlip.
+        rel_pures_r.
+        rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
+        rel_load_r.
+        rel_store_r.
+        rel_pures_r.
+        rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
+
+        (* Step the other thread's spec forward for their LP. *)
+        rewrite /tp_flip /tp_flip_done.
+        tp_rec j. tp_pures j.
+        (* Handle the acquire. *)
+        tp_rec j.
+        rewrite /is_locked_r. iDestruct "Hlk" as (lk' ->) "Hl".
+        tp_cmpxchg_suc j.
+        tp_pures j.
+        tp_load j.
+        tp_pures j.
+        tp_store j.
+        tp_pures j.
+        tp_rec j. tp_store j.
+        rewrite negb_involutive.
+
+        iDestruct ("Hrest" with "Hj") as "Hoff".
+        iMod ("Hclose" with "[-]") as "_".
+        { iNext. iExists _. iFrame. rewrite /is_locked_r. iExists _. iFrame. done. }
+        rel_pures_l.
+        rel_values. }
+      iIntros "Hoff".
+      iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+      rel_pures_l.
+
+      (* The second CAS. *)
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iExists _. iFrame "rfPts". iModIntro. iSplit.
+      2: {
+        iIntros ([= ->]). iNext. iIntros "rfPts".
+        rel_pures_l.
+        rel_rec_r.
+        rel_pures_r.
+        rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
+        rel_load_r.
+        rel_store_r.
+        rel_pures_r.
+        rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
+        iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+        rel_values. }
+      iIntros (_). iNext. iIntros "rfPts".
+      iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+      rel_pures_l.
+
+      (* The third CAS. *)
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iExists _. iFrame "rfPts". iModIntro. iSplit.
+      2: {
+        iIntros ([= ->]). iNext. iIntros "rfPts".
+        rel_pures_l.
+        rel_rec_r.
+        rel_pures_r.
+        rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
+        rel_load_r.
+        rel_store_r.
+        rel_pures_r.
+        rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
+        iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+        rel_values. }
+      iIntros (_). iNext. iIntros "rfPts".
+      iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+      rel_pures_l.
+
+      (* ALTERNATIVE fourth CAS. *)
+      iApply refines_split.
+      iIntros (k) "Hk".
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iDestruct "Hchan" as (n) "[>chanPts Hdisj]".
+      iModIntro. iExists _. iFrame. iSplit.
+      { (* If the CAS fails we didn't succeed in making and offer, we recurse
+           and use the IH. *)
+        iIntros (Heq). simplify_eq/=.
+        iNext. iIntros "Hchan".
+        iMod ("Hclose" with "[-IH Hk]") as "_".
+        { iNext. iExists _. iFrame. iExists _. iFrame. }
+        iApply (refines_combine with "[] Hk").
+        do 2 rel_pure_l _.
+        iApply "IH". }
+
+      iIntros (Heq). simplify_eq/=.
+      assert (n = 0) as -> by lia.
+      iNext. iIntros "Hchan".
+      iDestruct "Hdisj" as "[(_ & Htok & Hoff) | Hdisj]".
+      2: { iDestruct "Hdisj" as (?) "[[% _]|[% _]]"; by subst. }
+      iMod (no_offer_to_offer _ k  with "Hoff") as "Hoff".
+      iEval (rewrite -Qp_half_half) in "Hoff".
+      iDestruct (offer_split with "Hoff") as "[Hoff Hoff']".
+      iMod ("Hclose" with "[-IH Hoff Htok]") as "_".
+      { iNext. iExists _. iFrame. iExists 1. iFrame. iRight. iExists k. iLeft. by iFrame. }
+      rel_pures_l.
+
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iDestruct "Hchan" as (n) "[>chanPts Hdisj]".
+      iModIntro. iExists _. iFrame "chanPts". iSplit.
+      2: { (* Revoking the offer succeeded. *)
+        iIntros (?) "!> Hchan". simplify_eq/=.
+        assert (n = 1) as -> by lia.
+        iDestruct "Hdisj" as "[[% _] | Hdisj]"; first by subst.
+        iDestruct "Hdisj" as (?) "[(% & Hoff' & Hj) | [% _]]"; last by subst.
+        iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+        rewrite Qp_half_half.
+        iMod (offer_to_no_offer with "Hoff") as "Hoff".
+        iMod ("Hclose" with "[-IH Hj]") as "_".
+        { iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. by iFrame. }
+        do 2 rel_pure_l _.
+        iApply (refines_combine with "[] Hj").
+        iApply "IH". }
+
+      iIntros (Heq2) "!> Hchan".
+      iDestruct "Hdisj" as "[(% & _ & Hoff') | Hdisj]".
+      { iDestruct (no_offer_exclusive with "Hoff' Hoff") as %?. done. }
+      iDestruct "Hdisj" as (?) "[[% _] | (% & Hdisj)]"; first by subst.
+      iDestruct "Hdisj" as "[[Hoff' Hj] | Hoff']".
+      2: {
+        iDestruct (own_valid_2 with "Htok Hoff'") as %Hv.
+        by apply Qp_not_add_le_l in Hv. }
+      iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+      iDestruct (offer_token_split with "Htok") as "[Htok Htok']".
+      iMod ("Hclose" with "[-IH Hj Hoff Htok]") as "_".
+      { iNext. iExists _. iFrame. iExists n. iFrame. iRight.
+        iExists k. iRight. by iFrame. }
+      rel_pures_l.
+
+      (* Clean up the offer. *)
+      rel_store_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iDestruct "Hchan" as (m) "[>chanPts Hdisj]".
+      iModIntro. iExists _. iFrame "chanPts". iNext.
+      iIntros "chanPts".
+      iDestruct "Hdisj" as "[(_ & _ & Hoff') | Hdisj]".
+      { iDestruct (no_offer_exclusive with "Hoff' Hoff") as %?. done. }
+      iDestruct "Hdisj" as (?) "[(_ & Hoff' & _) | (% & Hdisj)]".
+      { iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+        rewrite Qp_half_half.
+        iDestruct (own_offer_valid with "Hoff") as %Hle.
+        by apply Qp_not_add_le_l in Hle. }
+      iDestruct "Hdisj" as "[[Hoff' _] | Htok']".
+      { iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+        rewrite Qp_half_half.
+        iDestruct (own_offer_valid with "Hoff") as %Hle.
+        by apply Qp_not_add_le_l in Hle. }
+      iCombine "Htok Htok'" as "Htok".
+      iEval (rewrite Qp_half_half) in "Hoff".
+      iMod (offer_to_no_offer with "Hoff") as "Hoff".
+      iMod ("Hclose" with "[-IH Hj]") as "_".
+      { iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
+      iApply (refines_combine with "[] Hj"). rel_pures_l. rel_values.
+  Qed.
+
+End proofs.
diff --git a/theories/prelude/arith.v b/theories/prelude/arith.v
new file mode 100644
index 0000000000000000000000000000000000000000..84ea7e73445a3ba5eef271a19286926cfbf13db3
--- /dev/null
+++ b/theories/prelude/arith.v
@@ -0,0 +1,124 @@
+(** Some arithmetical facts that we use in the MPMC queue case study *)
+From Coq Require Import ssreflect.
+From stdpp Require Import prelude base.
+
+(* TODO: move to std++? *)
+Lemma false_Is_true: ∀ b : bool, ¬ b →  b = false.
+Proof.
+  intros b Hb.
+  by apply negb_true_iff, Is_true_eq_true, negb_prop_intro.
+Qed.
+
+(* Even/odd *)
+Lemma Even_mul2 k : Nat.Even (2 * k).
+Proof.
+  assert (2 * k = 0 + 2 * k) as -> by lia.
+  apply Nat.even_spec.
+  by rewrite Nat.even_add_mul_2.
+Qed.
+Lemma Odd_mul2 k : ¬ Nat.Odd (2 * k).
+Proof.
+  assert (2 * k = 0 + 2 * k) as -> by lia.
+  rewrite -Nat.odd_spec.
+  by rewrite Nat.odd_add_mul_2.
+Qed.
+Lemma Odd_succ k : Nat.Odd (2 * k + 1).
+Proof.
+  assert (2 * k + 1 = 1 + 2 * k) as -> by lia.
+  apply Nat.odd_spec.
+  by rewrite Nat.odd_add_mul_2.
+Qed.
+Lemma even_succ k : ¬ Nat.even (S (2 * k)).
+Proof.
+  assert (S (2 * k) = 1 + 2 * k) as -> by lia.
+  apply negb_prop_elim.
+  by rewrite Nat.even_add_mul_2.
+Qed.
+Lemma even_lift k : Nat.Even k ↔ Nat.even k.
+Proof.
+  split; intro.
+  - by apply Is_true_eq_left, Nat.even_spec.
+  - by apply Nat.even_spec, Is_true_eq_true.
+Qed.
+Lemma odd_lift k : Nat.Odd k ↔ Nat.odd k.
+Proof.
+  split; intro.
+  - by apply Is_true_eq_left, Nat.odd_spec.
+  - by apply Nat.odd_spec, Is_true_eq_true.
+Qed.
+Lemma Even_succ k : ¬ Nat.Even (S (2 * k)).
+Proof. rewrite even_lift. apply even_succ. Qed.
+
+Lemma even_odd_case x :
+  (Nat.even x = true /\ exists z, x = 2 * z) \/
+  (Nat.even x = false /\ exists z, x = S (2 * z)).
+Proof.
+  induction x as [|x].
+  - left. split; eauto.
+  - destruct IHx as [[IHx [z ->]]|[IHx [z ->]]]; [right|left].
+    + split; last eauto.
+      apply false_Is_true.
+      rewrite -even_lift.
+      apply Even_succ.
+    + split.
+      * assert (S (S (2 * z)) = 2 * (S z)) as -> by lia.
+        apply Is_true_eq_true.
+        rewrite -even_lift.
+        apply Even_mul2.
+      * exists (S z). lia.
+Qed.
+
+Lemma even_odd_spec n :
+  (Nat.even n = true ∧ Nat.odd n = false) ∨ (Nat.even n = false ∧ Nat.odd n = true).
+Proof.
+  destruct (Nat.Even_or_Odd n) as [H%Nat.even_spec|H%Nat.odd_spec].
+  - left. split; first done. by rewrite -Nat.negb_even H.
+  - right. split; last done. by rewrite -Nat.negb_odd H.
+Qed.
+
+Lemma ltb_lt_1 n m : n < m → (n <? m) = true.
+Proof. apply ltb_lt. Qed.
+
+(* This is just [Nat.mul_comm] with things ordered differently. *)
+Lemma div_mod' (x y : nat) : y ≠ 0 →  (x `div` y) * y + x `mod` y = x.
+Proof. symmetry. rewrite Nat.mul_comm. apply Nat.div_mod. done. Qed.
+
+(* why is there an extra condition in Nat.mod_0_l? *)
+Lemma mod0 (a : nat) : 0 `mod` a = 0.
+Proof.
+  destruct a; first done.
+  by apply Nat.mod_0_l.
+Qed.
+Lemma div0 (a : nat) : 0 `div` a = 0.
+Proof.
+  destruct a; first done.
+  by apply Nat.div_0_l.
+Qed.
+
+
+Lemma set_seq_take_start `{SemiSet nat C} (start len1 len2 : nat) :
+  len2 <= len1 →
+  set_seq (C:=C) start len1 ≡ (set_seq start len2) ∪ (set_seq (start + len2) (len1 - len2)).
+Proof. intros Hle. set_solver by lia. Qed.
+
+Lemma set_seq_take_start_L `{SemiSet nat C, !LeibnizEquiv C} (start len1 len2 : nat) :
+  len2 <= len1 →
+  set_seq (C:=C) start len1 = (set_seq start len2) ∪ (set_seq (start + len2) (len1 - len2)).
+Proof. set_solver by lia. Qed.
+
+Lemma drop_nth {B : Type} i m (x : B) xs : drop i m = x :: xs → m !! i = Some x.
+Proof.
+  generalize dependent m.
+  induction i as [|? IH]; intros m.
+  - rewrite drop_0. intros ->. done.
+  - destruct m; first done. rewrite skipn_cons. apply IH.
+Qed.
+
+Lemma drop_ge_2 {B : Type} (l : list B) n : drop n l = [] → length l ≤ n.
+Proof.
+  generalize dependent l.
+  induction n as [|? IH]; intros l.
+  - destruct l; done.
+  - destruct l; simpl; first lia. intros H%IH. lia.
+Qed.
+