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

_CoqProject

@@ -54,6 +54,8 @@ theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
+theories/typing/lib/mutex/mutex.v
+theories/typing/lib/mutex/mutexguard.v
 theories/typing/lib/refcell/refcell.v
 theories/typing/lib/refcell/ref.v
 theories/typing/lib/refcell/refmut.v

theories/lang/lib/lock.v

@@ -45,21 +45,20 @@ Section proof.
   Qed.
 
   (** The main proofs. *)
-  Lemma lock_proto_create (E : coPset) (R : iProp Σ) l (b : bool) :
-    l ↦ #b -∗ (if b then True else ▷ R) ={E}=∗ ∃ γ, ▷ lock_proto γ l R.
+  Lemma lock_proto_create (R : iProp Σ) l (b : bool) :
+    l ↦ #b -∗ (if b then True else ▷ R) ==∗ ∃ γ, ▷ lock_proto γ l R.
   Proof.
     iIntros "Hl HR".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iExists _, _. iFrame "Hl". destruct b; first done. by iFrame.
   Qed.
 
-  Lemma lock_proto_destroy E γ l R :
-    ↑N ⊆ E → 
-    ▷ lock_proto γ l R ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else ▷ R.
+  Lemma lock_proto_destroy γ l R :
+    lock_proto γ l R -∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R.
   Proof.
-    iIntros (?) "Hlck". iDestruct "Hlck" as (b) "[>Hl HR]".
+    iIntros "Hlck". iDestruct "Hlck" as (b) "[Hl HR]".
     iExists b. iFrame "Hl". destruct b; first done.
-    iDestruct "HR" as "[_ $]". done.
+    iDestruct "HR" as "[_ $]".
   Qed.
 
   (* At this point, it'd be really nice to have some sugar for symmetric

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.base_logic Require Import big_op.
+From lrust.lang.lib Require Import memcpy lock.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing option.
+Set Default Proof Using "Type".
+
+Definition mutexN := lrustN .@ "mutex".
+
+(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific
+   interface, like the one provided by lang.lib.lock.
+   It turns out that we need an accessor-based spec for this purpose, so that
+   we can put the protocol into shared borrows.  Cancellable invariants
+   don't work because their cancelling view shift has a non-empty mask,
+   and it would have to be executed in the consequence view shift of
+   a borrow.
+*)
+
+Section mutex.
+  Context `{!typeG Σ, !lockG Σ}.
+
+  (*
+    pub struct Mutex<T: ?Sized> {
+      // Note that this mutex is in a *box*, not inlined into the struct itself.
+      // Once a native mutex has been used once, its address can never change (it
+      // can't be moved). This mutex type can be safely moved at any time, so to
+      // ensure that the native mutex is used correctly we box the inner lock to
+      // give it a constant address.
+      inner: Box<sys::Mutex>,
+      poison: poison::Flag,
+      data: UnsafeCell<T>,
+    }
+  *)
+
+  Program Definition mutex (ty : type) :=
+    {| ty_size := 1 + ty.(ty_size);
+       ty_own tid vl :=
+         match vl return _ with
+         | #(LitInt z) :: vl' =>
+           ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
+         | _ => False end;
+       ty_shr κ tid l :=
+         ∃ γ κ',
+           &shr{κ, mutexN} (lock_proto γ l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗ κ ⊑ κ'
+    |}%I.
+  Next Obligation.
+    iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
+    iIntros "[_ %] !% /=". congruence.
+  Qed.
+  Next Obligation.
+    iIntros (ty E κ l tid q ?) "#LFT Hbor Htok".
+    iMod (bor_acc_cons with "LFT Hbor Htok") as "[H Hclose]"; first done.
+    iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as ">[Hl H↦]".
+    iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->].
+    (* We need to turn the ohne borrow into two, so we close it -- and then
+       we open one of them again. *)
+    iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ (shift_loc l 1 ↦∗: ty_own ty tid))%I
+          with "[] [Hl H↦ Hown]") as "[Hbor Htok]".
+    { clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl".
+      iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl).
+      rewrite heap_mapsto_vec_cons. iFrame. iPureIntro. eauto. }
+    { iNext. iSplitL "Hl"; first by eauto.
+      iExists vl. iFrame. }
+    clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done.
+    iMod (bor_acc_cons with "LFT Hl Htok") as "[>Hl Hclose]"; first done.
+    iDestruct "Hl" as (b) "Hl".
+    iMod (lock_proto_create with "Hl [Hbor]") as (γ) "Hproto".
+    { destruct b; last by iExact "Hbor". done. }
+    iMod ("Hclose" with "[] Hproto") as "[Hl Htok]".
+    { clear b. iIntros "!> Hproto !>". iDestruct (lock_proto_destroy with "Hproto") as (b) "[Hl _]".
+      iNext. eauto with iFrame. }
+    iFrame "Htok". iExists γ, κ.
+    iMod (bor_share with "Hl") as "$"; [solve_ndisj..|].
+    iApply lft_incl_refl.
+  Qed.
+  Next Obligation.
+    iIntros (ty κ κ' tid l) "#Hincl H".
+    iDestruct "H" as (γ κ'') "(#Hlck & #Hlft)".
+    iExists _, _. iSplit; first by iApply shr_bor_shorten.
+    iApply lft_incl_trans; done.
+  Qed.
+
+  Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+End mutex.

theories/typing/lib/mutex/mutexguard.v

+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op.
+From lrust.lang.lib Require Import memcpy lock.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing util option mutex.
+Set Default Proof Using "Type".
+
+(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific
+   interface, like the one provided by lang.lib.lock.
+   It turns out that we need an accessor-based spec for this purpose, so that
+   we can put the protocol into shared borrows.  Cancellable invariants
+   don't work because their cancelling view shift has a non-empty mask,
+   and it would have to be executed in the consequence view shift of
+   a borrow.
+*)
+
+Section mguard.
+  Context `{!typeG Σ, !lockG Σ}.
+
+  (*
+    pub struct MutexGuard<'a, T: ?Sized + 'a> {
+      // funny underscores due to how Deref/DerefMut currently work (they
+      // disregard field privacy).
+      __lock: &'a Mutex<T>,
+      __poison: poison::Guard,
+    }
+  *)
+
+  Program Definition mutex_guard (α : lft) (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc l) ] =>
+           ∃ γ β, locked γ ∗ α ⊑ β ∗
+             &shr{α, mutexN} (lock_proto γ l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+             &{β} (shift_loc l 1 ↦∗: ty.(ty_own) tid)
+         | _ => False end;
+       ty_shr κ tid l :=
+         ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗
+            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α⊓κ]
+                ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α⊓κ) tid (shift_loc l' 1) ∗ q.[α⊓κ]
+    |}%I.
+  Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed.
+  (* This is to a large extend copy-pasted from RWLock's write guard. *)
+  Next Obligation.
+    iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+    iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
+    destruct vl as [|[[|l'|]|][]];
+      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+    setoid_rewrite heap_mapsto_vec_singleton.
+    iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
+    iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
+    iMod (bor_sep with "LFT Hb") as "[Hlcked H]"; first done.
+    iMod (bor_sep with "LFT H") as "[Hαβ H]"; first done.
+    iMod (bor_sep with "LFT H") as "[_ H]"; first done.
+    iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
+    iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
+    (* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
+       goal, as does "iApply (lft_intersect_mono with ">")". *)
+    iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+  Qed.
+  Next Obligation.
+    iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
+    iExists _. iSplit.
+    - by iApply frac_bor_shorten.
+    - iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+  Qed.
+
+  Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
+End mguard.

theories/typing/lib/rwlock/rwlock.v

@@ -149,7 +149,7 @@ Section rwlock.
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
-  Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
+  Global Instance rwlock_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.