From 094097c8e92b75b8dd6775cb8fb78299a438729c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 4 Mar 2017 11:11:56 +0100
Subject: [PATCH] Make [lft] an Opaque type, when seen from outside of the
lifetime logic model.
This will make it possible to declare ELCtx_Alive a coercion.
---
theories/lifetime/lifetime.v | 3 ++
theories/lifetime/lifetime_sig.v | 38 ++++++++++-------
theories/lifetime/model/borrow.v | 6 +--
theories/lifetime/model/definitions.v | 14 ++++++-
theories/lifetime/model/primitive.v | 42 +++++++++++--------
theories/lifetime/model/reborrow.v | 12 +++---
theories/typing/borrow.v | 2 +-
theories/typing/lft_contexts.v | 21 +++++-----
theories/typing/lib/refcell/ref.v | 8 ++--
theories/typing/lib/refcell/ref_code.v | 8 ++--
theories/typing/lib/refcell/refcell.v | 13 +++---
theories/typing/lib/refcell/refcell_code.v | 16 +++----
theories/typing/lib/refcell/refmut.v | 20 ++++-----
theories/typing/lib/refcell/refmut_code.v | 8 ++--
theories/typing/lib/rwlock/rwlock.v | 8 ++--
theories/typing/lib/rwlock/rwlock_code.v | 10 ++---
theories/typing/lib/rwlock/rwlockreadguard.v | 12 +++---
theories/typing/lib/rwlock/rwlockwriteguard.v | 16 +++----
.../typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
theories/typing/programs.v | 4 +-
theories/typing/uniq_bor.v | 14 +++----
21 files changed, 155 insertions(+), 122 deletions(-)
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 0efccc16..a2439938 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -5,6 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Module Export lifetime : lifetime_sig.
+ Definition lft := gmultiset positive.
Include definitions.
Include primitive.
Include borrow.
@@ -14,6 +15,8 @@ Module Export lifetime : lifetime_sig.
Include creation.
End lifetime.
+Instance lft_inhabited : Inhabited lft := populate static.
+
Canonical lftC := leibnizC lft.
Section derived.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 54cddeac..5245d4e8 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -9,13 +9,10 @@ Definition borN : namespace := lftN .@ "bor".
Definition inhN : namespace := lftN .@ "inh".
Definition mgmtN : namespace := lftN .@ "mgmt".
-Definition atomic_lft := positive.
-Notation lft := (gmultiset positive).
-Definition static : lft := ∅.
-
Module Type lifetime_sig.
(** CMRAs needed by the lifetime logic *)
- (* We can't instantie the module parameters with inductive types, so we have aliases here. *)
+ (* We can't instantie the module parameters with inductive types, so we
+ have aliases here. *)
Parameter lftG' : gFunctors → Set.
Global Notation lftG := lftG'.
Existing Class lftG'.
@@ -24,6 +21,10 @@ Module Type lifetime_sig.
Existing Class lftPreG'.
(** Definitions *)
+ Parameter lft : Type.
+ Parameter static : lft.
+ Parameter lft_intersect : lft → lft → lft.
+
Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
@@ -47,11 +48,19 @@ Module Type lifetime_sig.
(format "&{ κ , i } P", at level 20, right associativity) : uPred_scope.
Infix "⊑" := lft_incl (at level 70) : uPred_scope.
+ Infix "⊓" := lft_intersect (at level 40) : C_scope.
Section properties.
Context `{invG, lftG Σ}.
(** Instances *)
+ Global Declare Instance lft_intersect_comm : Comm eq lft_intersect.
+ Global Declare Instance lft_intersect_assoc : Assoc eq lft_intersect.
+ Global Declare Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ).
+ Global Declare Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ).
+ Global Declare Instance lft_intersect_left_id : LeftId eq static lft_intersect.
+ Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect.
+
Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
@@ -79,8 +88,8 @@ Module Type lifetime_sig.
AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
(** Laws *)
- Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
- Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ∪ κ2].
+ Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
+ Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ⊓ κ2].
Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [†κ] -∗ False.
Parameter lft_tok_static : ∀ q, q.[static]%I.
Parameter lft_dead_static : [†static] -∗ False.
@@ -103,7 +112,7 @@ Module Type lifetime_sig.
Parameter rebor : ∀ E κ κ' P,
↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Parameter bor_unnest : ∀ E κ κ' P,
- ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+ ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ⊓ κ'} P.
Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
@@ -128,14 +137,15 @@ Module Type lifetime_sig.
(* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
unless we want to prove them twice (both here and in model.primitive) *)
- Parameter lft_glb_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
- ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
- Parameter lft_le_incl : ∀ κ κ', κ' ⊆ κ → (κ ⊑ κ')%I.
+ Parameter lft_intersect_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
+ ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
+ Parameter lft_intersect_incl_l : ∀ κ κ', (κ ⊓ κ' ⊑ κ)%I.
+ Parameter lft_intersect_incl_r : ∀ κ κ', (κ ⊓ κ' ⊑ κ')%I.
Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
- Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
- Parameter lft_glb_mono : ∀ κ1 κ1' κ2 κ2',
- κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+ Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
+ Parameter lft_intersect_mono : ∀ κ1 κ1' κ2 κ2',
+ κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ⊓ κ2 ⊑ κ1' ⊓ κ2'.
Parameter lft_incl_acc : ∀ E κ κ' q,
↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 77e8b588..94d545f5 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -136,9 +136,9 @@ Lemma bor_combine E κ P Q :
Proof.
iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
- iMod (raw_rebor _ _ (κ1 ∪ κ2) with "LFT Hbor1") as "[Hbor1 _]".
+ iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "[Hbor1 _]".
done. by apply gmultiset_union_subseteq_l.
- iMod (raw_rebor _ _ (κ1 ∪ κ2) with "LFT Hbor2") as "[Hbor2 _]".
+ iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "[Hbor2 _]".
done. by apply gmultiset_union_subseteq_r.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
@@ -177,7 +177,7 @@ Proof.
-fmap_None -lookup_fmap !fmap_delete //. }
rewrite own_bor_op. iDestruct "Hbor" as "[Hâ— Hâ—¯]".
iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
- { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2).
+ { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ⊓ κ2).
iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
iExists γ. iFrame. iExists _. iFrame. iNext. iAlways.
by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 9c818279..7ee27388 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -6,6 +6,19 @@ From lrust.lifetime Require Export lifetime_sig.
Set Default Proof Using "Type".
Import uPred.
+Definition atomic_lft := positive.
+(* HACK : We need to make sure this is not in the top-level context,
+ so that it does not conflict with the *definition* of [lft] that we
+ use in lifetime.v. *)
+Module Export lft_notation.
+ Notation lft := (gmultiset atomic_lft).
+End lft_notation.
+
+Definition static : lft := (∅ : gmultiset _).
+Definition lft_intersect (κ κ' : lft) : lft := κ ∪ κ'.
+
+Infix "⊓" := lft_intersect (at level 40) : C_scope.
+
Inductive bor_state :=
| Bor_in
| Bor_open (q : frac)
@@ -67,7 +80,6 @@ Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
-
Section defs.
Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index cc70c535..1d640781 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -218,7 +218,7 @@ Qed.
Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
Proof. exists Λ. by rewrite lookup_insert. Qed.
Lemma lft_dead_in_alive_in_union A κ κ' :
- lft_dead_in A (κ ∪ κ') → lft_alive_in A κ → lft_dead_in A κ'.
+ lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
Proof.
intros (Λ & [Hin|Hin]%elem_of_union & HΛ) Halive.
- contradict HΛ. rewrite (Halive _ Hin). done.
@@ -261,13 +261,20 @@ Proof.
Qed.
(** Basic rules about lifetimes *)
-Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
+Instance lft_intersect_comm : Comm eq lft_intersect := _.
+Instance lft_intersect_assoc : Assoc eq lft_intersect := _.
+Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ) := _.
+Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ) := _.
+Instance lft_intersect_left_id : LeftId eq static lft_intersect := _.
+Instance lft_intersect_right_id : RightId eq static lft_intersect := _.
+
+Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
-Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ∪ κ2].
+Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ⊓ κ2].
Proof.
rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
- rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
+ rewrite -sep_or_r -pure_or. do 2 f_equiv. unfold lft_intersect. set_solver.
Qed.
Lemma lft_tok_dead q κ : q.[κ] -∗ [†κ] -∗ False.
@@ -325,16 +332,19 @@ Lemma lft_incl_intro κ κ' :
(lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
Proof. reflexivity. Qed.
-Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
+Lemma lft_intersect_incl_l κ κ': (κ ⊓ κ' ⊑ κ)%I.
Proof.
- iIntros (->%gmultiset_union_difference) "!#". iSplitR.
+ iIntros "!#". iSplitR.
- iIntros (q). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
rewrite <-lft_tok_sep. by iIntros "!>{$Hf}$".
- iIntros "? !>". iApply lft_dead_or. auto.
Qed.
+Lemma lft_intersect_incl_r κ κ': (κ ⊓ κ' ⊑ κ')%I.
+Proof. rewrite comm. apply lft_intersect_incl_l. Qed.
+
Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
-Proof. by apply lft_le_incl. Qed.
+Proof. iIntros "!#"; iSplitR; auto 10 with iFrame. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Proof.
@@ -347,8 +357,8 @@ Proof.
- iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
Qed.
-Lemma lft_glb_acc κ κ' q q' :
- q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
+Lemma lft_intersect_acc κ κ' q q' :
+ q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
Proof.
iIntros "Hκ Hκ'".
destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
@@ -356,27 +366,25 @@ Proof.
iDestruct "Hκ" as "[$$]". iDestruct "Hκ'" as "[$$]". auto.
Qed.
-Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
Proof.
rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
- iIntros (q) "[Hκ'1 Hκ'2]".
iMod ("H1" with "Hκ'1") as (q') "[Hκ' Hclose']".
iMod ("H2" with "Hκ'2") as (q'') "[Hκ'' Hclose'']".
- iDestruct (lft_glb_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
+ iDestruct (lft_intersect_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
iExists qq. iFrame. iIntros "!> Hqq".
iDestruct ("Hclose" with "Hqq") as "[Hκ' Hκ'']".
iMod ("Hclose'" with "Hκ'") as "$". by iApply "Hclose''".
- rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
Qed.
-Lemma lft_glb_mono κ1 κ1' κ2 κ2' :
- κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+Lemma lft_intersect_mono κ1 κ1' κ2 κ2' :
+ κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ⊓ κ2 ⊑ κ1' ⊓ κ2'.
Proof.
iIntros "#H1 #H2". iApply (lft_incl_glb with "[]").
- - iApply (lft_incl_trans with "[] H1").
- iApply lft_le_incl. apply gmultiset_union_subseteq_l.
- - iApply (lft_incl_trans with "[] H2").
- iApply lft_le_incl. apply gmultiset_union_subseteq_r.
+ - iApply (lft_incl_trans with "[] H1"). iApply lft_intersect_incl_l.
+ - iApply (lft_incl_trans with "[] H2"). iApply lft_intersect_incl_r.
Qed.
(** Basic rules about borrows *)
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 14b4c53d..22c8f503 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -27,10 +27,10 @@ Lemma rebor E κ κ' P :
lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Proof.
iIntros (?) "#LFT #H⊑". rewrite {1}/bor; iDestruct 1 as (κ'') "[#H⊑' Hκ'']".
- iMod (raw_rebor _ _ (κ' ∪ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
+ iMod (raw_rebor _ _ (κ' ⊓ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
{ apply gmultiset_union_subseteq_r. }
iModIntro. iSplitL "Hκ''".
- - rewrite /bor. iExists (κ' ∪ κ''). iFrame "Hκ''".
+ - rewrite /bor. iExists (κ' ⊓ κ''). iFrame "Hκ''".
iApply (lft_incl_glb with "[]"); first iApply lft_incl_refl.
by iApply (lft_incl_trans with "H⊑").
- iIntros "Hκ†". iMod ("Hclose" with "[Hκ†]") as "Hκ''".
@@ -40,7 +40,7 @@ Qed.
Lemma bor_unnest E κ κ' P :
↑lftN ⊆ E →
- lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+ lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ⊓ κ'} P.
Proof.
iIntros (?) "#LFT Hκ". rewrite {2}/bor.
iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
@@ -50,7 +50,7 @@ Proof.
{ iModIntro. iNext. iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
iApply lft_dead_or. iRight. done. }
iMod ("Hclose" with "Hκ⊑") as "_".
- set (κ'' := κ0 ∪ κ0').
+ set (κ'' := κ0 ⊓ κ0').
iMod (raw_rebor _ _ κ'' with "LFT Hκ") as "[Hκ _]"; first done.
{ apply gmultiset_union_subseteq_r. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -68,7 +68,7 @@ Proof.
iNext. iMod "Hclose" as "_".
iApply (bor_fake with "LFT >"); first done.
iApply (lft_incl_dead with "[] H†"); first done.
- by iApply (lft_glb_mono with "Hκ⊑"). }
+ by iApply (lft_intersect_mono with "Hκ⊑"). }
rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #Hislice]".
iDestruct "Hislice" as (P') "[#HPP' Hislice]".
rewrite lft_inv_alive_unfold;
@@ -100,6 +100,6 @@ Proof.
iFrame. rewrite /lft_inv lft_inv_alive_unfold. iLeft.
iFrame "%". iExists Pb'', Pi. iFrame. }
iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
- by iApply (lft_glb_mono with "Hκ⊑").
+ by iApply (lft_intersect_mono with "Hκ⊑").
Qed.
End reborrow.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 90bda252..65b4e4fc 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -144,7 +144,7 @@ Section borrow.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
- iAssert (κ ⊑ κ' ∪ κ)%I as "#Hincl'".
+ iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 0cd42e35..b03a8fe8 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -104,8 +104,8 @@ Section lft_contexts.
(* Local lifetime contexts. *)
Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
- let κ' := foldr (∪) static (x.2) in
- (∃ κ0, ⌜x.1 = κ' ∪ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,∅}▷=∗ [†κ0]))%I.
+ let κ' := foldr lft_intersect static (x.2) in
+ (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,∅}▷=∗ [†κ0]))%I.
Global Instance llctx_elt_interp_fractional x :
Fractional (llctx_elt_interp x).
Proof.
@@ -115,13 +115,13 @@ Section lft_contexts.
- iDestruct "H" as "[Hq Hq']".
iDestruct "Hq" as (κ0) "(% & Hq & #?)".
iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
- rewrite (inj (union (foldr (∪) static κs)) κ0' κ0); last congruence.
+ rewrite (inj (lft_intersect (foldr lft_intersect static κs)) κ0' κ0); last congruence.
iExists κ0. by iFrame "∗%".
Qed.
Typeclasses Opaque llctx_elt_interp.
Definition llctx_elt_interp_0 (x : llctx_elt) : Prop :=
- let κ' := foldr (∪) static (x.2) in (∃ κ0, x.1 = κ' ∪ κ0).
+ let κ' := foldr lft_intersect static (x.2) in (∃ κ0, x.1 = κ' ⊓ κ0).
Lemma llctx_elt_interp_persist x q :
llctx_elt_interp x q -∗ ⌜llctx_elt_interp_0 xâŒ.
Proof.
@@ -164,8 +164,7 @@ Section lft_contexts.
iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
{ rewrite Qp_mult_1_r. done. }
iModIntro. subst κ1. iSplit.
- - iApply lft_le_incl.
- rewrite <-!gmultiset_union_subseteq_l. done.
+ - iApply lft_incl_trans; iApply lft_intersect_incl_l.
- iApply (lft_incl_glb with "[]"); first iApply (lft_incl_glb with "[]").
+ iApply lft_incl_refl.
+ iApply lft_incl_static.
@@ -212,10 +211,10 @@ Section lft_contexts.
Proof.
iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
- iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
+ iApply lft_incl_trans; first iApply lft_intersect_incl_l.
clear -Hκ'κs. induction Hκ'κs.
- - apply gmultiset_union_subseteq_l.
- - etrans. done. apply gmultiset_union_subseteq_r.
+ - iApply lft_intersect_incl_l.
+ - iApply lft_incl_trans; last done. iApply lft_intersect_incl_r.
Qed.
Lemma lctx_lft_incl_local' κ κ' κ'' κs :
@@ -250,8 +249,8 @@ Section lft_contexts.
iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
- iAssert (∃ q', q'.[foldr union static κs] ∗
- (q'.[foldr union static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
+ iAssert (∃ q', q'.[foldr lft_intersect static κs] ∗
+ (q'.[foldr lft_intersect static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
with ">[HE HL1]" as "H".
{ move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 9fe6e746..839c173b 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -24,7 +24,7 @@ Section ref.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc lv); #(LitLoc lrc) ] =>
- ∃ ν q γ β ty', ty.(ty_shr) (α ∪ ν) tid lv ∗
+ ∃ ν q γ β ty', ty.(ty_shr) (α ⊓ ν) tid lv ∗
α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
q.[ν] ∗ own γ (◯ reading_st q ν)
| _ => False
@@ -32,7 +32,7 @@ Section ref.
ty_shr κ tid l :=
∃ ν q γ β ty' (lv lrc : loc),
κ ⊑ ν ∗ &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
- ▷ ty.(ty_shr) (α ∪ ν) tid lv ∗
+ ▷ ty.(ty_shr) (α ⊓ ν) tid lv ∗
▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
&na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
@@ -85,12 +85,12 @@ Section ref.
iDestruct "H" as (ν q γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
iExists ν, q, γ, β, ty'. iFrame "∗#". iSplit.
+ iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
iExists ν, q, γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
+ iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
Qed.
Global Instance ref_mono_flip E L :
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index e2858d93..e90a045f 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_st q ν) -∗
∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌠∗
own γ (◠Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν) ∗
- ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
((1).[ν] ={↑lftN,∅}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid) ∗
∃ q'', ⌜(q' + q'' = 1)%Qp⌠∗ q''.[ν].
Proof.
@@ -240,10 +240,10 @@ Section ref_functions.
iDestruct "HE" as "[HE HE']". iDestruct "Hν" as "[Hν Hν']".
remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
- iApply (type_type ((☀ (α ∪ ν)) :: E)%EL []
- [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&shr{α ∪ ν}ty2)])]%CC
+ iApply (type_type ((☀ (α ⊓ ν)) :: E)%EL []
+ [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&shr{α ⊓ ν}ty2)])]%CC
[ f ◠box (fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
- #lref ◠own_ptr 2 (&shr{α ∪ ν}ty1); env ◠box envty ]%TC
+ #lref ◠own_ptr 2 (&shr{α ⊓ ν}ty1); env ◠box envty ]%TC
with "[] LFT Hna [HE Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index aa8ee23e..9523a646 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -43,7 +43,7 @@ Section refcell_inv.
match st with
| Cinr (q, n) =>
(* Immutably borrowed. *)
- ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
∃ q', ⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν]
| _ => (* Mutably borrowed. *) True
end
@@ -51,8 +51,9 @@ Section refcell_inv.
Global Instance refcell_inv_type_ne n tid l γ α :
Proper (type_dist2 n ==> dist n) (refcell_inv tid l γ α).
- Proof.
- solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+ Proof.
+ solve_proper_core
+ ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
Qed.
Global Instance refcell_inv_ne tid l γ α : NonExpansive (refcell_inv tid l γ α).
@@ -135,9 +136,9 @@ Section refcell.
iMod (own_alloc (◠Some (to_agree ν, Cinr ((1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
- iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
+ iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ { iApply lft_intersect_incl_l. }
+ iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn". iExists _. iIntros "{$Hshr}".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index d807fb20..706404bd 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -178,7 +178,7 @@ Section refcell_functions.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
- ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
+ ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
own γ (◯ reading_st qν ν) ∗ refcell_inv tid lx γ β ty)%I
with ">[Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
{ destruct st as [[agν [|[q n]|]]|]; try done.
@@ -201,10 +201,10 @@ Section refcell_functions.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
- iDestruct (lft_glb_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+ iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ∪ ν) with "LFT [] Hst") as "[Hst Hh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". done.
+ { iApply lft_intersect_incl_l. }
iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame.
iExists _. iSplitR; first done. iFrame "Hshr". iSplitR "Htok2".
@@ -220,7 +220,7 @@ Section refcell_functions.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
- iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono. done. iApply lft_incl_refl. }
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy [unit; ref α ty]); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
@@ -279,8 +279,8 @@ Section refcell_functions.
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ (writing_st ν)). }
iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ∪ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
+ { iApply lft_intersect_incl_l. }
iModIntro. iMod ("Hclose'" with "[Hlx Hownst Hbh] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iExists ν. iSplit; first by auto. iNext. iSplitL; last by auto.
iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
@@ -292,7 +292,7 @@ Section refcell_functions.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
- iApply lft_glb_mono; first done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy [unit; refmut α ty]); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index bc9e076c..a5f90e56 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -24,7 +24,7 @@ Section refmut.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc lv); #(LitLoc lrc) ] =>
- ∃ ν γ β ty', &{α ∪ ν}(lv ↦∗: ty.(ty_own) tid) ∗
+ ∃ ν γ β ty', &{α ⊓ ν}(lv ↦∗: ty.(ty_own) tid) ∗
α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
1.[ν] ∗ own γ (◯ writing_st ν)
| _ => False
@@ -32,8 +32,8 @@ Section refmut.
ty_shr κ tid l :=
∃ (lv lrc : loc),
&frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
- □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ∪ κ]
- ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α ∪ κ) tid lv ∗ q.[α ∪ κ] |}%I.
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ]
+ ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
Next Obligation.
iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
Qed.
@@ -58,7 +58,7 @@ Section refmut.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iExists _, _. iFrame "H↦". rewrite {1}bor_unfold_idx.
iDestruct "Hb" as (i) "[#Hpb Hpbown]".
- iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ∪ κ) tid lv)%I
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ⊓ κ) tid lv)%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". clear HE.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
@@ -68,7 +68,7 @@ Section refmut.
iModIntro. iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
{ iApply bor_shorten; last done. rewrite -assoc.
- iApply lft_glb_mono; first by iApply lft_incl_refl.
+ iApply lft_intersect_mono; first by iApply lft_incl_refl.
iApply lft_incl_glb; first done. iApply lft_incl_refl. }
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
@@ -80,10 +80,10 @@ Section refmut.
- by iApply frac_bor_shorten.
- iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. iApply lft_incl_refl. done. }
+ { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
Qed.
Global Instance refmut_type_contractive α : TypeContractive (refmut α).
@@ -104,17 +104,17 @@ Section refmut.
iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
+ iApply bor_shorten; last iApply bor_iff; last done.
- * iApply lft_glb_mono; first done. iApply lft_incl_refl.
+ * iApply lft_intersect_mono; first done. iApply lft_incl_refl.
* iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
by iApply "Hs".
Qed.
Global Instance refmut_mono_flip E L :
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index b0c55bed..d410c343 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -35,7 +35,7 @@ Section refmut_functions.
iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
- iDestruct (lft_glb_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+ iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hα2β]");
[done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
@@ -193,10 +193,10 @@ Section refmut_functions.
iDestruct "HE" as "[HE HE']". iDestruct "Hν" as "[Hν Hν']".
remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
- iApply (type_type ((☀ (α ∪ ν)) :: E)%EL []
- [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&uniq{α ∪ ν}ty2)])]%CC
+ iApply (type_type ((☀ (α ⊓ ν)) :: E)%EL []
+ [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&uniq{α ⊓ ν}ty2)])]%CC
[ f ◠box (fn(∀ α, [☀α] ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2);
- #lref ◠own_ptr 2 (&uniq{α ∪ ν}ty1); env ◠box envty ]%TC
+ #lref ◠own_ptr 2 (&uniq{α ⊓ ν}ty1); env ◠box envty ]%TC
with "[] LFT Hna [HE Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 38985be1..1c342192 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -41,7 +41,7 @@ Section rwlock_inv.
∃ (ν : lft) q', agν ≡ to_agree ν ∗
□ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
([†ν] ={↑lftN}=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
- ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν]
| _ => (* Locked for write. *) True
end)%I.
@@ -131,9 +131,9 @@ Section rwlock.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_alloc (◠Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
- iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
- iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
+ iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ { iApply lft_intersect_incl_l. }
+ iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Hshr}".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index bb3f0400..cd4dc556 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -183,7 +183,7 @@ Section rwlock_functions.
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
+ iApply (wp_cas_int_suc with "Hlx"); first done. iNext. iIntros "Hlx".
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
- ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
+ ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
with ">[Hlx Hownst Hst Hβtok2]"
@@ -207,10 +207,10 @@ Section rwlock_functions.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
- iDestruct (lft_glb_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+ iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
iApply (fupd_mask_mono (↑lftN)). solve_ndisj.
- iMod (rebor _ _ (β ∪ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
+ { iApply lft_intersect_incl_l. }
iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". solve_ndisj.
iFrame "#". iDestruct ("Hclose" with "Htok") as "[$ Htok2]".
iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
@@ -226,7 +226,7 @@ Section rwlock_functions.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
tctx_hasty_val' //. iFrame.
iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
- iApply lft_glb_mono; first done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
{ rewrite {1}/elctx_interp big_sepL_singleton //. }
iApply (type_sum_assign [unit; rwlockreadguard α ty]); [solve_typing..|].
simpl. iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 6a61a4ad..d14f88a4 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -20,7 +20,7 @@ Section rwlockreadguard.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc l) ] =>
- ∃ ν q γ β, ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
α ⊑ β ∗ &shr{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
q.[ν] ∗ own γ (◯ reading_st q ν) ∗
(1.[ν] ={↑lftN,∅}▷=∗ [†ν])
@@ -29,7 +29,7 @@ Section rwlockreadguard.
ty_shr κ tid l :=
∃ (l' : loc),
&frac{κ} (λ q, l↦∗{q} [ #l']) ∗
- ▷ ty.(ty_shr) (α ∪ κ) tid (shift_loc l' 1) |}%I.
+ ▷ ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) |}%I.
Next Obligation. intros α ty tid [|[[]|] []]; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
@@ -52,12 +52,12 @@ Section rwlockreadguard.
iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "#Hκν".
{ iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
iExists _. iFrame "#". iApply ty_shr_mono; last done.
- iApply lft_glb_mono; last done. iApply lft_incl_refl.
+ iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
Next Obligation.
iIntros (α ty κ κ' tid l) "#Hκ'κ H". iDestruct "H" as (l') "[#Hf #Hshr]".
iExists l'. iSplit; first by iApply frac_bor_shorten.
- iApply ty_shr_mono; last done. iApply lft_glb_mono; last done.
+ iApply ty_shr_mono; last done. iApply lft_intersect_mono; last done.
iApply lft_incl_refl.
Qed.
@@ -84,13 +84,13 @@ Section rwlockreadguard.
iDestruct "H" as (ν q γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
iExists ν, q, γ, β. iFrame "∗#". iSplit; last iSplit.
+ iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
+ iApply (shr_bor_iff with "[] Hinv").
iIntros "!>!#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
- iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
iFrame. iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
Qed.
Global Instance rwlockreadguard_mono_flip E L :
Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L))
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index ac839732..e8a02e85 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -29,8 +29,8 @@ Section rwlockwriteguard.
ty_shr κ tid l :=
∃ (l' : loc),
&frac{κ} (λ q, l↦∗{q} [ #l']) ∗
- □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ∪ κ] ={F, F∖↑shrN∖↑lftN}▷=∗
- ty.(ty_shr) (α ∪ κ) tid (shift_loc l' 1) ∗ q.[α ∪ κ] |}%I.
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ] ={F, F∖↑shrN∖↑lftN}▷=∗
+ ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) ∗ q.[α ⊓ κ] |}%I.
Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
Next Obligation.
iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
@@ -46,7 +46,7 @@ Section rwlockwriteguard.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iExists _. iFrame "H↦". rewrite {1}bor_unfold_idx.
iDestruct "Hb" as (i) "[#Hpb Hpbown]".
- iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ∪ κ) tid (shift_loc l' 1))%I
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ⊓ κ) tid (shift_loc l' 1))%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". clear HE.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
@@ -55,7 +55,7 @@ Section rwlockwriteguard.
{ iApply bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
- { iApply (bor_shorten with "[] Hb"). iApply lft_glb_mono. done.
+ { iApply (bor_shorten with "[] Hb"). iApply lft_intersect_mono. done.
iApply lft_incl_refl. }
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
@@ -67,10 +67,10 @@ Section rwlockwriteguard.
- by iApply frac_bor_shorten.
- iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. iApply lft_incl_refl. done. }
+ { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
Qed.
Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
@@ -103,10 +103,10 @@ Section rwlockwriteguard.
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
by iApply "Hs".
Qed.
Global Instance rwlockwriteguard_mono_flip E L :
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 62077176..72a7e327 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -35,7 +35,7 @@ Section rwlockwriteguard_functions.
iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
rewrite heap_mapsto_vec_singleton.
- iDestruct (lft_glb_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+ iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hα2β]");
[done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index b18f2819..28a52c0e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -154,8 +154,8 @@ Section typing_rules.
Proof.
iIntros (Hc) "He". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
- set (κ' := foldr (∪) static κs). wp_seq.
- iApply ("He" $! (κ' ∪ Λ) with "LFT Htl HE [HL Htk] HC HT").
+ set (κ' := foldr lft_intersect static κs). wp_seq.
+ iApply ("He" $! (κ' ⊓ Λ) with "LFT Htl HE [HL Htk] HC HT").
rewrite /llctx_interp big_sepL_cons. iFrame "HL".
iExists Λ. iSplit; first done. iFrame. done.
Qed.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 1537f6b3..401a2078 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -17,8 +17,8 @@ Section uniq_bor.
end%I;
ty_shr κ' tid l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
- □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ∪κ']
- ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid l' ∗ q.[κ∪κ'])%I
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ⊓κ']
+ ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ'])%I
|}.
Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
@@ -29,7 +29,7 @@ Section uniq_bor.
iFrame. iExists l'. 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 shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid 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.
iDestruct "INV" as "[>Hbtok|#Hshr]".
@@ -43,8 +43,8 @@ Section uniq_bor.
Qed.
Next Obligation.
intros κ0 ty κ κ' tid l. iIntros "#Hκ #H".
- iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
- { iApply lft_glb_mono. iApply lft_incl_refl. done. }
+ iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
+ { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
iIntros "!# * % Htok".
iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try set_solver.
@@ -64,8 +64,8 @@ Section uniq_bor.
iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
- - iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
- { iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
+ { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
iMod ("Hupd" with "[%] Htok") as "Hupd'"; try done. iModIntro. iNext.
--
GitLab