.gitignore

@@ -14,7 +14,7 @@
 .coqdeps.d
 .coq-native/
 _opam
-build-dep/
+builddep/
 Makefile.coq
 Makefile.coq.conf
 .Makefile.coq.d

.gitlab-ci.yml

@@ -5,6 +5,7 @@ stages:
 
 variables:
   CPU_CORES: "10"
+  OCAML: "ocaml-base-compiler.4.14.0"
 
 .template: &template
   stage: build
@@ -27,11 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.13.0:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.0"
-    DENY_WARNINGS: "1"
+    OPAM_PINS: "coq version 8.20.0"
   tags:
   - fp-timing
 
@@ -40,7 +40,7 @@ trigger-iris.dev:
   variables:
     STDPP_REPO: "iris/stdpp"
     IRIS_REPO: "iris/iris"
-    OPAM_PINS: "coq version 8.13.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   except:
   only:
   - triggers

Makefile

-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
+# Default target
 all: Makefile.coq
-	+@make -f Makefile.coq all
+	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Permit local customization
+-include Makefile.local
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
+
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq .lia.cache
+	+@$(MAKE) -f Makefile.coq clean
+	@# Make sure not to enter the `_opam` folder.
+	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq .lia.cache builddep/*
 .PHONY: clean
 
 # Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep/opam: opam Makefile
-	@echo "# Creating build-dep package."
-	@mkdir -p build-dep
-	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
-	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
-
-build-dep: build-dep/opam phony
-	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install the build-deps now, but to also keep satisfying these
 	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
 	@# that are incompatible with our build requirements.
 	@# To achieve this, we create a fake opam package that has our build-dependencies as
 	@# dependencies, but does not actually install anything itself.
-	@echo "# Installing build-dep package."
-	@opam install $(OPAMFLAGS) build-dep/
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
 
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
 
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+# Some files that do *not* need to be forwarded to Makefile.coq.
+# ("::" lets Makefile.local overwrite this.)
+Makefile Makefile.local _CoqProject $(OPAMFILES):: ;

README.md

@@ -10,7 +10,7 @@ See the small ReLoC [docs/guide.md](docs/guide.md) and the Iris [ProofGuide.md](
 
 ## Building
 
-This project has been tested with Coq 8.13.0.
+This project has been tested with Coq 8.20.0.
 
 ### OPAM
 
@@ -43,13 +43,14 @@ they can illustrate the usage of the logic.
   + `bit.v` - "representation independence example" for a simple bit interface
   + `or.v` - expressing non-determinism with concurrency
   + `symbol.v` and `namegen.v` - generative ADTs for symbol and name generation
-  + `stack/refinement.v` - Treiber stack refines sequential stack
+  + `stack` - Treiber stack refines sequential stack
   + `cell.v` - higher-order cell objects
   + `ticket_lock.v` - ticket lock refines spin lock
   + `various.v` - lots of examples with higher-order functions with local state, in the style of "The effects of higher-order state and control on local relational reasoning" paper
   + `coinflip.v` and `lateearlychoice.v` - examples with prophecy variable
+  + `stack_helping` - linearizability of stack with helping, see [this technical appendix](https://cs.ru.nl/~dfrumin/reloc/tech-appendix.pdf) for a detailed description
+  + `folly_queue` - linearizability of the MPMC queue from the Folly library
 - `experimental` more "experimental" stuff
-  + `helping/helping_stack.v` - linearizability of stack with helping, see [this technical appendix](https://cs.ru.nl/~dfrumin/reloc/tech-appendix.pdf) for a detailed description
   + `hocap/` - hocap style specifications for a concurrent counter and a refinement proof for a ticket lock
   + `cka.v` - some axioms from the CKA equational theory
 

_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,13 +54,23 @@ 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/par.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/stack_helping/offers.v
+theories/examples/stack_helping/stack.v
+theories/examples/stack_helping/helping_wrapper.v
 
-theories/experimental/cka.v
 
-theories/experimental/helping/offers.v
-theories/experimental/helping/helping_stack.v
+theories/examples/par.v
+theories/experimental/cka.v
 
 theories/experimental/hocap/counter.v
 theories/experimental/hocap/ticket_lock.v

opam → coq-reloc.opam

-opam-version: "1.2"
-name: "coq-reloc"
+opam-version: "2.0"
 maintainer: "Ralf Jung <jung@mpi-sws.org>"
 authors: "Dan Frumin, Robbert Krebbers"
 homepage: "http://iris-project.org/"
 bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
-dev-repo: "https://gitlab.mpi-sws.org/dfrumin/reloc.git"
-build: [make "-j%{jobs}%"]
-install: [make "install"]
-remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
+dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
+
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-06-18.0.366d607e") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]

theories/examples/bit.v

 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** A simple bit module *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc Require Import reloc.
 Set Default Proof Using "Type".
 

theories/examples/coinflip.v

@@ -103,13 +103,11 @@ Section proofs.
         rel_store_l; repeat rel_pure_l.
       + rel_apply_r (refines_rand_r (extract_bool vs)).
         rel_store_r.
-        rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs. iFrame. iLeft. iFrame. }
+        rel_apply_l (refines_release_l with "Hlk Hlocked [$]").
         iNext. rel_values.
       + rel_apply_r (refines_rand_r (extract_bool vs)).
         rel_store_r.
-        rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs. iFrame. iLeft. iFrame. }
+        rel_apply_l (refines_release_l with "Hlk Hlocked [$]").
         iNext. rel_values.
   Qed.
 
@@ -130,13 +128,12 @@ Section proofs.
            (∃ (b : bool), is_locked_r lk false
                         ∗ ce ↦ #b
                         ∗ (cl ↦ₛ NONEV ∨ cl ↦ₛ SOMEV #b))%I
-            with "[-]") as "#Hinv".
-    { iNext. iExists false. iFrame. }
+            with "[$]") as "#Hinv".
     iApply refines_pair.
     - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
       rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
       rel_load_l_atomic. iInv coinN as (b) "(Hlk & Hce & H)" "Hclose".
-      iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
+      iModIntro. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
       rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
       repeat rel_pure_r.
       iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r.
@@ -144,28 +141,24 @@ Section proofs.
         rel_store_r. repeat rel_pure_r.
         rel_resolveproph_r. repeat rel_pure_r.
         rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
       + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
     - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
       rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
       rel_apply_l refines_rand_l. iNext. iIntros (b).
       rel_store_l_atomic. iInv coinN as (b') "(Hlk & Hce & H)" "Hclose".
-      iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
+      iModIntro. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
       rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
       repeat rel_pure_r.
       iDestruct "H" as "[Hcl|Hcl]"; rel_store_r; repeat rel_pure_r.
       + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
       + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
   Qed.
 
@@ -205,11 +198,11 @@ Section proofs.
         rel_apply_r (refines_rand_r b). repeat rel_pure_r.
         rel_cmpxchg_suc_r. repeat rel_pure_r.
         rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs'. iFrame. iRight. iExists b. iFrame. }
+        { iExists vs'. iFrame. iRight. iFrame. }
         iNext. repeat rel_pure_l; rel_values.
       + repeat rel_pure_r.
         rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs. iFrame. iRight. iExists x. iFrame. }
+        { iExists vs. iFrame. iRight. iFrame. }
         iNext. repeat rel_pure_l; rel_values.
     - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
       rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
@@ -244,7 +237,7 @@ Section proofs.
           ∗ (c' ↦ₛ NONEV ∗ c ↦ NONEV
             ∨ ∃ (b : bool), c' ↦ₛ SOMEV #b ∗ c ↦ SOMEV #b))%I
             with "[-]") as "#Hinv".
-    { iNext. iFrame. iRight. iExists false. iFrame. }
+    { iNext. iFrame. iRight. iFrame. }
     do 2 rel_pure_r.
 
     iApply refines_pair.
@@ -275,7 +268,7 @@ Section proofs.
           { eauto with iFrame. }
           rel_values.
         * iDestruct "H" as (x) "[Hc' Hc]".
-          iModIntro; iExists _. iFrame. iSplit; last first.
+          iModIntro; iFrame. iSplit; last first.
           { iIntros (?); simplify_eq/=. }
           iIntros (_). iNext. iIntros "Hc".
           rel_pures_l.
@@ -283,7 +276,7 @@ Section proofs.
           { eauto with iFrame. }
           iApply "IH".
       + iClear "IH".
-        iDestruct "H" as (b) "[Hc' Hc]". iExists _. iFrame. iNext. iIntros "Hc".
+        iDestruct "H" as (b) "[Hc' Hc]". iFrame. iNext. iIntros "Hc".
         repeat rel_pure_l.
         rel_apply_r (refines_acquire_r with "Hlk").
         iIntros "Hlk". repeat rel_pure_r. rel_load_r.
@@ -297,7 +290,7 @@ Section proofs.
       repeat rel_rec_l. repeat rel_rec_r. repeat rel_pure_l. repeat rel_pure_r.
       rel_store_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose";
         iModIntro.
-      + iExists _. iFrame. iNext. iIntros "Hc".
+      + iFrame. iNext. iIntros "Hc".
         rel_apply_r (refines_acquire_r with "Hlk").
         iIntros "Hlk". repeat rel_pure_r. rel_store_r.
         repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").
@@ -306,7 +299,7 @@ Section proofs.
         { eauto with iFrame. }
         rel_values.
       + iDestruct "H" as (x) "[Hc' Hc]".
-        iExists _. iFrame. iNext. iIntros "Hc".
+        iFrame. iNext. iIntros "Hc".
         rel_apply_r (refines_acquire_r with "Hlk").
         iIntros "Hlk". repeat rel_pure_r. rel_store_r.
         repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").

theories/examples/folly_queue/CG_queue.v

+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.

theories/examples/folly_queue/README.md

+# 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

theories/examples/folly_queue/mpmcqueue.v

+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").

theories/examples/folly_queue/refinement.v

+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_mono.
+
+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.
+
+Global Program Instance Op_Nat_mod : BinOp Nat.modulo :=
+  {| TBOp := Z.modulo ; TBOpInj := Nat2Z.inj_mod |}.
+Add Zify BinOp Op_Nat_mod.
+
+Global 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 length_app /= Nat.add_1_r.
+    rewrite seq_S /=.
+    rewrite zip_with_app /=.
+    2: { by rewrite length_seq. }
+    rewrite list_to_map_snoc; first done.
+    rewrite fst_zip. 2: { rewrite length_seq. 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 (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_pointsto γ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_pointsto γl (length xs) x.
+  Proof.
+    iIntros "HL".
+    rewrite /ghost_list /ghost_list_pointsto.
+    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 length_seq. done. }
+    rewrite elem_of_list_In.
+    rewrite in_seq. lia.
+  Qed.
+
+  Lemma dom_list_to_map {B : Type} (l : list (nat * B)) :
+    dom (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_pointsto γl i x -∗ ⌜i < length xs⌝.
+  Proof.
+    rewrite /ghost_list /ghost_list_pointsto /list_idx_to_map.
+    iIntros "Ha Hb".
+    iCombine "Ha Hb" gives %[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 length_seq. 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_pointsto γl i x.
+  Proof.
+    iIntros (Hs) "Hlist".
+    rewrite /ghost_list /ghost_list_pointsto /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 length_seq. 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 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".
+    iCombine "Ha Hf" gives %[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_pointsto γ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)%nat.
+
+  (* 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)%nat 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)%nat 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)%nat 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)%nat 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)%nat 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)%nat 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)%nat 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)%nat 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_pointsto γ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 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 mt ⊆ set_seq 0 popTicket →
+    own γm (● mt) ==∗
+    ⌜dom (<[ 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.
+    auto.
+  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.
+        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 length_app. 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 length_app. simpl. lia.
+        - apply drop_ge. rewrite length_app. 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.
+        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 iCombine "Htok Htok'" gives %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.
+        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.
+        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.
+      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.

theories/examples/folly_queue/set.v

+From stdpp Require Import base decidable.
+From iris.algebra Require Import numbers cmra excl stepindex_finite.
+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 Nat.even.
+Definition set_odd := set_cf Nat.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 ->%Nat.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 *)
+Global Hint Rewrite ltb_lt_1 using lia : natb.
+Global Hint Rewrite leb_correct_conv using lia : natb.
+Global Hint Rewrite leb_correct using lia : natb.
+Global Hint Rewrite set_above_lookup using lia : natb.
+Global Hint Rewrite @decide_False using lia : natb.
+Global Hint Rewrite @decide_True using lia : natb.
+Global Hint Rewrite set_above_lookup_none using lia : natb.
+Global Hint Rewrite set_upto_lookup_none using lia : natb.
+Global Hint Rewrite set_upto_lookup using lia : natb.
+Global Hint Rewrite set_singleton_lookup_none using lia : natb.
+Global Hint Rewrite set_singleton_lookup using lia : natb.
+Global Hint Rewrite div_mod' : natb.
+Global Hint Rewrite mod0 : natb.
+Global Hint Rewrite div0 : natb.
+Global Hint Rewrite Nat.add_0_r : natb.
+Global Hint Rewrite Nat.add_0_l : natb.
+Global Hint Rewrite Nat.ltb_irrefl : natb.
+Global Hint Rewrite Nat.max_0_r : natb.
+Global 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').
+  - case_decide; subst; by autorewrite with natb.
+  - 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.
+    assert (m < n ∨ m = n) as [] by lia.
+    * 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', (Nat.even n') && (2 * n <=? n')).
+
+(* All odd numbers except for the first n. *)
+Definition set_odd_drop n := set_cf (λ n', (Nat.odd n') && (2 * n + 1 <=? n')).
+
+Lemma set_even_drop_lookup n m : Nat.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.

theories/examples/folly_queue/singleElementQueue.v

+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 Nat.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.

theories/examples/folly_queue/ticketLock.v

+(* 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.

theories/examples/folly_queue/turnSequencer.v

+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].
+    - iCombine "Hturns Ht" gives %HI%set_upto_singleton_valid.
+      exfalso. lia.
+    - iDestruct "Hdisj" as "[[Hr ℓPts'] | Ht']"; last first.
+      { by iCombine "Ht Ht'" gives %?%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".
+      iCombine "ℓPts Hc" gives %[?%Qp.not_add_le_l _].
+      done. }
+    wp_load.
+    iDestruct (pointsto_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".
+      iCombine "ℓPts Hc" gives %[?%Qp.not_add_le_l _].
+      done. }
+    iDestruct (pointsto_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). eauto with iFrame. }
+    iModIntro. by iApply "Hϕ".
+  Qed.
+
+End spec.

theories/examples/namegen.v

@@ -64,7 +64,7 @@ Section namegen_refinement.
       { iIntros (Hy). destruct Hy as [y Hy].
         rewrite (big_sepS_elem_of _ L (l',y) Hy).
         iDestruct "HL" as "[Hl _]".
-        iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
+        iCombine "Hl Hl'" gives %[Hfoo _].
         compute in Hfoo. eauto. }
       iAssert (⌜(∃ x, (x, S n) ∈ L) → False⌝)%I with "[HL]" as %Hc.
       { iIntros (Hx). destruct Hx as [x Hy].

theories/examples/or.v

@@ -30,7 +30,8 @@ Notation "e1 ⊕ e2" := (or (λ: <>, e1)%V (λ: <>, e2)%V)
                         (at level 60) : val_scope.
 
 Section rules.
-  Context `{relocG Σ}.
+  Context `{!relocG Σ}.
+  Implicit Types e : expr.
 
   (** Symbolic execution rule for the LHS *)
   Definition or_inv x : iProp Σ :=
@@ -260,9 +261,9 @@ Section rules.
     end.
 
   Lemma seq_or_2' (f g h f' g' h' : expr) A :
-    is_closed_expr [] f →
-    is_closed_expr [] g →
-    is_closed_expr [] h →
+    is_closed_expr ∅ f →
+    is_closed_expr ∅ g →
+    is_closed_expr ∅ h →
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
@@ -274,7 +275,7 @@ Section rules.
   Proof.
     iIntros (???) "Hf Hg Hh". rel_pures_r.
     rel_newproph_l vs p as "Hp". repeat rel_pure_l.
-    (rewrite !(subst_is_closed []) //; try by set_solver); [].
+    (rewrite !(subst_is_closed ∅) //; try by set_solver); [].
     rel_apply_r or_refines_r.
     destruct (to_choice vs) as [|] eqn:Hchoice.
     - iLeft. iApply (refines_seq with "Hf").
@@ -297,9 +298,9 @@ Section rules.
 
   (** We then prove that the non-instrumented program refines the original one *)
   Lemma seq_or_2_instrument (f g h f' g' h' : expr) A :
-    is_closed_expr [] f' →
-    is_closed_expr [] g' →
-    is_closed_expr [] h' →
+    is_closed_expr ∅ f' →
+    is_closed_expr ∅ g' →
+    is_closed_expr ∅ h' →
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
@@ -311,7 +312,7 @@ Section rules.
   Proof.
     iIntros (???) "Hf Hg Hh".
     rel_newproph_r p. repeat rel_pure_r.
-    (rewrite !(subst_is_closed []) //; try by set_solver); [].
+    (rewrite !(subst_is_closed ∅) //; try by set_solver); [].
     iApply (refines_seq with "Hf").
     rel_pures_l. rel_pures_r.
     iApply (or_compatible with "[Hg] [Hh]").

theories/examples/par.v

@@ -24,6 +24,7 @@ Notation "e1 ∥ e2" := (((e1;; #()) ||| (e2;; #()));; #())%E
 
 Section rules.
   Context `{!relocG Σ, !spawnG Σ}.
+  Implicit Type e t : expr.
 
   Lemma par_l_2 e1 e2 t :
     (WP e1 {{ _, True }}) -∗
@@ -85,22 +86,35 @@ Section rules.
     rel_pures_l. rel_rec_l.
     rel_pures_l.
     pose (N:=nroot.@"par").
-    rewrite refines_eq /refines_def. iIntros (j K) "#Hspec Hj".
-    iModIntro. wp_bind (spawn _).
-    iApply (spawn_spec N (λ _, j ⤇ fill K #())%I with "[He1 Hj]").
+    iApply refines_split. iIntros (k) "Hk".
+    rel_bind_l (spawn _). iApply refines_wp_l.
+    iApply (spawn_spec N (λ _, refines_right k #())%I with "[He1 Hk]").
     - wp_pures. wp_bind e1.
-      iMod ("He1" with "Hspec Hj") as "He1".
+      rewrite refines_eq /refines_def /=.
+      iMod ("He1" with "Hk") as "He1".
       iApply (wp_wand with "He1").
       iIntros (?)  "P". wp_pures.
-      by iDestruct "P" as (v') "[Hj [-> ->]]".
+      by iDestruct "P" as (v') "[? [-> ->]]".
     - iNext. iIntros (l) "hndl". iSimpl.
-      wp_pures. wp_bind e2.
+      rel_pures_l. rel_bind_l e2.
+      iApply refines_wp_l.
       iApply (wp_wand with "He2"). iIntros (?) "_".
-      wp_pures.
-      wp_apply (join_spec with "hndl").
-      iIntros (?) "Hj". wp_pures. iExists #(). eauto with iFrame.
+      simpl. rel_pures_l. rel_bind_l (spawn.join _).
+      iApply refines_wp_l.
+      iApply (join_spec with "hndl"). iNext.
+      iIntros (?) "Hk". simpl. rel_pures_l. iApply (refines_combine with "[] Hk").
+      rel_values.
   Qed.
 
+  Lemma refines_right_cons k' Ki K e :
+    refines_right (RefId k' (Ki::K)) e =
+    refines_right (RefId k' K) (fill_item Ki e).
+  Proof. rewrite /refines_right /= //. Qed.
+  Lemma refines_right_fill k K e :
+    refines_right k (fill K e) =
+    refines_right (RefId (tp_id k) (K ++ tp_ctx k)) e.
+  Proof. rewrite /refines_right fill_app //. Qed.
+
   Lemma par_l_1' Q K e1 e2 t :
     (REL e1 << t : ()) -∗
     (WP e2 {{ _, Q }}) -∗
@@ -111,27 +125,27 @@ Section rules.
     rel_pures_l. rel_rec_l.
     rel_pures_l.
     pose (N:=nroot.@"par").
-    rewrite {1 3}refines_eq /refines_def. iIntros (j K') "#Hspec Hj".
-    iModIntro. wp_bind (spawn _).
-    iApply (spawn_spec N (λ _, j ⤇ fill (K++K') #())%I with "[He1 Hj]").
+    iApply refines_split. iIntros (k) "Hk".
+    rel_bind_l (spawn _). iApply refines_wp_l.
+    rewrite refines_right_bind.
+    iApply (spawn_spec N (λ _, refines_right k (fill K #()))%I with "[He1 Hk]").
     - wp_pures. wp_bind e1.
-      rewrite -fill_app.
-      iMod ("He1" with "Hspec Hj") as "He1".
+      rewrite refines_eq /refines_def.
+      iMod ("He1" with "Hk") as "He1".
       iApply (wp_wand with "He1").
       iIntros (?)  "P". wp_pures.
-      by iDestruct "P" as (v') "[Hj [-> ->]]".
-    - iNext. iIntros (l) "hndl". iSimpl.
-      wp_pures. wp_bind e2.
+      iDestruct "P" as (v') "[Hj [-> ->]]".
+      by rewrite refines_right_fill.
+    - iNext. iIntros (l) "Hl". simpl.
+      rel_pures_l. rel_bind_l e2.
+      iApply refines_wp_l.
       iApply (wp_wand with "He2"). iIntros (?) "HQ".
-      wp_pures.
-      wp_apply (join_spec with "hndl").
-      iIntros (?) "Hj".
-      iSpecialize ("Ht" with "HQ").
-      rewrite refines_eq /refines_def.
-      rewrite fill_app.
-      iMod ("Ht" with "Hspec Hj") as "Ht".
-      rewrite wp_value_fupd. iMod "Ht" as (?) "[Ht [_ ->]]".
-      wp_pures. iExists #(). eauto with iFrame.
+      simpl. rel_pures_l. rel_bind_l (spawn.join _).
+      iApply refines_wp_l.
+      wp_apply (join_spec with "Hl").
+      iIntros (?) "Hk".
+      iSpecialize ("Ht" with "HQ"). simpl.
+      rel_pures_l. iApply (refines_combine with "Ht Hk").
   Qed.
 
   (* Lemma par_r_1 e1 e2 t (A : lrel Σ) E : *)
@@ -188,8 +202,8 @@ Section rules.
 
   (* This proof is now simpler but it still requires unfolding the REL judgement *)
   Lemma par_comm e1 e2 :
-    is_closed_expr [] e1 →
-    is_closed_expr [] e2 →
+    is_closed_expr ∅ e1 →
+    is_closed_expr ∅ e2 →
     (REL e1 << e1 : ()) -∗
     (REL e2 << e2 : ()) -∗
     REL (e2 ∥ e1) << (e1 ∥ e2) : ().
@@ -202,14 +216,17 @@ Section rules.
     tp_pure i (App _ _). simpl.
     rel_pures_r.
     rel_bind_r e2.
-    iApply refines_spec_ctx. iIntros "#Hs".
-    iApply (par_l_1' (i ⤇ (#c2 <- InjR (#();; #())))%I
+    iApply (par_l_1' (refines_right i (#c2 <- InjR (#();; #())))%I
               with "He2 [He1 Hi]").
     { rewrite refines_eq /refines_def.
       tp_bind i e1.
-      iMod ("He1" with "Hs Hi") as "He1". simpl.
+      rewrite refines_right_bind.
+      iAssert (spec_ctx) with "[Hi]" as "#Hs".
+      { iDestruct "Hi" as "[$ _]". }
+      iMod ("He1" with "Hi") as "He1". simpl.
       iApply (wp_wand with "He1"). iIntros (?).
-      iDestruct 1 as (?) "[Hi [-> ->]]". done. }
+      iDestruct 1 as (?) "[Hi [-> ->]]".
+      rewrite /refines_right. by iFrame. }
     iIntros "Hi". simpl. rel_pures_r.
     tp_pures i. tp_store i.
     rel_rec_r. rel_load_r. rel_pures_r. rel_values.
@@ -229,8 +246,8 @@ Section rules.
   Qed.
 
   Lemma seq_par e1 e2 (A B : lrel Σ) :
-    is_closed_expr [] e1 →
-    is_closed_expr [] e2 →
+    is_closed_expr ∅ e1 →
+    is_closed_expr ∅ e2 →
     (REL e1 << e1 : A) -∗
     (REL e2 << e2 : B) -∗
     REL e1 ;; e2 << (e1 ||| e2)%V : lrel_true.
@@ -242,35 +259,40 @@ Section rules.
     { simpl. eauto. }
     repeat rel_pure_r.
     tp_rec i. simpl.
-    rewrite {3}refines_eq /refines_def.
-    iIntros (j K) "#Hs Hj". iModIntro.
+    rewrite {3}refines_eq /refines_def /=.
+    iIntros (j) "Hj". iModIntro.
     tp_bind j e2. tp_bind i e1.
     (* execute e1 *)
     wp_bind e1. tp_bind i e1.
-    rewrite {1}refines_eq /refines_def.
-    iMod ("He1" with "Hs Hi") as "He1".
+    rewrite !refines_right_fill.
+    rewrite {1}refines_eq /refines_def /=.
+    iMod ("He1" with "Hi") as "He1".
     iApply (wp_wand with "He1"). iIntros (v1).
     iDestruct 1 as (v2) "[Hi Hv]". wp_pures.
     (* execute e2 *)
     rewrite refines_eq /refines_def.
-    iMod ("He2" with "Hs Hj") as "He2".
+    iMod ("He2" with "Hj") as "He2".
     iApply wp_fupd.
     iApply (wp_wand with "He2"). iIntros (w1).
     iDestruct 1 as (w2) "[Hj Hw]".
     iSimpl in "Hi". iSimpl in "Hj".
+    rewrite !refines_right_cons /=.
+    change (RefId (tp_id i) (tp_ctx i)) with i.
+    change (RefId (tp_id j) (tp_ctx j)) with j.
     tp_pure i _.
     tp_store i.
     tp_pures j. tp_rec j.
     tp_load j.
     tp_pures j.
-    iModIntro. iExists _. iFrame.
+    iModIntro. iExists _.
+    by iFrame.
   Qed.
 
   Lemma interchange a b c d (A B C D : lrel Σ) :
-    is_closed_expr [] a →
-    is_closed_expr [] b →
-    is_closed_expr [] c →
-    is_closed_expr [] d →
+    is_closed_expr ∅ a →
+    is_closed_expr ∅ b →
+    is_closed_expr ∅ c →
+    is_closed_expr ∅ d →
     (REL a << a : A) -∗
     (REL b << b : B) -∗
     (REL c << c : C) -∗
@@ -286,45 +308,58 @@ Section rules.
     tp_rec i. simpl.
     rel_rec_l. repeat rel_pure_l.
     rewrite {5}refines_eq /refines_def.
-    iIntros (j K) "#Hs Hj". iModIntro.
+    iIntros (j) "Hj". iModIntro.
     pose (N:=nroot.@"par").
     wp_bind (spawn _).
     iApply (spawn_spec N with "[Ha Hj]").
     - wp_lam. rewrite refines_eq /refines_def.
       tp_bind j a.
-      iMod ("Ha" with "Hs Hj") as "Ha".
+      rewrite refines_right_fill.
+      iMod ("Ha" with "Hj") as "Ha".
       iExact "Ha".
     - iNext. iIntros (h) "Hdl". wp_pures.
       wp_bind b.
       rewrite {1}refines_eq /refines_def.
       tp_bind i b.
-      iMod ("Hb" with "Hs Hi") as "Hb".
+      rewrite refines_right_fill.
+      iMod ("Hb" with "Hi") as "Hb".
       iApply (wp_wand with "Hb").
       iIntros (bv). iDestruct 1 as (bv') "[Hi HB]". simpl.
       wp_pures. wp_bind (spawn.join _).
       iApply (join_spec with "Hdl").
       iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]".
-      wp_pures. tp_pures j. tp_pures i.
+      wp_pures.
+      rewrite !refines_right_cons /=.
+      change (RefId (tp_id i) (tp_ctx i)) with i.
+      change (RefId (tp_id j) (tp_ctx j)) with j.
+      tp_pures j. tp_pures i.
       wp_rec. wp_pures.
       wp_apply (spawn_spec N with "[Hc Hi]").
       { wp_pures.
-        rewrite refines_eq /refines_def.
+        rewrite refines_eq /refines_def /=.
         tp_bind i c.
-        iMod ("Hc" with "Hs Hi") as "Hc". iExact "Hc". }
+        rewrite refines_right_fill.
+        iMod ("Hc" with "Hi") as "Hc".
+        iExact "Hc". }
       clear h. iIntros (h) "Hdl". wp_pures.
       wp_bind d.
       rewrite refines_eq /refines_def.
       tp_bind j d.
-      iMod ("Hd" with "Hs Hj") as "Hd".
+      rewrite refines_right_fill.
+      iMod ("Hd" with "Hj") as "Hd".
       iApply (wp_wand with "Hd"). iIntros (dv).
       iDestruct 1 as (dv') "[Hj HD]".
       wp_pures. wp_apply (join_spec with "Hdl").
       iIntros (cv). iDestruct 1 as (cv') "[Hi HC]".
       iApply wp_fupd.
       wp_pures. iExists (cv', dv')%V. simpl.
+      rewrite !refines_right_cons /=.
+      change (RefId (tp_id i) (tp_ctx i)) with i.
+      change (RefId (tp_id j) (tp_ctx j)) with j.
       tp_pures i. tp_store i.
       tp_pures j.
       rewrite /spawn.join. tp_pures j.
-      tp_load j. tp_pures j. eauto with iFrame.
+      tp_load j. tp_pures j.
+      iModIntro; iSplit; eauto with iFrame.
   Qed.
 End rules.

theories/examples/red_blue_flag.v

+(* 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 iCombine "O P" gives %?. 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".
+    iCombine "O P" gives %[_ ?%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 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 "_".
+        { by iFrame. }
+        rel_pures_l.
+        rel_values. }
+      iIntros "Hoff".
+      iMod ("Hclose" with "[$]") as "_".
+      rel_pures_l.
+
+      (* The second CAS. *)
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      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 "[$]") as "_".
+        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: {
+        iCombine "Htok Hoff'" gives %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. 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.