diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 9f0f52588d223c763d1221b66e7687be832ea273..9dc03accee77dcb2659ab7bebf3eae3229a9fb25 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -34,35 +34,37 @@ Section cont_context.
Qed.
Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
- ∀ tid, lft_ctx -∗ elctx_interp_0 E -∗
- cctx_interp tid C1 -∗ cctx_interp tid C2.
+ ∀ tid q, lft_ctx -∗ (elctx_interp E q -∗ cctx_interp tid C1) -∗
+ (elctx_interp E q -∗ cctx_interp tid C2).
Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
Proof.
split.
- - iIntros (??) "_ _ $".
- - iIntros (??? H1 H2 ?) "#LFT #HE H".
- iApply (H2 with "LFT HE"). by iApply (H1 with "LFT HE").
+ - iIntros (???) "_ $".
+ - iIntros (??? H1 H2 ??) "#LFT HE".
+ iApply (H2 with "LFT"). by iApply (H1 with "LFT").
Qed.
Lemma incl_cctx_incl E C1 C2 : C1 ⊆ C2 → cctx_incl E C2 C1.
Proof.
- rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid) "_ _ H * %".
- iApply ("H" with "* [%]"). by apply HC1C2.
+ rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid ?) "_ H HE * %".
+ iApply ("H" with "HE * [%]"). by apply HC1C2.
Qed.
Lemma cctx_incl_cons E k L n T1 T2 C1 C2:
cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E (CctxElt k L n T1 :: C1) (CctxElt k L n T2 :: C2).
Proof.
- iIntros (HC1C2 HT1T2 ?) "#LFT #HE H". rewrite /cctx_interp.
+ iIntros (HC1C2 HT1T2 ??) "#LFT H HE". rewrite /cctx_interp.
iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
- - iIntros (args) "HL' HT".
- iDestruct (llctx_interp_persist with "HL'") as "#HL".
- iMod (HT1T2 with "LFT HE HL HT") as "HT".
- iApply ("H" $! (CctxElt _ _ _ _) with "[%] * HL' HT").
- by apply elem_of_cons; auto.
- - iApply (HC1C2 with "LFT HE [H] * [%]"); last done.
- iIntros (x') "%". iApply ("H" with "[%]"). by apply elem_of_cons; auto.
+ - iIntros (args) "HL HT".
+ iMod (HT1T2 with "LFT HE HL HT") as "(HE & HL & HT)".
+ iSpecialize ("H" with "HE").
+ iApply ("H" $! (CctxElt _ _ _ _) with "[%] * HL HT").
+ constructor.
+ - iApply (HC1C2 with "LFT [H] HE * [%]"); last done.
+ iIntros "HE". iIntros (x') "%".
+ (* FIXME: If specialize follows by apply works, why does doing both in one apply loop? *)
+ iSpecialize ("H" with "HE"). iApply ("H" with "[%]"). by apply elem_of_cons; auto.
Qed.
End cont_context.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index f6777051ea57f3f20b4b2f094e2586f2b0efe2ee..73ffb52bf1529122999b05e718f1c84cd34870fd 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -12,8 +12,8 @@ Section fn.
(tys : A → vec type n) (ty : A → type) : type :=
{| st_own tid vl := (∃ f, ⌜vl = [f]⌠∗ □ ∀ (x : A) (args : vec val n) (k : val),
typed_body (E x) []
- [CctxElt k [] 1 (λ v, [TCtx_holds (v!!!0) (ty x)])]
- (zip_with (TCtx_holds ∘ of_val) args (tys x))
+ [CctxElt k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
+ (zip_with (TCtx_hasty ∘ of_val) args (tys x))
(f (of_val <$> (args : list val))))%I |}.
Next Obligation.
iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
@@ -34,8 +34,11 @@ Section fn.
iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
iApply ("HC" $! (CctxElt _ _ _ _) with "[%] * HL >").
by apply elem_of_list_singleton.
- iApply (subtype_tctx_incl with "LFT [HE0] HL0 HT"). by apply Hty.
- rewrite /elctx_interp_0 big_sepL_app. by iSplit.
+ rewrite /tctx_interp !big_sepL_singleton /=.
+ iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
+ iDestruct (Hty x with "LFT [HE0 HE'] HL0") as "(_ & #Hty & _)".
+ { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
+ by iApply "Hty".
- rewrite /tctx_interp
-(fst_zip (tys1 x) (tys2 x)) ?vec_to_list_length //
-{1}(snd_zip (tys1 x) (tys2 x)) ?vec_to_list_length //
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 8423cd7753ec8438eb985db0b1294d9ead604952..1ece0d6fdaf8c03b1f7abc3209893daf3a428dc2 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -160,18 +160,18 @@ Section lft_contexts.
(* Lifetime aliveness *)
Definition lctx_lft_alive (κ : lft) : Prop :=
- ∀ F qE qL, ⌜↑lftN ⊆ F⌠-∗ elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
+ ∀ F qE qL, ↑lftN ⊆ F → elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
Lemma lctx_lft_alive_static : lctx_lft_alive static.
Proof.
- iIntros (F qE qL) "%$$". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
+ iIntros (F qE qL ?) "$$". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
Qed.
Lemma lctx_lft_alive_local κ κs:
(κ, κs) ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
Proof.
- iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL) "% HE HL".
+ iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL ?) "HE HL".
iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
@@ -182,7 +182,7 @@ Section lft_contexts.
iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
- iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
- iDestruct "HL1" as "[HL1 HL2]". iDestruct "HE" as "[HE1 HE2]".
- iMod (Hκ with "* [%] HE1 HL1") as (q') "[Htok' Hclose]". done.
+ iMod (Hκ with "* HE1 HL1") as (q') "[Htok' Hclose]". done.
iMod ("IH" with "* HE2 HL2") as (q'') "[Htok'' Hclose']".
destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
@@ -198,7 +198,7 @@ Section lft_contexts.
Lemma lctx_lft_alive_external κ: ELCtx_Alive κ ∈ E → lctx_lft_alive κ.
Proof.
- iIntros ([i HE]%elem_of_list_lookup_1 F qE qL) "% HE $ !>".
+ iIntros ([i HE]%elem_of_list_lookup_1 F qE qL ?) "HE $ !>".
rewrite /elctx_interp /elctx_elt_interp.
iDestruct (big_sepL_lookup_acc with "HE") as "[Hκ Hclose]". done.
iExists qE. iFrame. iIntros "?!>". by iApply "Hclose".
@@ -207,10 +207,10 @@ Section lft_contexts.
Lemma lctx_lft_alive_incl κ κ':
lctx_lft_alive κ → lctx_lft_incl κ κ' → lctx_lft_alive κ'.
Proof.
- iIntros (Hal Hinc F qE qL) "% HE HL".
+ iIntros (Hal Hinc F qE qL ?) "HE HL".
iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hinc with "[HE] [HL]").
by iApply elctx_interp_persist. by iApply llctx_interp_persist.
- iMod (Hal with "[%] HE HL") as (q') "[Htok Hclose]". done.
+ iMod (Hal with "HE HL") as (q') "[Htok Hclose]". done.
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with ">").
by iApply "Hclose'".
@@ -232,7 +232,7 @@ Section lft_contexts.
lctx_lft_alive κ → elctx_sat E' → elctx_sat (ELCtx_Alive κ :: E').
Proof.
iIntros (Hκ HE' qE qL F) "% [HE1 HE2] [HL1 HL2]".
- iMod (Hκ with "[%] HE1 HL1") as (q) "[Htok Hclose]". done.
+ iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
iMod (HE' with "[%] HE2 HL2") as (q') "[HE' Hclose']". done.
destruct (Qp_lower_bound q q') as (q0 & q2 & q'2 & -> & ->). iExists q0.
rewrite {5 6}/elctx_interp big_sepL_cons /=.
@@ -252,4 +252,4 @@ Section lft_contexts.
iExists q. rewrite {1 2 4 5}/elctx_interp big_sepL_cons /=.
iIntros "{$Hincl $HE'}!>[_ ?]". by iApply "Hclose'".
Qed.
-End lft_contexts.
\ No newline at end of file
+End lft_contexts.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 423c66d00c288b1ba5bfef97bd1b0f4ae9a0d816..b14129e452142f62f9e102d28c796b94228c5d91 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -52,45 +52,44 @@ Section own.
â–· freeable_sz n ty.(ty_size) l)%I;
ty_shr κ tid E l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
- □ (∀ F, ⌜E ∪ mgmtE ⊆ F⌠={F,F∖E∖↑lftN}▷=∗ ty.(ty_shr) κ tid E l' ∨ [†κ]))%I
+ □ (∀ F q, ⌜E ∪ mgmtE ⊆ F⌠-∗ q.[κ] ={F,F∖E∖↑lftN}▷=∗ ty.(ty_shr) κ tid E l' ∗ q.[κ]))%I
|}.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
Next Obligation.
- move=>n ty E N κ l tid ?? /=. iIntros "#LFT Hshr".
+ move=>n ty E N κ l tid ??? /=. iIntros "#LFT Hshr Htok".
iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
- iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver. iExists l'.
+ iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
- iMod (bor_persistent with "LFT EQ") as "[>%|#H†]". set_solver.
- - subst. rewrite heap_mapsto_vec_singleton.
- iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
- iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
- rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
- iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
- with "[Hpbown]") as "#Hinv"; first by eauto.
- iIntros "!>!#*%". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
- iDestruct "INV" as "[>Hbtok|#Hshr]".
- + iMod (bor_later with "LFT [Hbtok]") as "Hb". set_solver.
- { rewrite bor_unfold_idx. eauto. }
- iModIntro. iNext. iMod "Hb". iLeft.
- iMod (ty.(ty_share) with "LFT Hb") as "#$". done. set_solver.
- iApply "Hclose". auto.
- + iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
- iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
- - iSplitL. by iApply (frac_bor_fake with "LFT"). iIntros "!>!#*_".
- iApply step_fupd_intro. set_solver. auto.
+ iMod (bor_persistent_tok with "LFT EQ Htok") as "[>% Htok]". set_solver.
+ iFrame "Htok". iExists l'.
+ subst. rewrite heap_mapsto_vec_singleton.
+ iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
+ iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
+ rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
+ iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
+ with "[Hpbown]") as "#Hinv"; first by eauto.
+ iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+ iDestruct "INV" as "[>Hbtok|#Hshr]".
+ - iMod (bor_later with "LFT [Hbtok]") as "Hb". set_solver.
+ { rewrite bor_unfold_idx. eauto. }
+ iModIntro. iNext. iMod "Hb".
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ Htok]". done. set_solver.
+ iFrame "Htok". iApply "Hclose". auto.
+ - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
+ iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
Next Obligation.
intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
iDestruct "H" as (l') "[Hfb #Hvs]".
- iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!#*%".
+ iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
iApply (step_fupd_mask_mono F _ _ (F∖E∖↑lftN)). set_solver. set_solver.
- iMod ("Hvs" with "* [%]") as "Hvs'". set_solver. iModIntro. iNext.
- iMod "Hvs'" as "[Hshr|H†]".
- - iLeft. by iApply (ty.(ty_shr_mono) with "LFT Hκ").
- - iRight. iApply (lft_incl_dead with "Hκ H†"). set_solver.
+ iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first set_solver.
+ iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+ iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+ by iApply (ty.(ty_shr_mono) with "LFT Hκ").
Qed.
Global Instance own_mono E L n :
@@ -106,10 +105,9 @@ Section own.
iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
iExists _. by iFrame.
- iIntros (????) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
- iExists l'. iFrame. iIntros "!#". iIntros (F') "%".
- iMod ("Hvs" with "* [%]") as "Hvs'". done. iModIntro. iNext.
- iMod "Hvs'" as "[Hshr|H†]"; last by auto.
- iLeft. iApply ("Hs" with "Hshr").
+ iExists l'. iFrame. iIntros "!#". iIntros (F' q) "% Htok".
+ iMod ("Hvs" with "* [%] Htok") as "Hvs'". done. iModIntro. iNext.
+ iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
Qed.
Global Instance own_proper E L n :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index cf23254fef2f3bf686df7e6d2e2f9fb980013890..e01a07fb0e8e60c50f4ea3af9162b5302f78eda0 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -9,7 +9,7 @@ Section product.
Program Definition unit : type :=
{| ty_size := 0; ty_own tid vl := ⌜vl = []âŒ%I; ty_shr κ tid E l := True%I |}.
Next Obligation. iIntros (tid vl) "%". by subst. Qed.
- Next Obligation. by iIntros (???????) "_ _". Qed.
+ Next Obligation. by iIntros (????????) "_ _ $". Qed.
Next Obligation. by iIntros (???????) "_ _ $". Qed.
Global Instance unit_copy : Copy unit.
@@ -49,11 +49,11 @@ Section product.
iDestruct "H1" as %->. iDestruct "H2" as %->. done.
Qed.
Next Obligation.
- intros ty1 ty2 E N κ l tid ??. iIntros "#LFT /=H". rewrite split_prod_mt.
+ intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok". rewrite split_prod_mt.
iMod (bor_sep with "LFT H") as "[H1 H2]". set_solver.
- iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1") as "?". solve_ndisj. done.
- iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2") as "?". solve_ndisj. done.
- iModIntro. iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
+ iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
+ iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? Htok]". solve_ndisj. done.
+ iModIntro. iFrame "Htok". iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
Qed.
Next Obligation.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 57aafd1c6e7e3c8c4ca4047617c2cc2308124aca..27872076ef9b0018501b78eca54cc59a3030d7e4 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -39,22 +39,28 @@ Section typing.
Context `{typeG Σ}.
Lemma tctx_incl_share E L p κ ty :
- tctx_incl E L [TCtx_holds p (&uniq{κ}ty)] [TCtx_holds p (&shr{κ}ty)].
+ lctx_lft_alive E L κ → tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)] [TCtx_hasty p (&shr{κ}ty)].
Proof.
- iIntros (?) "#LFT _ _ Huniq". rewrite /tctx_interp !big_sepL_singleton /=.
- iDestruct "Huniq" as (v) "[% Huniq]". iExists _. iFrame "%".
+ iIntros (Hκ ???) "#LFT HE HL Huniq".
+ iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
+ rewrite /tctx_interp !big_sepL_singleton /=.
+ iDestruct "Huniq" as (v) "[% Huniq]".
iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
- iMod (ty.(ty_share) _ lrustN with "LFT H↦") as "Hown"; [solve_ndisj|done|].
+ iMod (ty.(ty_share) _ lrustN with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|done|].
+ iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
iIntros "!>/=". eauto.
Qed.
Lemma tctx_reborrow_shr E L p ty κ κ' :
lctx_lft_incl E L κ' κ →
- tctx_incl E L [TCtx_holds p (&shr{κ}ty)]
- [TCtx_holds p (&shr{κ'}ty); TCtx_guarded p κ (&shr{κ}ty)].
+ tctx_incl E L [TCtx_hasty p (&shr{κ}ty)]
+ [TCtx_hasty p (&shr{κ'}ty); TCtx_guarded p κ (&shr{κ}ty)].
Proof.
- iIntros (Hκκ' tid) "#LFT #HE #HL H". iDestruct (Hκκ' with "HE HL") as "Hκκ'".
+ iIntros (Hκκ' tid ??) "#LFT HE HL H".
+ iDestruct (elctx_interp_persist with "HE") as "#HE'".
+ iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
+ iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
iDestruct "H" as (v) "[% #H]". iDestruct "H" as (l) "[EQ Hshr]".
iDestruct "EQ" as %[=->]. simpl. iModIntro. iSplit.
@@ -88,19 +94,18 @@ Section typing.
(!ν)
(λ v, v ◠&shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
- iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
+ iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & [Htok1 Htok2]) & $)". wp_bind ν.
iApply (has_type_wp with "Hâ—"). iIntros (v) "Hνv Hâ—!>". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "Hâ—" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
- iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
+ iMod (lft_incl_acc with "H⊑ Htok1") as (q'') "[Htok1 Hclose]". done.
iDestruct "H↦" as (vl) "[H↦b #Hown]".
- iMod (frac_bor_acc with "LFT H↦b Htok") as (q''') "[>H↦ Hclose']". done.
- iApply (wp_fupd_step _ (⊤∖↑lrustN∖↑lftN) with "[Hown]"); try done.
- - iApply ("Hown" with "* [%]"). set_solver.
- - wp_read. iIntros "!>[Hshr|#H†]{$H⊑}".
- + iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
- iFrame. iApply "Hclose'". auto.
- + iMod ("Hclose'" with "[H↦]"). by auto.
- by iDestruct (lft_tok_dead with "[-] H†") as "[]".
+ iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+ iMod (lft_incl_acc with "H⊑ Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
+ iApply (wp_fupd_step _ (⊤∖↑lrustN∖↑lftN) with "[Hown Htok2]"); try done.
+ - iApply ("Hown" with "* [%] Htok2"). set_solver.
+ - wp_read. iIntros "!>[Hshr Htok2]{$H⊑}". iMod ("Hclose''" with "Htok2") as "$".
+ iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
+ iFrame. iApply "Hclose'". auto.
Qed.
Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
@@ -108,21 +113,21 @@ Section typing.
(!ν)
(λ v, v ◠&shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
Proof.
- iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
+ iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & [Htok1 Htok2] & #H⊑2) & $)". wp_bind ν.
iApply (has_type_wp with "Hâ—"). iIntros (v) "Hνv Hâ—!>". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "Hâ—" as (l) "[Heq Hshr]".
iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
- iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[Htok Hclose]". done.
- iMod (frac_bor_acc with "LFT H↦ Htok") as (q'') "[>H↦ Hclose']". done.
+ iMod (lft_incl_acc with "H⊑1 Htok1") as (q') "[Htok1 Hclose]". done.
+ iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
{ iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
- iApply (wp_fupd_step _ (_∖_) with "[Hown]"); try done.
- - iApply ("Hown" with "* [%]"). set_solver.
- - wp_read. iIntros "!>[#Hshr|#H†]{$H⊑1}".
- + iSplitR.
- * iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
- * iApply ("Hclose" with ">"). iApply ("Hclose'" with "[$H↦]").
- + iMod ("Hclose'" with "[H↦]"). by auto.
- by iDestruct (lft_tok_dead with "[-] H†") as "[]".
+ iMod (lft_incl_acc with "[] Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
+ { iApply (lft_incl_trans with "[]"); done. }
+ iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
+ - iApply ("Hown" with "* [%] Htok2"). set_solver.
+ - wp_read. iIntros "!>[#Hshr Htok2]{$H⊑1}".
+ iMod ("Hclose''" with "Htok2") as "$". iSplitR.
+ * iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+ * iApply ("Hclose" with ">"). iApply ("Hclose'" with "[$H↦]").
Qed.
End typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 00b11cb09862852b5c1e1e6632b98973eb5d730d..138f15ee16e902a68587636bbc0fdc0149309fcb 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,4 +1,5 @@
From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import fractional.
From lrust.lifetime Require Import borrow frac_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import type_incl.
@@ -8,20 +9,42 @@ Section sum.
Local Obligation Tactic := idtac.
- Program Definition emp : type := {| st_own tid vl := False%I |}.
+ Program Definition emp : type :=
+ {| ty_size := 1%nat;
+ ty_own tid vl := False%I;
+ ty_shr κ tid N l := False%I |}.
Next Obligation. iIntros (tid vl) "[]". Qed.
+ Next Obligation.
+ iIntros (E N κ l tid ???) "#LFT Hown Htok".
+ iMod (bor_acc with "LFT Hown Htok") as "[>H _]"; first done.
+ iDestruct "H" as (?) "[_ []]".
+ Qed.
+ Next Obligation.
+ iIntros (κ κ' tid E E' l ?) "#LFT #Hord []".
+ Qed.
+
Global Instance emp_empty : Empty type := emp.
+ Global Instance emp_copy : Copy ∅.
+ Proof.
+ split; first by apply _.
+ iIntros (???????) "? []".
+ Qed.
+
Definition list_max (l : list nat) := foldr max 0%nat l.
+ Definition is_pad i tyl (vl : list val) : iProp Σ :=
+ ⌜((nth i tyl ∅).(ty_size) + length vl)%nat =
+ (list_max $ map ty_size $ tyl)âŒ%I.
+
Lemma split_sum_mt l tid q tyl :
(l ↦∗{q}: λ vl,
∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌠∗
⌜length vl = S (list_max $ map ty_size $ tyl)⌠∗
ty_own (nth i tyl ∅) tid vl')%I
- ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: (nth i tyl ∅).(ty_own) tid ∗
- shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: λ vl,
- ⌜((nth i tyl ∅).(ty_size) + length vl)%nat = (list_max $ map ty_size $ tyl)âŒ.
+ ⊣⊢ ∃ (i : nat), (l ↦{q} #i ∗
+ shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
+ shift_loc l 1 ↦∗{q}: (nth i tyl ∅).(ty_own) tid.
Proof.
iSplit; iIntros "H".
- iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
@@ -29,11 +52,11 @@ Section sum.
(* TODO: I should not have to say '[#]' here, similar to iDestruct ... as %.... *)
iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)âŒ%I) with "[#]" as %Hvl'.
{ iApply ty_size_eq. done. }
- iDestruct (heap_mapsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitR "Htail".
- + iExists vl'. by iFrame.
+ iDestruct (heap_mapsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
+ iExists vl''. rewrite (shift_loc_assoc_nat _ 1) Hvl'. iFrame. iPureIntro.
rewrite -Hvl'. simpl in *. rewrite -app_length. congruence.
- - iDestruct "H" as (i) "(Hmt1 & Hown & Htail)".
+ + iExists vl'. by iFrame.
+ - iDestruct "H" as (i) "[[Hmt1 Htail] Hown]".
iDestruct "Hown" as (vl') "[Hmt2 Hown]". iDestruct "Htail" as (vl'') "[Hmt3 %]".
(* TODO: I should not have to say '[#]' here, similar to iDestruct ... as %.... *)
iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)âŒ%I) with "[#]" as %Hvl'.
@@ -50,39 +73,36 @@ Section sum.
⌜length vl = S (list_max $ map ty_size $ tyl)⌠∗
(nth i tyl ∅).(ty_own) tid vl')%I;
ty_shr κ tid N l :=
- (∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
- (nth i tyl ∅).(ty_shr) κ tid N (shift_loc l 1) ∗
- (&frac{κ} λ q, shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: λ vl,
- ⌜((nth i tyl ∅).(ty_size) + length vl)%nat = (list_max $ map ty_size $ tyl)âŒ))%I
+ (∃ (i : nat),
+ (&frac{κ} λ q, l ↦{q} #i ∗
+ shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
+ (nth i tyl ∅).(ty_shr) κ tid N (shift_loc l 1))%I
|}.
Next Obligation.
iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (i vl' vl'') "(%&%&_)".
subst. done.
Qed.
Next Obligation.
- intros tyl E N κ l tid ??. iIntros "#LFT Hown". rewrite split_sum_mt.
+ intros tyl E N κ l tid. iIntros (???) "#LFT Hown Htok". rewrite split_sum_mt.
iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". solve_ndisj.
- iMod (bor_sep with "LFT Hown") as "[Hown Htail]". solve_ndisj.
- iMod ((nth i tyl ∅).(ty_share) with "LFT Hown") as "#Hshr"; try done.
- iMod (bor_fracture with "LFT [Htail]") as "H";[set_solver| |]; last first.
- - iMod (bor_fracture with "LFT [Hmt]") as "H'";[set_solver| |]; last eauto.
+ (* FIXME: Why can't I directly frame Htok in the destruct after the following mod? *)
+ iMod ((nth i tyl ∅).(ty_share) with "LFT Hown Htok") as "[#Hshr Htok]"; try done.
+ iFrame "Htok". iMod (bor_fracture with "LFT [Hmt]") as "H'";[set_solver| |]; last eauto.
by iFrame.
- - by iFrame.
Qed.
Next Obligation.
- intros tyl κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
- iDestruct "H" as (i) "[Hown0 [Hown Htail]]". iExists i.
- iSplitL "Hown0"; last iSplitL "Hown".
+ iIntros (tyl κ κ' tid E E' l ?) "#LFT #Hord H".
+ iDestruct "H" as (i) "[Hown0 Hown]". iExists i.
+ iSplitL "Hown0".
- by iApply (frac_bor_shorten with "Hord").
- iApply ((nth i tyl ∅).(ty_shr_mono) with "LFT Hord"); last done. done.
- - by iApply (frac_bor_shorten with "Hord").
Qed.
- Global Instance sum_mono E L:
+ Global Instance sum_mono E L :
Proper (Forall2 (subtype E L) ==> subtype E L) sum.
Proof.
- intros tyl1 tyl2 Htyl. iIntros "#LFT #? %".
+ iIntros (tyl1 tyl2 Htyl) "#LFT #? %".
iAssert (⌜list_max (map ty_size tyl1) = list_max (map ty_size tyl2)âŒ%I) with "[#]" as %Hleq.
{ iInduction Htyl as [|???? Hsub] "IH"; first done.
iDestruct (Hsub with "LFT [] []") as "(% & _ & _)"; [done..|].
@@ -100,20 +120,36 @@ Section sum.
iExists i, vl', vl''. iSplit; first done.
iSplit; first by rewrite -Hleq.
iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
- - iIntros (κ tid F l) "H". iDestruct "H" as (i) "(Hmt & Hshr & Htail)".
- iExists i. iFrame "Hmt". iSplitL "Hshr".
- + iDestruct ("Hty" $! i) as "(_ & _ & #Htyi)". by iApply "Htyi".
- + rewrite -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
+ - iIntros (κ tid F l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
+ iExists i. iSplitR "Hshr".
+ + rewrite /is_pad -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
iDestruct "Hlen" as %<-. done.
+ + iDestruct ("Hty" $! i) as "(_ & _ & #Htyi)". by iApply "Htyi".
Qed.
- Global Instance sum_proper E L:
+ Global Instance sum_proper E L :
Proper (Forall2 (eqtype E L) ==> eqtype E L) sum.
Proof.
intros tyl1 tyl2 Heq; split; eapply sum_mono; [|rewrite -Forall2_flip];
(eapply Forall2_impl; [done|by intros ?? []]).
Qed.
+ Lemma nth_empty {A : Type} i (d : A) :
+ nth i [] d = d.
+ Proof. by destruct i. Qed.
+
+ Lemma emp_sum E L :
+ eqtype E L emp (sum []).
+ Proof.
+ split; (iIntros; iSplit; first done; iSplit; iAlways).
+ - iIntros (??) "[]".
+ - iIntros (κ tid F l) "[]".
+ - iIntros (??) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+ rewrite nth_empty. by iDestruct "Hown" as "[]".
+ - iIntros (????) "H". iDestruct "H" as (i) "(_ & Hshr)".
+ rewrite nth_empty. by iDestruct "Hshr" as "[]".
+ Qed.
+
Global Instance sum_copy tyl: LstCopy tyl → Copy (sum tyl).
Proof.
intros HFA. split.
@@ -122,28 +158,24 @@ Section sum.
intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
[by eapply List.Forall_forall| apply _].
- intros κ tid E F l q ?.
- iIntros "#LFT #H[[Htok1 [Htok2 Htok3]] Htl]".
- setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 [Hshr Hshrtail]]".
+ iIntros "#LFT #H[[Htok1 Htok2] Htl]".
+ setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
- iMod (frac_bor_acc with "LFT Hshrtail Htok2") as (q'2) "[Htail Hclose']". set_solver.
- iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok3 $Htl]")
- as (q'3) "[Hownq Hclose'']"; try done.
+ iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok2 $Htl]")
+ as (q'2) "[HownC Hclose']"; try done.
{ edestruct nth_in_or_default as [| ->]; last by apply _.
by eapply List.Forall_forall. }
- destruct (Qp_lower_bound q'1 q'2) as (q'0 & q'01 & q'02 & -> & ->).
- destruct (Qp_lower_bound q'0 q'3) as (q' & q'11 & q'12 & -> & ->).
- rewrite -(heap_mapsto_vec_prop_op _ q' q'12); last (by intros; apply ty_size_eq).
- rewrite -!Qp_plus_assoc.
- rewrite -(heap_mapsto_vec_prop_op _ q' (q'11 + q'02)
- (list_max (map ty_size tyl) - (ty_size (nth i tyl ∅)))%nat); last first.
- { intros. iIntros (<-). iPureIntro. by rewrite minus_plus. }
- iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 >Hown2]".
- iDestruct "Htail" as "[Htail1 Htail2]".
- iExists q'. iModIntro. iSplitL "Hown1 Hownq1 Htail1".
- + iNext. iExists i. by iFrame.
- + iIntros "H". iDestruct "H" as (i') "[>Hown1 [Hownq1 Htail1]]".
- iDestruct (heap_mapsto_agree with "[$Hown1 $Hown2]") as %[= ->%Z_of_nat_inj].
- iMod ("Hclose''" with "[$Hownq1 $Hownq2]"). iMod ("Hclose'" with "[$Htail1 $Htail2]").
+ destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
+ rewrite -(heap_mapsto_vec_prop_op _ q' q'02); last (by intros; apply ty_size_eq).
+ rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
+ iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 >Hown2]".
+ iExists q'. iModIntro. iSplitL "Hown1 HownC1".
+ + iNext. iExists i. iFrame.
+ + iIntros "H". iDestruct "H" as (i') "[>Hown1 HownC1]".
+ iDestruct (heap_mapsto_agree with "[Hown1 Hown2]") as "#Heq".
+ { iDestruct "Hown1" as "[$ _]". iDestruct "Hown2" as "[$ _]". }
+ iDestruct "Heq" as %[= ->%Z_of_nat_inj].
+ iMod ("Hclose'" with "[$HownC1 $HownC2]").
iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
Qed.
End sum.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 4e6f5c37d5d0233cf3119ffe0f7f832e61477da2..ddb31f4f1cbd49e425ed1e3374bf9a5f06ee8309 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -35,20 +35,21 @@ Section type.
invariants, which does not need the mask. Moreover, it is
more consistent with thread-local tokens, which we do not
give any. *)
- ty_share E N κ l tid : mgmtE ⊥ ↑N → mgmtE ⊆ E →
- lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) ={E}=∗ ty_shr κ tid (↑N) l;
+ ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
+ lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗
+ ty_shr κ tid (↑N) l ∗ q.[κ];
ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l
}.
Global Existing Instances ty_shr_persistent.
- Class Copy (ty : type) := {
- copy_persistent tid vl : PersistentP (ty.(ty_own) tid vl);
+ Class Copy (t : type) := {
+ copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
copy_shr_acc κ tid E F l q :
mgmtE ∪ F ⊆ E →
- lft_ctx -∗ ty.(ty_shr) κ tid F l -∗
- q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty.(ty_own) tid ∗
- (▷l ↦∗{q'}: ty.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)
+ lft_ctx -∗ t.(ty_shr) κ tid F l -∗
+ q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: t.(ty_own) tid ∗
+ (▷l ↦∗{q'}: t.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)
}.
Global Existing Instances copy_persistent.
@@ -76,42 +77,38 @@ Section type.
[subtype_shr_mono]. *)
ty_shr := λ κ tid _ l,
(∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
- (▷ st.(st_own) tid vl ∨ □|={↑lftN}=>[†κ]))%I
+ â–· st.(st_own) tid vl)%I
|}.
Next Obligation. intros. apply st_size_eq. Qed.
Next Obligation.
- intros st E N κ l tid ? ?. iIntros "#LFT Hmt".
+ intros st E N κ l tid ? ? ?. iIntros "#LFT Hmt Hκ".
iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]". set_solver.
- - iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
+ - iFrame "Hκ". iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
{ iExists vl. iFrame. auto. }
done. set_solver.
- - iExists []. iSplitL; last by auto. iApply (frac_bor_fake with "LFT"); auto.
+ - iExFalso. iApply (lft_tok_dead with "Hκ"). done.
Qed.
Next Obligation.
intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
iDestruct "H" as (vl) "[#Hf #Hown]".
- iExists vl. iSplit. by iApply (frac_bor_shorten with "Hord").
- iDestruct "Hown" as "[Hown|#H†]". auto. iRight. iIntros "!#".
- by iApply (lft_incl_dead with "Hord >").
+ iExists vl. iFrame "Hown". by iApply (frac_bor_shorten with "Hord").
Qed.
Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
Next Obligation.
intros st κ tid E F l q ?. iIntros "#LFT #Hshr[Hlft $]".
- iDestruct "Hshr" as (vl) "[Hf [Hown|#H†]]".
- - iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
- iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
- + iNext. iExists _. by iFrame.
- + iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
- iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
- { iNext. iDestruct (st_size_eq with "Hown") as %->.
- iDestruct (st_size_eq with "Hown'") as %->. done. }
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
- iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
- - iApply fupd_mask_mono; last iMod "H†". set_solver.
- iDestruct (lft_tok_dead with "Hlft H†") as "[]".
+ iDestruct "Hshr" as (vl) "[Hf Hown]".
+ iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+ iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
+ - iNext. iExists _. by iFrame.
+ - iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
+ iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
+ { iNext. iDestruct (st_size_eq with "Hown") as %->.
+ iDestruct (st_size_eq with "Hown'") as %->. done. }
+ iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+ iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
Qed.
End type.
@@ -180,7 +177,7 @@ Section subtyping.
intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
- iIntros. iApply (Hst with "* [] [] []"); done.
- iIntros (????) "H".
- iDestruct "H" as (vl) "[Hf [Hown|H†]]"; iExists vl; iFrame "Hf"; last by auto.
- iLeft. by iApply (Hst with "* [] [] []").
+ iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
+ by iApply (Hst with "* [] [] []").
Qed.
End subtyping.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 54c2a32b94ec5686fdca7c0181018272f1d92fef..7223a7f6842e276ae12eb71c4541b40265816203 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -20,13 +20,13 @@ Section type_context.
end.
Inductive tctx_elt : Type :=
- | TCtx_holds (p : path) (ty : type)
+ | TCtx_hasty (p : path) (ty : type)
| TCtx_guarded (p : path) (κ : lft) (ty : type).
Definition tctx := list tctx_elt.
Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
match x with
- | TCtx_holds p ty => ∃ v, ⌜eval_path p = Some v⌠∗ ty.(ty_own) tid [v]
+ | TCtx_hasty p ty => ∃ v, ⌜eval_path p = Some v⌠∗ ty.(ty_own) tid [v]
| TCtx_guarded p κ ty => ∃ v, ⌜eval_path p = Some v⌠∗
([†κ] ={⊤}=∗ ▷ ty.(ty_own) tid [v])
end%I.
@@ -38,41 +38,45 @@ Section type_context.
Proof. intros ???. by apply big_opL_permutation. Qed.
Definition tctx_incl (E : elctx) (L : llctx) (T1 T2 : tctx): Prop :=
- ∀ tid, lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
- tctx_interp tid T1 ={⊤}=∗ tctx_interp tid T2.
+ ∀ tid q1 q2, lft_ctx -∗ elctx_interp E q1 -∗ llctx_interp L q2 -∗
+ tctx_interp tid T1 ={⊤}=∗ elctx_interp E q1 ∗ llctx_interp L q2 ∗
+ tctx_interp tid T2.
Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
Proof.
split.
- - by iIntros (??) "_ _ _ $".
- - iIntros (??? H1 H2 ?) "#LFT #HE #HL H".
- iApply (H2 with "LFT HE HL >"). by iApply (H1 with "LFT HE HL").
+ - by iIntros (????) "_ $ $ $".
+ - iIntros (??? H1 H2 ???) "#LFT HE HL H".
+ iMod (H1 with "LFT HE HL H") as "(HE & HL & H)".
+ by iMod (H2 with "LFT HE HL H") as "($ & $ & $)".
Qed.
Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
Proof.
- rewrite /tctx_incl. iIntros (Hc ?) "_ _ _ H". by iApply big_sepL_contains.
+ rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_contains.
Qed.
Lemma tctx_incl_frame E L T T1 T2 :
tctx_incl E L T2 T1 → tctx_incl E L (T++T2) (T++T1).
Proof.
- intros Hincl ?. rewrite /tctx_interp !big_sepL_app. iIntros "#LFT #HE #HL [$ ?]".
+ intros Hincl ???. rewrite /tctx_interp !big_sepL_app. iIntros "#LFT HE HL [$ ?]".
by iApply (Hincl with "LFT HE HL").
Qed.
Lemma copy_tctx_incl E L p `(!Copy ty) :
- tctx_incl E L [TCtx_holds p ty] [TCtx_holds p ty; TCtx_holds p ty].
+ tctx_incl E L [TCtx_hasty p ty] [TCtx_hasty p ty; TCtx_hasty p ty].
Proof.
- iIntros (?) "_ _ _ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
+ iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
by iIntros "[#$ $]".
Qed.
Lemma subtype_tctx_incl E L p ty1 ty2 :
- subtype E L ty1 ty2 → tctx_incl E L [TCtx_holds p ty1] [TCtx_holds p ty2].
+ subtype E L ty1 ty2 → tctx_incl E L [TCtx_hasty p ty1] [TCtx_hasty p ty2].
Proof.
- iIntros (Hst ?) "#LFT #HE #HL H". rewrite /tctx_interp !big_sepL_singleton /=.
- iDestruct "H" as (v) "[% H]". iExists _. iFrame "%".
+ iIntros (Hst ???) "#LFT HE HL H". rewrite /tctx_interp !big_sepL_singleton /=.
+ iDestruct (elctx_interp_persist with "HE") as "#HE'".
+ iDestruct (llctx_interp_persist with "HL") as "#HL'".
+ iFrame "HE HL". iDestruct "H" as (v) "[% H]". iExists _. iFrame "%".
iDestruct (Hst with "* [] [] []") as "(_ & #Ho & _)"; [done..|].
iApply ("Ho" with "*"). done.
Qed.
@@ -80,7 +84,7 @@ Section type_context.
Definition deguard_tctx_elt κ x :=
match x with
| TCtx_guarded p κ' ty =>
- if decide (κ = κ') then TCtx_holds p ty else x
+ if decide (κ = κ') then TCtx_hasty p ty else x
| _ => x
end.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 1eeb4fe64fda6320ad7f8c807f6a6b6bc36ad488..7c092bd0a292ba734fb54e87008a615f9004b11b 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -26,11 +26,9 @@ Section typing.
Proof.
intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
iIntros (tid qE) "#LFT HE HL HC HT".
- iMod (HT with "LFT [#] [#] HT") as "HT".
- by iApply elctx_interp_persist. by iApply llctx_interp_persist.
+ iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
iApply ("H" with "LFT HE HL [HC] HT").
- iIntros "HE". iApply (HC with "LFT [#]").
- by iApply elctx_interp_persist. by iApply "HC".
+ iIntros "HE". by iApply (HC with "LFT HC").
Qed.
(* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 3743290b7cb85ee08ce9f06f52009bf9b57fe7a2..1600c4b016d9d8408a1ba65b58b28210eda4d9b3 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -16,36 +16,35 @@ Section uniq_bor.
(∃ (l:loc) P, (⌜vl = [ #l ]⌠∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
ty_shr κ' tid E l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
- â–¡ ∀ F, ⌜E ∪ mgmtE ⊆ FâŒ
- ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∨ [†κ'])%I
+ □ ∀ F q, ⌜E ∪ mgmtE ⊆ F⌠-∗ q.[κ∪κ']
+ ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q.[κ∪κ'])%I
|}.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l P) "[[% _] _]". by subst.
Qed.
Next Obligation.
- move=> κ ty E N κ' l tid ??/=. iIntros "#LFT Hshr".
+ move=> κ ty E N κ' l tid ???/=. iIntros "#LFT Hshr Htok".
iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
- iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver. iExists l'.
+ iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
iMod (bor_exists with "LFT Hb2") as (P) "Hb2". set_solver.
iMod (bor_sep with "LFT Hb2") as "[H Hb2]". set_solver.
- iMod (bor_persistent with "LFT H") as "[[>% #HPiff]|#H†]". set_solver.
- - subst. rewrite heap_mapsto_vec_singleton.
- iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
- rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
- iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
- with "[Hpbown]") as "#Hinv"; first by eauto.
- iIntros "!>!#*%". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
- iDestruct "INV" as "[>Hbtok|#Hshr]".
- + iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb".
- { set_solver. } { iApply bor_unfold_idx. eauto. }
- iModIntro. iNext. iMod "Hb".
- iMod (bor_iff with "LFT [] Hb") as "Hb". set_solver. by eauto.
- iMod (ty.(ty_share) with "LFT Hb") as "#Hshr". done. set_solver.
- iMod ("Hclose" with "[]") as "_"; auto.
- + iMod ("Hclose" with "[]") as "_". by eauto.
- iApply step_fupd_intro. set_solver. auto.
- - iSplitL. by iApply (frac_bor_fake with "LFT"). iIntros "!>!#*_".
+ iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HPiff] Htok]". set_solver.
+ iFrame "Htok". iExists l'.
+ subst. rewrite heap_mapsto_vec_singleton.
+ iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
+ rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
+ iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
+ with "[Hpbown]") as "#Hinv"; first by eauto.
+ iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+ iDestruct "INV" as "[>Hbtok|#Hshr]".
+ - iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb".
+ { set_solver. } { iApply bor_unfold_idx. eauto. }
+ iModIntro. iNext. iMod "Hb".
+ iMod (bor_iff with "LFT [] Hb") as "Hb". set_solver. by eauto.
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]". done. set_solver.
+ iMod ("Hclose" with "[]") as "_"; auto.
+ - iMod ("Hclose" with "[]") as "_". by eauto.
iApply step_fupd_intro. set_solver. auto.
Qed.
Next Obligation.
@@ -56,16 +55,16 @@ Section uniq_bor.
- iApply (lft_incl_trans with "[] Hκ").
iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
- iIntros "!#*%".
+ iIntros "!# * % Htok".
iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)); try set_solver.
- iMod ("Hvs" with "* [%]") as "Hvs'". set_solver. iModIntro. iNext.
- iMod "Hvs'" as "[#Hshr|H†]".
- - iLeft. by iApply (ty_shr_mono with "LFT Hκ0").
- - iRight. iApply (lft_incl_dead with "Hκ H†"). set_solver.
+ iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first set_solver.
+ iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+ iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+ by iApply (ty_shr_mono with "LFT Hκ0").
Qed.
Global Instance subtype_uniq_mono E L :
- Proper (lctx_lft_incl E L --> eqtype E L ==> subtype E L) uniq_bor.
+ Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 [Hty1 Hty2]. iIntros. iSplit; first done.
iDestruct (Hty1 with "* [] [] []") as "(_ & #Ho1 & #Hs1)"; [done..|clear Hty1].
@@ -84,10 +83,11 @@ Section uniq_bor.
- iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
apply gmultiset_union_subseteq_l.
- iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
- iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!#%%".
- iMod ("Hupd" with "* [%]") as "Hupd'"; try done. iModIntro. iNext.
- iMod "Hupd'" as "[H|H†]"; last by auto.
- iLeft. iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs1".
+ iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
+ iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
+ iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
+ iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+ iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs1".
Qed.
Global Instance subtype_uniq_mono' E L :
Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
@@ -104,10 +104,10 @@ Section typing.
Context `{typeG Σ}.
Lemma tctx_borrow E L p n ty κ :
- tctx_incl E L [TCtx_holds p (own n ty)]
- [TCtx_holds p (&uniq{κ}ty); TCtx_guarded p κ (own n ty)].
+ tctx_incl E L [TCtx_hasty p (own n ty)]
+ [TCtx_hasty p (&uniq{κ}ty); TCtx_guarded p κ (own n ty)].
Proof.
- iIntros (tid) "#LFT _ _ H".
+ iIntros (tid ??) "#LFT $ $ H".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l) "(EQ & Hmt & ?)".
iDestruct "EQ" as %[=->]. iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
@@ -119,10 +119,13 @@ Section typing.
Lemma tctx_reborrow_uniq E L p ty κ κ' :
lctx_lft_incl E L κ' κ →
- tctx_incl E L [TCtx_holds p (&uniq{κ}ty)]
- [TCtx_holds p (&uniq{κ'}ty); TCtx_guarded p κ (&uniq{κ}ty)].
+ tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
+ [TCtx_hasty p (&uniq{κ'}ty); TCtx_guarded p κ (&uniq{κ}ty)].
Proof.
- iIntros (Hκκ' tid) "#LFT #HE #HL H". iDestruct (Hκκ' with "HE HL") as "Hκκ'".
+ iIntros (Hκκ' tid ??) "#LFT HE HL H".
+ iDestruct (elctx_interp_persist with "HE") as "#HE'".
+ iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
+ iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.