mask tweaking

theories/typing/lib/rc.v

@@ -45,7 +45,7 @@ Section rc.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN∖↑lftN}▷=∗ q.[κ] ∗ ∃ γ ν q',
+             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q',
                 na_inv tid rc_invN (rc_inv tid ν γ l' ty) ∗
                 &na{κ, tid, rc_invN}(own γ (◯ Some (q', 1%positive))) ∗
                 ty.(ty_shr) κ tid (shift_loc l' 1)
@@ -70,9 +70,7 @@ Section rc.
       iClear "H↦ Hinv Hpb".
       iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
       set (X := (∃ _ _ _, _)%I).
-      (* TODO: Would be nice to have a lemma for the next two lines. *)
-      iMod fupd_intro_mask' as "Hclose3"; last iModIntro; first solve_ndisj. iNext.
-      iMod "Hclose3" as "_". iAssert (|={F ∖ ↑shrN}=> X )%I with "[HP]" as ">HX".
+      iModIntro. iNext. iAssert (|={F ∖ ↑shrN}=> X )%I with "[HP]" as ">HX".
       { iDestruct "HP" as "[[Hl' [H† Hown]]|$]"; last done.
         iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"; first solve_ndisj.
         (* TODO: We should consider changing the statement of bor_create to dis-entangle the two masks such that this is no longer necessary. *)

theories/typing/own.v

@@ -63,7 +63,7 @@ Section own.
          end%I;
        ty_shr κ tid l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
+            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
     |}.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
@@ -81,7 +81,7 @@ Section own.
     intros _ ty κ κ' tid l. iIntros "#Hκ #H".
     iDestruct "H" as (l') "[Hfb #Hvs]".
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)). set_solver. set_solver.
+    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)). set_solver. set_solver.
     iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first set_solver.
     iMod ("Hvs" with "[%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
     iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".

theories/typing/util.v

@@ -18,15 +18,15 @@ Section util.
   Lemma delay_borrow_step :
     lfeE ⊆ N → (∀ x, PersistentP (Post x)) →
     lft_ctx -∗ &{κ} P -∗
-      □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1,F2}▷=∗ Post x ∗ Frame x) ={N}=∗ 
-      □ (∀ x, Pre x -∗ Frame x ={F1,F2}▷=∗ Post x ∗ Frame x).
+      □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x) ={N}=∗ 
+      □ (∀ x, Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x).
    *)
 
   Lemma delay_sharing_later N κ l ty tid :
     lftE ⊆ N →
     lft_ctx -∗ &{κ} ▷ l ↦∗: ty_own ty tid ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
-       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F,F ∖ ↑shrN ∖ ↑lftN}▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
+       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
   Proof.
     iIntros (?) "#LFT Hbor". rewrite bor_unfold_idx.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
@@ -34,9 +34,9 @@ Section util.
           with "[Hpbown]") as "#Hinv"; first by eauto.
     iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
+    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj.
       { rewrite bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
+      iModIntro. iNext. iMod "Hdelay" as "[Hb Htok]".
       iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
       iApply "Hclose". auto.
     - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.