diff --git a/theories/typing/own.v b/theories/typing/own.v
index a6e703fa3f32178dbcc6f80929dbe83009febfaf..150a35ad349322b960c6bf5526233a12dc4317cc 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -50,15 +50,15 @@ Section own.
problems. *)
(∃ l:loc, ⌜vl = [ #l ]⌠∗ ▷ l ↦∗: ty.(ty_own) tid ∗
â–· freeable_sz n ty.(ty_size) l)%I;
- ty_shr κ tid E l :=
+ ty_shr κ tid l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
- □ (∀ F q, ⌜E ∪ lftE ⊆ F⌠-∗ q.[κ] ={F,F∖E∖↑lftN}▷=∗ ty.(ty_shr) κ tid E l' ∗ q.[κ]))%I
+ □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] ={F,F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) κ tid 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 Htok".
+ move=>n ty 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.
@@ -69,23 +69,26 @@ Section own.
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
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ tid l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+ (* FIXME We shouldn't have to add this manually to make the set_solver below work (instead, solve_ndisj below should do it). Also, this goal itself should be handled by solve_ndisj. *)
+ assert (↑shrN ⊥ ↑lftN). { eapply ndot_preserve_disjoint_l. solve_ndisj. }
iDestruct "INV" as "[>Hbtok|#Hshr]".
- - iMod (bor_later with "LFT [Hbtok]") as "Hb". set_solver.
+ - 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.
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ Htok]". 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".
+ intros _ ty κ κ' tid l. iIntros "#LFT #Hκ #H".
iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
- iApply (step_fupd_mask_mono F _ _ (F∖E∖↑lftN)). set_solver. set_solver.
+ iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)). set_solver. 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 "$".
@@ -104,7 +107,7 @@ Section own.
iDestruct ("Ho" with "* Hown") as "Hown".
iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
iExists _. by iFrame.
- - iIntros (????) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
+ - iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
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").
diff --git a/theories/typing/product.v b/theories/typing/product.v
index df8e3942d1f1bfd4ad622383e0754b48271de222..8864a0b36c835702851537bd903c799245978e0c 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -7,15 +7,15 @@ Section product.
Context `{typeG Σ}.
Program Definition unit : type :=
- {| ty_size := 0; ty_own tid vl := ⌜vl = []âŒ%I; ty_shr κ tid E l := True%I |}.
+ {| ty_size := 0; ty_own tid vl := ⌜vl = []âŒ%I; ty_shr κ tid 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.
+ Next Obligation. by iIntros (????) "_ _ $". Qed.
Global Instance unit_copy : Copy unit.
Proof.
split. by apply _.
- iIntros (???????) "_ _ $". iExists 1%Qp. iSplitL; last by auto.
+ iIntros (????????) "_ _ $". iExists 1%Qp. iSplitL; last by auto.
iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto.
Qed.
@@ -39,27 +39,23 @@ Section product.
{| ty_size := ty1.(ty_size) + ty2.(ty_size);
ty_own tid vl := (∃ vl1 vl2,
⌜vl = vl1 ++ vl2⌠∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
- ty_shr κ tid E l :=
- (∃ E1 E2, ⌜E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E⌠∗
- ty1.(ty_shr) κ tid E1 l ∗
- ty2.(ty_shr) κ tid E2 (shift_loc l ty1.(ty_size)))%I |}.
+ ty_shr κ tid l :=
+ (ty1.(ty_shr) κ tid l ∗
+ ty2.(ty_shr) κ tid (shift_loc l ty1.(ty_size)))%I |}.
Next Obligation.
iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
subst. rewrite app_length !ty_size_eq.
iDestruct "H1" as %->. iDestruct "H2" as %->. done.
Qed.
Next Obligation.
- intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok". rewrite split_prod_mt.
+ intros ty1 ty2 E κ 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 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.
+ iMod (ty1.(ty_share) with "LFT H1 Htok") as "[? Htok]". solve_ndisj.
+ iMod (ty2.(ty_share) with "LFT H2 Htok") as "[? Htok]". solve_ndisj.
+ iModIntro. iFrame "Htok". iFrame.
Qed.
Next Obligation.
- intros ty1 ty2 κ κ' tid E E' l ?. iIntros "#LFT /= #H⊑ H".
- iDestruct "H" as (N1 N2) "(% & H1 & H2)". iExists N1, N2.
- iSplit. iPureIntro. set_solver.
+ intros ty1 ty2 κ κ' tid l. iIntros "#LFT /= #H⊑ [H1 H2]".
iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
Qed.
@@ -74,8 +70,7 @@ Section product.
iExists _, _. iSplit. done. iSplitL "Hown1".
+ by iApply "Ho1".
+ by iApply "Ho2".
- - iIntros (????) "H". iDestruct "H" as (vl1 vl2) "(% & #Hshr1 & #Hshr2)".
- iExists _, _. iSplit; first done. iSplit.
+ - iIntros (???) "#[Hshr1 Hshr2]". iSplit.
+ by iApply "Hs1".
+ rewrite -(_ : ty_size ty11 = ty_size ty12) //. by iApply "Hs2".
Qed.
@@ -87,15 +82,17 @@ Section product.
Copy (product2 ty1 ty2).
Proof.
split; first (intros; apply _).
- intros κ tid E F l q ?. iIntros "#LFT H [[Htok1 Htok2] Htl]".
- iDestruct "H" as (E1 E2) "(% & H1 & H2)".
- assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->.
+ intros κ tid E F l q ? HF. iIntros "#LFT [H1 H2] [[Htok1 Htok2] Htl]".
+ simpl in HF. rewrite ->shr_locsE_shift in HF.
+ assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (shift_loc l (ty_size ty1)) (ty_size ty2)).
+ { apply shr_locsE_disj. }
+ assert (F = shr_locsE l (ty_size ty1) ∪ F∖(shr_locsE l (ty_size ty1))) as ->.
{ rewrite -union_difference_L; set_solver. }
- repeat setoid_rewrite na_own_union; first last.
- set_solver. set_solver. set_solver. set_solver.
- iDestruct "Htl" as "[[Htl1 Htl2] $]".
- iMod (@copy_shr_acc with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver.
- iMod (@copy_shr_acc with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver.
+ setoid_rewrite na_own_union; first last.
+ set_solver. set_solver.
+ iDestruct "Htl" as "[Htl1 Htl2]".
+ iMod (@copy_shr_acc with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver. done.
+ iMod (@copy_shr_acc with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver. set_solver.
destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
rewrite !split_prod_mt.
@@ -140,44 +137,39 @@ Section typing.
Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
Proof.
split; (iIntros; (iSplit; first by rewrite /= assoc); iSplit; iAlways;
- last iIntros (??); iIntros (??) "H").
+ last iIntros (?); iIntros (??) "H").
- iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
- - iDestruct "H" as (E1 E2') "(% & Hs1 & H)".
- iDestruct "H" as (E2 E3) "(% & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
- iExists (E1 ∪ E2), E3. iSplit. by iPureIntro; set_solver. iFrame.
- iExists E1, E2. iSplit. by iPureIntro; set_solver. by iFrame.
+ - iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
+ by iFrame.
- iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
- - iDestruct "H" as (E1' E3) "(% & H & Hs3)".
- iDestruct "H" as (E1 E2) "(% & Hs1 & Hs2)". rewrite /= shift_loc_assoc_nat.
- iExists E1, (E2 ∪ E3). iSplit. by iPureIntro; set_solver. iFrame.
- iExists E2, E3. iSplit. by iPureIntro; set_solver. by iFrame.
+ - iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
+ by iFrame.
Qed.
Global Instance prod2_unit_leftid E L : LeftId (eqtype E L) unit product2.
Proof.
intros ty. split; (iIntros; (iSplit; first done); iSplit; iAlways;
- last iIntros (??); iIntros (??) "H").
+ last iIntros (?); iIntros (??) "H").
- iDestruct "H" as (? ?) "(% & % & ?)". by subst.
- - iDestruct "H" as (? ?) "(% & ? & ?)". rewrite shift_loc_0.
- iApply (ty_shr_mono with "[] []"); [|done| | done].
- set_solver. iApply lft_incl_refl.
+ - iDestruct "H" as "(? & ?)". rewrite shift_loc_0.
+ iApply (ty_shr_mono with "[] []"); [done| | done].
+ iApply lft_incl_refl.
- iExists [], _. eauto.
- - iExists ∅, _. rewrite shift_loc_0. iFrame. by iPureIntro; set_solver.
+ - simpl. rewrite shift_loc_0. by iFrame.
Qed.
Global Instance prod2_unit_rightid E L : RightId (eqtype E L) unit product2.
Proof.
intros ty. split; (iIntros; (iSplit; first by rewrite /= -plus_n_O); iSplit; iAlways;
- last iIntros (??); iIntros (??) "H").
+ last iIntros (?); iIntros (??) "H").
- iDestruct "H" as (? ?) "(% & ? & %)". subst. by rewrite app_nil_r.
- - iDestruct "H" as (? ?) "(% & ? & _)".
- iApply (ty_shr_mono with "[] []"); [|done| |done]. set_solver. iApply lft_incl_refl.
+ - iDestruct "H" as "(? & _)". done.
- iExists _, []. rewrite app_nil_r. eauto.
- - iExists _, ∅. iFrame. by iPureIntro; set_solver.
+ - simpl. iFrame.
Qed.
Lemma eqtype_prod_flatten E L tyl1 tyl2 tyl3 :
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a39ce0e60daec0a036a3b08d2a2daf916f4ca0bd..d527fc91bb72222f841b554d82d5882de50e0f21 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -107,11 +107,9 @@ Section product_split.
rewrite /has_type /sep /product2 /=.
destruct (eval_expr ν) as [[[|l|]|]|];
iIntros (tid) "#LFT H"; try iDestruct "H" as "[]";
- iDestruct "H" as (l0) "(EQ & H)"; iDestruct "EQ" as %[=<-].
- iDestruct "H" as (E1 E2) "(% & H1 & H2)".
+ iDestruct "H" as (l0) "(EQ & [H1 H2])"; iDestruct "EQ" as %[=<-].
iSplitL "H1"; iExists _; (iSplitR; [done|]); iApply (ty_shr_mono with "LFT []");
- try by iFrame.
- set_solver. iApply lft_incl_refl. set_solver. iApply lft_incl_refl.
+ try by iFrame. iApply lft_incl_refl. iApply lft_incl_refl.
Qed.
Lemma perm_split_shr_bor_prod tyl κ ν :
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index d8802008bcdfe212b74306f73e0d7b8e9b552dc4..e951318d423e2f7024d4b4e0a1f5a238ac6ee3ed 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -9,7 +9,7 @@ Section shr_bor.
Program Definition shr_bor (κ : lft) (ty : type) : type :=
{| st_own tid vl :=
- (∃ (l:loc), ⌜vl = [ #l ]⌠∗ ty.(ty_shr) κ tid (↑lrustN) l)%I |}.
+ (∃ (l:loc), ⌜vl = [ #l ]⌠∗ ty.(ty_shr) κ tid l)%I |}.
Next Obligation.
iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
@@ -20,7 +20,7 @@ Section shr_bor.
intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
iDestruct "H" as (l) "(% & H)". subst. iExists _. iSplit. done.
- iApply (ty2.(ty_shr_mono) with "LFT Hκ"). reflexivity.
+ iApply (ty2.(ty_shr_mono) with "LFT Hκ").
iDestruct (Hty with "* [] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
by iApply "Hs1".
Qed.
@@ -47,7 +47,7 @@ Section typing.
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↦ Htok") as "[Hown Htok]"; [solve_ndisj|done|].
+ iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
iIntros "!>/=". eauto.
Qed.
@@ -80,7 +80,10 @@ Section typing.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
rewrite (union_difference_L (↑lrustN) ⊤); last done.
setoid_rewrite ->na_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
- iMod (copy_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
+ (* FIXME We shouldn't have to add this manually to make the set_solver below work (instead, solve_ndisj below should do it). *)
+ assert (↑shrN ⊆ (↑lrustN : coPset)). { solve_ndisj. }
+ iMod (copy_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; first set_solver.
+ { rewrite ->shr_locsE_shrN. solve_ndisj. }
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
@@ -102,7 +105,10 @@ Section typing.
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.
+ - (* FIXME: mask reasoning at its worst. Really we'd want the mask in the line above to be
+ ⊤∖↑shrN∖↑lftN, but then the wp_read fails. *)
+ assert (↑shrN ⊆ (↑lrustN : coPset)). { solve_ndisj. }
+ iApply step_fupd_mask_mono; last iApply ("Hown" with "* [%] Htok2"); [|reflexivity|]. set_solver. 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.
@@ -123,8 +129,11 @@ Section typing.
{ iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
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.
+ iApply (wp_fupd_step _ (⊤∖↑lrustN∖↑lftN) with "[Hown Htok2]"); try done.
+ - (* FIXME: mask reasoning at its worst. Really we'd want the mask in the line above to be
+ ⊤∖↑shrN∖↑lftN, but then the wp_read fails. *)
+ assert (↑shrN ⊆ (↑lrustN : coPset)). { solve_ndisj. }
+ iApply step_fupd_mask_mono; last iApply ("Hown" with "* [%] Htok2"); [|reflexivity|]. set_solver. 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").
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 6b39fd7face0388f3621ef3ad82aacc85aa2989a..b393efb72cde22a1e3c4f60d5d25630dd6e02e19 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -11,15 +11,15 @@ Section sum.
Program Definition emp : type :=
{| ty_size := 1%nat;
ty_own tid vl := False%I;
- ty_shr κ tid N l := False%I |}.
+ ty_shr κ tid l := False%I |}.
Next Obligation. iIntros (tid vl) "[]". Qed.
Next Obligation.
- iIntros (E N κ l tid ???) "#LFT Hown Htok".
+ iIntros (E κ 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 []".
+ iIntros (κ κ' tid l) "#LFT #Hord []".
Qed.
Global Instance emp_empty : Empty type := emp.
@@ -27,7 +27,7 @@ Section sum.
Global Instance emp_copy : Copy ∅.
Proof.
split; first by apply _.
- iIntros (???????) "? []".
+ iIntros (????????) "? []".
Qed.
Definition list_max (l : list nat) := foldr max 0%nat l.
@@ -71,18 +71,18 @@ Section sum.
(∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌠∗
⌜length vl = S (list_max $ map ty_size $ tyl)⌠∗
(nth i tyl ∅).(ty_own) tid vl')%I;
- ty_shr κ tid N l :=
+ ty_shr κ tid l :=
(∃ (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
+ (nth i tyl ∅).(ty_shr) κ tid (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 Htok". rewrite split_sum_mt.
+ intros tyl E κ 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.
(* FIXME: Why can't I directly frame Htok in the destruct after the following mod? *)
@@ -91,11 +91,11 @@ Section sum.
by iFrame.
Qed.
Next Obligation.
- iIntros (tyl κ κ' tid E E' l ?) "#LFT #Hord H".
+ iIntros (tyl κ κ' tid 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.
+ - iApply ((nth i tyl ∅).(ty_shr_mono) with "LFT Hord"); done.
Qed.
Global Instance sum_mono E L :
@@ -119,7 +119,7 @@ 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)".
+ - iIntros (κ tid 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.
@@ -142,10 +142,10 @@ Section sum.
Proof.
split; (iIntros; iSplit; first done; iSplit; iAlways).
- iIntros (??) "[]".
- - iIntros (κ tid F l) "[]".
+ - iIntros (κ tid l) "[]".
- iIntros (??) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
rewrite nth_empty. by iDestruct "Hown" as "[]".
- - iIntros (????) "H". iDestruct "H" as (i) "(_ & Hshr)".
+ - iIntros (???) "H". iDestruct "H" as (i) "(_ & Hshr)".
rewrite nth_empty. by iDestruct "Hshr" as "[]".
Qed.
@@ -156,18 +156,23 @@ Section sum.
cut (∀ i vl', PersistentP (ty_own (nth i tyl ∅) tid vl')). by apply _.
intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
[by eapply List.Forall_forall| apply _].
- - intros κ tid E F l q ?.
+ - intros κ tid E F l q ? HF.
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 (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok2 $Htl]")
+ iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[>Hown Hclose]". set_solver.
+ iAssert ((∃ vl, is_pad i tyl vl)%I) with "[#]" as %[vl Hpad].
+ { iDestruct "Hown" as "[_ Hpad]". iDestruct "Hpad" as (vl) "[_ %]".
+ eauto. }
+ 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. }
+ { rewrite <-HF. simpl. rewrite <-union_subseteq_r.
+ apply shr_locsE_subseteq. omega. }
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]".
+ 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]".
@@ -183,37 +188,3 @@ End sum.
as Î for products. We stick to the following form. *)
Notation "Σ[ ty1 ; .. ; tyn ]" :=
(sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.
-
-Section incl.
- Context `{typeG Σ}.
-
- (* TODO *)
- (* Lemma ty_incl_sum Ï n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) : *)
- (* Duplicable Ï â†’ Forall2 (ty_incl Ï) tyl1 tyl2 → *)
- (* ty_incl Ï (sum tyl1) (sum tyl2). *)
- (* Proof. *)
- (* iIntros (DUP FA tid) "#LFT #HÏ". rewrite /sum /=. iSplitR "". *)
- (* - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗ *)
- (* (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl *)
- (* → (nth i tyl2 ∅%T).(ty_own) tid vl)). *)
- (* { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH]. *)
- (* - iIntros "_ _!>*!#". eauto. *)
- (* - iIntros "#LFT #HÏ". iMod (IH with "LFT HÏ") as "#IH". *)
- (* iMod (Hincl with "LFT HÏ") as "[#Hh _]". *)
- (* iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". } *)
- (* iMod (Hincl with "LFT HÏ") as "#Hincl". iIntros "!>!#*H". *)
- (* iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done. *)
- (* by iApply "Hincl". *)
- (* - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗ *)
- (* (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l *)
- (* → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)). *)
- (* { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH]. *)
- (* - iIntros "#LFT _!>*!#". eauto. *)
- (* - iIntros "#LFT #HÏ". *)
- (* iMod (IH with "LFT HÏ") as "#IH". iMod (Hincl with "LFT HÏ") as "[_ #Hh]". *)
- (* iIntros "!>*!#*Hown". destruct i as [|i]; last by iApply "IH". *)
- (* by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". } *)
- (* iMod (Hincl with "LFT HÏ") as "#Hincl". iIntros "!>!#*H". iSplit; last done. *)
- (* iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl". *)
- (* Qed. *)
-End incl.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1efb7c858063f37a5089d344689eafe39a31206b..c5fdfa53da2441702bf4f20200f5e24b788dbd6b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -12,6 +12,7 @@ Class typeG Σ := TypeG {
Definition lftE := ↑lftN.
Definition lrustN := nroot .@ "lrust".
+Definition shrN := lrustN .@ "shr".
Section type.
Context `{typeG Σ}.
@@ -21,9 +22,9 @@ Section type.
Record type :=
{ ty_size : nat;
ty_own : thread_id → list val → iProp Σ;
- ty_shr : lft → thread_id → coPset → loc → iProp Σ;
+ ty_shr : lft → thread_id → loc → iProp Σ;
- ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
+ ty_shr_persistent κ tid l : PersistentP (ty_shr κ tid l);
ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_sizeâŒ;
(* The mask for starting the sharing does /not/ include the
@@ -39,19 +40,63 @@ Section type.
nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
we can have emp == sum [].
*)
- ty_share E N κ l tid q : lftE ⊥ ↑N → lftE ⊆ E →
+ ty_share E κ l tid q : lftE ⊆ 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
+ ty_shr κ tid l ∗ q.[κ];
+ ty_shr_mono κ κ' tid l :
+ lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid l -∗ ty_shr κ' tid l
}.
Global Existing Instances ty_shr_persistent.
+ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
+ match n with
+ | 0%nat => ∅
+ | S n => ↑shrN.@l ∪ shr_locsE (shift_loc l 1%nat) n
+ end.
+
+ Lemma shr_locsE_shift l n m :
+ shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (shift_loc l n) m.
+ Proof.
+ revert l; induction n; intros l.
+ - rewrite shift_loc_0. set_solver+.
+ - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
+ set_solver+.
+ Qed.
+
+ Lemma shr_locsE_disj l n m :
+ shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
+ Proof.
+ revert l; induction n; intros l.
+ - simpl. set_solver+.
+ - rewrite -Nat.add_1_l Nat2Z.inj_add /=.
+ apply disjoint_union_l. split; last (rewrite -shift_loc_assoc; exact: IHn).
+ clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
+ rewrite shift_loc_assoc. apply disjoint_union_r. split.
+ + apply ndot_ne_disjoint. destruct l. intros [=]. omega.
+ + rewrite -Z.add_assoc. move:(IHm (n + 1)%nat). rewrite Nat2Z.inj_add //.
+ Qed.
+
+ Lemma shr_locsE_shrN l n :
+ shr_locsE l n ⊆ ↑shrN.
+ Proof.
+ revert l; induction n; intros l.
+ - simpl. set_solver+.
+ - simpl. apply union_least; last by auto. solve_ndisj.
+ Qed.
+
+ Lemma shr_locsE_subseteq l n m :
+ (n ≤ m)%nat → shr_locsE l n ⊆ shr_locsE l m.
+ Proof.
+ induction 1; first done.
+ rewrite ->IHle. rewrite -Nat.add_1_l [(_ + _)%nat]comm. (* FIXME last rewrite is very slow. *)
+ rewrite shr_locsE_shift. set_solver+.
+ Qed.
+
Class Copy (t : type) := {
copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
copy_shr_acc κ tid E F l q :
- lftE ∪ F ⊆ E →
- lft_ctx -∗ t.(ty_shr) κ tid F l -∗
+ lftE ∪ ↑shrN ⊆ E → shr_locsE l t.(ty_size) ⊆ F →
+ lft_ctx -∗ t.(ty_shr) κ tid 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)
}.
@@ -79,13 +124,13 @@ Section type.
(* [st.(st_own) tid vl] needs to be outside of the fractured
borrow, otherwise I do not know how to prove the shr part of
[subtype_shr_mono]. *)
- ty_shr := λ κ tid _ l,
+ ty_shr := λ κ tid l,
(∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
â–· 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 Hκ".
+ iIntros (st E κ l tid ??) "#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.
@@ -95,14 +140,14 @@ Section type.
- iExFalso. iApply (lft_tok_dead with "Hκ"). done.
Qed.
Next Obligation.
- intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
+ intros st κ κ' tid l. iIntros "#LFT #Hord H".
iDestruct "H" as (vl) "[#Hf #Hown]".
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 $]".
+ intros st κ tid E ? l q ??. iIntros "#LFT #Hshr[Hlft $]".
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".
@@ -126,7 +171,7 @@ Section subtyping.
Definition type_incl (ty1 ty2 : type) : iProp Σ :=
(⌜ty1.(ty_size) = ty2.(ty_size)⌠∗
(□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
- (□ ∀ κ tid F l, ty1.(ty_shr) κ tid F l -∗ ty2.(ty_shr) κ tid F l))%I.
+ (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
(* Typeclasses Opaque type_incl. *)
@@ -180,7 +225,7 @@ Section subtyping.
Proof.
intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
- iIntros. iApply (Hst with "* [] [] []"); done.
- - iIntros (????) "H".
+ - iIntros (???) "H".
iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
by iApply (Hst with "* [] [] []").
Qed.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 02c451c05266d26cbd3293dd80861608425b4f1c..50518824925cd62901264a4653aabebdc1fac162 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -14,16 +14,16 @@ Section uniq_bor.
(wrt. subtyping) works without an update. *)
ty_own tid vl :=
(∃ (l:loc) P, (⌜vl = [ #l ]⌠∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
- ty_shr κ' tid E l :=
+ ty_shr κ' tid l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
- □ ∀ F q, ⌜E ∪ lftE ⊆ F⌠-∗ q.[κ∪κ']
- ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q.[κ∪κ'])%I
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ∪κ']
+ ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid 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 Htok".
+ move=> κ ty 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.
@@ -34,21 +34,23 @@ Section uniq_bor.
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
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+ (* FIXME We shouldn't have to add this manually to make the set_solver below work (instead, solve_ndisj below should do it). Also, this goal itself should be handled by solve_ndisj. *)
+ assert (↑shrN ⊥ ↑lftN). { eapply ndot_preserve_disjoint_l. solve_ndisj. }
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 (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]". set_solver.
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
iApply step_fupd_intro. set_solver. auto.
Qed.
Next Obligation.
- intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
+ intros κ0 ty κ κ' tid l. iIntros "#LFT #Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
{ iApply (lft_incl_glb with "[] []").
- iApply lft_le_incl. apply gmultiset_union_subseteq_l.
@@ -56,7 +58,7 @@ Section uniq_bor.
iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
iIntros "!# * % Htok".
- iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)); try set_solver.
+ iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try 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 "$".
@@ -78,7 +80,7 @@ Section uniq_bor.
by iApply "Ho1".
+ iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
by iApply "Ho2".
- - iIntros (κ ???) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
+ - iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "[] []").
- iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
apply gmultiset_union_subseteq_l.