diff --git a/ProofMode.md b/ProofMode.md
index ed7f788813bfa06bec042d9bace9c9b1b2bc26cd..49a5bb57304acfece56c90818a911b9fa69b673b 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -70,7 +70,11 @@ Elimination of logical connectives
 Separating logic specific tactics
 ---------------------------------
 
-- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. 
+- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. The
+  symbol `★` can be used to frame as much of the spatial context as possible,
+  and the symbol `#` can be used to repeatedly frame as much of the persistent
+  context as possible. When without arguments, it attempts to frame all spatial
+  hypotheses.
 - `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
   `H : P1 ★ P2`.
 
diff --git a/_CoqProject b/_CoqProject
index c2e66758e9d4ff54a1fddf3d1c4b7307d1e86254..1ff1ee86ecf91feccb32341d58118264afb0171a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -85,6 +85,7 @@ program_logic/auth.v
 program_logic/sts.v
 program_logic/namespaces.v
 program_logic/boxes.v
+program_logic/counter_examples.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
@@ -96,6 +97,7 @@ heap_lang/lib/spawn.v
 heap_lang/lib/par.v
 heap_lang/lib/assert.v
 heap_lang/lib/lock.v
+heap_lang/lib/ticket_lock.v
 heap_lang/lib/counter.v
 heap_lang/lib/barrier/barrier.v
 heap_lang/lib/barrier/specification.v
diff --git a/algebra/auth.v b/algebra/auth.v
index 301268fbddbbc9dc9c2ee456528ddd87598f0d5b..d7010787395562e486113d9517a785efdbb438d4 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -241,6 +241,28 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
 Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
 Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
 
+Program Definition authRF (F : urFunctor) : rFunctor := {|
+  rFunctor_car A B := authR (urFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(auth_map_id x).
+  apply auth_map_ext=>y; apply urFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
+  apply auth_map_ext=>y; apply urFunctor_compose.
+Qed.
+
+Instance authRF_contractive F :
+  urFunctorContractive F → rFunctorContractive (authRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+Qed.
+
 Program Definition authURF (F : urFunctor) : urFunctor := {|
   urFunctor_car A B := authUR (urFunctor_car F A B);
   urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
diff --git a/algebra/gset.v b/algebra/gset.v
index 3ae61b0fd28e13e7f9400e3c1ae7443445112a99..f0c1c709950bfb3ca13ae23bb615e2cbb7fea158 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -54,7 +54,6 @@ Section gset.
   Canonical Structure gset_disjUR :=
     discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.
 
-  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Arguments op _ _ _ _ : simpl never.
 
   Lemma gset_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
@@ -68,18 +67,10 @@ Section gset.
     - apply HQ; set_solver by eauto.
     - apply gset_disj_valid_op. set_solver by eauto.
   Qed.
-  Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X :
-    (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
-  Proof.
-    intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
-    intros Y ?; exists (fresh Y); eauto using is_fresh.
-  Qed.
   Lemma gset_alloc_updateP_strong' P X :
     (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
     GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i.
   Proof. eauto using gset_alloc_updateP_strong. Qed.
-  Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
-  Proof. eauto using gset_alloc_updateP. Qed.
 
   Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) :
     (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
@@ -88,15 +79,29 @@ Section gset.
     intros. apply (gset_alloc_updateP_strong P); eauto.
     intros i; rewrite right_id_L; auto.
   Qed.
-  Lemma gset_alloc_empty_updateP (Q : gset_disj K → Prop) :
-    (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
-  Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
   Lemma gset_alloc_empty_updateP_strong' P :
     (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
     GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i.
   Proof. eauto using gset_alloc_empty_updateP_strong. Qed.
-  Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
-  Proof. eauto using gset_alloc_empty_updateP. Qed.
+
+  Section fresh_updates.
+    Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
+
+    Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X :
+      (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
+    Proof.
+      intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
+      intros Y ?; exists (fresh Y); eauto using is_fresh.
+    Qed.
+    Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
+    Proof. eauto using gset_alloc_updateP. Qed.
+
+    Lemma gset_alloc_empty_updateP (Q : gset_disj K → Prop) :
+      (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
+    Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
+    Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
+    Proof. eauto using gset_alloc_empty_updateP. Qed.
+  End fresh_updates.
 
   Lemma gset_alloc_local_update X i Xf :
     i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
diff --git a/algebra/upred.v b/algebra/upred.v
index fe2debbb7902ada73b1a572224e948e0fdba3847..e8404b6c5684dbd39a85d44d6f0558698192dc57 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -371,11 +371,26 @@ Proof.
 Qed.
 Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
 Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
+
+Lemma soundness_later n : ¬ (True ⊢ ▷^n False).
+Proof.
+  unseal. intros [H].
+  assert ((▷^n @uPred_pure_def M False) n ∅)%I as Hn.
+  (* So Coq still has no nice way to say "make this precondition of that lemma a goal"?!? *)
+  { apply H; by auto using ucmra_unit_validN. }
+  clear H. induction n.
+  - done.
+  - move: Hn. simpl. unseal. done.
+Qed.
+Theorem soundness : ¬ (True ⊢ False).
+Proof. exact (soundness_later 0). Qed.
+
 Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
 Proof.
   split; [|by intros [??]; apply (anti_symm (⊢))].
   intros HPQ; split; split=> x i; apply HPQ.
 Qed.
+
 Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q).
 Proof. apply equiv_spec. Qed.
 Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q).
diff --git a/docs/algebra.tex b/docs/algebra.tex
index a970524c14c9d56940cf3b69c2550386d0851549..d6f2de09aa54f52fcc8c1b9f980e216878cdb8af 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -15,7 +15,7 @@ This definition varies slightly from the original one in~\cite{catlogic}.
     \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\
     \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\
     \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\
-    \All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl}
+    \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
   \end{align*}
 \end{defn}
 
@@ -35,7 +35,7 @@ In order to solve the recursive domain equation in \Sref{sec:model} it is also e
   A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} (written $f : \cofe \nfn \cofeB$) if
   \[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
   It is \emph{contractive} if
-  \[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x) \]
+  \[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
 \end{defn}
 Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data.
 Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.
@@ -211,7 +211,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
 \end{defn}
 Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
-\ralf{Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.}
+%TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/docs/logic.tex b/docs/logic.tex
index 95b5adf17c7876cb32563c729388549e6666e147..a7b4dd401e756c02d549bfed91cff0ccd9f052aa 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -135,7 +135,7 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
 Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
 We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
 If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
-\ralf{$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.}
+%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
 
 Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
 This is a \emph{meta-level} assertion about propositions, defined as follows:
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 65de4c44875bb15a58ad31bfb256a225b92706c6..adbcaa6760cf1cb3a74a23e3e8cfe9b6eab36595 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -144,8 +144,17 @@ Section heap.
     by apply pure_elim_r.
   Qed.
 
-  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
-  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
+  Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
+    l ↦{q1} v1 ★ l ↦{q2} v2 ⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
+  Proof. by rewrite heap_mapsto_op. Qed.
+
+  Lemma heap_mapsto_op_half l q v1 v2 :
+    l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q} v1.
+  Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.
+
+  Lemma heap_mapsto_op_half_1 l q v1 v2 :
+    l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊢ v1 = v2 ∧ l ↦{q} v1.
+  Proof. by rewrite heap_mapsto_op_half. Qed.
 
   (** Weakest precondition *)
   (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 879ac67ca45340116ee364ed291821299a213aab..ba12947ad01f07a030a232f256a9fc1f1cdd93dd 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -99,7 +99,7 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
 Proof.
   iIntros (HN) "[#? HΦ]".
   rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
-  iApply "HΦ".
+  iApply ("HΦ" with "|==>[-]").
   iPvs (saved_prop_alloc (F:=idCF) _ P) as (γ) "#?".
   iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
     as (γ') "[#? Hγ']"; eauto.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
new file mode 100644
index 0000000000000000000000000000000000000000..495208d7b3a12ad28554dee62449ce904a64ae46
--- /dev/null
+++ b/heap_lang/lib/ticket_lock.v
@@ -0,0 +1,196 @@
+From iris.program_logic Require Export global_functor auth.
+From iris.proofmode Require Import invariants ghost_ownership.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import gset.
+Import uPred.
+
+Definition wait_loop: val :=
+  rec: "wait_loop" "x" "l" :=
+    let: "o" := Fst !"l" in
+    if: "x" = "o"
+      then #() (* my turn *)
+      else "wait_loop" "x" "l".
+
+Definition newlock : val := λ: <>, ref((* owner *) #0, (* next *) #0).
+Definition acquire : val :=
+  rec: "acquire" "l" :=
+    let: "oldl" := !"l" in
+    if: CAS "l" "oldl" (Fst "oldl", Snd "oldl" + #1)
+      then wait_loop (Snd "oldl") "l"
+      else "acquire" "l".
+
+Definition release : val :=
+  rec: "release" "l" :=
+    let: "oldl" := !"l" in
+    if: CAS "l" "oldl" (Fst "oldl" + #1, Snd "oldl")
+      then #()
+      else "release" "l".
+
+Global Opaque newlock acquire release wait_loop.
+
+(** The CMRAs we need. *)
+Class tlockG Σ := TlockG {
+   tlock_G :> authG heap_lang Σ (gset_disjUR nat);
+   tlock_exclG  :> inG heap_lang Σ (exclR unitC)
+}.
+
+Definition tlockGF : gFunctorList :=
+  [authGF (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
+Instance inGF_tlockG `{H : inGFs heap_lang Σ tlockGF} : tlockG Σ.
+Proof. destruct H as (? & ? & ?). split. apply _. apply: inGF_inG. Qed.
+
+Section proof.
+Context `{!heapG Σ, !tlockG Σ} (N : namespace).
+Local Notation iProp := (iPropG heap_lang Σ).
+
+Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp :=
+  (gs = GSet (seq_set 0 n))%I.
+
+Definition lock_inv (γ1 γ2: gname) (l : loc) (R : iProp) : iProp :=
+  (∃ o n: nat, l ↦ (#o, #n) ★
+               auth_inv γ1 (tickets_inv n) ★
+               ((own γ2 (Excl ()) ★  R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
+
+Definition is_lock (l: loc) (R: iProp) : iProp :=
+  (∃ γ1 γ2, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ1 γ2 l R))%I.
+
+Definition issued (l : loc) (x: nat) (R : iProp) : iProp :=
+  (∃ γ1 γ2, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ1 γ2 l R) ∧
+            auth_own γ1 (GSet {[ x ]}))%I.
+
+Definition locked (l : loc) (R : iProp) : iProp :=
+  (∃ γ1 γ2, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ1 γ2 l R) ∧
+            own γ2 (Excl ()))%I.
+
+Global Instance lock_inv_ne n γ1 γ2 l : Proper (dist n ==> dist n) (lock_inv γ1 γ2 l).
+Proof. solve_proper. Qed.
+Global Instance is_lock_ne n l: Proper (dist n ==> dist n) (is_lock l).
+Proof. solve_proper. Qed.
+Global Instance locked_ne n l: Proper (dist n ==> dist n) (locked l).
+Proof. solve_proper. Qed.
+
+Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
+Proof. apply _. Qed.
+
+Lemma newlock_spec (R : iProp) Φ :
+  heapN ⊥ N →
+  heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
+Proof.
+  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
+  wp_seq. wp_alloc l as "Hl".
+  iPvs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
+  iPvs (own_alloc_strong (Auth (Excl' ∅) ∅) _ {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
+  iPvs (inv_alloc N _ (lock_inv γ1 γ2 l R) with "[-HΦ]"); first done.
+  { iNext. rewrite /lock_inv.
+    iExists 0%nat, 0%nat.
+    iFrame.
+    iSplitL "Hγ1".
+    { rewrite /auth_inv.
+      iExists (GSet ∅).
+      by iFrame. }
+    iLeft.
+    by iFrame. }
+  iPvsIntro.
+  iApply "HΦ".
+  iExists γ1, γ2.
+  iSplit; by auto.
+Qed.
+
+Lemma wait_loop_spec l x R (Φ : val → iProp) :
+  issued l x R ★ (∀ l, locked l R -★ R -★ Φ #()) ⊢ WP wait_loop #x #l {{ Φ }}.
+Proof.
+  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Ht)".
+  iLöb as "IH". wp_rec. wp_let. wp_focus (! _)%E.
+  iInv N as (o n) "[Hl Ha]".
+  wp_load. iPvsIntro.
+  destruct (decide (x = o)) as [Heq|Hneq].
+  - subst.
+    iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+    + iSplitL "Hl Hainv Ht".
+      * iNext.
+        iExists o, n.
+        iFrame.
+        by iRight.
+      * wp_proj. wp_let. wp_op=>[_|[]] //.
+        wp_if. iPvsIntro.
+        iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2; eauto.
+    + iExFalso. iCombine "Ht" "Haown" as "Haown".
+      iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
+      set_solver.
+  - iSplitL "Hl Ha".
+    + iNext. iExists o, n. by iFrame.
+    + wp_proj. wp_let. wp_op=>?; first omega.
+      wp_if. by iApply ("IH" with "Ht").
+Qed.
+
+Lemma acquire_spec l R (Φ : val → iProp) :
+  is_lock l R ★ (∀ l, locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}.
+Proof.
+  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #?)".
+  iLöb as "IH". wp_rec. wp_focus (! _)%E.
+  iInv N as (o n) "[Hl Ha]".
+  wp_load. iPvsIntro.
+  iSplitL "Hl Ha".
+  - iNext. iExists o, n. by iFrame.
+  - wp_let. wp_proj. wp_proj. wp_op.
+    wp_focus (CAS _ _ _).
+    iInv N as (o' n') "[Hl [Hainv Haown]]".
+    destruct (decide ((#o', #n') = (#o, #n)))%V
+      as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
+    + wp_cas_suc.
+      iDestruct "Hainv" as (s) "[Ho %]"; subst.
+      iPvs (own_update with "Ho") as "Ho".
+      { eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
+        rewrite elem_of_seq_set; omega. }
+      iDestruct "Ho" as "[Hofull Hofrag]".
+      iSplitL "Hl Haown Hofull".
+      * rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
+        rewrite -(seq_set_S_union_L 0).
+        iPvsIntro. iNext.
+        iExists o, (S n)%nat.
+        rewrite Nat2Z.inj_succ -Z.add_1_r.
+        iFrame. iExists (GSet (seq_set 0 (S n))).
+        by iFrame.
+      * iPvsIntro. wp_if. wp_proj.
+        iApply wait_loop_spec.
+        iSplitR "HΦ"; last by done.
+        rewrite /issued /auth_own; eauto 10.
+    + wp_cas_fail.
+      iPvsIntro.
+      iSplitL "Hl Hainv Haown".
+      { iNext. iExists o', n'. by iFrame. }
+      { wp_if. by iApply "IH". }
+Qed.
+
+Lemma release_spec R l (Φ : val → iProp):
+  locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}.
+Proof.
+  iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Hγ)".
+  iLöb as "IH". wp_rec. wp_focus (! _)%E.
+  iInv N as (o n) "[Hl Hr]".
+  wp_load. iPvsIntro.
+  iSplitL "Hl Hr".
+  - iNext. iExists o, n. by iFrame.
+  - wp_let. wp_focus (CAS _ _ _ ).
+    wp_proj. wp_op. wp_proj.
+    iInv N as (o' n') "[Hl Hr]".
+    destruct (decide ((#o', #n') = (#o, #n)))%V
+      as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
+    + wp_cas_suc.
+      iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
+      * iExFalso. iCombine "Hγ" "Ho" as "Ho".
+        iDestruct (own_valid with "#Ho") as %[].
+      * iSplitL "Hl HR Hγ Hainv".
+        { iPvsIntro. iNext. iExists (o + 1)%nat, n%nat.
+          iFrame. rewrite Nat2Z.inj_add.
+          iFrame. iLeft; by iFrame. }
+        { iPvsIntro. by wp_if. }
+    + wp_cas_fail.
+      iPvsIntro.
+      iSplitL "Hl Hr".
+      * iNext. iExists o', n'. by iFrame.
+      * wp_if. by iApply ("IH" with "Hγ HR").
+Qed.
+End proof.
+
+Typeclasses Opaque is_lock issued locked.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 68f480a12d057f378f9e49a0453b5bbbcfc9eae6..1fbd3665160f85e9a7ac34a2621a500d6ea693c7 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -13,7 +13,7 @@ Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
 
 Global Instance into_sep_mapsto l q v :
   IntoSep false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
+Proof. by rewrite /IntoSep heap_mapsto_op_eq Qp_div_2. Qed.
 
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →
diff --git a/prelude/collections.v b/prelude/collections.v
index 7762ce91a3398701a4cb186635d3d664a4afa9f2..850226e1571c4a65910ed62910d035490568c18c 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -948,3 +948,38 @@ Section more_finite.
     intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; set_solver.
   Qed.
 End more_finite.
+
+(** Sets of sequences of natural numbers *)
+(* The set [seq_seq start len] of natural numbers contains the sequence
+[start, start + 1, ..., start + (len-1)]. *)
+Fixpoint seq_set `{Singleton nat C, Union C, Empty C} (start len : nat) : C :=
+  match len with
+  | O => ∅
+  | S len' => {[ start ]} ∪ seq_set (S start) len'
+  end.
+
+Section seq_set.
+  Context `{SimpleCollection nat C}.
+  Implicit Types start len x : nat.
+
+  Lemma elem_of_seq_set start len x :
+    x ∈ seq_set start len ↔ start ≤ x < start + len.
+  Proof.
+    revert start. induction len as [|len IH]; intros start; simpl.
+    - rewrite elem_of_empty. omega.
+    - rewrite elem_of_union, elem_of_singleton, IH. omega.
+  Qed.
+
+  Lemma seq_set_S_disjoint start len : {[ start + len ]} ⊥ seq_set start len.
+  Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
+
+  Lemma seq_set_S_union start len :
+    seq_set start (C:=C) (S len) ≡ {[ start + len ]} ∪ seq_set start len.
+  Proof.
+    intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. omega.
+  Qed.
+
+  Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len :
+    seq_set start (S len) = {[ start + len ]} ∪ seq_set start len.
+  Proof. unfold_leibniz. apply seq_set_S_union. Qed.
+End seq_set.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 0dad1337861dfe92739d36d21f2e48c4549a8aad..a9088d1f36955a0fc846975a48934f3698d1c354 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -82,7 +82,7 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
 Notation lcm := Nat.lcm.
 Notation divide := Nat.divide.
 Notation "( x | y )" := (divide x y) : nat_scope.
-Instance divide_dec x y : Decision (x | y).
+Instance Nat_divide_dec x y : Decision (x | y).
 Proof.
   refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
 Defined.
@@ -94,6 +94,11 @@ Hint Extern 0 (_ | _) => reflexivity.
 Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
 Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
 
+Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
+Proof. done. Qed.
+Lemma Nat_iter_S_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
+Proof. induction n; f_equal/=; auto. Qed.
+
 (** * Notations and properties of [positive] *)
 Open Scope positive_scope.
 
@@ -226,16 +231,19 @@ Infix "`rem`" := Z.rem (at level 35) : Z_scope.
 Infix "≪" := Z.shiftl (at level 35) : Z_scope.
 Infix "≫" := Z.shiftr (at level 35) : Z_scope.
 
-Instance: Inj (=) (=) Zpos.
+Instance Zpos_inj : Inj (=) (=) Zpos.
 Proof. by injection 1. Qed.
-Instance: Inj (=) (=) Zneg.
+Instance Zneg_inj : Inj (=) (=) Zneg.
 Proof. by injection 1. Qed.
 
+Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
+Proof. intros n1 n2. apply Nat2Z.inj. Qed.
+
 Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y) := Z_le_dec.
 Instance Z_lt_dec: ∀ x y : Z, Decision (x < y) := Z_lt_dec.
 Instance Z_inhabited: Inhabited Z := populate 1.
-Instance: PartialOrder (≤).
+Instance Z_le_order : PartialOrder (≤).
 Proof.
   repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
 Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index ba098d733e1732ceb6d86d93e095ec1e612d2850..c5b8dc22f92a626a98b40c17db51e5ac4378de9c 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -56,6 +56,10 @@ Section auth.
   Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
 
+  Global Instance from_sep_own_authM γ a b :
+  FromSep (auth_own γ (a ⋅ b)) (auth_own γ a) (auth_own γ b) | 90.
+  Proof. by rewrite /FromSep auth_own_op. Qed.
+
   Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
   Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
 
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
new file mode 100644
index 0000000000000000000000000000000000000000..34795155f0a4ab40f1dc8fd1113b8d7a9458b1eb
--- /dev/null
+++ b/program_logic/counter_examples.v
@@ -0,0 +1,57 @@
+From iris.algebra Require Import upred.
+From iris.proofmode Require Import tactics.
+
+(** This proves that we need the â–· in a "Saved Proposition" construction with
+    name-dependend allocation. *)
+(** We fork in [uPred M] for any M, but the proof would work in any BI. *)
+Section savedprop.
+  Context (M : ucmraT).
+  Notation iProp := (uPred M).
+  Notation "¬ P" := (□ (P → False))%I : uPred_scope.
+  Implicit Types P : iProp.
+
+  (* Saved Propositions and view shifts. *)
+  Context (sprop : Type) (saved : sprop → iProp → iProp) (pvs : iProp → iProp).
+  Hypothesis pvs_mono : ∀ P Q, (P ⊢ Q) → pvs P ⊢ pvs Q.
+  Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
+  Hypothesis sprop_alloc_dep :
+    ∀ (P : sprop → iProp), True ⊢ pvs (∃ i, saved i (P i)).
+  Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ P ↔ Q.
+
+  (* Self-contradicting assertions are inconsistent *)
+  Lemma no_self_contradiction P `{!PersistentP P} : □ (P ↔ ¬ P) ⊢ False.
+  Proof.
+    iIntros "#[H1 H2]".
+    iAssert P as "#HP".
+    { iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). }
+    by iApply ("H1" with "[#]").
+  Qed.
+
+  (* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *)
+  Definition A (i : sprop) : iProp := ∃ P, saved i P ★ □ P.
+  Lemma saved_is_A i P `{!PersistentP P} : saved i P ⊢ □ (A i ↔ P).
+  Proof.
+    iIntros "#HS !". iSplit.
+    - iDestruct 1 as (Q) "[#HSQ HQ]".
+      iApply (sprop_agree i P Q with "[]"); eauto.
+    - iIntros "#HP". iExists P. by iSplit.
+  Qed.
+
+  (* Define [Q i] to be "negated assertion with name [i]". Show that this
+     implies that assertion with name [i] is equivalent to its own negation. *)
+  Definition Q i := saved i (¬ A i).
+  Lemma Q_self_contradiction i : Q i ⊢ □ (A i ↔ ¬ A i).
+  Proof. iIntros "#HQ !". by iApply (saved_is_A i (¬A i)). Qed.
+
+  (* We can obtain such a [Q i]. *)
+  Lemma make_Q : True ⊢ pvs (∃ i, Q i).
+  Proof. apply sprop_alloc_dep. Qed.
+
+  (* Put together all the pieces to derive a contradiction. *)
+  (* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *)
+  Lemma contradiction : True ⊢ pvs False.
+  Proof.
+    rewrite make_Q. apply pvs_mono. iDestruct 1 as (i) "HQ".
+    iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction.
+  Qed.
+End savedprop.
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index ddc588c5f005556d3ace6f6dccfe9acafbf76e96..d53bae6a6a99101f4884852470bd45bd29fb6b58 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -92,10 +92,12 @@ Global Instance from_later_sep P1 P2 Q1 Q2 :
 Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
 
 (* IntoWand *)
-Global Instance into_wand_wand P Q : IntoWand (P -★ Q) P Q.
-Proof. done. Qed.
-Global Instance into_wand_impl P Q : IntoWand (P → Q) P Q.
-Proof. apply impl_wand. Qed.
+Global Instance into_wand_wand P Q Q' :
+  FromAssumption false Q Q' → IntoWand (P -★ Q) P Q'.
+Proof. by rewrite /FromAssumption /IntoWand /= => ->. Qed.
+Global Instance into_wand_impl P Q Q' :
+  FromAssumption false Q Q' → IntoWand (P → Q) P Q'.
+Proof. rewrite /FromAssumption /IntoWand /= => ->. by rewrite impl_wand. Qed.
 Global Instance into_wand_iff_l P Q : IntoWand (P ↔ Q) P Q.
 Proof. by apply and_elim_l', impl_wand. Qed.
 Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
@@ -230,7 +232,7 @@ Global Instance make_and_true_l P : MakeAnd True P P.
 Proof. by rewrite /MakeAnd left_id. Qed.
 Global Instance make_and_true_r P : MakeAnd P True P.
 Proof. by rewrite /MakeAnd right_id. Qed.
-Global Instance make_and_default P Q : MakeSep P Q (P ★ Q) | 100.
+Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. done. Qed.
 Global Instance frame_and_l R P1 P2 Q Q' :
   Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 676710d71fdeaed2ca75e3fd6a3908ec13362a99..2de2ce5f9ba084d9caf79e4f22e2a370e7d17dc0 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -12,6 +12,10 @@ Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
 Global Instance from_assumption_pvs E p P Q :
   FromAssumption p P Q → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
+Global Instance into_wand_pvs E1 E2 R P Q :
+  IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
+
 Global Instance from_sep_pvs E P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
 Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
@@ -26,9 +30,6 @@ Qed.
 Global Instance frame_pvs E1 E2 R P Q :
   Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
-Global Instance into_wand_pvs E1 E2 R P Q :
-  IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
-Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
 Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
 Proof.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 89b691aa24367ca1803262e6a3dcff55de4f9dd6..107eea1e11ff94cc3db02aeaced447e6999ce42d 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -128,9 +128,9 @@ Record iTrm {X As} :=
 Arguments ITrm {_ _} _ _ _.
 
 Notation "( H $! x1 .. xn )" :=
-  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 0).
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
 Notation "( H $! x1 .. xn 'with' pat )" :=
-  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 0).
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
 Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
 
 Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
@@ -224,7 +224,7 @@ Tactic Notation "iIntoEntails" open_constr(t) :=
     | True ⊢ _ => apply t
     | _ ⊢ _ => apply (uPred.entails_wand _ _ t)
     | _ ⊣⊢ _ => apply (uPred.equiv_iff _ _ t)
-    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H)]
+    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
     | ∀ _ : ?T, _ =>
        (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
        (* This is a workarround for Coq bug #4969. *)
@@ -399,29 +399,6 @@ Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
      apply _ || fail "iSepDestruct:" H ":" P "not separating destructable"
     |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].
 
-Tactic Notation "iFrame" constr(Hs) :=
-  let rec go Hs :=
-    match Hs with
-    | [] => idtac
-    | ?H :: ?Hs =>
-       eapply tac_frame with _ H _ _ _;
-         [env_cbv; reflexivity || fail "iFrame:" H "not found"
-         |let R := match goal with |- Frame ?R _ _ => R end in
-          apply _ || fail "iFrame: cannot frame" R
-         |lazy iota beta; go Hs]
-    end
-  in let Hs := words Hs in go Hs.
-
-Tactic Notation "iFrame" :=
-  let rec go Hs :=
-    match Hs with
-    | [] => idtac
-    | ?H :: ?Hs => try iFrame H; go Hs
-    end in
-  match goal with
-  | |- of_envs ?Δ ⊢ _ => let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
-  end.
-
 Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
   eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
     [env_cbv; reflexivity || fail "iCombine:" H1 "not found"
@@ -431,6 +408,42 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
      apply _ || fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2
     |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
 
+(** Framing *)
+Local Ltac iFrameHyp H :=
+  eapply tac_frame with _ H _ _ _;
+    [env_cbv; reflexivity || fail "iFrame:" H "not found"
+    |let R := match goal with |- Frame ?R _ _ => R end in
+     apply _ || fail "iFrame: cannot frame" R
+    |lazy iota beta].
+
+Local Ltac iFramePersistent :=
+  let rec go Hs :=
+    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
+  match goal with
+  | |- of_envs ?Δ ⊢ _ =>
+     let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
+  end.
+
+Local Ltac iFrameSpatial :=
+  let rec go Hs :=
+    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
+  match goal with
+  | |- of_envs ?Δ ⊢ _ =>
+     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
+  end.
+
+Tactic Notation "iFrame" constr(Hs) :=
+  let rec go Hs :=
+    match Hs with
+    | [] => idtac
+    | "#" :: ?Hs => iFramePersistent; go Hs
+    | "★" :: ?Hs => iFrameSpatial; go Hs
+    | ?H :: ?Hs => iFrameHyp H; go Hs
+    end
+  in let Hs := words Hs in go Hs.
+
+Tactic Notation "iFrame" := iFrameSpatial.
+
 (** * Existential *)
 Tactic Notation "iExists" uconstr(x1) :=
   eapply tac_exist;