From efa2ccbbd0322d9fd9a61853e23268d3d77ce2a6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 13 Mar 2017 15:49:15 +0100
Subject: [PATCH] add Rc::try_unwrap code
---
theories/typing/lib/rc.v | 125 ++++++++++++++++++++++-----------------
1 file changed, 72 insertions(+), 53 deletions(-)
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 45e27b90..7f293a6b 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -128,6 +128,59 @@ End rc.
Section code.
Context `{!typeG Σ, !rcG Σ}.
+ Lemma rc_check_unique ty F tid (l : loc) :
+ ↑rc_invN ⊆ F →
+ {{{ na_own tid F ∗ ty_own (rc ty) tid [ #l ] }}}
+ !#l
+ {{{ c, RET #(Zpos c); l ↦ #(Zpos c) ∗
+ ((⌜c = 1%positive⌝ ∗ †{1%Qp}l…(S ty.(ty_size)) ∗ na_own tid F ∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid) ∨
+ (⌜(1 < c)%positive⌝ ∗ na_own tid (F ∖ ↑rc_invN) ∗
+ ∃ γ ν q q', na_inv tid rc_invN (rc_inv tid ν γ l ty) ∗
+ own γ (◯ Some (q, 1%positive)) ∗ own γ (● Some ((q + q')%Qp, c)) ∗
+ q.[ν] ∗ □ ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
+ ty.(ty_shr) ν tid (shift_loc l 1) ∗
+ (∀ c' q'', own γ (● Some (q'', c')) ∗ l ↦ #(Zpos c') ∗
+ (⌜(q + q')%Qp = q''⌝ ∨ ∃ qg, ⌜(q + q' = qg + q'')%Qp⌝ ∗ qg.[ν]) ∗ na_own tid (F ∖ ↑rc_invN) ={⊤}=∗
+ na_own tid F) )
+ ) }}}.
+ Proof.
+ iIntros (? Φ) "[Hna [(Hl & H† & Hown)|Hown]] HΦ".
+ - wp_read. iApply "HΦ". auto with iFrame.
+ - iDestruct "Hown" as (γ ν q) "(#Hinv & Htok & #Hshr & Hν1 & #Hνend)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
+ iDestruct "Hproto" as (st) "[>Hst Hproto]".
+ iDestruct (own_valid_2 with "Hst Htok") as %[[Hval|[? [[qa c] [[=<-] [-> Hst]]]]]%option_included _]%auth_valid_discrete_2; first done. (* Oh my, what a pattern... *)
+ iDestruct "Hproto" as (q') "(>Hl & H† & >% & >Hν2 & Hν† & _)". iApply wp_fupd.
+ destruct (decide (c ≤ 1)%positive) as [Hle|Hnle].
+ + (* Tear down the protocol. *)
+ assert (c = 1%positive) as ->.
+ { apply Pos.le_antisym; first done. exact: Pos.le_1_l. } clear Hle.
+ destruct Hst as [[??]|[_ Hle%pos_included]%prod_included]; last first.
+ { exfalso. eapply Pos.nlt_1_r. done. }
+ setoid_subst. iMod (own_update_2 with "Hst Htok") as "Hst".
+ { apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
+ apply cancel_local_update_empty, _. }
+ iMod ("Hclose" with "[$Hna Hst]") as "Hna".
+ { iExists None. auto. }
+ iSpecialize ("Hνend" with "[Hν1 Hν2]").
+ { rewrite -H0. iFrame. }
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|try solve_ndisj|].
+ { (* FIXME: solve_ndisj should solve this... *) set_solver+. }
+ wp_read. iIntros "#Hν". iMod ("Hν†" with "Hν") as "Hown". iModIntro.
+ iApply "HΦ". iFrame. iLeft. auto with iFrame.
+ + destruct Hst as [[??%leibniz_equiv]|[[q'' Hqa%leibniz_equiv] ?%pos_included]%prod_included].
+ { exfalso. simpl in *. subst c. apply Hnle. done. }
+ simpl in *. subst qa. wp_read. iApply "HΦ". iFrame. iRight. iModIntro. iSplit.
+ { iPureIntro. apply Pos.lt_nle. done. }
+ iFrame "Hna". iExists _, _, q, q''. iFrame "#∗%". iSplitR; first by iAlways.
+ iIntros (c' qx) "(Hst & Hl & Hq'' & Hna)". iApply "Hclose". iFrame "Hna".
+ iExists _. iFrame "Hst". iDestruct "Hq''" as "[%|Hq'']".
+ * iExists _. subst qx. iFrame "∗%". by iIntros "!> !#".
+ * iDestruct "Hq''" as (qg) "[% Hν']". iExists _.
+ iCombine "Hν2 Hν'" as "Hν". iFrame. iNext. iSplit; last by iAlways.
+ iPureIntro. rewrite [(q' + _)%Qp]comm_L assoc [(qx + _)%Qp]comm_L -H1. done.
+ Qed.
+
Definition rc_new ty : val :=
funrec: <> ["x"] :=
let: "rcbox" := new [ #(S ty.(ty_size)) ] in
@@ -282,6 +335,25 @@ Section code.
iApply type_jump; solve_typing.
Qed.
+ Definition rc_try_unwrap ty : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #(Σ[ ty; rc ty ]).(ty_size) ] in
+ withcont: "k":
+ let: "rc'" := !"rc" in
+ let: "count" := !("rc'" +ₗ #0) in
+ if: "count" = #1 then
+ "r" <-{ty.(ty_size),Σ 0} !("rc'" +ₗ #1);;
+ "k" []
+ else
+ "r" <-{(rc ty).(ty_size),Σ 1} !"rc";;
+ "k" []
+ cont: "k" [] :=
+ delete [ #1; "rc"];; return: ["r"].
+
+ Lemma rc_try_unwrap_type ty :
+ typed_val (rc_try_unwrap ty) (fn([]; rc ty) → Σ[ ty; rc ty ]).
+ Proof. Abort.
+
Definition rc_drop ty : val :=
funrec: <> ["rc"] :=
let: "x" := new [ #(option ty).(ty_size) ] in
@@ -300,59 +372,6 @@ Section code.
cont: "k" [] :=
delete [ #1; "rc"];; return: ["x"].
- Lemma rc_check_unique ty F tid (l : loc) :
- ↑rc_invN ⊆ F →
- {{{ na_own tid F ∗ ty_own (rc ty) tid [ #l ] }}}
- !#l
- {{{ c, RET #(Zpos c); l ↦ #(Zpos c) ∗
- ((⌜c = 1%positive⌝ ∗ †{1%Qp}l…(S ty.(ty_size)) ∗ na_own tid F ∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid) ∨
- (⌜(1 < c)%positive⌝ ∗ na_own tid (F ∖ ↑rc_invN) ∗
- ∃ γ ν q q', na_inv tid rc_invN (rc_inv tid ν γ l ty) ∗
- own γ (◯ Some (q, 1%positive)) ∗ own γ (● Some ((q + q')%Qp, c)) ∗
- q.[ν] ∗ □ ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
- ty.(ty_shr) ν tid (shift_loc l 1) ∗
- (∀ c' q'', own γ (● Some (q'', c')) ∗ l ↦ #(Zpos c') ∗
- (⌜(q + q')%Qp = q''⌝ ∨ ∃ qg, ⌜(q + q' = qg + q'')%Qp⌝ ∗ qg.[ν]) ∗ na_own tid (F ∖ ↑rc_invN) ={⊤}=∗
- na_own tid F) )
- ) }}}.
- Proof.
- iIntros (? Φ) "[Hna [(Hl & H† & Hown)|Hown]] HΦ".
- - wp_read. iApply "HΦ". auto with iFrame.
- - iDestruct "Hown" as (γ ν q) "(#Hinv & Htok & #Hshr & Hν1 & #Hνend)".
- iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
- iDestruct "Hproto" as (st) "[>Hst Hproto]".
- iDestruct (own_valid_2 with "Hst Htok") as %[[Hval|[? [[qa c] [[=<-] [-> Hst]]]]]%option_included _]%auth_valid_discrete_2; first done. (* Oh my, what a pattern... *)
- iDestruct "Hproto" as (q') "(>Hl & H† & >% & >Hν2 & Hν† & _)". iApply wp_fupd.
- destruct (decide (c ≤ 1)%positive) as [Hle|Hnle].
- + (* Tear down the protocol. *)
- assert (c = 1%positive) as ->.
- { apply Pos.le_antisym; first done. exact: Pos.le_1_l. } clear Hle.
- destruct Hst as [[??]|[_ Hle%pos_included]%prod_included]; last first.
- { exfalso. eapply Pos.nlt_1_r. done. }
- setoid_subst. iMod (own_update_2 with "Hst Htok") as "Hst".
- { apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
- apply cancel_local_update_empty, _. }
- iMod ("Hclose" with "[$Hna Hst]") as "Hna".
- { iExists None. auto. }
- iSpecialize ("Hνend" with "[Hν1 Hν2]").
- { rewrite -H0. iFrame. }
- iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|try solve_ndisj|].
- { (* FIXME: solve_ndisj should solve this... *) set_solver+. }
- wp_read. iIntros "#Hν". iMod ("Hν†" with "Hν") as "Hown". iModIntro.
- iApply "HΦ". iFrame. iLeft. auto with iFrame.
- + destruct Hst as [[??%leibniz_equiv]|[[q'' Hqa%leibniz_equiv] ?%pos_included]%prod_included].
- { exfalso. simpl in *. subst c. apply Hnle. done. }
- simpl in *. subst qa. wp_read. iApply "HΦ". iFrame. iRight. iModIntro. iSplit.
- { iPureIntro. apply Pos.lt_nle. done. }
- iFrame "Hna". iExists _, _, q, q''. iFrame "#∗%". iSplitR; first by iAlways.
- iIntros (c' qx) "(Hst & Hl & Hq'' & Hna)". iApply "Hclose". iFrame "Hna".
- iExists _. iFrame "Hst". iDestruct "Hq''" as "[%|Hq'']".
- * iExists _. subst qx. iFrame "∗%". by iIntros "!> !#".
- * iDestruct "Hq''" as (qg) "[% Hν']". iExists _.
- iCombine "Hν2 Hν'" as "Hν". iFrame. iNext. iSplit; last by iAlways.
- iPureIntro. rewrite [(q' + _)%Qp]comm_L assoc [(qx + _)%Qp]comm_L -H1. done.
- Qed.
-
Lemma rc_drop_type ty :
typed_val (rc_drop ty) (fn([]; rc ty) → option ty).
Proof.
--
GitLab