change sharing protocol to fixed mask based on location

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").

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 :

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 κ ν :

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").

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.

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.

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.