Merge the Folly queue case study

_CoqProject

@@ -10,6 +10,7 @@ theories/prelude/properness.v
 theories/prelude/asubst.v
 theories/prelude/bijections.v
 theories/prelude/lang_facts.v
+theories/prelude/arith.v
 
 theories/logic/spec_ra.v
 theories/logic/spec_rules.v
@@ -53,6 +54,15 @@ theories/examples/stack/refinement.v
 theories/examples/various.v
 theories/examples/lateearlychoice.v
 theories/examples/coinflip.v
+theories/examples/red_blue_flag.v
+
+theories/examples/folly_queue/set.v
+theories/examples/folly_queue/CG_queue.v
+theories/examples/folly_queue/turnSequencer.v
+theories/examples/folly_queue/singleElementQueue.v
+theories/examples/folly_queue/mpmcqueue.v
+theories/examples/folly_queue/refinement.v
+theories/examples/folly_queue/ticketLock.v
 
 theories/examples/par.v
 theories/experimental/cka.v

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/set.v

+From stdpp Require Import base decidable.
+From iris.algebra Require Import numbers cmra excl.
+From reloc.prelude Require Import arith.
+
+(* A camera of, potentially, infinite sets. Most of the lemmas are about sets of
+   natural numbers. *)
+
+Definition setUR (A : Type) := discrete_funUR (λ (a : A), optionUR (exclR unitO)).
+
+(* Sets of natural numbers. *)
+
+(* Create a set from a characteristic function. *)
+Definition set_cf {A : Type} (f : A → bool) : setUR A :=
+  λ a, if f a then Some (Excl ()) else None.
+
+Definition set_of (A : Type) := @set_cf A (const true).
+
+Definition set_singleton `{!EqDecision A} (a : A) :=
+  set_cf (λ a', if decide (a = a') then true else false).
+
+Definition set_nat := set_of nat.
+Definition set_even := set_cf even.
+Definition set_odd := set_cf odd.
+
+Lemma split_even_odd : set_nat ≡ set_even ⋅ set_odd.
+Proof.
+  intros n. rewrite /set_even /set_odd /set_cf. simpl.
+  rewrite discrete_fun_lookup_op.
+  destruct (even_odd_spec n) as [[-> ->]|[-> ->]]; done.
+Qed.
+
+(* Set of nats including and above n. *)
+Definition set_above n := set_cf (λ n', n <=? n').
+
+Definition set_upto n := set_cf (λ n', n' <? n).
+
+Lemma set_above_lookup n m : n ≤ m → set_above n m = Excl' ().
+Proof. rewrite /set_above /set_cf. by intros ->%leb_le. Qed.
+
+Lemma set_above_lookup_none n m : m < n → (set_above n) m = None.
+Proof. rewrite /set_above /set_cf. by intros ->%Nat.leb_gt. Qed.
+
+Lemma set_upto_lookup n m : m < n → (set_upto n) m = Excl' ().
+Proof. rewrite /set_upto /set_cf. by intros ->%Nat.ltb_lt. Qed.
+
+Lemma set_upto_lookup_none n m : n ≤ m → (set_upto n) m = None.
+Proof. rewrite /set_upto /set_cf. by intros ->%Nat.ltb_ge. Qed.
+
+Lemma set_above_zero : set_above 0 ≡ set_nat.
+Proof. intros n. rewrite set_above_lookup; [done | lia]. Qed.
+
+Lemma set_upto_zero : set_upto 0 ≡ ε.
+Proof.
+  intros n. rewrite /set_upto /set_cf.
+  assert (n <? 0 = false) as ->; last done.
+  apply leb_correct_conv. lia.
+Qed.
+
+Lemma discrete_fun_valid' (s : setUR nat) (n : nat) : ✓ s → ✓ (s n).
+Proof. done. Qed.
+
+Lemma set_singleton_lookup (n : nat) : set_singleton n n = Excl' ().
+Proof. rewrite /set_singleton /set_cf. rewrite decide_True; done. Qed.
+
+Lemma set_singleton_lookup_none (n m : nat) : n ≠ m → set_singleton n m = None.
+Proof.
+  intros H. rewrite /set_singleton /set_cf. rewrite decide_False; done.
+Qed.
+
+Lemma set_singleton_invalid (n : nat) : ¬ ✓ (set_singleton n ⋅ set_singleton n).
+Proof.
+  rewrite /set_singleton /set_cf.
+  intros Hv.
+  pose proof (Hv n) as Hv.
+  rewrite discrete_fun_lookup_op in Hv.
+  rewrite decide_True in Hv; done.
+Qed.
+
+Lemma set_singletons_valid (n m : nat) : ✓ (set_singleton n ⋅ set_singleton m) → n ≠ m.
+Proof.
+  intros Hv ->.
+  by apply set_singleton_invalid in Hv.
+Qed.
+
+(* Rewrite n <? m when true *)
+Hint Rewrite ltb_lt_1 using lia : natb.
+Hint Rewrite leb_correct_conv using lia : natb.
+Hint Rewrite leb_correct using lia : natb.
+Hint Rewrite set_above_lookup using lia : natb.
+Hint Rewrite @decide_False using lia : natb.
+Hint Rewrite @decide_True using lia : natb.
+Hint Rewrite set_above_lookup_none using lia : natb.
+Hint Rewrite set_upto_lookup_none using lia : natb.
+Hint Rewrite set_upto_lookup using lia : natb.
+Hint Rewrite set_singleton_lookup_none using lia : natb.
+Hint Rewrite set_singleton_lookup using lia : natb.
+Hint Rewrite div_mod' : natb.
+Hint Rewrite mod0 : natb.
+Hint Rewrite div0 : natb.
+Hint Rewrite Nat.add_0_r : natb.
+Hint Rewrite Nat.add_0_l : natb.
+Hint Rewrite Nat.ltb_irrefl : natb.
+Hint Rewrite Nat.max_0_r : natb.
+Hint Rewrite Nat.max_0_l : natb.
+
+Lemma set_upto_singleton_valid n m : ✓ (set_upto n ⋅ set_singleton m) → n ≤ m.
+Proof.
+  destruct (le_gt_dec n m); first done.
+  intros Hv.
+  pose proof (Hv m).
+  rewrite discrete_fun_lookup_op in H.
+  rewrite /set_singleton /set_cf in H.
+  autorewrite with natb in H.
+  done.
+Qed.
+
+Lemma take_first n : set_above n ≡ set_singleton n ⋅ set_above (n + 1).
+Proof.
+  intros n'.
+  rewrite /set_singleton. rewrite /set_cf.
+  rewrite discrete_fun_lookup_op.
+  destruct (le_lt_dec n n').
+  - autorewrite with natb.
+    destruct (le_lt_or_eq n n' l); autorewrite with natb; done.
+  - autorewrite with natb. done.
+Qed.
+
+Lemma set_upto_singleton n : set_singleton n ⋅ set_upto n ≡ set_upto (n + 1).
+Proof.
+  intros m.
+  rewrite discrete_fun_lookup_op.
+  destruct (le_gt_dec m n).
+  - rewrite (set_upto_lookup (n + 1)); last lia.
+    destruct (le_lt_or_eq m n l).
+    * autorewrite with natb. done.
+    * subst. autorewrite with natb. done.
+  - autorewrite with natb. done.
+Qed.
+
+(* Create a set from a decidable predicate. *)
+Definition set_prop {A : Type} (f : A → Prop) `{!∀ a, Decision (f a)} : setUR A :=
+  λ a, if decide (f a) then Some (Excl ()) else None.
+
+(* All even numbers except for the first n. *)
+Definition set_even_drop n := set_cf (λ n', (even n') && (2 * n <=? n')).
+
+(* All odd numbers except for the first n. *)
+Definition set_odd_drop n := set_cf (λ n', (odd n') && (2 * n + 1 <=? n')).
+
+Lemma set_even_drop_lookup n m : Even m → 2 * n ≤ m → set_even_drop n m = Excl' ().
+Proof.
+  intros He Hle.
+  rewrite /set_even_drop /set_cf.
+  assert (Nat.even m = true) as -> by by apply Nat.even_spec.
+  rewrite leb_correct; last done.
+  done.
+Qed.
+
+Lemma set_even_drop_zero : set_even_drop 0 ≡ set_even.
+Proof.
+  intros n.
+  rewrite /set_even_drop /set_even /set_cf.
+  destruct (Nat.even n); done.
+Qed.
+
+Lemma set_odd_drop_zero : set_odd_drop 0 ≡ set_odd.
+Proof.
+  intros n.
+  rewrite /set_odd_drop /set_odd /set_cf.
+  destruct n; first done.
+  destruct (Nat.odd (S n)); done.
+Qed.
+
+Lemma set_even_drop_singleton n : set_even_drop n ≡ set_even_drop (n + 1) ⋅ set_singleton (2 * n).
+Proof.
+  intros m.
+  rewrite /set_even_drop /set_singleton /set_cf /=.
+  autorewrite with natb.
+  rewrite discrete_fun_lookup_op.
+  destruct (Nat.Even_or_Odd m) as [[a b]|[a b]].
+  - replace (Nat.even m) with true.
+    + destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He]; autorewrite with natb; eauto.
+    + symmetry. apply Nat.even_spec. by econstructor.
+  - replace (Nat.even m) with false.
+    + by autorewrite with natb.
+    + rewrite -Nat.negb_odd.
+      cut (Nat.odd m = true); first by intros ->.
+      eapply Nat.odd_spec. by econstructor.
+Qed.
+
+Lemma set_odd_drop_singleton n : set_odd_drop n ≡ set_odd_drop (n + 1) ⋅ set_singleton (2 * n + 1).
+Proof.
+  intros m.
+  rewrite /set_odd_drop /set_singleton /set_cf /=.
+  autorewrite with natb.
+  rewrite discrete_fun_lookup_op.
+  destruct (Nat.Even_or_Odd m) as [[a b]|[a b]].
+  - replace (Nat.odd m) with false.
+    + destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He]; autorewrite with natb; eauto.
+    + rewrite -Nat.negb_even.
+      cut (Nat.even m = true); first by intros ->.
+      eapply Nat.even_spec. by econstructor.
+  - replace (Nat.odd m) with true.
+    + destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He];
+        autorewrite with natb; try lia; eauto.
+      destruct (gt_eq_gt_dec m ((n+1) + (n+1))) as [[He1|He1]|He1];
+        autorewrite with natb; try lia; eauto.
+    + symmetry. apply Nat.odd_spec. by econstructor.
+Qed.

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 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].
+    - iDestruct (own_valid_2 with "Hturns Ht") as %HI%set_upto_singleton_valid.
+      exfalso. lia.
+    - iDestruct "Hdisj" as "[[Hr ℓPts'] | Ht']"; last first.
+      { by iDestruct (own_valid_2 with "Ht Ht'") as %?%set_singleton_invalid. }
+      iMod ("Hcl" with "[Ht ℓPts Hturns]") as "_".
+      { iNext. iExists _. iFrame. }
+      iModIntro. wp_pures.
+      rewrite bool_decide_true //. wp_pures.
+      iApply "Hϕ". by iFrame.
+    - iMod ("Hcl" with "[-Hϕ Ht]") as "_".
+      { iNext. iExists _. iFrame. }
+      iModIntro. wp_pures.
+      case_bool_decide; simplify_eq; first lia.
+      wp_pures.
+      rewrite bool_decide_false; last lia.
+      wp_pures.
+      iApply ("IH" with "[$Ht]"); last done.
+      { iExists _. eauto with iFrame. }
+  Qed.
+
+  Lemma complete_spec γ R v n :
+    {{{ isTS γ R v ∗ R (n + 1) ∗ complete v n }}} completeTurn v #n {{{ RET #(); True }}}.
+  Proof.
+    iIntros (ϕ) "(#Hts & Hr & Hc) Hϕ".
+    wp_rec.
+    wp_pures.
+    wp_bind (! _)%E.
+    iDestruct "Hts" as (ℓ ->) "#Hinv".
+    iDestruct "Hc" as (ℓ1 ?) "Hc".
+    simplify_eq/=.
+    iInv N as (m) "(>ℓPts & >Hturns & [(_ & >Hc')|Ht])" "Hcl".
+    { rewrite /complete.
+      iDestruct "Hc'" as (ℓ1' ?) "Hc'".
+      simplify_eq/=.
+      iCombine "ℓPts Hc'" as "ℓPts".
+      iDestruct (mapsto_valid_2 with "ℓPts Hc") as %[?%Qp_not_add_le_l _].
+      done. }
+    wp_load.
+    iDestruct (mapsto_agree with "ℓPts Hc") as %[= Heq].
+    iMod ("Hcl" with "[Ht ℓPts Hturns]") as "_".
+    { iNext. iExists m. iFrame. }
+    iModIntro. wp_pures. simplify_eq/=.
+    rewrite bool_decide_true //.
+    wp_pures.
+    iInv N as (m) "(>ℓPts & >Hturns & [(_ & >Hc')|>Ht])" "Hcl".
+    { rewrite /complete.
+      iDestruct "Hc'" as (ℓ1' ?) "Hc'".
+      simplify_eq/=.
+      iCombine "ℓPts Hc'" as "ℓPts".
+      iDestruct (mapsto_valid_2 with "ℓPts Hc") as %[?%Qp_not_add_le_l _].
+      done. }
+    iDestruct (mapsto_combine with "ℓPts Hc") as "[ℓPts %Heq]".
+    simplify_eq/=.
+    rewrite dfrac_op_own Qp_half_half.
+    wp_store.
+    assert ((n + 1)%Z = (n + 1)%nat) as ->. { lia. }
+    iDestruct "ℓPts" as "[ℓPts ℓPts']".
+    iDestruct (turns_add with "Hturns Ht") as "Hturns".
+    iMod ("Hcl" with "[-Hϕ]") as "_".
+    { iNext. iExists (n + 1). iFrame. iLeft. iFrame. iExists _; eauto with iFrame. }
+    iModIntro. by iApply "Hϕ".
+  Qed.
+
+End spec.

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 iDestruct (own_valid_2 with "O P") as %?. Qed.
+
+  Lemma no_offer_to_offer γ k : no_offer γ ==∗ own_offer γ 1 k.
+  Proof.
+    iIntros "O".
+    iMod (own_update with "O") as "$"; last done.
+    by apply cmra_update_exclusive.
+  Qed.
+
+  Lemma offer_to_no_offer γ k : own_offer γ 1 k ==∗ no_offer γ.
+  Proof.
+    iIntros "O".
+    iMod (own_update with "O") as "$"; last done.
+    by apply cmra_update_exclusive.
+  Qed.
+
+  Lemma offer_agree γ q q' k k' :
+    own_offer γ q k -∗ own_offer γ q' k' -∗ ⌜k = k'⌝.
+  Proof.
+    iIntros "O P".
+    iDestruct (own_valid_2 with "O P") as %[_ ?%to_agree_op_inv]%pair_valid.
+    by unfold_leibniz.
+  Qed.
+
+  (** TODO: Implement Fractional and AsFractional instances *)
+  Lemma offer_split γ q q' k :
+    own_offer γ (q + q') k ⊣⊢ own_offer γ q k ∗ own_offer γ q' k.
+  Proof.
+    rewrite -own_op /own_offer.
+    rewrite /offer_elm.
+    rewrite -Cinr_op -pair_op.
+    rewrite frac_op.
+    by rewrite agree_idemp.
+  Qed.
+
+  Lemma offer_combine γ q q' k k' :
+    own_offer γ q k -∗ own_offer γ q' k' -∗ ⌜k = k'⌝ ∗ own_offer γ (q + q') k.
+  Proof.
+    iIntros "O P".
+    iDestruct (offer_agree with "O P") as %<-.
+    repeat iSplit; first done.
+    iCombine "O P" as "O".
+    rewrite -Cinr_op -pair_op frac_op.
+    by rewrite agree_idemp.
+  Qed.
+
+  Lemma half_offer_combine γ k k' :
+    half_offer γ k -∗ half_offer γ k' ==∗ ⌜k = k'⌝ ∗ no_offer γ.
+  Proof.
+    iIntros "O P".
+    iDestruct (offer_agree with "O P") as %<-.
+    iMod (own_update_2 _ _ _  (Cinl (Excl ())) with "O P") as "O".
+    { rewrite -Cinr_op -pair_op frac_op Qp_half_half.
+      apply cmra_update_exclusive. done. }
+    iModIntro. iFrame. done.
+  Qed.
+
+  Lemma no_offer_to_offers γ k : no_offer γ ==∗ own_offer γ (3/4) k ∗ quarter_offer γ k.
+  Proof.
+    iIntros "O".
+    iMod (no_offer_to_offer with "O") as "O".
+    rewrite -{1}Qp_three_quarter_quarter.
+    iDestruct (offer_split with "O") as "[Hhalf Hhalf']".
+    iModIntro. iFrame.
+  Qed.
+
+End offer_theory.
+
+Section proofs.
+  Context `{!relocG Σ, !lockG Σ, !offerPreG Σ}.
+
+  Definition offer_token γ q := own γ (q : frac).
+
+  Lemma offer_token_split γ : own γ 1%Qp ⊣⊢ own γ (1/2)%Qp ∗ own γ (1/2)%Qp.
+  Proof. rewrite -{1}Qp_half_half. rewrite -own_op. done. Qed.
+
+  (* The specification thread `k` is about to run a flip. *)
+  Definition tp_flip k bf lk := (refines_right k (blueFlip #bf lk))%I.
+
+  (* The specification thread `k` is done flipping. *)
+  Definition tp_flip_done k := (refines_right k (of_val #()))%I.
+
+  (** The offer invariant *)
+  Definition I_offer γ γ' (l : loc) bf lk : iProp Σ := ∃ (n : nat),
+    l ↦ #n ∗
+    (⌜n = 0⌝ ∗ offer_token γ' 1 ∗ no_offer γ (* No offer, everyone is free to make one. *)
+    ∨ (∃ k, (* The side channel is being used. *)
+          ⌜n = 1⌝ ∗ own_offer γ (1/2) k ∗ (refines_right k (blueFlip #bf lk)) (* An offer is made. *)
+        ∨ ⌜n = 2⌝ ∗ (own_offer γ (1/2) k ∗ (refines_right k #()) ∨ offer_token γ' (1/2)))). (* An offer is accepted. *)
+
+  Definition I γ γ' (rf bf chan : loc) lk : iProp Σ :=
+    ∃ (b : bool),
+      is_locked_r lk false ∗
+      rf ↦ #b ∗ bf ↦ₛ #b ∗
+      I_offer γ γ' chan bf lk.
+
+  Definition iN := nroot .@ "invariant".
+
+  (* When you take an offer you have to step whoever made the offer's
+     specification thread forward. *)
+  Lemma take_offer_l γ γ' l bf lk E t A K :
+    (|={⊤, E}=> ▷ I_offer γ γ' l bf lk ∗
+      ▷ ((I_offer γ γ' l bf lk -∗ REL fill K (of_val #false) << t @ E : A)
+        ∧ (∀ k, tp_flip k bf lk -∗ (tp_flip_done k -∗ I_offer γ γ' l bf lk) -∗
+            REL fill K (of_val #true) << t @ E : A))) -∗
+    REL fill K (CAS #l #1 #2) << t : A.
+  Proof.
+    iIntros "Hlog".
+    rel_cmpxchg_l_atomic.
+    iMod "Hlog" as "(Hoff & Hcont)".
+    iDestruct "Hoff" as (n) "[lPts Hdisj]".
+    iModIntro. iExists _. iFrame "lPts". iSplit.
+    - iIntros (Hneq).
+      iNext. iIntros "lPts".
+      rel_pures_l.
+      iDestruct "Hcont" as "[Hcont _]".
+      iApply "Hcont".
+      iExists _. iFrame.
+    - iIntros ([= Heq]).
+      iNext. iIntros "lPts".
+      iDestruct "Hdisj" as "[[% _] | Hdisj]"; first by subst.
+      iDestruct "Hdisj" as (k) "[(_ & Hoff & Hs) | [% _]]"; last by subst.
+      iDestruct "Hcont" as "[_ Hcont]".
+      rel_pures_l.
+      iApply ("Hcont" with "Hs").
+      iIntros "HI". iExists 2. iFrame "lPts".
+      iRight. iExists _. iRight. iFrame. iSplit; first done. iLeft. iFrame.
+  Qed.
+
+  Lemma blue_refines_red :
+    ⊢ REL redFlag << blueFlag : () → (() → lrel_bool) * (() → ()).
+  Proof.
+    rewrite /redFlag /blueFlag.
+    rel_arrow_val. iIntros (?? [-> ->]).
+    rel_pures_l.
+    rel_pures_r.
+    (* Implementation initialization. *)
+    rel_alloc_l rf as "rfPts".
+    rel_alloc_l chan as "chanPts".
+    rel_pures_l.
+    (* Specification initialization. *)
+    rel_alloc_r bf as "bfPts".
+    rel_pures_r.
+    rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
+    do 2 rel_pure_r.
+    (* Allocate the invariant. *)
+    iMod no_offer_alloc as (γ) "Hno".
+    iMod (own_alloc (1%Qp)) as (γ') "Htok"; first done.
+    iMod (inv_alloc iN _ (I γ γ' rf bf chan lk) with "[-]") as "#Hinv".
+    { iNext. iFrame. iExists _. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
+    iApply refines_pair.
+
+    (* Refines read. *)
+    - rel_rec_l.
+      rel_arrow_val. iIntros (?? [-> ->]).
+      rel_pures_l.
+      rel_pures_r.
+      rel_load_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & chanPts)" "Hclose".
+      iExists _. iFrame "rfPts". iModIntro. iNext. iIntros "rfPts".
+      rel_rec_r.
+      rel_load_r.
+      iMod ("Hclose" with "[-]") as "_".
+      { iNext. iExists _. iFrame. }
+      rel_values.
+
+    (* Refines flip. *)
+    - rel_rec_l.
+      rel_pures_l.
+      rel_pures_r.
+      rel_arrow_val. iIntros (?? [-> ->]).
+      fold blueFlip.
+      rel_pures_r.
+      iLöb as "IH".
+      rel_pures_l.
+
+      (* The first CAS. *)
+      rel_apply_l take_offer_l.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iModIntro. iFrame "Hchan". iNext. iSplit.
+      (* Taking the offer succeeded. *)
+      2: {
+        iIntros (j) "Hj Hrest".
+
+        (* Step our specification forward for our LP. *)
+        rewrite /blueFlip.
+        rel_pures_r.
+        rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
+        rel_load_r.
+        rel_store_r.
+        rel_pures_r.
+        rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
+
+        (* Step the other thread's spec forward for their LP. *)
+        rewrite /tp_flip /tp_flip_done.
+        tp_rec j. tp_pures j.
+        (* Handle the acquire. *)
+        tp_rec j.
+        rewrite /is_locked_r. iDestruct "Hlk" as (lk' ->) "Hl".
+        tp_cmpxchg_suc j.
+        tp_pures j.
+        tp_load j.
+        tp_pures j.
+        tp_store j.
+        tp_pures j.
+        tp_rec j. tp_store j.
+        rewrite negb_involutive.
+
+        iDestruct ("Hrest" with "Hj") as "Hoff".
+        iMod ("Hclose" with "[-]") as "_".
+        { iNext. iExists _. iFrame. rewrite /is_locked_r. iExists _. iFrame. done. }
+        rel_pures_l.
+        rel_values. }
+      iIntros "Hoff".
+      iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+      rel_pures_l.
+
+      (* The second CAS. *)
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iExists _. iFrame "rfPts". iModIntro. iSplit.
+      2: {
+        iIntros ([= ->]). iNext. iIntros "rfPts".
+        rel_pures_l.
+        rel_rec_r.
+        rel_pures_r.
+        rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
+        rel_load_r.
+        rel_store_r.
+        rel_pures_r.
+        rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
+        iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+        rel_values. }
+      iIntros (_). iNext. iIntros "rfPts".
+      iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+      rel_pures_l.
+
+      (* The third CAS. *)
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iExists _. iFrame "rfPts". iModIntro. iSplit.
+      2: {
+        iIntros ([= ->]). iNext. iIntros "rfPts".
+        rel_pures_l.
+        rel_rec_r.
+        rel_pures_r.
+        rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
+        rel_load_r.
+        rel_store_r.
+        rel_pures_r.
+        rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
+        iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+        rel_values. }
+      iIntros (_). iNext. iIntros "rfPts".
+      iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+      rel_pures_l.
+
+      (* ALTERNATIVE fourth CAS. *)
+      iApply refines_split.
+      iIntros (k) "Hk".
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iDestruct "Hchan" as (n) "[>chanPts Hdisj]".
+      iModIntro. iExists _. iFrame. iSplit.
+      { (* If the CAS fails we didn't succeed in making and offer, we recurse
+           and use the IH. *)
+        iIntros (Heq). simplify_eq/=.
+        iNext. iIntros "Hchan".
+        iMod ("Hclose" with "[-IH Hk]") as "_".
+        { iNext. iExists _. iFrame. iExists _. iFrame. }
+        iApply (refines_combine with "[] Hk").
+        do 2 rel_pure_l _.
+        iApply "IH". }
+
+      iIntros (Heq). simplify_eq/=.
+      assert (n = 0) as -> by lia.
+      iNext. iIntros "Hchan".
+      iDestruct "Hdisj" as "[(_ & Htok & Hoff) | Hdisj]".
+      2: { iDestruct "Hdisj" as (?) "[[% _]|[% _]]"; by subst. }
+      iMod (no_offer_to_offer _ k  with "Hoff") as "Hoff".
+      iEval (rewrite -Qp_half_half) in "Hoff".
+      iDestruct (offer_split with "Hoff") as "[Hoff Hoff']".
+      iMod ("Hclose" with "[-IH Hoff Htok]") as "_".
+      { iNext. iExists _. iFrame. iExists 1. iFrame. iRight. iExists k. iLeft. by iFrame. }
+      rel_pures_l.
+
+      rel_cmpxchg_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iDestruct "Hchan" as (n) "[>chanPts Hdisj]".
+      iModIntro. iExists _. iFrame "chanPts". iSplit.
+      2: { (* Revoking the offer succeeded. *)
+        iIntros (?) "!> Hchan". simplify_eq/=.
+        assert (n = 1) as -> by lia.
+        iDestruct "Hdisj" as "[[% _] | Hdisj]"; first by subst.
+        iDestruct "Hdisj" as (?) "[(% & Hoff' & Hj) | [% _]]"; last by subst.
+        iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+        rewrite Qp_half_half.
+        iMod (offer_to_no_offer with "Hoff") as "Hoff".
+        iMod ("Hclose" with "[-IH Hj]") as "_".
+        { iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. by iFrame. }
+        do 2 rel_pure_l _.
+        iApply (refines_combine with "[] Hj").
+        iApply "IH". }
+
+      iIntros (Heq2) "!> Hchan".
+      iDestruct "Hdisj" as "[(% & _ & Hoff') | Hdisj]".
+      { iDestruct (no_offer_exclusive with "Hoff' Hoff") as %?. done. }
+      iDestruct "Hdisj" as (?) "[[% _] | (% & Hdisj)]"; first by subst.
+      iDestruct "Hdisj" as "[[Hoff' Hj] | Hoff']".
+      2: {
+        iDestruct (own_valid_2 with "Htok Hoff'") as %Hv.
+        by apply Qp_not_add_le_l in Hv. }
+      iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+      iDestruct (offer_token_split with "Htok") as "[Htok Htok']".
+      iMod ("Hclose" with "[-IH Hj Hoff Htok]") as "_".
+      { iNext. iExists _. iFrame. iExists n. iFrame. iRight.
+        iExists k. iRight. by iFrame. }
+      rel_pures_l.
+
+      (* Clean up the offer. *)
+      rel_store_l_atomic.
+      iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
+      iDestruct "Hchan" as (m) "[>chanPts Hdisj]".
+      iModIntro. iExists _. iFrame "chanPts". iNext.
+      iIntros "chanPts".
+      iDestruct "Hdisj" as "[(_ & _ & Hoff') | Hdisj]".
+      { iDestruct (no_offer_exclusive with "Hoff' Hoff") as %?. done. }
+      iDestruct "Hdisj" as (?) "[(_ & Hoff' & _) | (% & Hdisj)]".
+      { iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+        rewrite Qp_half_half.
+        iDestruct (own_offer_valid with "Hoff") as %Hle.
+        by apply Qp_not_add_le_l in Hle. }
+      iDestruct "Hdisj" as "[[Hoff' _] | Htok']".
+      { iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
+        rewrite Qp_half_half.
+        iDestruct (own_offer_valid with "Hoff") as %Hle.
+        by apply Qp_not_add_le_l in Hle. }
+      iCombine "Htok Htok'" as "Htok".
+      iEval (rewrite Qp_half_half) in "Hoff".
+      iMod (offer_to_no_offer with "Hoff") as "Hoff".
+      iMod ("Hclose" with "[-IH Hj]") as "_".
+      { iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
+      iApply (refines_combine with "[] Hj"). rel_pures_l. rel_values.
+  Qed.
+
+End proofs.

theories/prelude/arith.v

+(** Some arithmetical facts that we use in the MPMC queue case study *)
+From Coq Require Import ssreflect.
+From stdpp Require Import prelude base.
+
+(* TODO: move to std++? *)
+Lemma false_Is_true: ∀ b : bool, ¬ b →  b = false.
+Proof.
+  intros b Hb.
+  by apply negb_true_iff, Is_true_eq_true, negb_prop_intro.
+Qed.
+
+(* Even/odd *)
+Lemma Even_mul2 k : Nat.Even (2 * k).
+Proof.
+  assert (2 * k = 0 + 2 * k) as -> by lia.
+  apply Nat.even_spec.
+  by rewrite Nat.even_add_mul_2.
+Qed.
+Lemma Odd_mul2 k : ¬ Nat.Odd (2 * k).
+Proof.
+  assert (2 * k = 0 + 2 * k) as -> by lia.
+  rewrite -Nat.odd_spec.
+  by rewrite Nat.odd_add_mul_2.
+Qed.
+Lemma Odd_succ k : Nat.Odd (2 * k + 1).
+Proof.
+  assert (2 * k + 1 = 1 + 2 * k) as -> by lia.
+  apply Nat.odd_spec.
+  by rewrite Nat.odd_add_mul_2.
+Qed.
+Lemma even_succ k : ¬ Nat.even (S (2 * k)).
+Proof.
+  assert (S (2 * k) = 1 + 2 * k) as -> by lia.
+  apply negb_prop_elim.
+  by rewrite Nat.even_add_mul_2.
+Qed.
+Lemma even_lift k : Nat.Even k ↔ Nat.even k.
+Proof.
+  split; intro.
+  - by apply Is_true_eq_left, Nat.even_spec.
+  - by apply Nat.even_spec, Is_true_eq_true.
+Qed.
+Lemma odd_lift k : Nat.Odd k ↔ Nat.odd k.
+Proof.
+  split; intro.
+  - by apply Is_true_eq_left, Nat.odd_spec.
+  - by apply Nat.odd_spec, Is_true_eq_true.
+Qed.
+Lemma Even_succ k : ¬ Nat.Even (S (2 * k)).
+Proof. rewrite even_lift. apply even_succ. Qed.
+
+Lemma even_odd_case x :
+  (Nat.even x = true /\ exists z, x = 2 * z) \/
+  (Nat.even x = false /\ exists z, x = S (2 * z)).
+Proof.
+  induction x as [|x].
+  - left. split; eauto.
+  - destruct IHx as [[IHx [z ->]]|[IHx [z ->]]]; [right|left].
+    + split; last eauto.
+      apply false_Is_true.
+      rewrite -even_lift.
+      apply Even_succ.
+    + split.
+      * assert (S (S (2 * z)) = 2 * (S z)) as -> by lia.
+        apply Is_true_eq_true.
+        rewrite -even_lift.
+        apply Even_mul2.
+      * exists (S z). lia.
+Qed.
+
+Lemma even_odd_spec n :
+  (Nat.even n = true ∧ Nat.odd n = false) ∨ (Nat.even n = false ∧ Nat.odd n = true).
+Proof.
+  destruct (Nat.Even_or_Odd n) as [H%Nat.even_spec|H%Nat.odd_spec].
+  - left. split; first done. by rewrite -Nat.negb_even H.
+  - right. split; last done. by rewrite -Nat.negb_odd H.
+Qed.
+
+Lemma ltb_lt_1 n m : n < m → (n <? m) = true.
+Proof. apply ltb_lt. Qed.
+
+(* This is just [Nat.mul_comm] with things ordered differently. *)
+Lemma div_mod' (x y : nat) : y ≠ 0 →  (x `div` y) * y + x `mod` y = x.
+Proof. symmetry. rewrite Nat.mul_comm. apply Nat.div_mod. done. Qed.
+
+(* why is there an extra condition in Nat.mod_0_l? *)
+Lemma mod0 (a : nat) : 0 `mod` a = 0.
+Proof.
+  destruct a; first done.
+  by apply Nat.mod_0_l.
+Qed.
+Lemma div0 (a : nat) : 0 `div` a = 0.
+Proof.
+  destruct a; first done.
+  by apply Nat.div_0_l.
+Qed.
+
+
+Lemma set_seq_take_start `{SemiSet nat C} (start len1 len2 : nat) :
+  len2 <= len1 →
+  set_seq (C:=C) start len1 ≡ (set_seq start len2) ∪ (set_seq (start + len2) (len1 - len2)).
+Proof. intros Hle. set_solver by lia. Qed.
+
+Lemma set_seq_take_start_L `{SemiSet nat C, !LeibnizEquiv C} (start len1 len2 : nat) :
+  len2 <= len1 →
+  set_seq (C:=C) start len1 = (set_seq start len2) ∪ (set_seq (start + len2) (len1 - len2)).
+Proof. set_solver by lia. Qed.
+
+Lemma drop_nth {B : Type} i m (x : B) xs : drop i m = x :: xs → m !! i = Some x.
+Proof.
+  generalize dependent m.
+  induction i as [|? IH]; intros m.
+  - rewrite drop_0. intros ->. done.
+  - destruct m; first done. rewrite skipn_cons. apply IH.
+Qed.
+
+Lemma drop_ge_2 {B : Type} (l : list B) n : drop n l = [] → length l ≤ n.
+Proof.
+  generalize dependent l.
+  induction n as [|? IH]; intros l.
+  - destruct l; done.
+  - destruct l; simpl; first lia. intros H%IH. lia.
+Qed.
+