From ca3925dc009812788bc8b57aa15a3eb84e26ef11 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 11 May 2018 18:44:45 +0200
Subject: [PATCH] port RC
---
_CoqProject | 2 +
theories/typing/lib/rc/rc.v | 1130 ++++++++++++++++++++++++++++++++
theories/typing/lib/rc/weak.v | 488 ++++++++++++++
theories/typing/lib/take_mut.v | 2 +-
theories/typing/own.v | 2 +-
theories/typing/type.v | 2 +-
6 files changed, 1623 insertions(+), 3 deletions(-)
create mode 100644 theories/typing/lib/rc/rc.v
create mode 100644 theories/typing/lib/rc/weak.v
diff --git a/_CoqProject b/_CoqProject
index 733ff617..7ca49608 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -49,3 +49,5 @@ theories/typing/lib/option.v
theories/typing/lib/panic.v
theories/typing/lib/swap.v
theories/typing/lib/take_mut.v
+theories/typing/lib/rc/rc.v
+theories/typing/lib/rc/weak.v
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
new file mode 100644
index 00000000..8d785417
--- /dev/null
+++ b/theories/typing/lib/rc/rc.v
@@ -0,0 +1,1130 @@
+From Coq.QArith Require Import Qcanon.
+From iris.algebra Require Import auth csum frac agree.
+From lrust.lang Require Import memcpy.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing option.
+Set Default Proof Using "Type".
+
+Definition rc_stR :=
+ prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitC))) natUR.
+Class rcG Σ :=
+ RcG :> inG Σ (authR rc_stR).
+Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
+Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
+Proof. solve_inG. Qed.
+
+Definition rc_tok q : authR rc_stR :=
+ ◯ (Some $ Cinl (q, 1%positive), 0%nat).
+Definition rc_dropping_tok : authR rc_stR :=
+ ◯ (Some $ Cinr $ Excl (), 0%nat).
+Definition weak_tok : authR rc_stR := ◯ (None, 1%nat).
+
+Definition rcN := lrustN .@ "rc".
+Definition rc_invN := rcN .@ "inv".
+Definition rc_shrN := rcN .@ "shr".
+
+Section rc.
+ Context `{!typeG Σ, !rcG Σ}.
+
+ (* The RC can be in four different states :
+ - The living state, meaning that some strong reference exists. The
+ authoritative state is something like (Some (Cinl (q, strong)), weak),
+ where q is the total fraction owned by strong references, strong is
+ the number of strong references and weak is the number of weak
+ references.
+ - The "dropping" state, meaning that the last strong reference has been
+ dropped, and that the content in being dropped. The authoritative
+ state is something like (Some (Cinr (Excl ())), weak), where weak is
+ the number of weak references. The client owning the Excl also owns
+ the content of the box.
+ In our case, this state is not really necesary, because we do not
+ properly support dropping the content, but just copy it out of the RC
+ box. However, including it is more realistic, and this state is
+ still necessary for Arc anyway.
+ - The weak state, meaning that there only exists weak references. The
+ authoritative state is something like (None, weak), where weak is the
+ number of weak references.
+ - The dead state, meaning that no reference exist anymore. The
+ authoritative state is something like (None, 0).
+
+ Note that when we are in the living or dropping states, the weak reference
+ count stored in the heap is actually one plus the actual number of weak
+ references. This hack (which also exists in Rust's implementation) makes the
+ implementation of weak_drop easier, because it does not have to check the
+ strong count. *)
+
+ Definition rc_inv (tid : thread_id) ν (γ : gname) (l : loc) (ty : type) : vProp Σ :=
+ (∃ st : rc_stR, ⎡own γ (● st)⎤ ∗
+ match st with
+ | (Some (Cinl (q, strong)), weak) => ∃ q',
+ l ↦ #(Zpos strong) ∗ (l >> 1) ↦ #(S weak) ∗ ⎡† l…(2 + ty.(ty_size))⎤ ∗
+ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
+ (* We keep this view shift decomposed because we store the persistent
+ part in ty_own, to make it available with one step less. *)
+ ([†ν] ={↑lftN}=∗ ▷ (l >> 2) ↦∗: ty.(ty_own) tid)
+ | (Some (Cinr _), weak) =>
+ l ↦ #0 ∗ (l >> 1) ↦ #(S weak)
+ | (None, (S _) as weak) =>
+ l ↦ #0 ∗ (l >> 1) ↦ #weak ∗ ⎡† l…(2 + ty.(ty_size))⎤ ∗
+ (l >> 2) ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝
+ | _ => True
+ end)%I.
+
+ Global Instance rc_inv_ne ν γ l n :
+ Proper (type_dist2 n ==> dist n) (rc_inv tid ν γ l).
+ Proof.
+ solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
+ Qed.
+
+ Definition rc_persist tid ν (γ : gname) (l : loc) (ty : type) : vProp Σ :=
+ tc_opaque (∃ ty', ▷ type_incl ty' ty ∗
+ na_inv tid.(tid_na_inv_pool) rc_invN (rc_inv tid ν γ l ty') ∗
+ (* We use this disjunction, and not simply [ty_shr] here,
+ because [weak_new] cannot prove ty_shr, even for a dead
+ lifetime. *)
+ (ty.(ty_shr) ν tid (l >> 2) ∨ [†ν]) ∗
+ □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I.
+
+ Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
+ Proof. unfold rc_persist, tc_opaque. apply _. Qed.
+
+ Global Instance rc_persist_ne ν γ l n :
+ Proper (type_dist2 n ==> dist n) (rc_persist tid ν γ l).
+ Proof.
+ solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+ f_type_equiv || f_contractive || f_equiv).
+ Qed.
+
+ Lemma rc_persist_type_incl tid ν γ l ty1 ty2:
+ type_incl ty1 ty2 -∗ rc_persist tid ν γ l ty1 -∗ rc_persist tid ν γ l ty2.
+ Proof.
+ iIntros "#Hincl H". iDestruct "H" as (ty) "#(?&?& Hs &?)". iExists ty.
+ iFrame "#". iSplit.
+ - iNext. by iApply type_incl_trans.
+ - iDestruct "Hs" as "[?|?]"; last auto.
+ iLeft. iDestruct "Hincl" as "(_&_&Hincls)". by iApply "Hincls".
+ Qed.
+
+ Program Definition rc (ty : type) :=
+ {| ty_size := 1;
+ ty_own tid vl :=
+ match vl return _ with
+ | [ #(LitLoc l) ] =>
+ (* The ty_own part of the rc type cointains either the
+ shared protocol or the full ownership of the
+ content. The reason is that get_mut does not have the
+ masks to rebuild the invariants. *)
+ (l ↦ #1 ∗ (l >> 1) ↦ #1 ∗ ⎡† l…(2 + ty.(ty_size))⎤ ∗
+ ▷ (l >> 2) ↦∗: ty.(ty_own) tid) ∨
+ (∃ γ ν q, rc_persist tid ν γ l ty ∗ ⎡own γ (rc_tok q)⎤ ∗ q.[ν])
+ | _ => False end;
+ ty_shr κ tid l :=
+ ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+ ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
+ rc_persist tid ν γ l' ty ∗
+ &na{κ, tid.(tid_na_inv_pool), rc_shrN}(⎡own γ (rc_tok q')⎤)
+ |}%I.
+ Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
+ Next Obligation.
+ 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.
+ iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
+ destruct vl as [|[[|l'|]|][|]];
+ try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
+ setoid_rewrite own_loc_na_vec_singleton.
+ iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
+ iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
+ iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
+ set (C := (∃ γ ν q', _ ⊑ _ ∗ rc_persist _ _ _ _ _ ∗ &na{_,_,_} _)%I).
+ iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I
+ with "[Hpbown]") as "#Hinv"; [by iLeft; iFrame|].
+ iIntros "!> !#" (F q' ?) "Htok".
+ iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+ iDestruct "INV" as "[>Hbtok|#Hshr]".
+ - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
+ { rewrite bor_unfold_idx. iExists _. by iFrame. }
+ iClear "H↦ Hinv Hpb".
+ rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ remember ((∃ _ _ _, rc_persist _ _ _ _ _ ∗ _)%I) as X.
+ iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; [solve_ndisj|].
+ iModIntro. iNext. iAssert (X V) with "[>HP]" as "HX".
+ { iDestruct "HP" as "[(Hl'1 & Hl'2 & H† & Hown)|?]"; [|done].
+ iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"; first solve_ndisj.
+ (* TODO: We should consider changing the statement of
+ bor_create to dis-entangle the two masks such that this is no
+ longer necessary. *)
+ iApply (fupd_mask_mono (↑lftN)); first solve_ndisj.
+ setoid_rewrite <- monPred_at_sep. rewrite -monPred_at_exist -monPred_at_later.
+ iMod (bor_create with "LFT Hown") as "[HP HPend]"; first solve_ndisj.
+ iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
+ ◯ (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat))) as (γ) "[Ha Hf]".
+ { by apply auth_valid_discrete_2. }
+ iMod (na_inv_alloc tid.(tid_na_inv_pool) _ _ (rc_inv tid ν γ l' ty)
+ with "[Ha Hν2 Hl'1 Hl'2 H† HPend]") as "#?".
+ { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame "Ha". iExists _.
+ iFrame "H† Hl'1 Hl'2 Hν2 HPend". rewrite Qp_div_2; auto. }
+ iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
+ subst X. iExists _, _, _. iFrame. iExists ty. iFrame "#". iSplitR; last by auto.
+ by iApply type_incl_refl. }
+ subst X. iDestruct "HX" as (γ ν q'') "(#Hpersist & Hrctok)".
+ iMod ("Hclose2" $! (⎡own γ (rc_tok q'')⎤ ∗ (q'').[ν])%I
+ with "[] [$Hrctok]") as "[HX $]".
+ { iIntros "!>" (V') "-> [??] !> !>". auto 10 with iFrame. }
+ iAssert (C V) with "[>HX]" as "#$".
+ { iExists _, _, _. iFrame "Hpersist".
+ iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
+ iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
+ { iApply (bor_fracture with "LFT Hlft");
+ [split; [by rewrite Qp_mult_1_r|apply _]|solve_ndisj]. }
+ iApply (bor_na with "Hrc"); solve_ndisj. }
+ iApply ("Hclose1" with "[]"). by auto.
+ - iMod ("Hclose1" with "[]") as "_"; first by iRight.
+ iApply step_fupd_intro; first solve_ndisj. iFrame.
+ iApply (monPred_in_elim with "Hin"). by rewrite monPred_at_later.
+ Qed.
+ Next Obligation.
+ iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
+ iExists _. iSplit; first by iApply frac_bor_shorten.
+ iAlways. iIntros (F q) "% Htok".
+ iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
+ iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
+ iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
+ iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν ?) "(? & ? & ?)".
+ iExists _, _, _. iModIntro. iFrame. iSplit.
+ - by iApply lft_incl_trans.
+ - by iApply na_bor_shorten.
+ Qed.
+
+ Global Instance rc_wf ty `{!TyWf ty} : TyWf (rc ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+ Global Instance rc_type_contractive : TypeContractive rc.
+ Proof.
+ constructor;
+ solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+ f_type_equiv || f_contractive || f_equiv).
+ Qed.
+
+ Global Instance rc_ne : NonExpansive rc.
+ Proof. apply type_contractive_ne, _. Qed.
+
+ Lemma rc_subtype ty1 ty2 :
+ type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
+ Proof.
+ iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
+ iSplit; first done. iSplit; iAlways.
+ - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+ iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
+ { iLeft. iFrame. iDestruct "Hsz" as %->.
+ iFrame. iApply (own_loc_na_pred_wand with "Hc"). iApply "Hoincl". }
+ iDestruct "Hvl" as (γ ν q) "(#Hpersist & Htk & Hν)".
+ iRight. iExists _, _, _. iFrame "#∗". by iApply rc_persist_type_incl.
+ - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
+ iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+ iModIntro. iNext. iMod "H" as "[$ H]".
+ iDestruct "H" as (γ ν q') "(Hlft & Hpersist & Hna)".
+ iExists _, _, _. iFrame. by iApply rc_persist_type_incl.
+ Qed.
+
+ Global Instance rc_mono E L :
+ Proper (subtype E L ==> subtype E L) rc.
+ Proof.
+ iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+ iIntros "!# #HE". iApply rc_subtype. by iApply "Hsub".
+ Qed.
+ Global Instance rc_proper E L :
+ Proper (eqtype E L ==> eqtype E L) rc.
+ Proof. intros ??[]. by split; apply rc_mono. Qed.
+End rc.
+
+Section code.
+ Context `{!typeG Σ, !rcG Σ}.
+
+ Lemma rc_check_unique ty F tid (l : loc) :
+ ↑rc_invN ⊆ F →
+ {{{ na_own tid.(tid_na_inv_pool) F ∗ ty_own (rc ty) tid [ #l ] }}}
+ !#l in tid.(tid_tid)
+ {{{ strong, RET #(Zpos strong); l ↦ #(Zpos strong) ∗
+ (((⌜strong = 1%positive⌝ ∗
+ (∃ weak : Z, (l >> 1) ↦ #weak ∗
+ ((⌜weak = 1⌝ ∗
+ |={⊤,∅}▷=> ⎡† l…(2 + ty.(ty_size))⎤ ∗
+ ▷ (l >> 2) ↦∗: ty.(ty_own) tid ∗ na_own tid.(tid_na_inv_pool) F) ∨
+ (⌜weak > 1⌝ ∗
+ ((l ↦ #1 -∗ (l >> 1) ↦ #weak
+ ={⊤}=∗ na_own tid.(tid_na_inv_pool) F ∗ ty_own (rc ty) tid [ #l ]) ∧
+ (l ↦ #0 -∗ (l >> 1) ↦ #(weak - 1)
+ ={⊤,∅}▷=∗ ▷ (l >> 2) ↦∗: ty.(ty_own) tid ∗
+ ((l >> 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
+ ={⊤}=∗ na_own tid.(tid_na_inv_pool) F)))))) ∧
+ (l ↦ #0 ={⊤,∅}▷=∗
+ ▷ (l >> 2) ↦∗: ty.(ty_own) tid ∗ ⎡† l…(2 + ty.(ty_size))⎤ ∗
+ na_own tid.(tid_na_inv_pool) F ∗
+ (na_own tid.(tid_na_inv_pool) F ={⊤}=∗ ∃ weak : Z,
+ (l >> 1) ↦ #weak ∗
+ ((⌜weak = 1⌝ ∗ l ↦ #0 ∗ na_own tid.(tid_na_inv_pool) F) ∨
+ (⌜weak > 1⌝ ∗
+ (⎡† l…(2 + ty.(ty_size))⎤ -∗ (l >> 1) ↦ #(weak-1) -∗
+ (l >> 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
+ ={⊤}=∗ na_own tid.(tid_na_inv_pool) F))))))
+ ) ∨
+ (⌜(1 < strong)%positive⌝ ∗
+ ((l ↦ #(Zpos strong) ={⊤}=∗
+ na_own tid.(tid_na_inv_pool) F ∗ ty_own (rc ty) tid [ #l ]) ∧
+ (l ↦ #(Zpos strong - 1) ={⊤}=∗ na_own tid.(tid_na_inv_pool) F))))
+ }}}.
+ Proof.
+ iIntros (? Φ) "[Hna [(Hl1 & Hl2 & H† & Hown)|Hown]] HΦ".
+ - wp_read. iApply "HΦ". iFrame "Hl1". iLeft. iSplit. done. iSplit.
+ + iExists _. iFrame "Hl2". iLeft. iFrame. iSplit; first done.
+ iApply step_fupd_intro; auto.
+ + iIntros "Hl1". iFrame. iApply step_fupd_intro; first done.
+ auto 10 with iFrame.
+ - iDestruct "Hown" as (γ ν q) "(#Hpersist & Htok & Hν1)".
+ iPoseProof "Hpersist" as (ty') "(Hincl & Hinv & _ & #Hνend)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
+ iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
+ iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+ simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl].
+ + destruct st' as [[]| |]; try by inversion Hincl. apply (inj Cinl) in Hincl.
+ apply (inj2 pair) in Hincl. destruct Hincl as [<-%leibniz_equiv <-%leibniz_equiv].
+ iDestruct "Hproto" as (q') "(Hl1 & Hl2 & Hl† & >Hqq' & Hν & Hν†)".
+ iDestruct "Hqq'" as %Hqq'. iPoseProof "Hincl" as "(>Hincls & Hinclo & _)".
+ iDestruct "Hincls" as %Hincls.
+ wp_read. iApply "HΦ". iFrame "Hl1". iLeft. iSplit; first done. iSplit.
+ * iExists _. iFrame "Hl2". destruct weak.
+ -- iLeft. iSplit; first done. rewrite Hincls. iFrame "Hl†".
+ iMod (own_update_2 with "Hst Htok") as "Hst".
+ { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
+ apply cancel_local_update_unit, _. }
+ rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans.
+ iApply step_fupd_mask_mono;
+ last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
+ iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
+ iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
+ iModIntro. iNext. iDestruct "Hty" as (vl) "[??]". iExists _. iFrame.
+ by iApply "Hinclo".
+ -- iRight. iSplit; first by auto with lia. iSplit.
+ ++ iIntros "Hl1 Hl2".
+ iMod ("Hclose" with "[-Htok Hν1]") as "$"; last by auto 10 with iFrame.
+ iFrame. iExists _. auto with iFrame.
+ ++ iIntros "Hl1 Hl2".
+ rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans.
+ iApply step_fupd_mask_mono;
+ last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
+ iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
+ iMod (own_update_2 with "Hst Htok") as "Hst".
+ { apply auth_update_dealloc, prod_local_update_1,
+ (cancel_local_update_unit (Some _) None). }
+ iSplitL "Hty".
+ { iDestruct "Hty" as (vy) "[H Hty]". iExists vy. iFrame.
+ by iApply "Hinclo". }
+ iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame. iExists _.
+ iFrame. rewrite Hincls /=. iFrame. destruct Pos.of_succ_nat; try done.
+ rewrite /= ?Pos.pred_double_succ //.
+ * iIntros "Hl1".
+ iMod (own_update_2 with "Hst Htok") as "[Hst Htok]".
+ { apply auth_update. etrans.
+ - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_unit, _.
+ - apply (op_local_update _ _ (Some (Cinr (Excl tt)), 0%nat)). auto. }
+ rewrite -[(|={∅,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
+ iApply step_fupd_mask_mono;
+ last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
+ iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
+ iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
+ first by iExists _; iFrame; iFrame.
+ rewrite Hincls. iFrame. iSplitL "Hty".
+ { iDestruct "Hty" as (vl) "[??]". iExists _. iFrame. by iApply "Hinclo". }
+ iIntros "!> Hna". iClear "Hνend". clear q' Hqq' weak Hval.
+ iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
+ iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
+ iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+ simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl]; first last.
+ { apply csum_included in Hincl. destruct Hincl as
+ [->|[(?&?&[=]&?)|(?&?&[=<-]&->&?%exclusive_included)]]; try done. apply _. }
+ setoid_subst. iDestruct "Hproto" as ">(Hl1 & Hl2)". iExists _. iFrame.
+ rewrite right_id. destruct weak as [|weak].
+ -- iLeft. iFrame. iSplitR; first done.
+ iApply ("Hclose" with "[>- $Hna]"). iExists (None, 0%nat).
+ iMod (own_update_2 with "Hst Htok") as "$"; last done.
+ apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
+ apply cancel_local_update_unit, _.
+ -- iRight. iSplitR; first by auto with lia. iIntros "!> Hl† Hl2 Hvl".
+ iApply ("Hclose" with "[>- $Hna]"). iExists (None, S weak).
+ rewrite Hincls. iFrame. iSplitR "Hl2"; last first.
+ { simpl. destruct Pos.of_succ_nat; rewrite /= ?Pos.pred_double_succ //. }
+ iMod (own_update_2 with "Hst Htok") as "$"; last done.
+ apply auth_update_dealloc, prod_local_update', reflexivity.
+ rewrite -{1}(right_id None _ (Some _)). apply cancel_local_update_unit, _.
+ + apply csum_included in Hincl.
+ destruct Hincl as [->|[(?&(?,?)&[=<-]&->&(q',strong)&[]%(inj2 pair))|
+ (?&?&[=]&?)]]; first done. setoid_subst.
+ iDestruct "Hproto" as (q'') "(Hl1 & Hl2 & Hl† & >Hqq' & Hν & Hν†)".
+ iDestruct "Hqq'" as %Hqq'. wp_read. iApply "HΦ". iFrame "Hl1". iRight.
+ iSplit; first by rewrite !pos_op_plus; auto with lia. iSplit; iIntros "H↦".
+ * iMod ("Hclose" with "[- Htok Hν1]") as "$"; last by auto 10 with iFrame.
+ iFrame. iExists _. iFrame. auto with iFrame.
+ * iMod (own_update_2 with "Hst Htok") as "Hst".
+ { apply auth_update_dealloc.
+ rewrite -pair_op -Cinl_op Some_op -{1}(left_id 0%nat _ weak) -pair_op.
+ apply (cancel_local_update_unit _ (_, _)). }
+ iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
+ iSplitL; first last.
+ { rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
+ destruct strong=>//=. by rewrite Pos.pred_double_succ.
+ Qed.
+
+ Definition rc_strong_count : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "strong" := !("rc''" +ₗ #0) in
+ "r" <- "strong";;
+ delete [ #1; "rc" ];; return: ["r"].
+
+ Lemma rc_strong_count_type ty `{!TyWf ty} :
+ typed_val rc_strong_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & Hrctokb)".
+ iModIntro. wp_let. wp_op. rewrite shift_0.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+ setoid_subst; try done; last first.
+ { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
+ apply csum_included in Hincl. naive_solver. }
+ iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >% & Hνtok & Hν†)".
+ wp_read. wp_let.
+ (* And closing it again. *)
+ iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok Hν† $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); r ◁ box (uninit 1);
+ #(Z.pos s0) ◁ int ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock.
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+ iFrame. }
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition rc_weak_count : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "weak" := !("rc''" +ₗ #1) in
+ let: "one" := #1 in
+ let: "weak" := "weak" - "one" in
+ "r" <- "weak";;
+ delete [ #1; "rc" ];; return: ["r"].
+
+ Lemma rc_weak_count_type ty `{!TyWf ty} :
+ typed_val rc_weak_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & Hrctokb)".
+ iModIntro. wp_let. wp_op.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+ setoid_subst; try done; last first.
+ { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
+ apply csum_included in Hincl. naive_solver. }
+ iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >% & Hνtok & Hν†)".
+ wp_read. wp_let.
+ (* And closing it again. *)
+ iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok Hν† $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); r ◁ box (uninit 1);
+ #(S weak) ◁ int ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock.
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+ iFrame. }
+ iApply type_int. iIntros (?). simpl_subst.
+ iApply type_minus; [solve_typing..|]. iIntros (?). simpl_subst.
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition rc_new ty : val :=
+ funrec: <> ["x"] :=
+ let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+ let: "rc" := new [ #1 ] in
+ "rcbox" +ₗ #0 <- #1;;
+ "rcbox" +ₗ #1 <- #1;;
+ "rcbox" +ₗ #2 <-{ty.(ty_size)} !"x";;
+ "rc" <- "rcbox";;
+ delete [ #ty.(ty_size); "x"];; return: ["rc"].
+
+ Lemma rc_new_type ty `{!TyWf ty} :
+ typed_val (rc_new ty) (fn(∅; ty) → rc ty).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
+ rewrite !tctx_hasty_val.
+ iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
+ iDestruct (ownptr_uninit_own with "Hrcbox")
+ as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
+ iDestruct (own_loc_na_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+ iDestruct (own_loc_na_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+ rewrite shift_lblock_assoc.
+ iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
+ inv_vec vlrc=>?. rewrite own_loc_na_vec_singleton.
+ (* All right, we are done preparing our context. Let's get going. *)
+ wp_op. rewrite shift_0. wp_write. wp_op. wp_write.
+ wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
+ wp_apply (wp_memcpy with "[$Hrcbox↦2 $Hx↦]"); [by auto using vec_to_list_length..|].
+ iIntros "[Hrcbox↦2 Hx↦]". wp_seq. wp_write.
+ iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
+ iSplitL "Hx↦".
+ { iExists _. rewrite uninit_own. auto. }
+ iNext. iExists [_]. rewrite own_loc_na_vec_singleton. iFrame. iLeft.
+ rewrite freeable_sz_full_S. iFrame. iExists _. iFrame. }
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition rc_clone : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "strong" := !("rc''" +ₗ #0) in
+ "rc''" +ₗ #0 <- "strong" + #1;;
+ "r" <- "rc''";;
+ delete [ #1; "rc" ];; return: ["r"].
+
+ Lemma rc_clone_type ty `{!TyWf ty} :
+ typed_val rc_clone (fn(∀ α, ∅; &shr{α}(rc ty)) → rc ty).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[x]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
+ subst r. inv_vec vlr=>r. rewrite own_loc_na_vec_singleton.
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & Hrctokb)".
+ iModIntro. wp_let. wp_op. rewrite shift_0.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+ setoid_subst; try done; last first.
+ { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
+ apply csum_included in Hincl. naive_solver. }
+ iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >% & Hνtok & Hν†)".
+ wp_read. wp_let. wp_op. rewrite shift_0. wp_op. wp_write. wp_write.
+ (* And closing it again. *)
+ iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
+ { apply auth_update_alloc, prod_local_update_1,
+ (op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
+ split; simpl; last done. apply frac_valid'. rewrite -H comm_L -{2}(Qp_div_2 qb).
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
+ apply Qcplus_le_mono_r, Qp_ge_0. }
+ rewrite right_id -Some_op Cinl_op pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
+ iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok2 Hν† $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
+ rewrite [_ ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); #lr ◁ box (rc ty)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
+ rewrite own_loc_na_vec_singleton /=. simpl. eauto 10 with 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'" +ₗ #2);;
+ delete [ #1; "rc" ];; return: ["x"].
+
+ Lemma rc_deref_type ty `{!TyWf ty} :
+ typed_val rc_deref (fn(∀ α, ∅; &shr{α}(rc ty)) → &shr{α}ty).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
+ rewrite !tctx_hasty_val [[rcx]]lock.
+ iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
+ subst x. inv_vec vlrc2=>?. rewrite own_loc_na_vec_singleton.
+ destruct rc' as [[|rc'|]|]; try done. simpl of_val.
+ iDestruct "Hrc'" as (l') "[Hrc' #Hdelay]".
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hdelay" with "[] Hα1"); last iApply (wp_step_fupd with "Hdelay"); [done..|].
+ iMod (frac_bor_acc with "LFT Hrc' Hα2") as (q') "[Hrc'↦ Hclose2]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose2" with "[$Hrc'↦]") as "Hα2". iIntros "!> [Hα1 #Hproto] !>".
+ iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & _)".
+ iDestruct "Hpersist" as (ty') "(_ & _ & [Hshr|Hν†] & _)"; last first.
+ { iMod (lft_incl_acc with "Hαν Hα1") as (qν) "[Hν _]"; [done|].
+ iDestruct (lft_tok_dead with "Hν Hν†") as %[]. }
+ wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ rcx ◁ box (&shr{α}(rc ty)); #lrc2 ◁ box (&shr{α}ty)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite own_loc_na_vec_singleton.
+ iFrame "Hx". by iApply ty_shr_mono. }
+ iApply type_delete; [solve_typing..|].
+ 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: "strong" := !("rc'" +ₗ #0) in
+ if: "strong" = #1 then
+ (* Decrement strong *)
+ "rc'" +ₗ #0 <- #0;;
+ Skip;;
+ (* Return content *)
+ "r" <-{ty.(ty_size),Σ 0} !("rc'" +ₗ #2);;
+ (* 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'" ];;
+ "k" []
+ else
+ "rc'" +ₗ #1 <- "weak" - #1;;
+ "k" []
+ else
+ "r" <-{Σ 1} "rc'";;
+ "k" []
+ cont: "k" [] :=
+ delete [ #1; "rc"];; return: ["r"].
+
+ Lemma rc_try_unwrap_type ty `{!TyWf ty} :
+ typed_val (rc_try_unwrap ty) (fn(∅; rc ty) → Σ[ ty; rc ty ]).
+ Proof.
+ (* TODO: There is a *lot* of duplication between this proof and the one for drop. *)
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply (type_new (Σ[ ty; rc ty ]).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply (type_cont [] [ϝ ⊑ₗ []]
+ (λ _, [rcx ◁ box (uninit 1); r ◁ box (Σ[ ty; rc ty ])])) ;
+ [solve_typing..| |]; last first.
+ { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing. }
+ iIntros (k). simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
+ destruct rc' as [[|rc'|]|]; try done.
+ rewrite [[ #rc' ]]lock. wp_op. rewrite shift_0 -(lock [ #rc' ]).
+ wp_apply (rc_check_unique with "[$Hna $Hrc']"); first solve_ndisj.
+ iIntros (strong) "[Hrc Hc]". wp_let.
+ iDestruct "Hc" as "[[% [_ Hproto]]|[% [Hproto _]]]".
+ - subst strong. wp_op. wp_if. wp_op.
+ rewrite shift_0. wp_write. wp_bind (#☠;;#☠)%E.
+ iApply (wp_step_fupd with "[Hproto Hrc]");
+ [| |by iApply ("Hproto" with "Hrc")|];
+ [done..|wp_seq; iIntros "(Hty&H†&Hna&Hproto) !>"].
+ rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
+ iDestruct "H†" as "[H†1 H†2]". wp_seq. wp_bind (_<-_;;_)%E.
+ iApply (wp_wand with "[Hna HL Hty Hr H†2]").
+ { iApply (type_sum_memcpy_instr 0 [_; (rc ty)] with "LFT HE Hna HL"); first done.
+ { by eapply (write_own _ (uninit _)). } { apply read_own_move. }
+ iSplitL "Hr"; first by unlock; rewrite tctx_hasty_val. iSplitL; last done.
+ rewrite tctx_hasty_val'; last done. iFrame. }
+ iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
+ iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
+ iDestruct "Hproto" as "[(% & H↦strong & Hna)|[% Hproto]]".
+ + subst. wp_op. wp_if.
+ iApply (type_type _ _ _
+ [ r ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (Σ[ ty; rc ty]);
+ rcx ◁ box (uninit 1);
+ #rc' +ₗ #2 ◁ own_ptr (2 + ty.(ty_size)) (uninit (ty.(ty_size)));
+ #rc' +ₗ #0 ◁ own_ptr (2 + ty.(ty_size)) (uninit 2)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
+ rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
+ rewrite shift_0 /=. iFrame. iExists [_; _].
+ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+ auto with iFrame. }
+ iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ + rewrite (tctx_hasty_val' _ (#rc' +ₗ #2)); last done.
+ iDestruct "Hrc" as "[Hrc H†2]". wp_op; case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
+ iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
+ { rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
+ iApply (type_type _ _ _
+ [ r ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (Σ[ ty; rc ty]);
+ rcx ◁ box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+ iApply type_jump; solve_typing.
+ - wp_op; case_bool_decide as Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "[Hna Hrc]".
+ iApply (type_type _ _ _ [ r ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (uninit _);
+ rcx ◁ box (uninit 1); #rc' ◁ rc ty ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton.
+ rewrite !tctx_hasty_val tctx_hasty_val' //. unlock. iFrame. }
+ iApply (type_sum_assign Σ[ ty; rc ty ]); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition rc_drop ty : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #(option ty).(ty_size) ] in
+ withcont: "k":
+ let: "rc'" := !"rc" in
+ let: "strong" := !("rc'" +ₗ #0) in
+ "rc'" +ₗ #0 <- "strong" - #1;;
+ if: "strong" = #1 then
+ (* Return content. *)
+ "r" <-{ty.(ty_size),Σ some} !("rc'" +ₗ #2);;
+ (* 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'" ];;
+ "k" []
+ else
+ "rc'" +ₗ #1 <- "weak" - #1;;
+ "k" []
+ else
+ "r" <-{Σ none} ();;
+ "k" []
+ cont: "k" [] :=
+ delete [ #1; "rc"];; return: ["r"].
+
+ Lemma rc_drop_type ty `{!TyWf ty} :
+ typed_val (rc_drop ty) (fn(∅; rc ty) → option ty).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply (type_new (option ty).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply (type_cont [] [ϝ ⊑ₗ []]
+ (λ _, [rcx ◁ box (uninit 1); r ◁ box (option ty)]));
+ [solve_typing..| |]; last first.
+ { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing. }
+ iIntros (k). simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
+ destruct rc' as [[|rc'|]|]; try done. rewrite [[ #rc' ]]lock.
+ wp_op. rewrite shift_0. rewrite -(lock [ #rc' ]).
+ wp_apply (rc_check_unique with "[$Hna $Hrc']"); first solve_ndisj.
+ iIntros (strong) "[Hrc Hc]". wp_let. wp_op. rewrite shift_0.
+ rewrite {3}[Z.pos strong]lock. wp_op. unlock. wp_write.
+ iDestruct "Hc" as "[[% [_ Hproto]]|[% [_ Hproto]]]".
+ - subst strong. wp_bind (#1 = #1)%E.
+ iApply (wp_step_fupd with "[Hproto Hrc]");
+ [| |by iApply ("Hproto" with "Hrc")|];
+ [done..|wp_op; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
+ rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
+ iDestruct "H†" as "[H†1 H†2]". wp_bind (_<-_;;_)%E.
+ iApply (wp_wand with "[Hna HL Hty Hr H†2]").
+ { iApply (type_sum_memcpy_instr 1 [unit; _] with "LFT HE Hna HL"); first done.
+ { by eapply (write_own _ (uninit _)). } { apply read_own_move. }
+ iSplitL "Hr"; first by unlock; rewrite tctx_hasty_val. iSplitL; last done.
+ rewrite tctx_hasty_val'; last done. iFrame. }
+ iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
+ iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
+ iDestruct "Hproto" as "[(% & H↦strong & Hna)|[% Hproto]]".
+ + subst. wp_op. wp_if.
+ iApply (type_type _ _ _
+ [ r ◁ own_ptr (ty_size (option ty)) (option ty);
+ rcx ◁ box (uninit 1);
+ #rc' +ₗ #2 ◁ own_ptr (2 + ty.(ty_size)) (uninit (ty.(ty_size)));
+ #rc' +ₗ #0 ◁ own_ptr (2 + ty.(ty_size)) (uninit 2)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
+ rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
+ rewrite shift_0 /=. iFrame. iExists [_; _].
+ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+ auto with iFrame. }
+ iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ + rewrite (tctx_hasty_val' _ (#rc' +ₗ #2)); last done.
+ iDestruct "Hrc" as "[Hrc H†2]". wp_op. case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
+ iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
+ { rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
+ iApply (type_type _ _ _
+ [ r ◁ own_ptr (ty_size (option ty)) (option ty); rcx ◁ box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+ iApply type_jump; solve_typing.
+ - wp_op; case_bool_decide as Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "Hna".
+ iApply (type_type _ _ _ [ r ◁ own_ptr (ty_size (option ty)) (uninit _);
+ rcx ◁ box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton.
+ rewrite !tctx_hasty_val. iFrame. }
+ iApply (type_sum_unit (option ty)); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition rc_get_mut : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #2 ] in
+ withcont: "k":
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "strong" := !("rc''" +ₗ #0) in
+ if: "strong" = #1 then
+ let: "weak" := !("rc''" +ₗ #1) in
+ if: "weak" = #1 then
+ "r" <-{Σ some} ("rc''" +ₗ #2);;
+ "k" []
+ else
+ "r" <-{Σ none} ();;
+ "k" []
+ else
+ "r" <-{Σ none} ();;
+ "k" []
+ cont: "k" [] :=
+ delete [ #1; "rc"];; return: ["r"].
+
+ Lemma rc_get_mut_type ty `{!TyWf ty} :
+ typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α}(rc ty)) → option (&uniq{α}ty)).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply (type_cont [] [ϝ ⊑ₗ []]
+ (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α}ty)]));
+ [solve_typing..| |]; last first.
+ { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing. }
+ iIntros (k). simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
+ destruct rc' as [[|rc'|]|]; try done.
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
+ iMod (bor_acc_cons with "LFT Hrc' Hα") as "[Hrc' Hclose2]"; first solve_ndisj.
+ iDestruct (own_loc_na_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
+ inv_vec vl=>l. rewrite own_loc_na_vec_singleton.
+ wp_read. destruct l as [[|l|]|]; try done.
+ wp_let. wp_op. rewrite shift_0.
+ wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
+ { (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
+ iLeft. by iFrame. }
+ iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; case_bool_decide as Hc.
+ - wp_if. iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
+ iDestruct "Hc" as (weak) "[Hl2 Hweak]". wp_op. wp_read. wp_let.
+ iDestruct "Hweak" as "[[% Hrc]|[% [Hrc _]]]".
+ + subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
+ wp_op. iIntros "(Hl† & Hty & Hna)!>". wp_if.
+ iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα]"; [|iNext; iExact "Hty"|].
+ { iIntros "!> Hty". iExists [_]. rewrite own_loc_na_vec_singleton. iFrame "Hrc'".
+ iLeft. by iFrame. }
+ iMod ("Hclose1" with "Hα HL") as "HL".
+ iApply (type_type _ _ _ [ r ◁ box (uninit 2); #l +ₗ #2 ◁ &uniq{α}ty;
+ rcx ◁ box (uninit 1)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame. }
+ iApply (type_sum_assign (option (&uniq{_}_))); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ + wp_op; case_bool_decide; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
+ iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
+ { iIntros "!> HX". iModIntro. iExact "HX". }
+ { iExists [_]. rewrite own_loc_na_vec_singleton. iFrame. auto. }
+ iMod ("Hclose1" with "Hα HL") as "HL".
+ iApply (type_type _ _ _ [ r ◁ box (uninit 2); rcx ◁ box (uninit 1)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ unlock. iFrame. }
+ iApply (type_sum_unit (option (&uniq{_}_))); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ - wp_if. iDestruct "Hc" as "[[% _]|[% [Hproto _]]]"; first lia.
+ iMod ("Hproto" with "Hl1") as "[Hna Hrc]".
+ iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
+ { iIntros "!> HX". iModIntro. iExact "HX". }
+ { iExists [_]. rewrite own_loc_na_vec_singleton. iFrame. auto. }
+ iMod ("Hclose1" with "Hα HL") as "HL".
+ iApply (type_type _ _ _ [ r ◁ box (uninit 2); rcx ◁ box (uninit 1)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ unlock. iFrame. }
+ iApply (type_sum_unit (option (&uniq{_}_))); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ (* TODO : it is not nice that we have to inline the definition of
+ rc_new and of rc_deref. *)
+ Definition rc_make_mut (ty : type) (clone : val) : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #1 ] in
+ withcont: "k":
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "strong" := !("rc''" +ₗ #0) in
+ 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 ? *)
+ (* Inlined rc_new("c") begins. *)
+ let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+ "rcbox" +ₗ #0 <- #1;;
+ "rcbox" +ₗ #1 <- #1;;
+ "rcbox" +ₗ #2 <-{ty.(ty_size)} !"c";;
+ delete [ #ty.(ty_size); "c"];;
+ "rc'" <- "rcbox";;
+ (* Inlined rc_new ends. *)
+ letalloc: "rcold" <- "rc''" in
+ (* FIXME : here, we are dropping the old rc pointer. In the
+ case another strong reference has been dropped while
+ cloning, it is possible that we are actually dropping the
+ last reference here. This means that we may have to drop an
+ instance of [ty] here. Instead, we simply forget it. *)
+ let: "drop" := rc_drop ty in
+ letcall: "content" := "drop" ["rcold"]%E in
+ delete [ #(option ty).(ty_size); "content"];;
+ "r" <- "rcbox" +ₗ #2;;
+ "k" []
+ cont: "k" [] :=
+ delete [ #1; "rc"];; return: ["r"].
+
+ Lemma rc_make_mut_type ty `{!TyWf ty} clone :
+ (* ty : Clone, as witnessed by the impl clone *)
+ typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
+ typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(rc ty)) → &uniq{α}ty).
+ Proof.
+ intros Hclone E L. iApply type_fn; [solve_typing..|].
+ rewrite [(2 + ty_size ty)%nat]lock.
+ iIntros "/= !#". iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply (type_cont [] [ϝ ⊑ₗ []]
+ (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α}ty)]));
+ [solve_typing..| |]; last first.
+ { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing. }
+ iIntros (k). simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
+ destruct rc' as [[|rc'|]|]; try done.
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
+ [solve_typing..|].
+ iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"; first solve_ndisj.
+ iDestruct (own_loc_na_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
+ inv_vec vl=>l. rewrite own_loc_na_vec_singleton.
+ wp_read. destruct l as [[|l|]|]; try done. wp_let. wp_op. rewrite shift_0.
+ wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
+ { (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
+ iLeft. by iFrame. }
+ iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; case_bool_decide as Hc; wp_if.
+ - iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
+ iDestruct "Hc" as (weak) "[Hl2 Hweak]". wp_op. wp_read. wp_let.
+ iDestruct "Hweak" as "[[% Hrc]|[% [_ Hrc]]]".
+ + subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
+ wp_op. iIntros "(Hl† & Hty & Hna)!>". wp_if.
+ iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα1]"; [|iNext; iExact "Hty"|].
+ { iIntros "!> Hty". iExists [_]. rewrite own_loc_na_vec_singleton. iFrame "Hrc'".
+ iLeft. by iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{α}ty;
+ rcx ◁ box (uninit 1)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ tctx_hasty_val' //. unlock. iFrame. }
+ iApply type_assign; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ + wp_op; case_bool_decide; first lia. wp_if. wp_op. rewrite shift_0. wp_write. wp_op.
+ wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
+ iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia. done.
+ rewrite -!lock Nat2Z.id.
+ iNext. iIntros (lr) "/= ([H†|%] & H↦lr) [Hty Hproto] !>"; last lia.
+ rewrite 2!own_loc_na_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
+ wp_let. wp_op. rewrite shift_0. wp_write. wp_op. wp_write. wp_op. wp_op.
+ iDestruct "Hty" as (vlr) "[H↦vlr Hty]". rewrite shift_lblock_assoc.
+ iDestruct (ty_size_eq with "Hty") as %Hsz.
+ wp_apply (wp_memcpy with "[$Hlr3 $H↦vlr]").
+ { by rewrite repeat_length. } { by rewrite Hsz. }
+ iIntros "[Hlr3 Hvlr]". wp_seq. wp_write. wp_op.
+ iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
+ iMod ("Hclose2" $! ((lr >> 2) ↦∗: ty_own ty tid)%I
+ with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hα1]".
+ { iIntros "!> H !>". iExists [_]. rewrite own_loc_na_vec_singleton. iFrame.
+ iLeft. iFrame. }
+ { iExists _. iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(lr >> 2) ◁ &uniq{α}ty;
+ rcx ◁ box (uninit 1)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ tctx_hasty_val' //. unlock. iFrame. }
+ iApply type_assign; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ - wp_apply wp_new; first lia. done.
+ iIntros (lr) "/= ([H†|%] & H↦lr)"; last lia.
+ iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
+ iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
+ rewrite own_loc_na_vec_singleton. wp_write.
+ iAssert (∃ γ ν q, rc_persist tid ν γ l ty ∗ ⎡own γ (rc_tok q)⎤ ∗ q.[ν])%I
+ with "[>Hty]" as (γ ν q') "(Hty & Htok & Hν)".
+ { iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]"; last done.
+ iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
+ rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]"=>//.
+ iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"=>//.
+ iApply (fupd_mask_mono (↑lftN))=>//. iExists γ, ν, (1/2)%Qp. iFrame.
+ iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
+ iSplitR; first by iApply type_incl_refl.
+ iMod (ty_share with "LFT Hb Hν1") as "[Hty Hν]"=>//.
+ iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _. do 2 iFrame.
+ iExists _. iFrame. by rewrite Qp_div_2. }
+ iDestruct "Hty" as (ty') "#(Hty'ty & Hinv & Hs & Hν†)".
+ iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
+ wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
+ { iApply (Hclone _ [] with "LFT HE Hna").
+ by rewrite /llctx_interp. by rewrite /tctx_interp. }
+ clear clone Hclone. iIntros (clone) "(Hna & _ & Hclone)".
+ wp_let. wp_let. rewrite tctx_interp_singleton tctx_hasty_val.
+ iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
+ rewrite -[α ⊓ ν](right_id_L static lft_intersect).
+ iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_]
+ with "LFT HE Hna Hαν Hclone [H† H↦lr]"); [solve_typing| |].
+ { rewrite bi.big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
+ iFrame. iExists [_]. rewrite own_loc_na_vec_singleton. iFrame.
+ iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
+ iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
+ iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
+ iDestruct (ty_size_eq with "Hown") as %Hsz.
+ iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
+ wp_apply wp_new=>//. lia. iIntros (l') "(Hl'† & Hl')". wp_let. wp_op.
+ rewrite shift_0. rewrite -!lock Nat2Z.id.
+ rewrite !own_loc_na_vec_cons shift_lblock_assoc.
+ iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
+ wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]").
+ { by rewrite repeat_length. } { by rewrite Hsz. }
+ iIntros "[Hl'2 Hcl↦]". wp_seq. rewrite freeable_sz_full.
+ wp_apply (wp_delete with "[$Hcl↦ Hcl†]"); [lia|rewrite Hsz|].
+ { iDestruct "Hcl†" as "[?|%]"; auto. }
+ iIntros "_". wp_seq. wp_write.
+ iMod ("Hclose2" $! ((l' >> 2) ↦∗: ty_own ty tid)%I with
+ "[Hrc' Hl' Hl'1 Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
+ { iIntros "!> H". iExists [_]. rewrite own_loc_na_vec_singleton. iFrame.
+ iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
+ { iExists _. iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ iApply (type_type _ _ _ [ #l ◁ rc ty; #l' +ₗ #2 ◁ &uniq{α}ty;
+ r ◁ box (uninit 1); rcx ◁ box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ !tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
+ unfold rc_persist, tc_opaque. iFrame "∗#". eauto. }
+ iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
+ iApply type_let. apply rc_drop_type. solve_typing. iIntros (drop). simpl_subst.
+ iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_assign; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+End code.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
new file mode 100644
index 00000000..73376549
--- /dev/null
+++ b/theories/typing/lib/rc/weak.v
@@ -0,0 +1,488 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From lrust.lang Require Import memcpy.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing option.
+From lrust.typing.lib Require Export rc.
+Set Default Proof Using "Type".
+
+Section weak.
+ Context `{!typeG Σ, !rcG Σ}.
+
+ Program Definition weak (ty : type) :=
+ {| ty_size := 1;
+ ty_own tid vl :=
+ match vl return _ with
+ | [ #(LitLoc l) ] => ∃ γ ν, rc_persist tid ν γ l ty ∗ ⎡own γ weak_tok⎤
+ | _ => False end;
+ ty_shr κ tid l :=
+ ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+ ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν, rc_persist tid ν γ l' ty ∗
+ &na{κ, tid.(tid_na_inv_pool), rc_shrN}(⎡own γ weak_tok⎤)
+ |}%I.
+ Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
+ Next Obligation.
+ 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 with "LFT Hb Htok") as "[>[] _]".
+ setoid_rewrite own_loc_na_vec_singleton.
+ iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
+ iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
+ iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
+ set (C := (∃ _ _, rc_persist _ _ _ _ _ ∗ &na{_,_,_} _)%I).
+ iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I with "[Hpbown]") as "#Hinv";
+ [by iLeft; iFrame|].
+ iIntros "!> !#" (F q' ?) "Htok".
+ iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+ iDestruct "INV" as "[>Hbtok|#Hshr]".
+ - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
+ { rewrite bor_unfold_idx. iExists _. by iFrame. }
+ iClear "H↦ Hinv Hpb".
+ rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
+ iDestruct "HP" as (γ ν) "(#Hpersist & Hweak)".
+ iModIntro. iNext. rewrite -(monPred_at_embed V (own γ weak_tok)).
+ iMod ("Hclose2" with "[] Hweak") as "[Hb $]".
+ { iIntros "!> % -> ? !> !>". by eauto. }
+ iAssert (C V) with "[>Hb]" as "#HC".
+ { iExists _, _. iFrame "Hpersist". iApply (bor_na with "Hb"). solve_ndisj. }
+ iMod ("Hclose1" with "[]") as "_"; by auto.
+ - iMod ("Hclose1" with "[]") as "_"; [by iRight|].
+ iApply step_fupd_intro; first solve_ndisj. iFrame.
+ iApply monPred_in_elim; [done|]. by rewrite monPred_at_later.
+ Qed.
+ Next Obligation.
+ iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
+ iExists _. iSplit; first by iApply frac_bor_shorten.
+ iAlways. iIntros (F q) "% Htok".
+ iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
+ iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
+ iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
+ iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν) "(? & ?)".
+ iExists _, _. iFrame. by iApply na_bor_shorten.
+ Qed.
+
+ Global Instance weak_wf ty `{!TyWf ty} : TyWf (weak ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+ Global Instance weak_type_contractive : TypeContractive weak.
+ Proof.
+ constructor;
+ solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+ f_type_equiv || f_contractive || f_equiv).
+ Qed.
+
+ Global Instance weak_ne : NonExpansive weak.
+ Proof. apply type_contractive_ne, _. Qed.
+
+ Lemma weak_subtype ty1 ty2 :
+ type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
+ Proof.
+ iIntros "#Hincl". iPoseProof "Hincl" as "(Hsz & #Hoincl & #Hsincl)".
+ iSplit; first done. iSplit; iAlways.
+ - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+ iDestruct "Hvl" as (γ ν) "(#Hpersist & Htok)".
+ iExists _, _. iFrame "Htok". by iApply rc_persist_type_incl.
+ - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
+ iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+ iModIntro. iNext. iMod "H" as "[$ H]". iDestruct "H" as (γ ν) "(Hpersist & Hshr)".
+ iExists _, _. iFrame "Hshr". by iApply rc_persist_type_incl.
+ Qed.
+
+ Global Instance weak_mono E L :
+ Proper (subtype E L ==> subtype E L) weak.
+ Proof.
+ iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+ iIntros "!# #HE". iApply weak_subtype. iApply "Hsub"; done.
+ Qed.
+ Global Instance weak_proper E L :
+ Proper (eqtype E L ==> eqtype E L) weak.
+ Proof. intros ??[]. by split; apply weak_mono. Qed.
+End weak.
+
+Section code.
+ Context `{!typeG Σ, !rcG Σ}.
+
+ Definition rc_upgrade : val :=
+ funrec: <> ["w"] :=
+ let: "r" := new [ #2 ] in
+ withcont: "k":
+ let: "w'" := !"w" in
+ let: "w''" := !"w'" in
+ let: "strong" := !("w''" +ₗ #0) in
+ if: "strong" = #0 then
+ "r" <-{Σ none} ();;
+ "k" []
+ else
+ "w''" +ₗ #0 <- "strong" + #1;;
+ "r" <-{Σ some} "w''";;
+ "k" []
+ cont: "k" [] :=
+ delete [ #1; "w" ];; return: ["r"].
+
+ Lemma rc_upgrade_type ty `{!TyWf ty} :
+ typed_val rc_upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (rc ty)).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>w. simpl_subst.
+ iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply (type_cont [] [ϝ ⊑ₗ []]
+ (λ _, [w ◁ box (&shr{α}(weak ty)); r ◁ box (option (rc ty))])) ;
+ [solve_typing..| |]; last first.
+ { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing. }
+ iIntros (k). simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (w'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' [Hr _]]]".
+ rewrite !tctx_hasty_val [[w]]lock.
+ destruct w' as [[|lw|]|]; try done. iDestruct "Hw'" as (l') "[#Hlw #Hshr]".
+ iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
+ subst r. inv_vec vlr=>r0 r1. rewrite !own_loc_na_vec_cons.
+ iDestruct "Hr" as "(Hr1 & Hr2 & _)".
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlw Hα2") as (q') "[Hlw↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlw↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν) "#(Hpersist & Hwtokb)".
+ iModIntro. wp_let. wp_op. rewrite shift_0.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hwtok") as
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_valid_discrete_2.
+ destruct st as [[[q'' strong]| |]|]; try done.
+ - (* Success case. *)
+ iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >Hq''q0 & [Hν1 Hν2] & Hν†)".
+ iDestruct "Hq''q0" as %Hq''q0.
+ wp_read. wp_let. wp_op. wp_if. wp_op. rewrite shift_0. wp_op. wp_write.
+ (* Closing the invariant. *)
+ iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
+ { apply auth_update_alloc, prod_local_update_1,
+ (op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
+ split; simpl; last done. apply frac_valid'.
+ rewrite -Hq''q0 comm_L -{2}(Qp_div_2 qb).
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
+ apply Qcplus_le_mono_r, Qp_ge_0. }
+ rewrite right_id -Some_op Cinl_op pair_op.
+ iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hν2 Hν† $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
+ rewrite [_ ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2);
+ #l' ◁ rc ty ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
+ unlock. iFrame "Hr† Hw". iSplitL "Hr1 Hr2".
+ - iExists [_;_].
+ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. auto with iFrame.
+ - iRight. auto with iFrame. }
+ iApply (type_sum_assign (option (rc ty))); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ - (* Failure : dropping *)
+ (* TODO : The two failure cases are almost identical. *)
+ iDestruct "Hrcst" as "[Hl'1 Hl'2]". wp_read. wp_let. wp_op. wp_if.
+ (* Closing the invariant. *)
+ iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 $Hna]") as "Hna".
+ { iExists _. auto with iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame. iExists [_;_].
+ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. auto with iFrame. }
+ iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ - (* Failure : general case *)
+ destruct weakc as [|weakc]; first by simpl in *; lia.
+ iDestruct "Hrcst" as "[Hl'1 Hrcst]". wp_read. wp_let. wp_op. wp_if.
+ (* Closing the invariant. *)
+ iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hrcst $Hna]") as "Hna".
+ { iExists _. auto with iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame. iExists [_;_].
+ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. auto with iFrame. }
+ iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition rc_downgrade : val :=
+ funrec: <> ["rc"] :=
+ let: "r" := new [ #1 ] in
+ let: "rc'" := !"rc" in
+ let: "rc''" := !"rc'" in
+ let: "weak" := !("rc''" +ₗ #1) in
+ "rc''" +ₗ #1 <- "weak" + #1;;
+ "r" <- "rc''";;
+ delete [ #1; "rc" ];; return: ["r"].
+
+ Lemma rc_downgrade_type ty `{!TyWf ty} :
+ typed_val rc_downgrade (fn(∀ α, ∅; &shr{α}(rc ty)) → weak ty).
+ Proof.
+ (* TODO : this is almost identical to rc_clone *)
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[x]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
+ subst r. inv_vec vlr=>r. rewrite own_loc_na_vec_singleton.
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & Hrctokb)".
+ iModIntro. wp_let. wp_op.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
+ %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+ setoid_subst; try done; last first.
+ { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
+ apply csum_included in Hincl. naive_solver. }
+ iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hrcst)".
+ wp_read. wp_let. wp_op. wp_op. wp_write. wp_write.
+ (* And closing it again. *)
+ iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
+ { by apply auth_update_alloc, prod_local_update_2, (op_local_update_discrete _ _ 1%nat). }
+ iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+ iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hrcst $Hna]") as "Hna".
+ { iExists _. iFrame "Hrc●". iExists _. rewrite /Z.add Pos.add_1_r. iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); #lr ◁ box (weak ty)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
+ rewrite own_loc_na_vec_singleton /=. eauto 10 with iFrame. }
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ (* Exact same code as downgrade *)
+ Definition weak_clone : val :=
+ funrec: <> ["w"] :=
+ let: "r" := new [ #1 ] in
+ let: "w'" := !"w" in
+ let: "w''" := !"w'" in
+ let: "weak" := !("w''" +ₗ #1) in
+ "w''" +ₗ #1 <- "weak" + #1;;
+ "r" <- "w''";;
+ delete [ #1; "w" ];; return: ["r"].
+
+ Lemma weak_clone_type ty `{!TyWf ty} :
+ typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
+ Proof.
+ (* TODO : this is almost identical to rc_clone *)
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[x]]lock.
+ destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+ iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
+ subst r. inv_vec vlr=>r. rewrite own_loc_na_vec_singleton.
+ (* All right, we are done preparing our context. Let's get going. *)
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+ wp_bind (!_)%E.
+ iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+ iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+ iApply wp_fupd. wp_read.
+ iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+ iDestruct "Hproto" as (γ ν) "#[Hpersist Hwtokb]".
+ iModIntro. wp_let. wp_op.
+ (* Finally, finally... opening the thread-local Rc protocol. *)
+ iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
+ iAssert (∃ wv : Z, (l' >> 1) ↦ #wv ∗ ((l' >> 1) ↦ #(wv + 1) ={⊤}=∗
+ na_own tid.(tid_na_inv_pool) ⊤ ∗ (q / 2).[α] ∗ ⎡own γ weak_tok⎤))%I
+ with "[> Hna Hα1]" as (wv) "[Hwv Hclose2]".
+ { iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
+ iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hwtok") as
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_valid_discrete_2.
+ iMod (own_update with "Hrc●") as "[Hrc● $]".
+ { by apply auth_update_alloc, prod_local_update_2,
+ (op_local_update_discrete _ _ 1%nat). }
+ destruct st as [[[q'' strong]| |]|]; try done.
+ - iExists _. iDestruct "Hrcst" as (q0) "(Hl'1 & >$ & Hrcst)".
+ iIntros "!> Hl'2". iMod ("Hclose3" with "[$Hwtok] Hna") as "[$ Hna]".
+ iApply ("Hclose2" with "[- $Hna]"). iExists _. iFrame "Hrc●".
+ iExists _. rewrite /Z.add /= Pos.add_1_r. iFrame.
+ - iExists _. iDestruct "Hrcst" as "[Hl'1 >$]". iIntros "!> Hl'2".
+ iMod ("Hclose3" with "[$Hwtok] Hna") as "[$ Hna]".
+ iApply ("Hclose2" with "[- $Hna]"). iExists _. iFrame "Hrc●".
+ rewrite /Z.add /= Pos.add_1_r. iFrame.
+ - destruct weakc as [|weakc]; first by simpl in Hweak; lia.
+ iExists _. iDestruct "Hrcst" as "(Hl'1 & >$ & Hrcst)". iIntros "!> Hl'2".
+ iMod ("Hclose3" with "[$Hwtok] Hna") as "[$ Hna]".
+ iApply ("Hclose2" with "[- $Hna]"). iExists _. iFrame "Hrc●".
+ rewrite /Z.add /= Pos.add_1_r. iFrame. }
+ wp_read. wp_let. wp_op. wp_op. wp_write.
+ iMod ("Hclose2" with "Hwv") as "(Hna & Hα1 & Hwtok)".
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL". wp_write.
+ (* Finish up the proof. *)
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #lr ◁ box (weak ty)]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame. iExists [# #l']. rewrite own_loc_na_vec_singleton /=.
+ auto 10 with iFrame. }
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition weak_drop ty : val :=
+ funrec: <> ["w"] :=
+ withcont: "k":
+ let: "w'" := !"w" in
+ let: "weak" := !("w'" +ₗ #1) in
+ if: "weak" = #1 then
+ delete [ #(2 + ty.(ty_size)); "w'" ];;
+ "k" []
+ else
+ "w'" +ₗ #1 <- "weak" - #1;;
+ "k" []
+ cont: "k" [] :=
+ let: "r" := new [ #0] in
+ delete [ #1; "w"];; return: ["r"].
+
+ Lemma weak_drop_type ty `{!TyWf ty} :
+ typed_val (weak_drop ty) (fn(∅; weak ty) → unit).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (_ ϝ ret arg). inv_vec arg=>w. simpl_subst.
+ iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [w ◁ box (uninit 1)]));
+ [solve_typing..| |]; last first.
+ { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing. }
+ iIntros (k). simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (w'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' _]]".
+ rewrite !tctx_hasty_val [[w]]lock. destruct w' as [[|lw|]|]; try done. wp_op.
+ iDestruct "Hw'" as (γ ν) "[#Hpersist Hwtok]".
+ iAssert (∃ wv : Z, (lw >> 1) ↦ #wv ∗
+ ((⌜wv = 1⌝ ∗ na_own tid.(tid_na_inv_pool) ⊤ ∗
+ ∃ s, lw ↦ s ∗ ((lw >> 2) ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝) ∗
+ ⎡† lw … (2 + ty_size ty)⎤) ∨
+ (⌜wv > 1⌝ ∗ ((lw >> 1) ↦ #(wv - 1) ={⊤}=∗ na_own tid.(tid_na_inv_pool) ⊤))))%I
+ with "[>Hna Hwtok]" as (wv) "[Hlw [(% & Hna & H)|[% Hclose]]]".
+ { iPoseProof "Hpersist" as (ty') "([>Hszeq _] & Hinv & _ & _)".
+ iDestruct "Hszeq" as %Hszeq.
+ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|].
+ iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
+ iDestruct (own_valid_2 with "Hrc● Hwtok") as
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_valid_discrete_2.
+ destruct weakc; first by simpl in *; lia.
+ iMod (own_update_2 with "Hrc● Hwtok") as "Hrc●".
+ { apply auth_update_dealloc, prod_local_update_2,
+ (cancel_local_update_unit 1%nat), _. }
+ destruct st as [[[q'' strong]| |]|]; try done.
+ - iExists _. iDestruct "Hrcst" as (q0) "(Hlw & >$ & Hrcst)". iRight.
+ iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
+ iExists _. iFrame. iExists _. iFrame. simpl. destruct Pos.of_succ_nat; try done.
+ by rewrite /= Pos.pred_double_succ.
+ - iExists _. iDestruct "Hrcst" as "[Hlw >$]". iRight.
+ iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
+ iExists _. iFrame. simpl. destruct Pos.of_succ_nat; try done.
+ by rewrite /= Pos.pred_double_succ.
+ - iExists _. iDestruct "Hrcst" as "(>Hlw & >$ & >H† & >H)". destruct weakc.
+ + iLeft. iSplitR; first done. iMod ("Hclose" with "[$Hna Hrc●]") as "$".
+ { iExists _. iFrame. }
+ rewrite Hszeq. auto with iFrame.
+ + iRight. iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose".
+ iFrame. iExists _. iFrame. simpl. destruct Pos.of_succ_nat; try done.
+ by rewrite /= Pos.pred_double_succ. }
+ - subst. wp_read. wp_let. wp_op. wp_if.
+ iApply (type_type _ _ _ [ w ◁ box (uninit 1); #lw ◁ box (uninit (2 + ty.(ty_size))) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ unlock. iFrame. iDestruct "H" as (?) "(? & H↦ & ?)". iDestruct "H↦" as (?) "[? %]".
+ rewrite /= freeable_sz_full_S. iFrame. iExists (_::_::_).
+ rewrite 2!own_loc_na_vec_cons shift_lblock_assoc. iFrame.
+ iIntros "!> !%". simpl. congruence. }
+ iApply type_delete; [try solve_typing..|].
+ iApply type_jump; solve_typing.
+ - wp_read. wp_let. wp_op; case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
+ iMod ("Hclose" with "Hlw") as "Hna".
+ iApply (type_type _ _ _ [ w ◁ box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { unlock. by rewrite tctx_interp_singleton tctx_hasty_val. }
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition weak_new ty : val :=
+ funrec: <> [] :=
+ let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+ let: "w" := new [ #1 ] in
+ "rcbox" +ₗ #0 <- #0;;
+ "rcbox" +ₗ #1 <- #1;;
+ "w" <- "rcbox";;
+ return: ["w"].
+
+ Lemma weak_new_type ty `{!TyWf ty} :
+ typed_val (weak_new ty) (fn(∅) → weak ty).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (_ ϝ ret arg). inv_vec arg. simpl_subst.
+ iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (w); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]". rewrite !tctx_hasty_val.
+ iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox)
+ "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
+ iDestruct (own_loc_na_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+ iDestruct (own_loc_na_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+ iDestruct (ownptr_uninit_own with "Hw") as (lw vlw) "(% & Hw↦ & Hw†)". subst w.
+ inv_vec vlw=>?. rewrite own_loc_na_vec_singleton.
+ (* All right, we are done preparing our context. Let's get going. *)
+ wp_op. rewrite shift_0. wp_write. wp_op. wp_write.
+ iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
+ iPoseProof ("Hν†" with "Hν") as "H†". wp_bind (_ <- _)%E.
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [solve_ndisj..|].
+ wp_write. iIntros "#Hν !>". wp_seq.
+ iApply (type_type _ _ _ [ #lw ◁ box (weak ty)]
+ with "[] LFT HE Hna HL Hk [> -]"); last first.
+ { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
+ iExists [_]. rewrite own_loc_na_vec_singleton. iFrame.
+ iMod (own_alloc (● _ ⋅ ◯ _)) as (γ) "[??]"; last (iExists _, _; iFrame).
+ { apply auth_valid_discrete_2. by split. }
+ iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
+ iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
+ iExists _. iFrame. rewrite freeable_sz_full_S shift_lblock_assoc. iFrame.
+ iExists _. iFrame. rewrite vec_to_list_length. auto. }
+ iApply type_jump; solve_typing.
+ Qed.
+End code.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 2c1617eb..a7a76692 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -35,7 +35,7 @@ Section code.
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]".
+ iDestruct (own_loc_na_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.
(* Call the function. *)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index de3b28ca..7ae43e4d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -194,7 +194,7 @@ Section util.
Proof.
iSplit.
- iIntros "Hown". destruct v as [[|l|]|]; try done.
- iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_mapsto_ty_own.
+ iExists l. iDestruct "Hown" as "[Hown $]". rewrite own_loc_na_ty_own.
iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
- iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
iFrame. iExists _. iFrame.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 100c45cf..15390680 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -674,7 +674,7 @@ End subtyping.
Section type_util.
Context `{typeG Σ}.
- Lemma heap_mapsto_ty_own l ty tid :
+ Lemma own_loc_na_ty_own l ty tid :
l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
Proof.
iSplit.
--
GitLab