diff --git a/_CoqProject b/_CoqProject
index cad9366d9174fa2c564bc015e2132995cfea0a51..d8213fe7d866dc030d6f350bdd74b65fdb3d26e1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -64,6 +64,7 @@ program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
 program_logic/tests.v
+program_logic/auth.v
 program_logic/ghost_ownership.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
diff --git a/algebra/auth.v b/algebra/auth.v
index 8a170d076f73489f5584f7519e96aa17927cbe8f..515be218613b1a9b636772a6791482051eb033c7 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -146,6 +146,8 @@ Proof.
 Qed.
 Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
+Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
+Proof. by rewrite /op /auth_op /= left_id. Qed.
 
 Lemma auth_update a a' b b' :
   (∀ n af, ✓{S n} a → a ≡{S n}≡ a' ⋅ af → b ≡{S n}≡ b' ⋅ af ∧ ✓{S n} b) →
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 69732e0f780064a23caf2a604ad1af9a29bae9a2..1728cb76b5a3744030a82f4e4a31b1021f5b6c53 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,91 +1,53 @@
 Require Export algebra.auth algebra.functor.
-Require Import program_logic.language program_logic.weakestpre.
-Import uPred.
-
-(* RJ: This is a work-in-progress playground.
-   FIXME: Finish or remove. *)
+Require Export program_logic.invariants program_logic.ghost_ownership.
+Import uPred ghost_ownership.
 
 Section auth.
-  (* TODO what should be implicit, what explicit? *)
-  Context {Λ : language}.
-  Context {C : nat → cmraT}.
-  Context (i : nat).
-  Context {A : cmraT}.
-
-  Hypothesis Ci : C i = authRA A.
-  Let Σ : iFunctor := iprodF (mapF positive ∘ constF ∘ C).
-
-  Definition tr (a : authRA A) : C i.
-  rewrite Ci. exact a. Defined.
-  Definition tr' (c : C i) : authRA A.
-  rewrite -Ci. exact c. Defined.
-
-  Lemma tr'_tr a :
-    tr' $ tr a = a.
-  Proof.
-    rewrite /tr' /tr. by destruct Ci.
-  Qed.
-
-  Lemma tr_tr' c :
-    tr $ tr' c = c.
-  Proof.
-    rewrite /tr' /tr. by destruct Ci.
-  Qed.
-
-  Lemma tr_proper : Proper ((≡) ==> (≡)) tr.
-  Proof.
-    move=>a1 a2 Heq. rewrite /tr. by destruct Ci.
-  Qed.
-
-  Lemma Ci_op (c1 c2: C i) :
-    c1 â‹… c2 = tr (tr' c1 â‹… tr' c2).
-  Proof.
-    rewrite /tr' /tr. by destruct Ci.
-  Qed.
-
-  Lemma A_val a :
-    ✓a = ✓(tr a).
-  Proof.
-    rewrite /tr. by destruct Ci.
-  Qed.
-
-  (* FIXME RJ: I'd rather not have to specify Σ by hand here. *)
-  Definition A2m (p : positive) (a : authRA A) : iGst Λ Σ :=
-    iprod_singleton i (<[p:=tr a]>∅).
-  Definition ownA (p : positive) (a : authRA A) : iProp Λ Σ :=
-    ownG (Σ:=Σ) (A2m p a).
-
-  Lemma ownA_op p a1 a2 :
-    (ownA p a1 ★ ownA p a2)%I ≡ ownA p (a1 ⋅ a2).
+  Context {A : cmraT} `{Empty A, !CMRAIdentity A}.
+  Context {Λ : language} {Σ : gid → iFunctor} (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}.
+  (* TODO: Come up with notation for "iProp Λ (globalC Σ)". *)
+  Context (N : namespace) (φ : A → iProp Λ (globalC Σ)).
+  Implicit Types P Q R : iProp Λ (globalC Σ).
+  Implicit Types a b : A.
+  Implicit Types γ : gname.
+
+  (* TODO: Need this to be proven somewhere. *)
+  (* FIXME ✓ binds too strong, I need parenthesis here. *)
+  Hypothesis auth_valid :
+    forall a b, (✓(Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
+
+  (* FIXME how much would break if we had a global instance from ∅ to Inhabited? *)
+  Local Instance auth_inhabited : Inhabited A.
+  Proof. split. exact ∅. Qed.
+
+  Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) :=
+    (∃ a, own AuthI γ (●a) ★ φ a)%I.
+  Definition auth_own (γ : gname) (a : A) := own AuthI γ (◯a).
+  Definition auth_ctx (γ : gname) := inv N (auth_inv γ).
+
+  Lemma auth_alloc a :
+    ✓a → φ a ⊑ pvs N N (∃ γ, auth_ctx γ ∧ auth_own γ a).
   Proof.
-    rewrite /ownA /A2m /iprod_singleton /iprod_insert -ownG_op. apply ownG_proper=>j /=.
-    rewrite iprod_lookup_op. destruct (decide (i = j)).
-    - move=>q. destruct e. rewrite lookup_op /=.
-      destruct (decide (p = q)); first subst q.
-      + rewrite !lookup_insert.
-        rewrite /op /cmra_op /=. f_equiv.
-        rewrite Ci_op. apply tr_proper.
-        rewrite !tr'_tr. reflexivity.
-      + by rewrite !lookup_insert_ne //.
-    - by rewrite left_id.
+    intros Ha. rewrite -(right_id True%I (★)%I (φ _)).
+    rewrite (own_alloc AuthI (Auth (Excl a) a) N) //; [].
+    rewrite pvs_frame_l. apply pvs_strip_pvs.
+    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
+    transitivity (▷auth_inv γ ★ auth_own γ a)%I.
+    { rewrite /auth_inv -later_intro -(exist_intro a).
+      rewrite (commutative _ _ (φ _)) -associative. apply sep_mono; first done.
+      rewrite /auth_own -own_op auth_both_op. done. }
+    rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
+    by rewrite always_and_sep_l'.
   Qed.
 
-  (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
-     assertion. However, the map_updateP_alloc does not suffice to show this. *)
-  Lemma ownA_alloc E a :
-    ✓a → True ⊑ pvs E E (∃ p, ownA p a).
+  Lemma auth_opened a γ :
+    (▷auth_inv γ ★ auth_own γ a) ⊑ (▷∃ a', φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
-    intros Ha. set (P m := ∃ p, m = A2m p a).
-    set (a' := tr a).
-    rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
-    - rewrite -pvs_updateP_empty //; [].
-      subst P. eapply (iprod_singleton_updateP_empty i).
-      + eapply map_updateP_alloc' with (x:=a'). subst a'.
-        by rewrite -A_val.
-      + simpl. move=>? [p [-> ?]]. exists p. done.
-    - apply exist_elim=>m. apply const_elim_l.
-      move=>[p ->] {P}. by rewrite -(exist_intro p).
-  Qed.      
-    
+    rewrite /auth_inv. rewrite [auth_own _ _]later_intro -later_sep.
+    apply later_mono. rewrite sep_exist_r. apply exist_elim=>b.
+    rewrite /auth_own [(_ ★ φ _)%I]commutative -associative -own_op.
+    rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
+    rewrite [∅ ⋅ _]left_id -(exist_intro a').
+  Abort.
 End auth.
 
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index ad0bb23c1b86dd165ed5c181b0ba8dc2559405d7..72529d620a80bbc4050f194090d922de055d4128 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -8,6 +8,7 @@ Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
 Local Hint Extern 99 ({[ _ ]} ⊆ _) => apply elem_of_subseteq_singleton.
 
+
 Definition namespace := list positive.
 Definition nnil : namespace := nil.
 Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
@@ -91,7 +92,7 @@ Qed.
 
 Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) :
   atomic e → nclose N ⊆ E →
-  (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)))%I ⊑ wp E e Q.
+  (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v))) ⊑ wp E e Q.
 Proof.
   move=>He HN.
   rewrite /inv and_exist_r. apply exist_elim=>i.
@@ -108,7 +109,7 @@ Proof.
   apply pvs_mask_frame'; solve_elem_of.
 Qed.
 
-Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P).
+Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
 Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
 
 End inv.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 03ce44e374e46f50e2e731e6132f9fc7c825356b..f76066f5fb585fbf5d1679edc146605aad79e973 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -132,6 +132,8 @@ Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
 Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P.
 Proof. apply pvs_trans; solve_elem_of. Qed.
+Lemma pvs_strip_pvs E P Q : P ⊑ pvs E E Q → pvs E E P ⊑ pvs E E Q.
+Proof. move=>->. by rewrite pvs_trans'. Qed.
 Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q).
 Proof. rewrite !(commutative _ P); apply pvs_frame_r. Qed.
 Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 96f9fd7ee3088c3e1b5c637e5b3a2a7410d7436a..e86145e48fc9f79dd26d9596864df41906f4841b 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -100,7 +100,7 @@ Proof.
 Qed.
 
 Lemma vs_alloc (N : namespace) P : â–· P ={N}=> inv N P.
-Proof. by intros; apply vs_alt, pvs_alloc. Qed.
+Proof. by intros; apply vs_alt, inv_alloc. Qed.
 
 End vs.
 
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index aa37a5df872d00f1f6c56c20f60d8cdd9f5d57bd..3618e8753f046428e8e0a73ecc3deefefb1771dd 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -206,6 +206,8 @@ Proof. by apply wp_mask_frame_mono. Qed.
 Global Instance wp_mono' E e :
   Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
 Proof. by intros Q Q' ?; apply wp_mono. Qed.
+Lemma wp_strip_pvs E e P Q : P ⊑ wp E e Q → pvs E E P ⊑ wp E e Q.
+Proof. move=>->. by rewrite pvs_wp. Qed.
 Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
 Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).