From dbb14153668a48f5a4fbb2efe300147ba55b07d8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Mar 2017 09:19:01 +0100
Subject: [PATCH] Rc::deref
---
theories/typing/lib/rc.v | 56 ++++++++++++++++++++++++++++++++++++----
1 file changed, 51 insertions(+), 5 deletions(-)
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index b0cb325a..d46e6ddf 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -44,7 +44,7 @@ Section rc.
ty.(ty_shr) ν tid (shift_loc l 1))
| _ => False end;
ty_shr κ tid l :=
- ∃ (l' : loc), &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
+ ∃ (l' : loc), &frac{κ} (λ q, l ↦∗{q} [ #l']) ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
na_inv tid rc_invN (rc_inv tid ν γ l' ty) ∗
@@ -56,6 +56,8 @@ 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 "[>[] _]".
@@ -189,8 +191,8 @@ Section code.
iIntros "[Hx [Hrc' Hrc2]]". rewrite [[x]]lock.
destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
destruct rc2 as [[|lrc2|]|]; try done. iDestruct "Hrc2" as "[Hrc2 Hrc2†]".
- iDestruct "Hrc2" as (vl) "Hrc2". rewrite uninit_own.
- iDestruct "Hrc2" as "[>Hrc2↦ >SZ]". destruct vl as [|]; iDestruct "SZ" as %[=].
+ iDestruct "Hrc2" as (vl) "[>Hrc2 >SZ]". rewrite uninit_own.
+ destruct vl as [|]; iDestruct "SZ" as %[=].
destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
rewrite {1}/elctx_interp big_sepL_singleton.
@@ -224,10 +226,54 @@ Section code.
iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lrc2 ◁ box (rc ty)]%TC
with "[] LFT Hna [Hα1 Hα2] HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- unlock. iFrame "Hx". iFrame "Hrc2†". iExists _. erewrite heap_mapsto_vec_singleton.
- iFrame "Hrc2↦". iNext. iRight. iExists _, ν, _. iFrame "#∗". }
+ unlock. iFrame "Hx". iFrame "Hrc2†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+ iFrame "Hrc2". iNext. iRight. iExists _, ν, _. iFrame "#∗". }
{ rewrite /elctx_interp big_sepL_singleton. iFrame. }
iApply type_delete; [solve_typing..|].
iApply (type_jump [ #_ ]); solve_typing.
Qed.
+
+ Definition rc_deref : val :=
+ funrec: <> ["rc"] :=
+ let: "x" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ "x" <- (!"rc'" +ₗ #1);;
+ delete [ #1; "rc" ];; return: ["x"].
+
+ Lemma rc_deref_type ty :
+ typed_val rc_deref (fn(∀ α, [α]; &shr{α} rc ty) → &shr{α} ty).
+ Proof.
+ intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id 1).
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE HL Hk".
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iIntros "[Hrcx [Hrc' Hx]]".
+ destruct x as [[|x|]|]; try done.
+ (* FIXME why is x printed in the code as "LitV x", not "#x"? *)
+ iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[>Hx >SZ]".
+ rewrite uninit_own. destruct vl as [|]; iDestruct "SZ" as %[=].
+ destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
+ rewrite [[rcx]]lock. destruct rc' as [[|rc'|]|]; try done. simpl.
+ iDestruct "Hrc'" as (l') "[#Hrc' #Hdelay]".
+ (* All right, we are done preparing our context. Let's get going. *)
+ rewrite {1}/elctx_interp big_sepL_singleton. iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
+ iSpecialize ("Hdelay" with "[] Hα1"); last iApply (wp_fupd_step with "Hdelay"); [done..|].
+ iMod (frac_bor_acc with "LFT Hrc' Hα2") as (q') "[Hrc'↦ Hclose]"; first solve_ndisj.
+ rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hrc'↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "(#Hincl & #Hinv & #Hrctokb & #Hshr)". iModIntro.
+ wp_op. wp_write.
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} rc ty); #x ◁ box (&shr{α} ty)]%TC
+ with "[] LFT Hna [Hα1 Hα2] HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
+ unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+ iFrame "Hx". iNext. iApply ty_shr_mono; done. }
+ { rewrite /elctx_interp big_sepL_singleton. iFrame. }
+ iApply type_delete; [solve_typing..|].
+ iApply (type_jump [ #_ ]); solve_typing.
+ Qed.
+
End code.
--
GitLab