Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq

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,6 +62,22 @@ Section proof.
     iDestruct "HR" as "[_ $]".
   Qed.
 
+  Lemma mklock_unlocked_spec (R : iProp Σ) (l : loc) v :
+    {{{ l ↦ v ∗ ▷ R }}} mklock_unlocked [ #l ] {{{ γ, RET #(); ▷ lock_proto γ l R }}}.
+  Proof.
+    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,90 @@ 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.
+
+  Definition mutex_into_inner ty : val :=
+    funrec: <> ["m"] :=
+      let: "x" := new [ #ty.(ty_size) ] in
+      "x" <-{ty.(ty_size)} !("m" +ₗ #1);;
+      delete [ #(mutex ty).(ty_size); "m"];; return: ["x"].
+
+  Lemma mutex_into_inner_type ty `{!TyWf ty} :
+    typed_val (mutex_into_inner ty) (fn(∅; mutex ty) → ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>m. simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst.
+    rewrite (Nat2Z.id ty.(ty_size)).
+    (* Switch to Iris. *)
+    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"? *)
+    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 ">[]".
+    simpl. iDestruct (heap_mapsto_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..|].
+    (* FIXME: Swapping the order of $Hx and $Hm breaks. *)
+    iIntros "[Hx Hm]". wp_seq.
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ #lx ◁ box ty; #lm ◁ box (uninit (mutex ty).(ty_size))]
+        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. iSplitR "Hm0 Hm".
+      - iExists _. iFrame.
+      - iExists (_ :: _). rewrite heap_mapsto_vec_cons. iFrame.
+        rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+End code.

theories/typing/lib/mutex/mutexguard.v

@@ -29,7 +29,7 @@ Section mguard.
     }
   *)
 
-  Program Definition mutex_guard (α : lft) (ty : type) :=
+  Program Definition mutexguard (α : lft) (ty : type) :=
     {| ty_size := 1;
        ty_own tid vl :=
          match vl return _ with
@@ -80,3 +80,60 @@ Section mguard.
     { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
 
 End mguard.
+
+Section code.
+  Context `{!typeG Σ, !lockG Σ}.
+
+  Lemma mutex_acc E γ l ty tid q α κ :
+    ↑lftN ⊆ E → ↑mutexN ⊆ E →
+    let R := (&{κ} shift_loc l 1 ↦∗: ty_own ty tid)%I in
+    lft_ctx -∗ &shr{α,mutexN} lock_proto γ l R -∗ α ⊑ κ -∗
+    □ ((q).[α] ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ (q).[α])).
+  Proof.
+    (* FIXME: This should work: iIntros (?? R). *) intros ?? R.
+    iIntros "#LFT #Hshr #Hlincl !# Htok".
+    iMod (shr_bor_acc_tok with "LFT Hshr Htok") as "[Hproto Hclose1]"; [done..|].
+    iMod (fupd_intro_mask') as "Hclose2"; last iModIntro; first solve_ndisj.
+    iFrame. iIntros "Hproto". iMod "Hclose2" as "_".
+    iMod ("Hclose1" with "Hproto") as "$". done.
+  Qed.
+
+  Definition mutex_lock : val :=
+    funrec: <> ["mutex"] :=
+      let: "m" := !"mutex" in
+      let: "guard" := new [ #1 ] in
+      acquire ["m"];;
+      "guard" +ₗ #0 <- "m";;
+      delete [ #1; "mutex"];; return: ["guard"].
+
+  Lemma mutex_lock_type ty `{!TyWf ty} :
+    typed_val mutex_lock (fn(∀ α, ∅; &shr{α} mutex ty) → mutexguard α ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    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ακ']".
+    iDestruct (ownptr_uninit_own with "Hg") as (lg vlg) "(% & Hg & Hg†)".
+    subst g. inv_vec vlg=>g. rewrite heap_mapsto_vec_singleton.
+    (* All right, we are done preparing our context. Let's get going. *)
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
+    wp_apply (acquire_spec with "[] Hα"); first by iApply (mutex_acc with "LFT Hshr Hακ'").
+    iIntros "[Hlocked [Hcont Htok]]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
+    iMod ("Hclose1" with "Htok HL") as "HL".
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ x ◁ own_ptr _ _; #lg ◁ box (mutexguard α 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' //.
+      unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hg".
+      iExists _, _. iFrame "#∗". }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+End code.

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' →