give even zero-sized types some thread-local storage

theories/typing/mem.v

@@ -103,16 +103,14 @@ Section typing.
     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 %[=->].
     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']".
+    iMod (copy_shr_acc with "LFT Hshr Htok Htl") as (q'') "(H↦ & Htl & Hclose')".
     { assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
-    { rewrite ->shr_locsE_shrN. solve_ndisj. }
+    { done. }
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
     iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
-    iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
+    iMod ("Hclose'" with "[H↦] Htl") as "[Htok $]". iExists _; by iFrame.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 

theories/typing/product.v

@@ -13,9 +13,11 @@ Section product.
 
   Global Instance unit_copy : Copy unit.
   Proof.
-    split. by apply _.
-    iIntros (????????) "_ _ $". iExists 1%Qp. iSplitL; last by auto.
-    iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto.
+    split. by apply _. iIntros (????????) "_ _ $ Htok".
+    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
+    iExists 1%Qp. iModIntro. iSplitR.
+    { iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
+    iIntros "_ Htok2". iApply "Htok". done.
   Qed.
 
   Global Instance unit_send : Send unit.
@@ -87,17 +89,16 @@ Section product.
     Copy (product2 ty1 ty2).
   Proof.
     split; first (intros; apply _).
-    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. }
-    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.
+    intros κ tid E F l q ? HF. iIntros "#LFT [H1 H2] [Htok1 Htok2] Htl".
+    iMod (@copy_shr_acc with "LFT H1 Htok1 Htl") as (q1) "(H1 & Htl & Hclose1)"; first set_solver.
+    { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. omega. }
+    iMod (@copy_shr_acc with "LFT H2 Htok2 Htl") as (q2) "(H2 & Htl & Hclose2)"; first set_solver.
+    { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
+      assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (shift_loc l (ty_size ty1)) (ty_size ty2 + 1))
+             by exact: shr_locsE_disj.
+      set_solver. }
+    iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
+    { generalize (shr_locsE_shift l ty1.(ty_size) ty2.(ty_size)). simpl. 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.
@@ -108,7 +109,7 @@ Section product.
     iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
     iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
     - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
-    - iIntros "[H1 H2]".
+    - iIntros "[H1 H2] Htl". iDestruct ("Htlclose" with "Htl") as "Htl".
       iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
       iAssert (▷ ⌜length vl1' = ty1.(ty_size)⌝)%I with "[#]" as ">%".
       { iNext. by iApply ty_size_eq. }
@@ -117,8 +118,8 @@ Section product.
       iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
       rewrite !heap_mapsto_vec_op; try by congruence.
       iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
-      iMod ("Hclose1" with "[H1 H↦1]") as "[$$]". by iExists _; iFrame.
-      iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
+      iMod ("Hclose2" with "[H2 H↦2] Htl") as "[$ Htl]". by iExists _; iFrame.
+      iMod ("Hclose1" with "[H1 H↦1] Htl") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
   Global Instance product2_send `{!Send ty1} `{!Send ty2} :

theories/typing/sum.v

@@ -163,29 +163,36 @@ Section sum.
       intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
                                         [by eapply List.Forall_forall| apply _].
     - intros κ tid E F l q ? HF.
-      iIntros "#LFT #H[[Htok1 Htok2] Htl]".
+      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.
       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.
+      iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr Htok2 Htl")
+        as (q'2) "(HownC & Htl & 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. }
+      iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
+      { (* Really, we don't even have a lemma for anti-monotonicity of difference...? *)
+        cut (shr_locsE (shift_loc l 1) (ty_size (nth i tyl ∅)) ⊆
+                  shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
+        - simpl. set_solver+.
+        - apply shr_locsE_subseteq. omega. }
       destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
       rewrite -(heap_mapsto_pred_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]".
+      + iIntros "H Htl". iDestruct "H" as (i') "[>Hown1 HownC1]".
+        iDestruct ("Htlclose" with "Htl") as "Htl".
         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 "[$HownC1 $HownC2] Htl") as "[? $]".
         iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.
 

theories/typing/type.v

@@ -92,14 +92,52 @@ Section type.
     rewrite shr_locsE_shift. set_solver+.
   Qed.
 
+  Lemma shr_locsE_split_tok l n m tid :
+    na_own tid (shr_locsE l (n + m)) ⊣⊢ na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
+  Proof.
+    rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
+  Qed.
+
+  Lemma na_own_acc F2 F1 tid :
+    F2 ⊆ F1 →
+    na_own tid F1 -∗ na_own tid F2 ∗
+           (na_own tid F2 -∗ na_own tid F1).
+  Proof.
+    intros HF. assert (F1 = F2 ∪ (F1 ∖ F2)) as -> by exact: union_difference_L.
+    rewrite na_own_union; last by set_solver+.
+    iIntros "[$ $]". auto.
+  Qed.
+
+(*  Lemma shr_locsE_get_tok l n F tid :
+    shr_locsE l n ⊆ F →
+    na_own tid F -∗ na_own tid (shr_locsE l n) ∗ 
+         (na_own tid (shr_locsE l n) -∗ na_own tid F).
+  Proof.
+    intros HF.
+    assert (F = shr_locsE l n ∪ (F ∖ shr_locsE l n)) as -> by exact: union_difference_L.
+    rewrite na_own_union; last by set_solver+.
+    iIntros "[$ $]". by iIntros "?".
+  Qed.
+
+  Lemma shr_locsE_get_tokS l n F tid :
+    shr_locsE l (n + 1) ⊆ F →
+    na_own tid F -∗ na_own tid (shr_locsE l n) ∗ 
+         (na_own tid (shr_locsE l n) -∗ na_own tid F).
+  Proof.
+    intros HF. apply shr_locsE_get_tok. rewrite <-HF.
+    apply shr_locsE_subseteq. omega.
+  Qed.
+*)
   (** Copy types *)
   Class Copy (t : type) := {
     copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
     copy_shr_acc κ tid E F l q :
-      lftE ∪ ↑shrN ⊆ E → shr_locsE l t.(ty_size) ⊆ F →
+      lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ 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)
+        q.[κ] -∗ na_own tid F ={E}=∗ ∃ q', ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
+                                     na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
+         (▷l ↦∗{q'}: t.(ty_own) tid -∗ na_own tid (F ∖ shr_locsE l t.(ty_size))
+                                                    ={E}=∗ q.[κ] ∗ na_own tid F)
   }.
   Global Existing Instances copy_persistent.
 
@@ -166,12 +204,14 @@ Section type.
 
   Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
   Next Obligation.
-    intros st κ tid E ? l q ??. iIntros "#LFT #Hshr[Hlft $]".
+    intros st κ tid E ? l q ? HF. iIntros "#LFT #Hshr Hlft Htok".
+    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
     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']".
+    - iIntros "Hmt1 Htok2". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
+      iDestruct ("Htok" with "Htok2") as "$".
       iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
       { iNext. iDestruct (st_size_eq with "Hown") as %->.
         iDestruct (st_size_eq with "Hown'") as %->. done. }