prove MutexGuard::deref_mut

theories/typing/lib/mutex/mutex.v

@@ -151,7 +151,7 @@ Section code.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hm _]]".
     rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Hx") as (lx vlx) "(% & Hx & Hx†)".
-    subst x. (* FIXME: Shouldn't things be printed as "#x"? *)
+    subst x. simpl.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as "[Hm Hm†]".
     iDestruct (heap_mapsto_ty_own with "Hm") as (vlm) "[>Hm Hvlm]".
     inv_vec vlm=>m vlm. destruct m as [[|m|]|]; try by iDestruct "Hvlm" as ">[]".

theories/typing/lib/mutex/mutexguard.v

@@ -135,6 +135,56 @@ Section code.
     iApply type_jump; solve_typing.
   Qed.
 
+  Definition mutexguard_derefmut : val :=
+    funrec: <> ["g"] :=
+      let: "g'" := !"g" in
+      let: "m" := !"g'" in
+      letalloc: "r" <- ("m" +ₗ #1) in
+      delete [ #1; "g"];; return: ["r"].
+
+  Lemma mutexguard_derefmut_type ty `{!TyWf ty} :
+    typed_val mutexguard_derefmut (fn (fun '(α, β) =>
+      FP_wf ∅ [# &uniq{α}(mutexguard β ty)]%T (&uniq{α}ty)%T)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (g'); simpl_subst.
+    (* Switch to Iris. *)
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hg' _]]".
+    rewrite !tctx_hasty_val [[g]]lock /=.
+    destruct g' as [[|lg|]|]; try done. simpl.
+    iMod (bor_exists with "LFT Hg'") as (vl) "Hbor"; first done.
+    iMod (bor_sep with "LFT Hbor") as "[H↦ Hprot]"; first done.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
+      [solve_typing..|].
+    destruct vl as [|[[|lm|]|] [|]]; simpl;
+      try by iMod (bor_persistent_tok with "LFT Hprot Hα") as "[>[] _]".
+    rewrite heap_mapsto_vec_singleton.
+    iMod (bor_exists with "LFT Hprot") as (γ) "Hprot"; first done.
+    iMod (bor_exists with "LFT Hprot") as (κ) "Hprot"; first done.
+    iMod (bor_sep with "LFT Hprot") as "[_ Hprot]"; first done.
+    iMod (bor_sep with "LFT Hprot") as "[Hβκ Hprot]"; first done.
+    iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
+    iMod (bor_persistent_tok with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
+    iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hclose2]"; first done.
+    wp_bind (!_)%E. iApply (wp_step_fupd with "[Hlm]");
+      [done| |by iApply (bor_unnest with "LFT Hlm")|]; first done.
+    wp_read. iIntros "Hlm !>". wp_let.
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iMod ("Hclose2" with "H↦") as "[_ Hα]".
+    iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ g ◁ own_ptr _ _; #lm +ₗ #1 ◁ &uniq{α} ty ]
+        with "[] LFT HE Hna HL Hk"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame. iApply bor_shorten; last done.
+      iApply lft_incl_glb; last by iApply lft_incl_refl.
+      iApply lft_incl_trans; done. }
+    iApply type_letalloc_1; [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
   Definition mutexguard_drop : val :=
     funrec: <> ["g"] :=
       let: "m" := !"g" in