prove Mutex::into_inner

theories/typing/lib/mutex/mutex.v

@@ -103,7 +103,7 @@ Section code.
     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.
+      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.
@@ -134,4 +134,44 @@ Section code.
     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.