From e431e1855921155819900ee5d46daef0dd257a87 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 May 2017 10:48:46 +0200
Subject: [PATCH] prove take_mut

---
 _CoqProject                    |  1 +
 theories/typing/lib/take_mut.v | 92 ++++++++++++++++++++++++++++++++++
 2 files changed, 93 insertions(+)
 create mode 100644 theories/typing/lib/take_mut.v

diff --git a/_CoqProject b/_CoqProject
index e7edaf13..66f9c191 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -53,6 +53,7 @@ theories/typing/lib/option.v
 theories/typing/lib/fake_shared_box.v
 theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
+theories/typing/lib/take_mut.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
 theories/typing/lib/arc.v
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
new file mode 100644
index 00000000..8572a07c
--- /dev/null
+++ b/theories/typing/lib/take_mut.v
@@ -0,0 +1,92 @@
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
+From lrust.lang.lib Require Import memcpy.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section code.
+  Context `{typeG Σ}.
+
+  Definition take ty : val :=
+    funrec: <> ["x"; "f"; "env"] :=
+      let: "x'" := !"x" in
+      let: "f'" := !"f" in
+      letalloc: "t" <-{ty.(ty_size)} !"x'" in
+      letcall: "r" := "f'" ["env"; "t"]%E in
+      Endlft;;
+      "x'" <-{ty.(ty_size)} !"r";;
+      delete [ #1; "x"];; delete [ #1; "f"];;  delete [ #ty.(ty_size); "r"];;
+      let: "r" := new [ #0] in return: ["r"].
+
+  Lemma take_type ty envty `{!TyWf ty, !TyWf envty} :
+    typed_val (take ty)
+      (fn(∀ α, ∅; &uniq{α} ty, fn(∅; envty, ty) → ty, envty) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+      inv_vec arg=>x f env. simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (x'); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (f'); simpl_subst.
+    iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (t); simpl_subst.
+    (* Switch to Iris. *)
+    iIntros (tid) "#LFT #HE Hna HL Hk [Ht [Hf [Hf' [Hx [Hx' [Henv _]]]]]]".
+    rewrite !tctx_hasty_val [[x]]lock [[f]]lock [[f']]lock [[env]]lock.
+    iDestruct (ownptr_uninit_own with "Ht") as (tl tvl) "(% & >Htl & Htl†)". subst t. simpl.
+    destruct x' as [[|lx'|]|]; try done. simpl.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & Hclose2)"; [solve_typing..|].
+    iMod (bor_acc with "LFT Hx' Hα") as "[Hx' Hclose3]"; first done.
+    iDestruct (heap_mapsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
+    wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using vec_to_list_length..|].
+    iIntros "[Htl Hx'↦]". wp_seq.
+    (* Prepare the lifetime, call the function.
+       In principle, we could try to make the β we create here the ϝ of the called
+       function, but that seems to actually be more work because we could not use
+       the lemmas proven in function.v. *)
+    iMod (lft_create with "LFT") as (β) "[Hβ Hβ†]"; first done.
+    iMod (bor_create with "LFT Hϝ") as "[Hβϝ Hβ†ϝ]"; first done.
+    iDestruct (frac_bor_lft_incl β ϝ with "LFT [>Hβϝ]") as "#Hβϝ".
+    { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
+    match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
+      assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
+    iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
+    iApply (type_type ((β ⊑ₑ ϝ) :: _) [β ⊑ₗ []]
+        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box ty])]
+        [ f' ◁ fn(∅; envty, ty) → ty; #tl ◁ box ty; env ◁ box envty ]
+       with "[] LFT [] Hna [Hβ Hβ†] [-Hf' Htl Htl† Hx'vl Henv]"); swap 1 3; swap 4 5.
+    { rewrite /llctx_interp. iSplitL; last done. (* FIXME: iSplit should work as one side is 'True', thus persistent. *)
+      iExists β. simpl. iSplit; first by rewrite left_id. iFrame "∗#". }
+    { iSplitL; last iApply "HE". iExact "Hβϝ". }
+    { iApply (type_call ()); solve_typing. (* This is showing that the lifetime bounds of f' are satisfied. *) }
+    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame. iExists _. iFrame. }
+    (* Prove the continuation of the function call. *)
+    iIntros (? ->%elem_of_list_singleton arg) "Hna Hβ". inv_vec arg=>r.
+    iIntros "[Hr _]". rewrite tctx_hasty_val /=.
+    iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
+    apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
+    { repeat econstructor. } simpl_subst. iNext.
+    iDestruct "Hβ" as "[Hβ _]". iDestruct "Hβ" as (Λ) "(% & Hβ & #Hβ†)".
+    simpl in *. subst β. rewrite (left_id static). iSpecialize ("Hβ†" with "Hβ").
+    wp_bind Endlft. iApply wp_mask_mono; last iApply (wp_step_fupd with "Hβ†"); auto with ndisj.
+    wp_seq. iIntros "#H↠!>". wp_seq.
+    wp_apply (wp_memcpy with "[$Hx'↦ $Hlr]"); [by auto using vec_to_list_length..|].
+    iIntros "[Hlx' Hlr]". wp_seq. iMod ("Hβ†ϝ" with "Hβ†") as ">Hϝ".
+    iMod ("Hclose3" with "[Hlx' Hrvl]") as "[Hlx' Hα]".
+    { iExists _. iFrame. }
+    iMod ("Hclose2" with "Hϝ HL") as "HL".
+    iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ x ◁ _; f ◁ _; #lr ◁ box (uninit ty.(ty_size)) ]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply (type_new _); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+
+End code.
-- 
GitLab