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

theories/lang/lib/lock.v

@@ -27,7 +27,7 @@ Section proof.
 
   Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
 
-  Global Instance lock_inv_ne γ l : NonExpansive (lock_proto γ l).
+  Global Instance lock_proto_ne γ l : NonExpansive (lock_proto γ l).
   Proof. solve_proper. Qed.
 
   Global Instance locked_timeless γ : TimelessP (locked γ).

theories/typing/lib/mutex/mutex.v

@@ -87,6 +87,20 @@ 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.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance mutex_ne : NonExpansive mutex.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
+  (* TODO: compat with eqtype, Send+Sync if ty is Send. *)
+
 End mutex.
 
 Section code.
@@ -174,4 +188,41 @@ Section code.
     iApply type_jump; solve_typing.
   Qed.
 
+  Definition mutex_get_mut : val :=
+    funrec: <> ["m"] :=
+      let: "m'" := !"m" in
+      "m" <- ("m'" +ₗ #1);;
+      return: ["m"].
+
+  Lemma mutex_get_mut_type ty `{!TyWf ty} :
+    typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α} mutex ty) → &uniq{α} ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg); inv_vec arg=>m; simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (m'); simpl_subst.
+    (* Go to Iris *)
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hm [Hm' _]]".
+    rewrite !tctx_hasty_val [[m]]lock.
+    destruct m' as [[|lm'|]|]; try done. simpl.
+    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']".
+    destruct vl as [|[[|m'|]|] vl]; try done. simpl.
+    iDestruct (heap_mapsto_vec_cons with "H↦") as "[H↦1 H↦2]".
+    iDestruct "Hm'" as "[% Hvl]".
+    iMod ("Hclose2" $! (shift_loc 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 vl. iFrame. }
+    iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ m ◁ own_ptr _ _; #(shift_loc 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 type_assign; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
 End code.

theories/typing/lib/mutex/mutexguard.v

@@ -79,6 +79,18 @@ Section mguard.
   Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
     { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
 
+  Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv
+                                    || exact: type_dist2_S).
+  Qed.
+  Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  (* TODO: compat with lft_incl and eqtype.
+     MutexGuard is Sync if T is Send. *)
+
 End mguard.
 
 Section code.
@@ -255,4 +267,7 @@ Section code.
     iApply type_jump; solve_typing.
   Qed.
 
+  (* TODO:
+     Should we do try_lock?
+   *)
 End code.

theories/typing/lib/rwlock/rwlockreadguard.v

@@ -112,6 +112,8 @@ Section rwlockreadguard.
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     eqtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
   Proof. intros. by eapply rwlockreadguard_proper. Qed.
+
+  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
 End rwlockreadguard.
 
 Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.

theories/typing/lib/rwlock/rwlockwriteguard.v

@@ -115,6 +115,8 @@ Section rwlockwriteguard.
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
   Proof. intros. by eapply rwlockwriteguard_proper. Qed.
+
+  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.

theories/typing/lib/spawn.v

@@ -56,6 +56,9 @@ Section join_handle.
   Qed.
   Global Instance join_handle_ne : NonExpansive join_handle.
   Proof. apply type_contractive_ne, _. Qed.
+
+  (* TODO: Looks like in Rust, we have T: Send -> JoinHandle<T>: Send and
+     T:Sync -> JoinHandle<T>: Sync. *)
 End join_handle.
 
 Section spawn.