prove Mutex::new

theories/lang/lib/lock.v

@@ -5,7 +5,8 @@ From iris.algebra Require Import excl.
 From lrust.lang Require Import lang proofmode notation.
 Set Default Proof Using "Type".
 
-Definition newlock : val := λ: [], let: "l" := Alloc #1 in "l" <- #false ;; "l".
+Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
+Definition mklock_locked : val := λ: ["l"], "l" <- #true.
 Definition try_acquire : val := λ: ["l"], CAS "l" #false #true.
 Definition acquire : val :=
   rec: "acquire" ["l"] := if: try_acquire ["l"] then #() else "acquire" ["l"].
@@ -61,16 +62,22 @@ Section proof.
     iDestruct "HR" as "[_ $]".
   Qed.
 
-  Lemma newlock_spec (R : iProp Σ) :
-    {{{ ▷ R }}} newlock [] {{{ l γ, RET #l; ▷ lock_proto γ l R ∗ † l … 1 }}}.
+  Lemma mklock_unlocked_spec (R : iProp Σ) (l : loc) v :
+    {{{ l ↦ v ∗ ▷ R }}} mklock_unlocked [ #l ] {{{ γ, RET #(); ▷ lock_proto γ l R }}}.
   Proof.
-    (* FIXME: Why is there no space between (l : loc)(γ : gname) as printed? *)
-    iIntros (Φ) "HR HΦ". wp_lam. wp_alloc l vl as "Hl" "H†". inv_vec vl=>v.
-    rewrite heap_mapsto_vec_singleton -wp_fupd. wp_let. wp_write.
+    iIntros (Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
     iMod (lock_proto_create with "Hl HR") as (γ) "Hproto".
     iApply "HΦ". by iFrame.
   Qed.
 
+  Lemma mklock_locked_spec (R : iProp Σ) (l : loc) v :
+    {{{ l ↦ v }}} mklock_locked [ #l ] {{{ γ, RET #(); ▷ lock_proto γ l R }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
+    iMod (lock_proto_create with "Hl [//]") as (γ) "Hproto".
+    iApply "HΦ". by iFrame.
+  Qed.
+
   (* At this point, it'd be really nice to have some sugar for symmetric
      accessors. *)
   Lemma try_acquire_spec E γ l R P :

theories/typing/lib/mutex/mutex.v

@@ -88,3 +88,50 @@ Section mutex.
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
 End mutex.
+
+Section code.
+  Context `{!typeG Σ, !lockG Σ}.
+
+  Definition mutex_new ty : val :=
+    funrec: <> ["x"] :=
+      let: "m" := new [ #(mutex ty).(ty_size) ] in
+      "m" +ₗ #1 <-{ty.(ty_size)} !"x";;
+      mklock_unlocked ["m" +ₗ #0];;
+      delete [ #ty.(ty_size); "x"];; return: ["m"].
+
+  Lemma mutex_new_type ty `{!TyWf ty} :
+    typed_val (mutex_new ty) (fn(∅; ty) → mutex ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (m); simpl_subst.
+    rewrite (Nat2Z.id (S ty.(ty_size))). (* FIXME: Having to do this after every type_new is rather annoying... *)
+    (* FIXME: The following should work.  We could then go into Iris later.
+    iApply (type_memcpy ty); [solve_typing..|]. *)
+    (* Switch to Iris. *)
+    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]".
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct (heap_mapsto_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.
+    (* 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.
+    (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
+      iFrame. iSplitL "Hx".
+      - iExists _. iFrame. rewrite uninit_own vec_to_list_length.
+          by iNext. (* FIXME: Just "done" should work here. *)
+      - iExists (_ :: vl). rewrite heap_mapsto_vec_cons. iFrame.
+        (* FIXME: Why does calling `iFrame` twice even make a difference? *)
+        iFrame. eauto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+End code.

theories/typing/lib/mutex/mutexguard.v

@@ -114,6 +114,7 @@ Section code.
     iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (g); simpl_subst.
     rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hx [Hm _]]]".
     rewrite !tctx_hasty_val [[x]]lock /=.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (γ κ') "[#Hshr #Hακ']".

theories/typing/programs.v

@@ -280,7 +280,7 @@ Section typing_rules.
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.
 
-  Lemma type_memcpy {E L} ty1 ty2 (n : Z) C T T' ty ty1' ty2' p1 p2 e:
+  Lemma type_memcpy {E L} ty ty1 ty2 (n : Z) C T T' ty1' ty2' p1 p2 e:
     Closed [] e →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
     typed_write E L ty1 ty ty1' →