From b07dd0b53c858a342982c3a7d549751e0b28a909 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 00:10:04 +0100
Subject: [PATCH] Use bundled type classes for ghost ownership.

* These type classes bundle an identifier into the global CMRA with a proof
  that the identifier points to the correct CMRA. Bundling allows us to get
  rid of many arguments everywhere.

* I have setup the type classes so that we no longer have to keep track of the
  global CMRA identifiers. These are implicit and resolved automatically.

* For heap I am also bundling the name of the heap RA instance. There always
  should be at most one heap instance so this does not introduce ambiguities.

* We now have a "maps to" notation!
---
 barrier/barrier.v               |  33 ++++-----
 heap_lang/heap.v                | 125 +++++++++++++++++---------------
 heap_lang/tests.v               |   6 +-
 program_logic/auth.v            |  63 ++++++++--------
 program_logic/ghost_ownership.v |  84 ++++++++++-----------
 program_logic/saved_prop.v      |  18 ++---
 program_logic/sts.v             |  75 +++++++++----------
 program_logic/viewshifts.v      |  12 +--
 8 files changed, 209 insertions(+), 207 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index b0b10a625..c556bd9e9 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -68,9 +68,8 @@ Module barrier_proto.
   (* The set of low states *)
   Definition low_states : set stateT :=
     mkSet (λ s, if state_phase s is Low then True else False).
-  
-  Lemma low_states_closed :
-    sts.closed low_states {[ Send ]}.
+
+  Lemma low_states_closed : sts.closed low_states {[ Send ]}.
   Proof.
     split.
     - apply (non_empty_inhabited(State Low ∅)). by rewrite !mkSet_elem_of /=.
@@ -97,9 +96,9 @@ Section proof.
   Context {Σ : iFunctorG} (N : namespace).
   (* TODO: Bundle HeapI and HeapG and have notation so that we can just write
      "l ↦ '0". *)
-  Context (HeapI : gid) `{!HeapInG Σ HeapI} (HeapG : gname) (HeapN : namespace).
-  Context (StsI : gid) `{!STSInG heap_lang Σ StsI sts}.
-  Context (SpI : gid) `{!SavedPropInG heap_lang Σ SpI}.
+  Context `{heapG Σ} (HeapN : namespace).
+  Context `{stsG heap_lang Σ sts}.
+  Context `{savedPropG heap_lang Σ}.
   (* TODO We could alternatively construct the namespaces to be disjoint.
      But that would take a lot of flexibility from the client, who probably
      wants to also use the heap_ctx elsewhere. *)
@@ -109,28 +108,28 @@ Section proof.
 
   Definition waiting (P : iProp) (I : gset gname) : iProp :=
     (∃ R : gname → iProp, ▷(P -★ Π★{set I} (λ i, R i)) ★
-                             Π★{set I} (λ i, saved_prop_own SpI i (R i)))%I.
+                             Π★{set I} (λ i, saved_prop_own i (R i)))%I.
 
   Definition ress (I : gset gname) : iProp :=
-    (Π★{set I} (λ i, ∃ R, saved_prop_own SpI i R ★ ▷R))%I.
+    (Π★{set I} (λ i, ∃ R, saved_prop_own i R ★ ▷R))%I.
 
   Local Notation state_to_val s :=
     (match s with State Low _ => 0 | State High _ => 1 end).
   Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
-    (heap_mapsto HeapI HeapG l '(state_to_val s) ★
+    (l !=> '(state_to_val s) ★
      match s with State Low I' => waiting P I' | State High I' => ress I' end
     )%I.
 
   Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
-    (heap_ctx HeapI HeapG HeapN ★ sts_ctx StsI sts γ N (barrier_inv l P))%I.
+    (heap_ctx HeapN ★ sts_ctx γ N (barrier_inv l P))%I.
 
   Definition send (l : loc) (P : iProp) : iProp :=
-    (∃ γ, barrier_ctx γ l P ★ sts_ownS StsI sts γ low_states {[ Send ]})%I.
+    (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I.
 
   Definition recv (l : loc) (R : iProp) : iProp :=
-    (∃ γ (P Q : iProp) i, barrier_ctx γ l P ★ sts_ownS StsI sts γ (i_states i) {[ Change i ]} ★
-        saved_prop_own SpI i Q ★ ▷(Q -★ R))%I.
-    
+    (∃ γ (P Q : iProp) i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
+        saved_prop_own i Q ★ ▷(Q -★ R))%I.
+
   Lemma newchan_spec (P : iProp) (Q : val → iProp) :
     (∀ l, recv l P ★ send l P -★ Q (LocV l)) ⊑ wp coPset_all (newchan '()) Q.
   Proof.
@@ -142,9 +141,9 @@ Section proof.
     rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
     apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
     (* I think some evars here are better than repeating *everything* *)
-    eapply (sts_fsaS sts _ (wp_fsa _)) with (N0:=N) (γ0:=γ);simpl; eauto with I.
+    eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ);simpl; eauto with I.
     { solve_elem_of+. (* FIXME eauto should do this  *) }
-    rewrite [(_ ★ sts_ownS _ _ _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
+    rewrite [(_ ★ sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
     apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
     apply const_elim_sep_l=>Hs. destruct p; last done.
     rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
@@ -156,7 +155,7 @@ Section proof.
       erewrite later_sep. apply sep_mono_r. apply later_intro. }
     apply wand_intro_l. rewrite -(exist_intro (State High I)).
     rewrite -(exist_intro ∅). rewrite const_equiv /=; last first.
-    { constructor; first constructor; rewrite /= /tok /=; solve_elem_of+. }
+    { constructor; first constructor; rewrite /= /tok /=; solve_elem_of. }
     rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
     rewrite !assoc [(_ ★ P)%I]comm !assoc -2!assoc.
     apply sep_mono; last first.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index f7e5715eb..e43497074 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -9,28 +9,32 @@ Import uPred.
 
 Definition heapRA := mapRA loc (exclRA (leibnizC val)).
 
-Class HeapInG Σ (i : gid) := heap_inG :> InG heap_lang Σ i (authRA heapRA).
-Instance heap_inG_auth `{HeapInG Σ i} : AuthInG heap_lang Σ i heapRA.
-Proof. split; apply _. Qed.
+Class heapG Σ := HeapG {
+  heap_inG : inG heap_lang Σ (authRA heapRA);
+  heap_name : gname
+}.
+Instance heap_authG `{i : heapG Σ} : authG heap_lang Σ heapRA :=
+  {| auth_inG := heap_inG |}.
 
 Definition to_heap : state → heapRA := fmap Excl.
 Definition of_heap : heapRA → state := omap (maybe Excl).
 
-Definition heap_mapsto {Σ} (i : gid) `{HeapInG Σ i}
-    (γ : gname) (l : loc) (v : val) : iPropG heap_lang Σ :=
-  auth_own i γ {[ l ↦ Excl v ]}.
-Definition heap_inv {Σ} (i : gid) `{HeapInG Σ i}
-  (h : heapRA) : iPropG heap_lang Σ := ownP (of_heap h).
-Definition heap_ctx {Σ} (i : gid) `{HeapInG Σ i}
-  (γ : gname) (N : namespace) : iPropG heap_lang Σ := auth_ctx i γ N (heap_inv i).
+Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
+  auth_own heap_name {[ l ↦ Excl v ]}.
+Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
+  ownP (of_heap h).
+Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
+  auth_ctx heap_name N heap_inv.
+
+(* FIXME: ↦ is already used for the singleton empty map. Resolve that... *)
+Notation "l !=> v" := (heap_mapsto l v) (at level 20) : uPred_scope.
 
 Section heap.
-  Context {Σ : iFunctorG} (HeapI : gid) `{!HeapInG Σ HeapI}.
+  Context {Σ : iFunctorG}.
   Implicit Types N : namespace.
   Implicit Types P : iPropG heap_lang Σ.
   Implicit Types σ : state.
   Implicit Types h g : heapRA.
-  Implicit Types γ : gname.
 
   (** Conversion to heaps and back *)
   Global Instance of_heap_proper : Proper ((≡) ==> (=)) of_heap.
@@ -58,25 +62,15 @@ Section heap.
     by case: (h !! l)=> [[]|]; auto.
   Qed.
 
-  (** Propers *)
-  Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) (heap_inv HeapI).
-  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
-
-  (** General properties of mapsto *)
-  Lemma heap_mapsto_disjoint γ l v1 v2 :
-    (heap_mapsto HeapI γ l v1 ★ heap_mapsto HeapI γ l v2)%I ⊑ False.
-  Proof.
-    rewrite /heap_mapsto -auto_own_op auto_own_valid map_op_singleton.
-    rewrite map_validI (forall_elim l) lookup_singleton.
-    by rewrite option_validI excl_validI.
-  Qed.
-
+  (** Allocation *)
   Lemma heap_alloc N σ :
-    ownP σ ⊑ pvs N N (∃ γ, heap_ctx HeapI γ N ∧ Π★{map σ} heap_mapsto HeapI γ).
+    authG heap_lang Σ heapRA →
+    ownP σ ⊑ pvs N N (∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto).
   Proof.
-    rewrite -{1}(from_to_heap σ); etransitivity;
-      first apply (auth_alloc (ownP ∘ of_heap) N (to_heap σ)), to_heap_valid.
-    apply pvs_mono, exist_mono=> γ; apply and_mono_r.
+    rewrite -{1}(from_to_heap σ). etransitivity.
+    { apply (auth_alloc (ownP ∘ of_heap) N (to_heap σ)), to_heap_valid. }
+    apply pvs_mono, exist_elim=> γ.
+    rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
     induction σ as [|l v σ Hl IH] using map_ind.
     { rewrite big_sepM_empty; apply True_intro. }
     rewrite to_heap_insert big_sepM_insert //.
@@ -85,18 +79,32 @@ Section heap.
     by rewrite auto_own_op IH.
   Qed.
 
+  Context `{heapG Σ}.
+
+  (** Propers *)
+  Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) heap_inv.
+  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
+
+  (** General properties of mapsto *)
+  Lemma heap_mapsto_disjoint l v1 v2 : (l !=> v1 ★ l !=> v2)%I ⊑ False.
+  Proof.
+    rewrite /heap_mapsto -auto_own_op auto_own_valid map_op_singleton.
+    rewrite map_validI (forall_elim l) lookup_singleton.
+    by rewrite option_validI excl_validI.
+  Qed.
+
   (** Weakest precondition *)
-  Lemma wp_alloc N E γ e v P Q :
+  Lemma wp_alloc N E e v P Q :
     to_val e = Some v → nclose N ⊆ E →
-    P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (▷ ∀ l, heap_mapsto HeapI γ l v -★ Q (LocV l)) →
+    P ⊑ heap_ctx N →
+    P ⊑ (▷ ∀ l, l !=> v -★ Q (LocV l)) →
     P ⊑ wp E (Alloc e) Q.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
-    transitivity (pvs E E (auth_own HeapI γ ∅ ★ P))%I.
-    { by rewrite -pvs_frame_r -(auth_empty E γ) left_id. }
-    apply wp_strip_pvs, (auth_fsa (heap_inv HeapI) (wp_fsa (Alloc e)))
-      with N γ ∅; simpl; eauto with I.
+    transitivity (pvs E E (auth_own heap_name ∅ ★ P))%I.
+    { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
+    apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
+      with N heap_name ∅; simpl; eauto with I.
     rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
     rewrite -assoc left_id; apply const_elim_sep_l=> ?.
     rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
@@ -113,16 +121,16 @@ Section heap.
     apply later_intro.
   Qed.
 
-  Lemma wp_load N E γ l v P Q :
+  Lemma wp_load N E l v P Q :
     nclose N ⊆ E →
-    P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (▷ heap_mapsto HeapI γ l v ★ ▷ (heap_mapsto HeapI γ l v -★ Q v)) →
+    P ⊑ heap_ctx N →
+    P ⊑ (▷ l !=> v ★ ▷ (l !=> v -★ Q v)) →
     P ⊑ wp E (Load (Loc l)) Q.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ.
-    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id)
-      with N γ {[ l ↦ Excl v ]}; simpl; eauto with I.
-    rewrite HPQ{HPQ}. apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
+    apply (auth_fsa' heap_inv (wp_fsa _) id)
+      with N heap_name {[ l ↦ Excl v ]}; simpl; eauto with I.
+    rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
     rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
@@ -132,16 +140,15 @@ Section heap.
     apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
   Qed.
 
-  Lemma wp_store N E γ l v' e v P Q :
+  Lemma wp_store N E l v' e v P Q :
     to_val e = Some v → nclose N ⊆ E → 
-    P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (▷ heap_mapsto HeapI γ l v' ★
-          ▷ (heap_mapsto HeapI γ l v -★ Q (LitV LitUnit))) →
+    P ⊑ heap_ctx N →
+    P ⊑ (▷ l !=> v' ★ ▷ (l !=> v -★ Q (LitV LitUnit))) →
     P ⊑ wp E (Store (Loc l) e) Q.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPQ.
-    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v) l))
-      with N γ {[ l ↦ Excl v' ]}; simpl; eauto with I.
+    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
+      with N heap_name {[ l ↦ Excl v' ]}; simpl; eauto with I.
     rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
@@ -153,17 +160,16 @@ Section heap.
     apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
   Qed.
 
-  Lemma wp_cas_fail N E γ l v' e1 v1 e2 v2 P Q :
+  Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Q :
     to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
     nclose N ⊆ E →
-    P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (▷ heap_mapsto HeapI γ l v' ★
-          ▷ (heap_mapsto HeapI γ l v' -★ Q (LitV (LitBool false)))) →
+    P ⊑ heap_ctx N →
+    P ⊑ (▷ l !=> v' ★ ▷ (l !=> v' -★ Q (LitV (LitBool false)))) →
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPQ.
-    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id)
-      with N γ {[ l ↦ Excl v' ]}; simpl; eauto 10 with I.
+    apply (auth_fsa' heap_inv (wp_fsa _) id)
+      with N heap_name {[ l ↦ Excl v' ]}; simpl; eauto 10 with I.
     rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
@@ -174,17 +180,16 @@ Section heap.
     apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
   Qed.
 
-  Lemma wp_cas_suc N E γ l e1 v1 e2 v2 P Q :
+  Lemma wp_cas_suc N E l e1 v1 e2 v2 P Q :
     to_val e1 = Some v1 → to_val e2 = Some v2 →
     nclose N ⊆ E →
-    P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (▷ heap_mapsto HeapI γ l v1 ★
-          ▷ (heap_mapsto HeapI γ l v2 -★ Q (LitV (LitBool true)))) →
+    P ⊑ heap_ctx N →
+    P ⊑ (▷ l !=> v1 ★ ▷ (l !=> v2 -★ Q (LitV (LitBool true)))) →
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPQ.
-    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v2) l))
-      with N γ {[ l ↦ Excl v1 ]}; simpl; eauto 10 with I.
+    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
+      with N heap_name {[ l ↦ Excl v1 ]}; simpl; eauto 10 with I.
     rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index c4d9b90ff..150917f08 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -22,15 +22,15 @@ Section LangTests.
 End LangTests.
 
 Section LiftingTests.
-  Context {Σ : iFunctorG} (HeapI : gid) `{!HeapInG Σ HeapI}.
+  Context `{heapG Σ}.
   Implicit Types P : iPropG heap_lang Σ.
   Implicit Types Q : val → iPropG heap_lang Σ.
 
   Definition e  : expr :=
     let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
-  Goal ∀ γh N, heap_ctx HeapI γh N ⊑ wp N e (λ v, v = '2).
+  Goal ∀ N, heap_ctx N ⊑ wp N e (λ v, v = '2).
   Proof.
-    move=> γh N. rewrite /e.
+    move=> N. rewrite /e.
     wp_focus (ref '1)%L. eapply wp_alloc; eauto; [].
     rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
     wp_rec.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index cb70202c6..3fbeeb7cc 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -2,53 +2,52 @@ From algebra Require Export auth.
 From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
-Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
-  auth_inG :> InG Λ Σ i (authRA A);
+(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
+is constantly valid. *)
+Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
+  auth_inG :> inG Λ Σ (authRA A);
   auth_identity :> CMRAIdentity A;
   auth_timeless (a : A) :> Timeless a;
 }.
 
-(* TODO: Once we switched to RAs, it is no longer necessary to remember that a is
-   constantly valid. *)
 Section definitions.
-  Context {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A} (γ : gname).
+  Context `{authG Λ Σ A} (γ : gname).
   Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
-    (∃ a, (■ ✓ a ∧ own i γ (● a)) ★ φ a)%I.
-  Definition auth_own (a : A) : iPropG Λ Σ := own i γ (◯ a).
+    (∃ a, (■ ✓ a ∧ own γ (● a)) ★ φ a)%I.
+  Definition auth_own (a : A) : iPropG Λ Σ := own γ (◯ a).
   Definition auth_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
     inv N (auth_inv φ).
 End definitions.
-Instance: Params (@auth_inv) 7.
-Instance: Params (@auth_own) 7.
-Instance: Params (@auth_ctx) 8.
+Instance: Params (@auth_inv) 6.
+Instance: Params (@auth_own) 6.
+Instance: Params (@auth_ctx) 7.
 
 Section auth.
-  Context `{AuthInG Λ Σ AuthI A}.
+  Context `{AuthI : authG Λ Σ A}.
   Context (φ : A → iPropG Λ Σ) {φ_proper : Proper ((≡) ==> (≡)) φ}.
   Implicit Types N : namespace.
   Implicit Types P Q R : iPropG Λ Σ.
   Implicit Types a b : A.
   Implicit Types γ : gname.
 
-  Global Instance auth_own_ne n γ :
-    Proper (dist n ==> dist n) (auth_own AuthI γ).
+  Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
   Proof. by rewrite /auth_own=> a b ->. Qed.
-  Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own AuthI γ).
+  Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own γ).
   Proof. by rewrite /auth_own=> a b ->. Qed.
   Lemma auto_own_op γ a b :
-    auth_own AuthI γ (a ⋅ b) ≡ (auth_own AuthI γ a ★ auth_own AuthI γ b)%I.
+    auth_own γ (a ⋅ b) ≡ (auth_own γ a ★ auth_own γ b)%I.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
-  Lemma auto_own_valid γ a : auth_own AuthI γ a ⊑ ✓ a.
+  Lemma auto_own_valid γ a : auth_own γ a ⊑ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
   Lemma auth_alloc N a :
-    ✓ a → φ a ⊑ pvs N N (∃ γ, auth_ctx AuthI γ N φ ∧ auth_own AuthI γ a).
+    ✓ a → φ a ⊑ pvs N N (∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
   Proof.
     intros Ha. eapply sep_elim_True_r.
-    { by eapply (own_alloc AuthI (Auth (Excl a) a) N). }
+    { by eapply (own_alloc (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 AuthI γ φ ★ auth_own AuthI γ a)%I.
+    transitivity (▷ auth_inv γ φ ★ auth_own γ a)%I.
     { rewrite /auth_inv -later_intro -(exist_intro a).
       rewrite const_equiv // left_id.
       rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done.
@@ -57,12 +56,12 @@ Section auth.
     by rewrite always_and_sep_l.
   Qed.
 
-  Lemma auth_empty E γ : True ⊑ pvs E E (auth_own AuthI γ ∅).
-  Proof. by rewrite own_update_empty /auth_own. Qed.
+  Lemma auth_empty γ E : True ⊑ pvs E E (auth_own γ ∅).
+  Proof. by rewrite /auth_own -own_update_empty. Qed.
 
   Lemma auth_opened E γ a :
-    (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ a)
-    ⊑ pvs E E (∃ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
+    (▷ auth_inv γ φ ★ auth_own γ a)
+    ⊑ pvs E E (∃ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
     rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
     rewrite later_sep [(▷(_ ∧ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
@@ -71,7 +70,7 @@ Section auth.
     rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
     apply exist_elim=>a'.
     rewrite left_id -(exist_intro a').
-    apply (eq_rewrite b (a ⋅ a') (λ x, ■✓x ★ ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
+    apply (eq_rewrite b (a ⋅ a') (λ x, ■ ✓ x ★ ▷ φ x ★ own γ (● x ⋅ ◯ a))%I).
     { by move=>n ? ? /timeless_iff ->. }
     { by eauto with I. }
     rewrite const_equiv // left_id comm.
@@ -81,8 +80,8 @@ Section auth.
 
   Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
     Lv a → ✓ (L a ⋅ a') →
-    (▷ φ (L a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
-    ⊑ pvs E E (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ (L a)).
+    (▷ φ (L a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a))
+    ⊑ pvs E E (▷ auth_inv γ φ ★ auth_own γ (L a)).
   Proof.
     intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a â‹… a')).
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
@@ -99,12 +98,12 @@ Section auth.
   Lemma auth_fsa E N P (Q : V → iPropG Λ Σ) γ a :
     fsaV →
     nclose N ⊆ E →
-    P ⊑ auth_ctx AuthI γ N φ →
-    P ⊑ (▷ auth_own AuthI γ a ★ ∀ a',
+    P ⊑ auth_ctx γ N φ →
+    P ⊑ (▷ auth_own γ a ★ ∀ a',
           ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-            (auth_own AuthI γ (L a) -★ Q x))) →
+            (auth_own γ (L a) -★ Q x))) →
     P ⊑ fsa E Q.
   Proof.
     rewrite /auth_ctx=>? HN Hinv Hinner.
@@ -131,12 +130,12 @@ Section auth.
   Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Q: V → iPropG Λ Σ) γ a :
     fsaV →
     nclose N ⊆ E →
-    P ⊑ auth_ctx AuthI γ N φ →
-    P ⊑ (▷ auth_own AuthI γ a ★ (∀ a',
+    P ⊑ auth_ctx γ N φ →
+    P ⊑ (▷ auth_own γ a ★ (∀ a',
           ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x,
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-            (auth_own AuthI γ (L a) -★ Q x)))) →
+            (auth_own γ (L a) -★ Q x)))) →
     P ⊑ fsa E Q.
   Proof.
     intros ??? HP. eapply auth_fsa with N γ a; eauto.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index b5b8cedc6..cfcae20e5 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -11,101 +11,103 @@ Definition gname := positive.
 Definition globalF (Σ : gid → iFunctor) : iFunctor :=
   iprodF (λ i, mapF gname (Σ i)).
 
-Class InG (Λ : language) (Σ : gid → iFunctor) (i : gid) (A : cmraT) :=
-  inG : A = Σ i (laterC (iPreProp Λ (globalF Σ))).
+Class inG (Λ : language) (Σ : gid → iFunctor) (A : cmraT) := InG {
+  inG_id : gid;
+  inG_prf : A = Σ inG_id (laterC (iPreProp Λ (globalF Σ)))
+}.
 
-Definition to_globalF {Λ Σ A}
-    (i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
-  iprod_singleton i {[ γ ↦ cmra_transport inG a ]}.
-Definition own {Λ Σ A}
-    (i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
-  ownG (to_globalF i γ a).
-Instance: Params (@to_globalF) 6.
-Instance: Params (@own) 6.
+Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
+  iprod_singleton inG_id {[ γ ↦ cmra_transport inG_prf a ]}.
+Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
+  ownG (to_globalF γ a).
+Instance: Params (@to_globalF) 5.
+Instance: Params (@own) 5.
 Typeclasses Opaque to_globalF own.
 
 Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
 Notation iFunctorG := (gid → iFunctor).
 
 Section global.
-Context {Λ : language} {Σ : iFunctorG} (i : gid) `{!InG Λ Σ i A}.
+Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
 
 (** * Properties of to_globalC *)
-Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF i γ).
+Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
 Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
 Lemma to_globalF_op γ a1 a2 :
-  to_globalF i γ (a1 ⋅ a2) ≡ to_globalF i γ a1 ⋅ to_globalF i γ a2.
+  to_globalF γ (a1 ⋅ a2) ≡ to_globalF γ a1 ⋅ to_globalF γ a2.
 Proof.
   by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
 Qed.
-Lemma to_globalF_unit γ a : unit (to_globalF i γ a) ≡ to_globalF i γ (unit a).
+Lemma to_globalF_unit γ a : unit (to_globalF γ a) ≡ to_globalF γ (unit a).
 Proof.
   by rewrite /to_globalF
     iprod_unit_singleton map_unit_singleton cmra_transport_unit.
 Qed.
-Instance to_globalF_timeless γ m : Timeless m → Timeless (to_globalF i γ m).
+Instance to_globalF_timeless γ m : Timeless m → Timeless (to_globalF γ m).
 Proof. rewrite /to_globalF; apply _. Qed.
 
 (** * Transport empty *)
-Instance inG_empty `{Empty A} : Empty (Σ i (laterC (iPreProp Λ (globalF Σ)))) :=
-  cmra_transport inG ∅.
+Instance inG_empty `{Empty A} :
+  Empty (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))) := cmra_transport inG_prf ∅.
 Instance inG_empty_spec `{Empty A} :
-  CMRAIdentity A → CMRAIdentity (Σ i (laterC (iPreProp Λ (globalF Σ)))).
+  CMRAIdentity A → CMRAIdentity (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))).
 Proof.
   split.
   * apply cmra_transport_valid, cmra_empty_valid.
-  * intros x; rewrite /empty /inG_empty; destruct inG. by rewrite left_id.
+  * intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
   * apply _.
 Qed.
 
 (** * Properties of own *)
-Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
+Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
 Proof. by intros m m' Hm; rewrite /own Hm. Qed.
-Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
+Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own γ) := ne_proper _.
 
-Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I.
+Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I.
 Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
-Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own i γ).
+Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own γ).
 Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
-Lemma always_own_unit γ a : (□ own i γ (unit a))%I ≡ own i γ (unit a).
+Lemma always_own_unit γ a : (□ own γ (unit a))%I ≡ own γ (unit a).
 Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
-Lemma own_valid γ a : own i γ a ⊑ ✓ a.
+Lemma own_valid γ a : own γ a ⊑ ✓ a.
 Proof.
   rewrite /own ownG_valid /to_globalF.
-  rewrite iprod_validI (forall_elim i) iprod_lookup_singleton.
+  rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
   rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
-  by destruct inG.
+  by destruct inG_prf.
 Qed.
-Lemma own_valid_r γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
+Lemma own_valid_r γ a : own γ a ⊑ (own γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r _ _), own_valid. Qed.
-Lemma own_valid_l γ a : own i γ a ⊑ (✓ a ★ own i γ a).
+Lemma own_valid_l γ a : own γ a ⊑ (✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
-Global Instance own_timeless γ a : Timeless a → TimelessP (own i γ a).
+Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. unfold own; apply _. 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 own_alloc_strong a E (G : gset gname) : ✓ a → True ⊑ pvs E E (∃ γ, ■(γ ∉ G) ∧ own i γ a).
+Lemma own_alloc_strong a E (G : gset gname) :
+  ✓ a → True ⊑ pvs E E (∃ γ, ■(γ ∉ G) ∧ own γ a).
 Proof.
   intros Ha.
-  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF i γ a) ∧ ownG m)%I).
-  * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
-      first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha); naive_solver.
+  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
+  * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty inG_id);
+      first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
+      naive_solver.
   * apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
     by rewrite -(exist_intro γ) const_equiv.
 Qed.
-Lemma own_alloc a E : ✓ a → True ⊑ pvs E E (∃ γ, own i γ a).
+Lemma own_alloc a E : ✓ a → True ⊑ pvs E E (∃ γ, own γ a).
 Proof.
   intros Ha. rewrite (own_alloc_strong a E ∅) //; []. apply pvs_mono.
   apply exist_mono=>?. eauto with I.
 Qed.
 
 Lemma own_updateP P γ a E :
-  a ~~>: P → own i γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own i γ a').
+  a ~~>: P → own γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own γ a').
 Proof.
   intros Ha.
-  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF i γ a' ∧ P a') ∧ ownG m)%I).
+  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
   * eapply pvs_ownG_updateP, iprod_singleton_updateP;
       first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
     naive_solver.
@@ -114,10 +116,10 @@ Proof.
 Qed.
 
 Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E :
-  ∅ ~~>: P → True ⊑ pvs E E (∃ a, ■ P a ∧ own i γ a).
+  ∅ ~~>: P → True ⊑ pvs E E (∃ a, ■ P a ∧ own γ a).
 Proof.
   intros Hemp.
-  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF i γ a' ∧ P a') ∧ ownG m)%I).
+  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
   * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
       first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp.
     naive_solver.
@@ -125,14 +127,14 @@ Proof.
     rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
 Qed.
 
-Lemma own_update γ a a' E : a ~~> a' → own i γ a ⊑ pvs E E (own i γ a').
+Lemma own_update γ a a' E : a ~~> a' → own γ a ⊑ pvs E E (own γ a').
 Proof.
   intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
 Qed.
 
 Lemma own_update_empty `{Empty A, !CMRAIdentity A} γ E :
-  True ⊑ pvs E E (own i γ ∅).
+  True ⊑ pvs E E (own γ ∅).
 Proof.
   rewrite (own_updateP_empty (∅ =)); last by apply cmra_updateP_id.
   apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index b2e8706a8..e313311c2 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -2,29 +2,29 @@ From algebra Require Export agree.
 From program_logic Require Export ghost_ownership.
 Import uPred.
 
-Class SavedPropInG Λ Σ (i : gid) :=
-  saved_prop_inG :> InG Λ Σ i (agreeRA (laterC (iPreProp Λ (globalF Σ)))).
+Notation savedPropG Λ Σ :=
+  (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
-Definition saved_prop_own {Λ Σ} (i : gid) `{SavedPropInG Λ Σ i}
+Definition saved_prop_own `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
-  own i γ (to_agree (Next (iProp_unfold P))).
-Instance: Params (@saved_prop_own) 5.
+  own γ (to_agree (Next (iProp_unfold P))).
+Instance: Params (@saved_prop_own) 4.
 
 Section saved_prop.
-  Context `{SavedPropInG Λ Σ SPI}.
+  Context `{savedPropG Λ Σ}.
   Implicit Types P Q : iPropG Λ Σ.
   Implicit Types γ : gname.
 
   Lemma saved_prop_alloc_strong N P (G : gset gname) :
-    True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own SPI γ P).
+    True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ P).
   Proof. by apply own_alloc_strong. Qed.
 
   Lemma saved_prop_alloc N P :
-    True ⊑ pvs N N (∃ γ, saved_prop_own SPI γ P).
+    True ⊑ pvs N N (∃ γ, saved_prop_own γ P).
   Proof. by apply own_alloc. Qed.
 
   Lemma saved_prop_agree γ P Q :
-    (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ≡ Q).
+    (saved_prop_own γ P ★ saved_prop_own γ Q) ⊑ ▷ (P ≡ Q).
   Proof.
     rewrite /saved_prop_own -own_op own_valid agree_validI.
     rewrite agree_equivI later_equivI /=; apply later_mono.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 1574e303f..9371f23e3 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -2,31 +2,31 @@ From algebra Require Export sts.
 From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
-Class STSInG Λ Σ (i : gid) (sts : stsT) := {
-  sts_inG :> ghost_ownership.InG Λ Σ i (stsRA sts);
+Class stsG Λ Σ (sts : stsT) := StsG {
+  sts_inG :> inG Λ Σ (stsRA sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
+Coercion sts_inG : stsG >-> inG.
 
 Section definitions.
-  Context {Λ Σ} (i : gid) (sts : stsT) `{!STSInG Λ Σ i sts} (γ : gname).
+  Context `{i : stsG Λ Σ sts} (γ : gname).
   Import sts.
   Definition sts_inv (φ : state sts → iPropG Λ Σ) : iPropG Λ Σ :=
-    (∃ s, own i γ (sts_auth s ∅) ★ φ s)%I.
+    (∃ s, own γ (sts_auth s ∅) ★ φ s)%I.
   Definition sts_ownS (S : states sts) (T : tokens sts) : iPropG Λ Σ:=
-    own i γ (sts_frag S T).
+    own γ (sts_frag S T).
   Definition sts_own (s : state sts) (T : tokens sts) : iPropG Λ Σ :=
-    own i γ (sts_frag_up s T).
+    own γ (sts_frag_up s T).
   Definition sts_ctx (N : namespace) (φ: state sts → iPropG Λ Σ) : iPropG Λ Σ :=
     inv N (sts_inv φ).
 End definitions.
-Instance: Params (@sts_inv) 6.
-Instance: Params (@sts_ownS) 6.
-Instance: Params (@sts_own) 7.
-Instance: Params (@sts_ctx) 7.
+Instance: Params (@sts_inv) 5.
+Instance: Params (@sts_ownS) 5.
+Instance: Params (@sts_own) 6.
+Instance: Params (@sts_ctx) 6.
 
 Section sts.
-  Context {Λ Σ} (i : gid) (sts : stsT) `{!STSInG Λ Σ StsI sts}.
-  Context (φ : sts.state sts → iPropG Λ Σ).
+  Context `{stsG Λ Σ sts} (φ : sts.state sts → iPropG Λ Σ).
   Implicit Types N : namespace.
   Implicit Types P Q R : iPropG Λ Σ.
   Implicit Types γ : gname.
@@ -35,57 +35,55 @@ Section sts.
 
   (** Setoids *)
   Global Instance sts_inv_ne n γ :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv StsI sts γ).
+    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ).
   Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
   Global Instance sts_inv_proper γ :
-    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_inv StsI sts γ).
+    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_inv γ).
   Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
-  Global Instance sts_ownS_proper γ :
-    Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS StsI sts γ).
+  Global Instance sts_ownS_proper γ : Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS γ).
   Proof. intros S1 S2 HS T1 T2 HT. by rewrite /sts_ownS HS HT. Qed.
-  Global Instance sts_own_proper γ s :
-    Proper ((≡) ==> (≡)) (sts_ownS StsI sts γ s).
+  Global Instance sts_own_proper γ s : Proper ((≡) ==> (≡)) (sts_ownS γ s).
   Proof. intros T1 T2 HT. by rewrite /sts_ownS HT. Qed.
   Global Instance sts_ctx_ne n γ N :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx StsI sts γ N).
+    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
   Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
   Global Instance sts_ctx_proper γ N :
-    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx StsI sts γ N).
+    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx γ N).
   Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
 
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)
   Lemma sts_ownS_weaken E γ S1 S2 T :
     S1 ⊆ S2 → sts.closed S2 T →
-    sts_ownS StsI sts γ S1 T ⊑ pvs E E (sts_ownS StsI sts γ S2 T).
+    sts_ownS γ S1 T ⊑ pvs E E (sts_ownS γ S2 T).
   Proof. intros. by apply own_update, sts_update_frag. Qed.
 
   Lemma sts_own_weaken E γ s S T :
     s ∈ S → sts.closed S T →
-    sts_own StsI sts γ s T ⊑ pvs E E (sts_ownS StsI sts γ S T).
+    sts_own γ s T ⊑ pvs E E (sts_ownS γ S T).
   Proof. intros. by apply own_update, sts_update_frag_up. Qed.
 
   Lemma sts_alloc N s :
-    φ s ⊑ pvs N N (∃ γ, sts_ctx StsI sts γ N φ ∧
-                        sts_own StsI sts γ s (set_all ∖ sts.tok s)).
+    φ s ⊑ pvs N N (∃ γ, sts_ctx γ N φ ∧
+                        sts_own γ s (set_all ∖ sts.tok s)).
   Proof.
     eapply sep_elim_True_r.
-    { apply (own_alloc StsI (sts_auth s (set_all ∖ sts.tok s)) N).
+    { apply (own_alloc (sts_auth s (set_all ∖ sts.tok s)) N).
       apply sts_auth_valid; solve_elem_of. }
     rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
-    transitivity (▷ sts_inv StsI sts γ φ ★
-                    sts_own StsI sts γ s (set_all ∖ sts.tok s))%I.
+    transitivity (▷ sts_inv γ φ ★
+                    sts_own γ s (set_all ∖ sts.tok s))%I.
     { rewrite /sts_inv -later_intro -(exist_intro s).
       rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono_r.
-      by rewrite -own_op sts_op_auth_frag_up; last solve_elem_of+. }
+      by rewrite -own_op sts_op_auth_frag_up; last solve_elem_of. }
     rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
   Qed.
 
   Lemma sts_opened E γ S T :
-    (▷ sts_inv StsI sts γ φ ★ sts_ownS StsI sts γ S T)
-    ⊑ pvs E E (∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own StsI γ (sts_auth s T)).
+    (▷ sts_inv γ φ ★ sts_ownS γ S T)
+    ⊑ pvs E E (∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
   Proof.
     rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s.
     rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
@@ -101,14 +99,13 @@ Section sts.
 
   Lemma sts_closing E γ s T s' T' :
     sts.step (s, T) (s', T') →
-    (▷ φ s' ★ own StsI γ (sts_auth s T))
-    ⊑ pvs E E (▷ sts_inv StsI sts γ φ ★ sts_own StsI sts γ s' T').
+    (▷ φ s' ★ own γ (sts_auth s T)) ⊑ pvs E E (▷ sts_inv γ φ ★ sts_own γ s' T').
   Proof.
     intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
     rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
     rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
-    transitivity (pvs E E (own StsI γ (sts_auth s' T'))).
+    transitivity (pvs E E (own γ (sts_auth s' T'))).
     { by apply own_update, sts_update_auth. }
     by rewrite -own_op sts_op_auth_frag_up; last by inversion_clear Hstep.
   Qed.
@@ -117,12 +114,12 @@ Section sts.
 
   Lemma sts_fsaS E N P (Q : V → iPropG Λ Σ) γ S T :
     fsaV → nclose N ⊆ E →
-    P ⊑ sts_ctx StsI sts γ N φ →
-    P ⊑ (sts_ownS StsI sts γ S T ★ ∀ s,
+    P ⊑ sts_ctx γ N φ →
+    P ⊑ (sts_ownS γ S T ★ ∀ s,
           ■ (s ∈ S) ★ ▷ φ s -★
           fsa (E ∖ nclose N) (λ x, ∃ s' T',
             ■ sts.step (s, T) (s', T') ★ ▷ φ s' ★
-            (sts_own StsI sts γ s' T' -★ Q x))) →
+            (sts_own γ s' T' -★ Q x))) →
     P ⊑ fsa E Q.
   Proof.
     rewrite /sts_ctx=>? HN Hinv Hinner.
@@ -146,12 +143,12 @@ Section sts.
 
   Lemma sts_fsa E N P (Q : V → iPropG Λ Σ) γ s0 T :
     fsaV → nclose N ⊆ E →
-    P ⊑ sts_ctx StsI sts γ N φ →
-    P ⊑ (sts_own StsI sts γ s0 T ★ ∀ s,
+    P ⊑ sts_ctx γ N φ →
+    P ⊑ (sts_own γ s0 T ★ ∀ s,
           ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
           fsa (E ∖ nclose N) (λ x, ∃ s' T',
             ■ (sts.step (s, T) (s', T')) ★ ▷ φ s' ★
-            (sts_own StsI sts γ s' T' -★ Q x))) →
+            (sts_own γ s' T' -★ Q x))) →
     P ⊑ fsa E Q.
   Proof. apply sts_fsaS. Qed.
 End sts.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 962a4d5bb..a268e20f4 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -20,6 +20,7 @@ Notation "P ={ E }=> Q" := (True ⊑ vs E E P%I Q%I)
 Section vs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q R : iProp Λ Σ.
+Implicit Types N : namespace.
 
 Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P ={E1,E2}=> Q.
 Proof.
@@ -99,25 +100,24 @@ Proof.
   by rewrite /vs always_elim impl_elim_r.
 Qed.
 
-Lemma vs_alloc (N : namespace) P : â–· P ={N}=> inv N P.
+Lemma vs_alloc N P : â–· P ={N}=> inv N P.
 Proof. by intros; apply vs_alt, inv_alloc. Qed.
 
 End vs.
 
 Section vs_ghost.
-Context {Λ : language} {Σ : iFunctorG} (i : gid) `{!InG Λ Σ i A}.
+Context `{inG Λ Σ A}.
 Implicit Types a : A.
 Implicit Types P Q R : iPropG Λ Σ.
 
 Lemma vs_own_updateP E γ a φ :
-  a ~~>: φ → own i γ a ={E}=> ∃ a', ■ φ a' ∧ own i γ a'.
+  a ~~>: φ → own γ a ={E}=> ∃ a', ■ φ a' ∧ own γ a'.
 Proof. by intros; apply vs_alt, own_updateP. Qed.
 
 Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A} E γ φ :
-  ∅ ~~>: φ → True ={E}=> ∃ a', ■ φ a' ∧ own i γ a'.
+  ∅ ~~>: φ → True ={E}=> ∃ a', ■ φ a' ∧ own γ a'.
 Proof. by intros; eapply vs_alt, own_updateP_empty. Qed.
 
-Lemma vs_update E γ a a' : a ~~> a' → own i γ a ={E}=> own i γ a'.
+Lemma vs_update E γ a a' : a ~~> a' → own γ a ={E}=> own γ a'.
 Proof. by intros; apply vs_alt, own_update. Qed.
-
 End vs_ghost.
-- 
GitLab