complete mutex

_CoqProject

@@ -52,6 +52,7 @@ theories/typing/lib/swap.v
 theories/typing/lib/take_mut.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
+theories/typing/lib/mutex/mutex.v
 theories/typing/lib/refcell/refcell_code.v
 theories/typing/lib/refcell/refcell.v
 theories/typing/lib/refcell/ref_code.v

theories/lang/lock.v

@@ -42,6 +42,8 @@ Section proof.
 
   Global Instance lock_proto_inv_ne l γ: NonExpansive (lock_proto_inv l γ).
   Proof. rewrite /lock_proto_inv =>????. apply GPS_PPInv_ne. solve_proper. Qed.
+  Global Instance lock_proto_lc_ne l γ R: NonExpansive (lock_proto_lc l γ R).
+  Proof. rewrite /lock_proto_lc =>????. solve_proper. Qed.
 
   Global Instance lock_proto_lc_persistent: Persistent (lock_proto_lc l γ R0 R) := _.
 

theories/typing/lib/mutex/mutex.v

-From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import big_op.
 From lrust.lang Require Import memcpy lock.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Export type.
@@ -11,7 +8,7 @@ Set Default Proof Using "Type".
 Definition mutexN := lrustN .@ "mutex".
 
 Section mutex.
-  Context `{!typeG Σ, lockG Σ}.
+  Context `{!typeG Σ, !lockG Σ}.
 
   (*
     pub struct Mutex<T: ?Sized> {
@@ -80,17 +77,17 @@ Section mutex.
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
-  (* Global Instance mutex_type_ne : TypeNonExpansive mutex.
+  Global Instance mutex_type_ne : TypeNonExpansive mutex.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
                                               f_type_equiv || f_contractive || f_equiv).
-  Qed. *)
+  Qed.
 
-  (* Global Instance mutex_ne : NonExpansive mutex.
+  Global Instance mutex_ne : NonExpansive mutex.
   Proof.
     constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
-  Qed. *)
+  Qed.
 
   Global Instance mutex_mono E L : Proper (eqtype E L ==> subtype E L) mutex.
   Proof.
@@ -133,7 +130,7 @@ Section mutex.
 End mutex.
 
 Section code.
-  Context `{!typeG Σ}.
+  Context `{!typeG Σ, !lockG Σ}.
 
   Definition mutex_new ty : val :=
     funrec: <> ["x"] :=
@@ -156,13 +153,13 @@ Section code.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hm [Hx _]]".
     rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Hm") as (lm vlm) "(% & Hm & Hm†)".
-    subst m. inv_vec vlm=>m vlm. simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+    subst m. inv_vec vlm=>m vlm. simpl. iDestruct (own_loc_na_vec_cons with "Hm") as "[Hm0 Hm]".
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
-    iDestruct (heap_mapsto_ty_own with "Hx") as (vl) "[>Hx Hxown]".
+    iDestruct (own_loc_na_ty_own with "Hx") as (vl) "[>Hx Hxown]".
     (* All right, we are done preparing our context. Let's get going. *)
-    wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [by rewrite vec_to_list_length..|].
-    iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_loc_0. wp_lam.
-    wp_write.
+    wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [done|by rewrite vec_to_list_length..|].
+    iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_0. wp_lam.
+    iApply (wp_hist_inv); [done|]. iIntros "#HINV". wp_write.
     (* Switch back to typing mode. *)
     iApply (type_type _ _ _ [ #lx ◁ box (uninit ty.(ty_size)); #lm ◁ box (mutex ty)]
         with "[] LFT HE Hna HL Hk"); last first.
@@ -170,7 +167,8 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
       iFrame. iSplitL "Hx".
       - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
-      - iExists (#false :: vl). rewrite heap_mapsto_vec_cons. iFrame; eauto. }
+      - iExists (#false :: vl). rewrite own_loc_na_vec_cons.
+        iFrame "∗ HINV". eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -193,12 +191,12 @@ Section code.
     iDestruct (ownptr_uninit_own with "Hx") as (lx vlx) "(% & Hx & Hx†)".
     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]".
+    iDestruct (own_loc_na_ty_own with "Hm") as (vlm) "[>Hm [#HINV Hvlm]]".
     inv_vec vlm=>m vlm. destruct m as [[|m|]|]; try by iDestruct "Hvlm" as ">[]".
-    simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+    simpl. iDestruct (own_loc_na_vec_cons with "Hm") as "[Hm0 Hm]".
     iDestruct "Hvlm" as "[_ Hvlm]".
     (* All right, we are done preparing our context. Let's get going. *)
-    wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [by rewrite vec_to_list_length..|].
+    wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [done|by rewrite vec_to_list_length..|].
     (* FIXME: Swapping the order of $Hx and $Hm breaks. *)
     iIntros "[Hx Hm]". wp_seq.
     (* Switch back to typing mode. *)
@@ -208,7 +206,7 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
       iFrame. iSplitR "Hm0 Hm".
       - iExists _. iFrame.
-      - iExists (_ :: _). rewrite heap_mapsto_vec_cons. iFrame.
+      - iExists (_ :: _). rewrite own_loc_na_vec_cons. iFrame.
         rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -233,17 +231,17 @@ Section code.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
       [solve_typing..|].
     iMod (bor_acc_cons with "LFT Hm' Hα") as "[Hm' Hclose2]"; first done.
-    wp_op. iDestruct "Hm'" as (vl) "[H↦ Hm']".
+    wp_op. iDestruct "Hm'" as (vl) "[H↦ [#HINV Hm']]".
     destruct vl as [|[[|m'|]|] vl]; try done. simpl.
-    iDestruct (heap_mapsto_vec_cons with "H↦") as "[H↦1 H↦2]".
+    iDestruct (own_loc_na_vec_cons with "H↦") as "[H↦1 H↦2]".
     iDestruct "Hm'" as "[% Hvl]".
-    iMod ("Hclose2" $! ((lm' +ₗ 1) ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
+    iMod ("Hclose2" $! ((lm' >> 1) ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
     { iIntros "!> Hlm' !>". iNext. clear vl. iDestruct "Hlm'" as (vl) "[H↦ Hlm']".
-      iExists (_ :: _). rewrite heap_mapsto_vec_cons. do 2 iFrame. done. }
+      iExists (_ :: _). rewrite own_loc_na_vec_cons. do 2 iFrame. iFrame "HINV". eauto. }
     { iExists vl. iFrame. }
     iMod ("Hclose1" with "Hα HL") as "HL".
     (* Switch back to typing mode. *)
-    iApply (type_type _ _ _ [ m ◁ own_ptr _ _; #(lm' +ₗ 1) ◁ &uniq{α} ty]
+    iApply (type_type _ _ _ [ m ◁ 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. }