experiment with fractured borrows as accessors

theories/lifetime/frac_borrow.v

@@ -132,6 +132,16 @@ Section frac_bor.
     iIntros (?) "#LFT#H†". iApply (bor_fracture with "LFT [>]"); first done.
     by iApply (bor_fake with "LFT").
   Qed.
+
+  (** Fractured borrows are accessors *)
+  Global Instance into_acc_cinv E q κ `{Fractional _ φ} :
+    IntoAcc (X:=Qp) (&frac{κ}φ)
+            (↑lftN ⊆ E) (lft_ctx ∗ q.[κ]) E E
+            (λ q', ▷ φ q')%I (λ q', ▷ φ q')%I (λ _, Some q.[κ])%I.
+  Proof.
+    rewrite /IntoAcc /accessor. iIntros (?) "#Hinv [#Hlft Htok]".
+    iApply (frac_bor_acc with "Hlft Hinv Htok"). done.
+  Qed.
 End frac_bor.
 
 Lemma frac_bor_lft_incl `{invG Σ, lftG Σ, frac_borG Σ} κ κ' q:

theories/typing/lib/mutex/mutexguard.v

@@ -247,18 +247,19 @@ Section code.
     iDestruct "Hg'" as (lm) "[Hlg Hshr]".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose1)";
       [solve_typing..|].
-    iMod (frac_bor_acc with "LFT Hlg Hα1") as (qlx') "[H↦ Hclose2]"; first done.
+    wp_bind (!_)%E. iInv "Hlg" with "[$Hα1 $LFT]" as (qlx') "H↦".
     iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose3)";
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hclose4]".
-    wp_bind (!_)%E. iApply (wp_step_fupd with "[Hshr Hα2β]");
+    iApply (wp_step_fupd with "[Hshr Hα2β]");
          [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
-    wp_read. iIntros "[#Hshr Hα2β] !>". wp_let.
+    wp_read. iIntros "[#Hshr Hα2β] !>".
     iDestruct ("Hclose4" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hclose3" with "Hβ HL") as "HL".
-    iMod ("Hclose2" with "H↦") as "Hα1".
+    iFrame "H↦". iIntros "!> Hα1".
     iMod ("Hclose1" with "[$] HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    wp_let.
     (* Switch back to typing mode. *)
     iApply (type_type _ _ _ [ g ◁ own_ptr _ _; #lm +ₗ #1 ◁ &shr{α} ty ]
         with "[] LFT HE Hna HL Hk"); last first.