Simplifying thread local invariants

By using the global ghost maps instead of our own ones.

program_logic/sts.v

@@ -127,8 +127,7 @@ Section sts.
        around accessors". *)
     iVs (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
     iVsIntro. iExists s. iFrame. iIntros (s' T') "H".
-    iVs ("HclSts" $! s' T' with "H") as "(Hinv & ?)". iFrame.
-    iVs ("Hclose" with "Hinv"). done.
+    iVs ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
   Qed.
 
   Lemma sts_open E N γ s0 T :

program_logic/thread_local.v

@@ -2,14 +2,10 @@ From iris.algebra Require Export gmap gset coPset.
 From iris.proofmode Require Import invariants tactics.
 Import uPred.
 
-Definition thread_id := positive.
+Definition thread_id := gname.
 
-Class thread_localG Σ := {
-  tl_enabled_inG :> inG Σ (gmapUR thread_id coPset_disjR);
-  tl_disabled_inG :> inG Σ (gmapUR thread_id (gset_disjR positive));
-  tl_enabled_name : gname;
-  tl_disabled_name : gname
-}.
+Class thread_localG Σ :=
+  tl_inG :> inG Σ (prodUR coPset_disjUR (gset_disjUR positive)).
 
 Definition tlN : namespace := nroot .@ "tl".
 
@@ -17,12 +13,11 @@ Section defs.
   Context `{irisG Λ Σ, thread_localG Σ}.
 
   Definition tl_tokens (tid : thread_id) (E : coPset) : iProp Σ :=
-    own tl_enabled_name {[ tid := CoPset E ]}.
+    own tid (CoPset E, ∅).
 
   Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
     (∃ i, ■ (i ∈ nclose N) ∧
-          inv tlN (P ★ own tl_disabled_name {[ tid := GSet {[i]} ]}
-                   ∨ tl_tokens tid {[i]}))%I.
+          inv tlN (P ★ own tid (∅, GSet {[i]}) ∨ tl_tokens tid {[i]}))%I.
 End defs.
 
 Instance: Params (@tl_tokens) 2.
@@ -33,41 +28,35 @@ Section proofs.
 
   Lemma tid_alloc :
     True =r=> ∃ tid, tl_tokens tid ⊤.
-  Proof.
-    iIntros.
-    iVs (own_empty (A:=gmapUR thread_id coPset_disjR) tl_enabled_name) as "Hempty".
-    iVs (own_updateP with "Hempty") as (m) "[Hm Hown]".
-      by apply alloc_updateP' with (x:=CoPset ⊤).
-    iDestruct "Hm" as %(tid & -> & _). eauto.
-  Qed.
+  Proof. by apply own_alloc. Qed.
 
   Lemma tl_tokens_disj tid E1 E2 :
     tl_tokens tid E1 ★ tl_tokens tid E2 ⊢ ■ (E1 ⊥ E2).
   Proof.
-    by rewrite /tl_tokens -own_op op_singleton own_valid -coPset_disj_valid_op
-               discrete_valid singleton_valid.
+    rewrite /tl_tokens -own_op own_valid -coPset_disj_valid_op discrete_valid.
+    by iIntros ([? _])"!%".
   Qed.
 
   Lemma tl_tokens_union tid E1 E2 :
     E1 ⊥ E2 → tl_tokens tid (E1 ∪ E2) ⊣⊢ tl_tokens tid E1 ★ tl_tokens tid E2.
   Proof.
-    intros ?. by rewrite /tl_tokens -own_op op_singleton coPset_disj_union.
+    intros ?. by rewrite /tl_tokens -own_op pair_op left_id coPset_disj_union.
   Qed.
 
-  Lemma tl_inv_alloc tid E N P : ▷ P ={E}=> tl_inv tid N P.
+  Lemma tl_inv_alloc tid E N P :
+    ▷ P ={E}=> tl_inv tid N P.
   Proof.
     iIntros "HP".
-    iVs (own_empty (A:=gmapUR thread_id (gset_disjR positive)) tl_disabled_name)
-      as "Hempty".
-    iVs (own_updateP with "Hempty") as (m) "[Hm Hown]".
-    { eapply alloc_unit_singleton_updateP' with (u:=∅) (i:=tid). done. apply _.
+    iVs (own_empty tid) as "Hempty".
+    iVs (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
+    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
       apply (gset_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)).
       intros Ef. exists (coPpick (nclose N ∖ coPset.of_gset Ef)).
       rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
       apply coPpick_elem_of=> Hfin.
       eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
       apply of_gset_finite. }
-    iDestruct "Hm" as %(? & -> & i & -> & ?).
+    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
     iVs (inv_alloc tlN with "[-]"). 2:iVsIntro; iExists i; eauto.
     iNext. iLeft. by iFrame.
   Qed.
@@ -87,9 +76,8 @@ Section proofs.
       iIntros "!==>[HP ?]". iFrame.
       iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
       + iCombine "Hdis" "Hdis2" as "Hdis".
-        iDestruct (own_valid with "Hdis") as %Hval.
-        revert Hval. rewrite op_singleton singleton_valid gset_disj_valid_op.
-        set_solver.
+        iDestruct (own_valid with "Hdis") as %[_ Hval]. revert Hval.
+        rewrite gset_disj_valid_op. set_solver.
       + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
     - iDestruct (tl_tokens_disj tid {[i]} {[i]} with "[-]") as %?. by iFrame.
       set_solver.