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

theories/lang/lib/spawn.v

@@ -47,7 +47,8 @@ Definition finish_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (∃ γf γj v, own γf (Excl ()) ∗ shift_loc c 1 ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
 
 Definition join_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
-  (∃ γf γj, own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ))%I.
+  (∃ γf γj Ψ', own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ') ∗
+   □ (∀ v, Ψ' v -∗ Ψ v))%I.
 
 Global Instance spawn_inv_ne n γf γj c :
   Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γf γj c).
@@ -96,7 +97,7 @@ Qed.
 Lemma join_spec (Ψ : val → iProp Σ) c :
   {{{ join_handle c Ψ }}} join [ #c] {{{ v, RET v; Ψ v }}}.
 Proof.
-  iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj) "(Hj & H† & #?)".
+  iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
   iLöb as "IH". wp_rec.
   wp_bind (!ˢᶜ _)%E. iInv N as "[[_ >Hj']|Hinv]" "Hclose".
   { iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
@@ -112,8 +113,17 @@ Proof.
   iModIntro. iApply wp_if. iNext. wp_op. wp_read. wp_let.
   iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
   { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
-  wp_free; first done. iApply "HΦ". done.
+  wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
 Qed.
+
+Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
+  □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
+Proof.
+  iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
+  iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?".
+  iApply "HΨ". iApply "HΨ'". done.
+Qed.
+
 End proof.
 
 Typeclasses Opaque finish_handle join_handle.

theories/typing/lib/cell.v

@@ -82,9 +82,6 @@ End cell.
 Section typing.
   Context `{typeG Σ}.
 
-  (* TODO RJ: Consider setting this globally. *)
-  Arguments ty_own : simpl never.
-
   (* Constructing a cell. *)
   Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
 

theories/typing/lib/mutex/mutexguard.v

@@ -267,7 +267,5 @@ Section code.
     iApply type_jump; solve_typing.
   Qed.
 
-  (* TODO:
-     Should we do try_lock?
-   *)
+  (* TODO: Should we do try_lock? *)
 End code.

theories/typing/lib/rc/rc.v

@@ -130,8 +130,6 @@ Section rc.
     iIntros (ty E κ l tid q ?) "#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.
-    (* Ideally, we'd change ty_shr to say "l ↦{q} #l" in the fractured borrow,
-       but that would be additional work here... *)
     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 "[>[] _]".
@@ -538,7 +536,7 @@ Section code.
       let: "rc'" := !"rc" in
       let: "rc''" := !"rc'" in
       let: "strong" := !("rc''" +ₗ #0) in
-      "rc''" +ₗ #0 <- "strong" +#1;;
+      "rc''" +ₗ #0 <- "strong" + #1;;
       "r" <- "rc''";;
       delete [ #1; "rc" ];; return: ["r"].
 
@@ -652,7 +650,8 @@ Section code.
         Skip;;
         (* Return content *)
         "r" <-{ty.(ty_size),Σ 0} !("rc'" +ₗ #2);;
-        (* Decrement weak, and deallocate if appropriate *)
+        (* Decrement weak (removing the one weak ref collectively held by all
+           strong refs), and deallocate if weak count reached 0. *)
         let: "weak" := !("rc'" +ₗ #1) in
         if: "weak" = #1 then
           delete [ #(2 + ty.(ty_size)); "rc'" ];;
@@ -747,7 +746,8 @@ Section code.
       if: "strong" = #1 then
         (* Return content. *)
         "r" <-{ty.(ty_size),Σ some} !("rc'" +ₗ #2);;
-        (* Decrement weak, and deallocate if appropriate *)
+        (* Decrement weak (removing the one weak ref collectively held by all
+           strong refs), and deallocate if weak count reached 0. *)
         let: "weak" := !("rc'" +ₗ #1) in
         if: "weak" = #1 then
           delete [ #(2 + ty.(ty_size)); "rc'" ];;
@@ -932,24 +932,35 @@ Section code.
       if: "strong" = #1 then
         let: "weak" := !("rc''" +ₗ #1) in
         if: "weak" = #1 then
+          (* This is the last strong ref, and there is no weak ref.
+             We just return a deep ptr into the Rc. *)
           "r" <- "rc''" +ₗ #2;;
           "k" []
         else
+          (* This is the last strong ref, but there are weak refs.
+             We make ourselves a new Rc, move the content, and mark the old one killed
+             (strong count becomes 0, strong idx removed from weak cnt).
+             We store the new Rc in our argument (which is a &uniq rc),
+             and return a deep ptr into it. *)
           "rc''" +ₗ #0 <- #0;;
           "rc''" +ₗ #1 <- "weak" - #1;;
+          (* Inlined rc_new("rc''" +ₗ #2) begins. *)
           let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
           "rcbox" +ₗ #0 <- #1;;
           "rcbox" +ₗ #1 <- #1;;
           "rcbox" +ₗ #2 <-{ty.(ty_size)} !"rc''" +ₗ #2;;
           "rc'" <- "rcbox";;
+          (* Inlined rc_new ends. *)
           "r" <- "rcbox" +ₗ #2;;
           "k" []
       else
+        (* There are other strong refs, we have to make a copy and clone the content. *)
         let: "x" := new [ #1 ] in
         "x" <- "rc''" +ₗ #2;;
         let: "clone" := clone in
         letcall: "c" := "clone" ["x"]%E in (* FIXME : why do I need %E here ? *)
         Endlft;;
+        (* Inlined rc_new("c") begins. *)
         let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
         "rcbox" +ₗ #0 <- #1;;
         "rcbox" +ₗ #1 <- #1;;
@@ -957,6 +968,7 @@ Section code.
         delete [ #ty.(ty_size); "c"];;
         let: "rc''" := !"rc'" in
         letalloc: "rcold" <- "rc''" in
+          (* Inlined rc_new ends. *)
         "rc'" <- "rcbox";;
         (* FIXME : here, we are dropping the old rc pointer. In the
            case another strong reference has been dropped while

theories/typing/lib/rwlock/rwlockwriteguard.v

@@ -116,7 +116,7 @@ Section rwlockwriteguard.
     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. *)
+  (* TODO: In Rust, the write guard is Sync if ty is Send+Sync. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.

theories/typing/lib/spawn.v

@@ -17,8 +17,7 @@ Section join_handle.
     {| ty_size := 1;
        ty_own tid vl :=
          match vl return _ with
-         | [ #(LitLoc l) ] =>
-           ∃ ty', ▷ type_incl ty' ty ∗ join_handle spawnN l (join_inv tid ty')
+         | [ #(LitLoc l) ] =>join_handle spawnN l (join_inv tid ty)
          | _ => False
          end%I;
        ty_shr κ tid l := True%I |}.
@@ -34,8 +33,9 @@ Section join_handle.
   Proof.
     iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
-      iDestruct "Hvl" as (ty) "[Hincl' ?]". iExists ty. iFrame.
-      iApply (type_incl_trans with "Hincl'"). done.
+      simpl. iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hown".
+      iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
+      iApply "Hincl". done.
     - iIntros "* _". auto.
   Qed.
 
@@ -57,8 +57,22 @@ Section join_handle.
   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. *)
+  Global Instance join_handle_send ty :
+    Send ty → Send (join_handle ty).
+  Proof.
+    iIntros (??? vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+    simpl. iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hv".
+    unfold join_inv. iApply own_send. (* FIXME: Why does "iApply send_change_tid" not work? *)
+    done.
+  Qed.
+
+  Global Instance join_handle_sync ty :
+    Sync (join_handle ty).
+  Proof.
+    iIntros (????) "**". (* FIXME: Why did it throw away the assumption we should have gotten? *)
+    done.
+  Qed.
+
 End join_handle.
 
 Section spawn.
@@ -88,7 +102,7 @@ Section spawn.
       iApply (spawn_spec _ (join_inv tid retty) with "[-]");
                               first solve_to_val; last first; last simpl_subst.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
-        iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
+        iIntros "?". by iFrame. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
       (* FIXME this is horrible. *)
       refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
@@ -129,12 +143,10 @@ Section spawn.
     iApply (type_let _ _ _ _ ([c' ◁ _])
                              (λ r, [r ◁ box retty])); try solve_typing; [|].
     { iIntros (tid) "#LFT _ $ $".
-      rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
-      destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
-      iApply (join_spec with "Hc'"). iNext. iIntros "* Hret".
-      rewrite tctx_interp_singleton tctx_hasty_val.
-      iDestruct (box_type_incl with "[$Hsub]") as "(_ & Hincl & _)".
-      iApply "Hincl". done. }
+      rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc".
+      destruct c' as [[|c'|]|]; try done.
+      iApply (join_spec with "Hc"). iNext. iIntros "* Hret".
+      rewrite tctx_interp_singleton tctx_hasty_val. done. }
     iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.