diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 2e275346b04efca7ca73ddaa2a379b01d9957c29..e1607db0bf7f7248872aea468a20354222b9cc64 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -6,9 +6,9 @@ From iris.bi Require Import fractional.
Set Default Proof Using "Type".
Definition lftN : namespace := nroot .@ "lft".
-(** A mask inside the lifetime logic namespace that users may use.
-This is still available in the "consequence" view shift of borrow accessors. *)
-Definition lft_userN : namespace := nroot .@ "lft" .@ "usr".
+(** A (disjoint) mask that is available in the "consequence" view shift of
+ borrow accessors. *)
+Definition lft_userN : namespace := nroot .@ "lft_usr".
Module Type lifetime_sig.
(** CMRAs needed by the lifetime logic *)
@@ -96,7 +96,7 @@ Module Type lifetime_sig.
Parameter lft_dead_static : [†static] -∗ False.
Parameter lft_create : ∀ E, ↑lftN ⊆ E →
- lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN}[↑lft_userN]▷=∗ [†κ]).
+ lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
Parameter bor_create : ∀ E κ P,
↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
Parameter bor_fake : ∀ E κ P,
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 82e47fa94c9ebe1b6798afcaecc3de08899c1c2b..980fa111f56e520ad03cae59a6872ce387231d47 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -80,7 +80,7 @@ Proof.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
- iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hf & HP')".
- solve_ndisj.
+ { solve_ndisj. }
iDestruct ("HPP'" with "HP'") as "$".
iMod ("Hclose'" with "[-Hf Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 92016023e6c12daf252f02f4cbd85aca69b2595f..b9b2fbeea4b68676ffa3b89893425eaa87ee33e2 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -16,7 +16,7 @@ Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
([∗ set] κ' ∈ K', lft_inv_alive κ'))%I in
(∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K) →
(∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K') →
- Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑lft_userN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
+ Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑lft_userN ∪ ↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
Proof.
iIntros (Iinv HK HK') "(HI & Hdead & Halive) Hlalive Hκ".
rewrite lft_inv_alive_unfold;
@@ -34,15 +34,15 @@ Proof.
iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
as %[?%nat_included _]%auth_both_valid; lia. }
iMod (box_empty with "Hbox") as "[HP Hbox]"=>//.
- { (* FIXME [solve_ndisj] fails *)
- etrans; last exact: union_subseteq_l. solve_ndisj. }
+ { (* FIXME [solve_ndisj] fails *) set_solver-. }
{ intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
as "[Halive Halive']".
{ intros κ'. rewrite elem_of_dom. eauto. }
- iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
+ iApply fupd_trans. iApply fupd_mask_mono; last
iMod ("Hvs" $! I with "[HI Halive] HP Hκ") as "(Hinv & HQ & Hcnt')".
+ { set_solver-. }
{ rewrite lft_vs_inv_unfold. iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(HI&Halive)".
iSpecialize ("Halive'" with "Halive").
@@ -63,7 +63,7 @@ Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lf
(∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
(∀ κ, lft_alive_in A κ → is_Some (I !! κ) → κ ∉ K → κ ∈ K') →
Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
- ={↑lft_userN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
+ ={↑lft_userN ∪ ↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
Proof.
intros Iinv. revert K'.
induction (set_wf K) as [K _ IH]=> K' HKK' HK HK'.
@@ -110,7 +110,7 @@ Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
Lemma lft_create E :
↑lftN ⊆ E →
- lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN}[↑lft_userN]▷=∗ [†κ]).
+ lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
Proof.
iIntros (?) "#LFT".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -128,8 +128,14 @@ Proof.
iModIntro; iExists {[ Λ ]}.
rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
clear I A HΛ. iIntros "!# HΛ".
- iApply (step_fupd_mask_mono (↑lftN) _ (↑lftN∖↑mgmtN)); [solve_ndisj..|].
+ iApply (step_fupd_mask_mono (↑lftN ∪ ↑lft_userN) _ ((↑lftN ∪ ↑lft_userN)∖↑mgmtN)).
+ { (* FIXME solve_ndisj should really handle this... *)
+ assert (↑lft_userN ## ↑mgmtN) by solve_ndisj.
+ set_solver. }
+ { done. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+ { (* FIXME solve_ndisj should really handle this... *)
+ assert (↑mgmtN ⊆ ↑lftN) by solve_ndisj. set_solver. }
rewrite /lft_tok big_sepMS_singleton.
iDestruct (own_valid_2 with "HA HΛ")
as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid.
@@ -150,8 +156,16 @@ Proof.
iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])%I with "[HinvK]" as "HinvK".
{ iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
- iApply fupd_trans. iApply (fupd_mask_mono (↑lft_userN ∪ ↑inhN));
- first by apply union_least; solve_ndisj.
+ iApply fupd_trans.
+ iApply (fupd_mask_mono (↑lft_userN ∪ ↑borN ∪ ↑inhN)).
+ { (* FIXME can we make solve_ndisj handle this? *)
+ clear. rewrite -assoc. apply union_least.
+ - assert (↑lft_userN ##@{coPset} ↑mgmtN) by solve_ndisj. set_solver.
+ - assert (↑inhN ##@{coPset} ↑mgmtN) by solve_ndisj.
+ assert (↑inhN ⊆@{coPset} ↑lftN) by solve_ndisj.
+ assert (↑borN ##@{coPset} ↑mgmtN) by solve_ndisj.
+ assert (↑borN ⊆@{coPset} ↑lftN) by solve_ndisj.
+ set_solver. }
iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
{ done. }
{ intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 0bf99ce9cdf9fefbcf0b6444e89b0de125080d00..ecc32eb893dfd72acc5fede1dce34ef0ff1d345b 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -6,9 +6,7 @@ Import uPred.
Definition inhN : namespace := lftN .@ "inh".
Definition mgmtN : namespace := lftN .@ "mgmt".
-(** We put borrows into the "user" namespace, so that they are available
-in [lft_vs]. *)
-Definition borN : namespace := lft_userN .@ "bor".
+Definition borN : namespace := lftN .@ "bor".
Definition atomic_lft := positive.
(* HACK : We need to make sure this is not in the top-level context,
@@ -142,7 +140,7 @@ Section defs.
own_cnt κ (◠n) ∗
∀ I : gmap lft lft_names,
lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ
- ={↑lft_userN}=∗
+ ={↑lft_userN ∪ ↑borN}=∗
lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
Definition lft_inv_alive_go (κ : lft)
@@ -270,7 +268,7 @@ Lemma lft_vs_unfold κ Pb Pi :
lft_vs κ Pb Pi ⊣⊢ ∃ n : nat,
own_cnt κ (◠n) ∗
∀ I : gmap lft lft_names,
- lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑lft_userN}=∗
+ lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑lft_userN ∪ ↑borN}=∗
lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
Proof. done. Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 4429a175ad68d9aaea6245504daf7bf4a974d685..8d7d0ddf09c458831b824bde251154e73a67c8eb 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -490,7 +490,7 @@ Proof.
Qed.
Lemma lft_vs_cons κ Pb Pb' Pi :
- (▷ Pb'-∗ [†κ] ={↑lft_userN}=∗ ▷ Pb) -∗
+ (▷ Pb'-∗ [†κ] ={↑lft_userN ∪ ↑borN}=∗ ▷ Pb) -∗
lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi.
Proof.
iIntros "Hcons Hvs". rewrite !lft_vs_unfold.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 0802fcea5309a270a07af756f0cce04af88c8d97..b3e9f4fd31debf00c5d20bfe1a32a44eca3bc12d 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -81,7 +81,8 @@ Proof.
(exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iMod (slice_fill _ _ false with "Hislice HP Hbox")
- as "Hbox"; first by solve_ndisj.
+ as "Hbox".
+ { set_solver-. }
{ by rewrite lookup_fmap HB. }
iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
rewrite /=. iDestruct "Hcnt" as "[% H1â—¯]".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 0f7e78ac8fb8727a44991826f35c0609ecfd2067..a070f0643697100d3ab2ffd4685e4e2484355445 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -285,8 +285,8 @@ Section typing.
iDestruct "HÏ" as (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
iSpecialize ("Hinh" with "Htk"). iClear "Hκs".
- iApply (wp_mask_mono _ (↑lftN)); first done.
- iApply (wp_step_fupd with "Hinh"); [solve_ndisj..|]. wp_seq.
+ iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
+ iApply (wp_step_fupd with "Hinh"); [set_solver-..|]. wp_seq.
iIntros "#Htok !>". wp_seq. iMod ("HκsI" with "Htok") as ">Hκs".
iApply ("Hk" with "Htl HL Hκs"). rewrite tctx_hasty_val. done.
+ rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 3017ca810ad7c2bc01b5759354ecee60465f0af7..f8b22f40d0e386deecd0204466408d4ef4bd157d 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -41,7 +41,7 @@ Section lft_contexts.
(* Local lifetime contexts. *)
Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
let κ' := lft_intersect_list (x.2) in
- (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN}[↑lft_userN]▷=∗ [†κ0]))%I.
+ (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ0]))%I.
Global Instance llctx_elt_interp_fractional x :
Fractional (llctx_elt_interp x).
Proof.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 09a3d7630025083cf8d37eef0a8970630a85bcee..627bd6a48fb6a2696286975647bd81e0b3b81048 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -27,7 +27,7 @@ Section arc.
(* because [weak_new] cannot prove ty_shr, even for a dead *)
(* lifetime. *)
(ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
- □ (1.[ν] ={↑lftN ∪ ↑arc_endN}[↑lft_userN]▷=∗
+ □ (1.[ν] ={↑lftN ∪ ↑lft_userN ∪ ↑arc_endN}[↑lft_userN]▷=∗
[†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ †l…(2 + ty.(ty_size))))%I.
Global Instance arc_persist_ne tid ν γ l n :
@@ -88,10 +88,14 @@ Section arc.
iMod (inv_acc with "INV") as "[[H†|[$ Hvs]] Hclose]";
[set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|].
rewrite difference_union_distr_l_L difference_diag_L right_id_L
- difference_disjoint_L; last solve_ndisj.
+ difference_disjoint_L; last first.
+ { apply disjoint_union_l. split; solve_ndisj. }
iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
- iMod "H" as "#Hν". iMod ("Hvs" with "Hν") as "$". iIntros "{$Hν} !>".
- iApply "Hclose". auto.
+ iMod "H" as "#Hν".
+ iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
+ { set_solver-. }
+ iIntros "{$Hν} !>".
+ iMod "Hclose2" as "_". iApply "Hclose". auto.
Qed.
Program Definition arc (ty : type) :=
@@ -394,7 +398,7 @@ Section arc.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lft_create with "LFT") as (ν) "[Hν Hν†]"; first done.
wp_bind (_ +ₗ _)%E. iSpecialize ("Hν†" with "Hν").
- iApply wp_mask_mono; last iApply (wp_step_fupd with "Hν†"); [solve_ndisj..|].
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hν†"); [set_solver-..|].
wp_op. iIntros "#H†!>". rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_write.
iApply (type_type _ _ _ [ #lrc â— box (weak ty)]
with "[] LFT HE Hna HL Hk [>-]"); last first.
@@ -768,8 +772,7 @@ Section arc.
iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
- { (* FIXME [solve_ndisj] fails *)
- etrans; last exact: union_subseteq_l. solve_ndisj. }
+ { set_solver-. (* FIXME [solve_ndisj] fails *) }
iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
@@ -873,8 +876,7 @@ Section arc.
iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
- { (* FIXME [solve_ndisj] fails *)
- etrans; last exact: union_subseteq_l. solve_ndisj. }
+ { (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
@@ -949,8 +951,7 @@ Section arc.
wp_apply (is_unique_spec with "Hi Htoks"). iIntros ([]) "H"; wp_if.
- iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
- { (* FIXME [solve_ndisj] fails *)
- etrans; last exact: union_subseteq_l. solve_ndisj. }
+ { (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_seq. iIntros "(#Hν & Hown & H†) !>". wp_seq.
iMod ("Hclose2" with "[Hrc Hrc1 H†] Hown") as "[Hb Hα]".
{ iIntros "!> Hown !>". iLeft. iFrame. }
@@ -1036,8 +1037,7 @@ Section arc.
- iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ +â‚— _)%E.
iSpecialize ("Hc" with "HP1").
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
- { (* FIXME [solve_ndisj] fails *)
- etrans; last exact: union_subseteq_l. solve_ndisj. }
+ { (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
{ iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -1053,8 +1053,7 @@ Section arc.
iApply type_jump; solve_typing.
- iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
- { (* FIXME [solve_ndisj] fails *)
- etrans; last exact: union_subseteq_l. solve_ndisj. }
+ { (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_apply wp_new=>//. lia. iIntros (l) "(H†& Hlvl) (#Hν & Hown & H†') !>".
rewrite -!lock Nat2Z.id.
wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 529b04c8703ac2f229f0799b748b200129caf780..36eadb4f851e29a0a9dfd757ae5e1b66437a73da 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -85,7 +85,7 @@ Section rc.
because [weak_new] cannot prove ty_shr, even for a dead
lifetime. *)
(ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
- □ (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν]))%I.
+ □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I.
Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
Proof. unfold rc_persist, tc_opaque. apply _. Qed.
@@ -298,7 +298,10 @@ Section code.
rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
- iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
+ iModIntro. iNext. iMod "H†".
+ iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
+ { set_solver-. }
+ iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
iModIntro. iNext. iDestruct "Hty" as (vl) "[??]". iExists _. iFrame.
by iApply "Hinclo".
@@ -310,7 +313,10 @@ Section code.
rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
- iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
+ iModIntro. iNext. iMod "H†".
+ iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
+ { set_solver-. }
+ iMod "Hclose2" as "_". iModIntro.
iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc, prod_local_update_1,
(cancel_local_update_unit (Some _) None). }
@@ -328,7 +334,10 @@ Section code.
rewrite -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
- iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
+ iModIntro. iNext. iMod "H†".
+ iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
+ { set_solver-. }
+ iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
first by iExists _; iFrame; iFrame.
rewrite Hincls. iFrame. iSplitL "Hty".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index e70716071d9330882256389019a630dd9c843d9b..9680aee6b6b6c30aacccaf050bdc06b28b0d25a9 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -466,7 +466,7 @@ Section code.
wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
iPoseProof ("Hν†" with "Hν") as "H†". wp_bind (_ <- _)%E.
- iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [solve_ndisj..|].
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [set_solver-..|].
wp_write. iIntros "#Hν !>". wp_seq.
iApply (type_type _ _ _ [ #lw â— box (weak ty)]
with "[] LFT HE Hna HL Hk [> -]"); last first.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 5ad3cb6592fcd4aae40537b7c5736762add25e7e..25dc3ea207b4feaea2ec2142c4e23d2abeabf649 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -15,7 +15,7 @@ Section ref_functions.
own γ (◯ reading_stR q ν) -∗
∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌠∗
own γ (◠(refcell_st_to_R $ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν) ∗
- ((1).[ν] ={↑lftN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
+ ((1).[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
(∃ q'', ⌜(q' + q'' = 1)%Qp⌠∗ q''.[ν]) ∗
ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1).
Proof.
@@ -162,7 +162,7 @@ Section ref_functions.
as (q' n) "(H↦lrc & >% & Hâ—â—¯ & H†& Hq' & Hshr)".
iDestruct "Hq'" as (q'') ">[% Hν']".
wp_read. wp_let. wp_op. wp_write.
- iAssert (|={↑lftN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
+ iAssert (|={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
with "[H↦lrc Hâ—â—¯ Hν Hν' Hshr H†]" as "INV".
{ iDestruct (own_valid with "Hâ—â—¯") as
%[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
@@ -180,10 +180,10 @@ Section ref_functions.
{ apply auth_update_dealloc.
rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
apply (cancel_local_update_unit (reading_stR q ν)), _. }
- iApply step_fupd_intro; first solve_ndisj. iExists (q+q'')%Qp. iFrame.
+ iApply step_fupd_intro; first set_solver-. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
- wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
- iApply (wp_step_fupd with "INV"); [solve_ndisj..|]. wp_seq.
+ wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
+ iApply (wp_step_fupd with "INV"); [set_solver-..|]. wp_seq.
iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ #lx â— box (uninit 2)] with "[] LFT HE Hna HL Hk");
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 27a92d38b6124c569d55ca58ae9da5e8476b98bd..d58a9b07a3a0004fcb2ce59199c93d19581293cf 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -49,7 +49,7 @@ Section refcell_inv.
(* Not borrowed. *)
&{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
| Some (ν, rw, q, _) =>
- (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
(∃ q', ⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν]) ∗
if rw then (* Mutably borrowed. *) True
else (* Immutably borrowed. *) ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1)
@@ -151,11 +151,11 @@ Section refcell.
iExists γ, _. iFrame "Hst Hn Hshr".
iSplitR "Htok2"; last by iExists _; iFrame; rewrite Qp_div_2.
iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
- iApply fupd_mask_mono; last iApply "Hh". done. rewrite -lft_dead_or. auto.
+ iApply fupd_mask_mono; last iApply "Hh". set_solver-. rewrite -lft_dead_or. auto.
- iMod (own_alloc (◠(refcell_st_to_R $ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
- { rewrite -step_fupd_intro. auto. solve_ndisj. }
+ { rewrite -step_fupd_intro. auto. set_solver-. }
iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
iApply lft_tok_static.
Qed.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index a480a68a23b10f45f6a5e624f4262bc271f156a7..70979851be15379f04aea93af6ce578cfe7e2852 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -204,7 +204,11 @@ Section refcell_functions.
iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame "∗#".
iSplitR "Htok2".
+ iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
- iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto.
+ iNext. iMod "Hν".
+ iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
+ { set_solver-. }
+ * rewrite -lft_dead_or. auto.
+ * done.
+ iExists _. iFrame. by rewrite Qp_div_2. }
iMod ("Hclose''" with "[$INV] Hna") as "[Hβtok1 Hna]".
iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
@@ -281,7 +285,10 @@ Section refcell_functions.
iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh Htok1] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iNext. iSplitL "Hbh".
- iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
- iApply "Hbh". rewrite -lft_dead_or. auto.
+ iMod fupd_intro_mask' as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
+ { set_solver-. }
+ * rewrite -lft_dead_or. auto.
+ * done.
- iSplitL; [|done]. iExists _. iFrame. by rewrite Qp_div_2. }
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index bffd384c00efe5a667dafce13b6e7d03da45806e..621b03cdf76148c2ce4e6e37d1d331dc636a2210 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -127,7 +127,7 @@ Section refmut_functions.
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct "INV" as (st) "(H↦lrc & H◠& INV)". wp_read. wp_let. wp_op. wp_write.
- iAssert (|={↑lftN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
+ iAssert (|={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
with "[H↦lrc H◠H◯ Hν INV]" as "INV".
{ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as
%[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
@@ -139,7 +139,8 @@ Section refmut_functions.
iMod (own_update_2 with "Hâ— Hâ—¯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
apply cancel_local_update_unit, _. }
- iDestruct "INV" as "(H†& Hq & _)". iApply "H†".
+ iDestruct "INV" as "(H†& Hq & _)".
+ iApply "H†".
iDestruct "Hq" as (q) "(<- & ?)". iFrame.
- simpl in *. setoid_subst. iExists (Some (_, _, _, _)).
iMod (own_update_2 with "Hâ— Hâ—¯") as "$".
@@ -148,11 +149,11 @@ Section refmut_functions.
iDestruct "INV" as "(H†& Hq & _)".
rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
last (rewrite pos_op_plus; lia). iFrame.
- iApply step_fupd_intro; [solve_ndisj|]. iSplitL; [|done].
+ iApply step_fupd_intro; [set_solver-|]. iSplitL; [|done].
iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
rewrite assoc (comm _ q'' q) //. }
- wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
- iApply (wp_step_fupd with "INV"); [solve_ndisj|]. wp_seq. iIntros "{Hb} Hb !>".
+ wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
+ iApply (wp_step_fupd with "INV"); [set_solver-|]. wp_seq. iIntros "{Hb} Hb !>".
iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
iApply (type_type _ _ _ [ #lx â— box (uninit 2)]
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 97fcea2a9730e1662702e7bf22430efbebb15560..c57eea56a2405108100b9391bb33c2da746d9264 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -39,7 +39,7 @@ Section rwlock_inv.
| Some (Cinr (agν, q, n)) =>
(* Locked for read. *)
∃ (ν : lft) q', agν ≡ to_agree ν ∗
- □ (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν]) ∗
+ □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]) ∗
([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν]
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index cbb8f13c2e32c2ded7bc1d43b40cd47b742c3f95..f0b3ac79e6693155ca886397df37fc637b9f0444 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -183,7 +183,7 @@ Section rwlock_functions.
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
- ((1).[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν]))%I
+ ((1).[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I
with "[> Hlx Hownst Hst Hβtok2]"
as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
{ destruct st' as [[|[[agν q] n]|]|]; try done.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 2773fa07e21c1a07ed1cb52fcaebda5ff44609dc..7b468ca82d1144a7543fe8755d6577e5980f1a46 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
q.[ν] ∗ own γ (◯ reading_st q ν) ∗
- (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν])
+ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν])
| _ => False
end;
ty_shr κ tid l :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index b5698df18544bce0a9909b42ad17b23ae1d4793b..f5f3804cf0cdd0f76221d30f78d57c34056bb94c 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -83,7 +83,7 @@ Section rwlockreadguard_functions.
iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
iDestruct "INV" as (st') "(Hlx & >Hâ— & Hst)".
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
- + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN]▷=>
+ + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ ↑lft_userN]▷=>
(lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
with "[H◠H◯ Hx' Hν Hst H†]" as "INV".
{ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
@@ -94,12 +94,17 @@ Section rwlockreadguard_functions.
iDestruct "Hst" as (ν' q') "(>EQν & _ & Hh & _ & >Hq & >Hν')".
rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
- iApply (step_fupd_mask_mono (↑lftN ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN)));
- last iApply (step_fupd_mask_frame_r _ (↑lft_userN)); [set_solver+ || solve_ndisj..| |].
+ iApply (step_fupd_mask_mono ((↑lftN ∪ ↑lft_userN) ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ ↑lft_userN)));
+ last iApply (step_fupd_mask_frame_r _ (↑lft_userN)).
+ { set_solver-. }
+ { solve_ndisj. }
+ { rewrite difference_difference. apply: disjoint_difference_r1. done. }
{ (* FIXME [solve_ndisj] fails. *)
- apply: disjoint_difference_r1. solve_ndisj. }
+ apply: disjoint_difference_r1. done. }
iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
- iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
+ iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
+ { set_solver-. }
+ iMod "Hclose" as "_". iIntros "!> Hlx". iExists None. iFrame.
iApply (own_update_2 with "Hâ— Hâ—¯"). apply auth_update_dealloc.
rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
- iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 371164d38daade419bddba7373323abbe3ba385a..6686b012687e1311dd47db18b0e8d9a6844d9912 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -181,8 +181,8 @@ Section typing_rules.
iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
- iApply (wp_mask_mono _ (↑lftN)); first done.
- iApply (wp_step_fupd with "Hend"); first solve_ndisj. wp_seq.
+ iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
+ iApply (wp_step_fupd with "Hend"); first set_solver-. wp_seq.
iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
Qed.