Commit acddfae5 authored by Ralf Jung's avatar Ralf Jung

Change the sharing view shift to frame a token

This also needs changes in type and continuation context inclusion.
It allows us to prove that the empty sum is equal to the empty type.
I also took the opportunity to rename TCtx_holds to TCtx_hasty, which at least says what is "holding".
parent 3fedc856
......@@ -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.
......@@ -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 //
......
......@@ -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.
......@@ -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,FE∖↑lftN}= ty.(ty_shr) κ tid E l' [κ]))%I
( F q, E mgmtE F - q.[κ] ={F,FE∖↑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 _ _ (FE∖↑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 :
......
......@@ -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.
......
......@@ -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.
This diff is collapsed.
......@@ -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.
......@@ -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.
......
......@@ -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] ? *)
......
......@@ -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, FE∖↑lftN}= ty.(ty_shr) (κ∪κ') tid E l' [κ'])%I
F q, E mgmtE F - q.[κ∪κ']
={F, FE∖↑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