diff --git a/iris b/iris
index 8f33e2828ae7b286adee0071ffa5c40fb4977fcd..2c21612f6edaa36b6bbadba09b310281af21fd14 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 8f33e2828ae7b286adee0071ffa5c40fb4977fcd
+Subproject commit 2c21612f6edaa36b6bbadba09b310281af21fd14
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
index f68755d8bd070e3514cd8968297116dfc1d7c891..3206ab3dc0f2ad498a8663f99dc54832c138a894 100644
--- a/theories/frac_borrow.v
+++ b/theories/frac_borrow.v
@@ -1,5 +1,5 @@
From Coq Require Import Qcanon.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics fractional.
From iris.algebra Require Import frac.
From lrust Require Export lifetime shr_borrow.
@@ -18,84 +18,91 @@ Section frac_borrow.
Global Instance frac_borrow_proper :
Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ).
Proof. solve_proper. Qed.
- Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _.
+ Global Instance frac_borrow_persistent : PersistentP (&frac{κ}Φ) := _.
- Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ:
- lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
+ Lemma borrow_fracture Φ `(nclose lftN ⊆ E) κ:
+ lft_ctx ⊢ &{κ}(Φ 1%Qp) ={E}=∗ &frac{κ}Φ.
Proof.
- iIntros "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
- iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H†Hclose]]". done.
- - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
- { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
+ iIntros "#LFT HΦ". iMod (own_alloc 1%Qp) as (γ) "?". done.
+ iMod (borrow_acc_atomic_strong with "LFT HΦ") as "[[HΦ Hclose]|[H†Hclose]]". done.
+ - iMod ("Hclose" with "*[-]") as "HΦ"; last first.
+ { iExists γ, κ. iSplitR; last by iApply (borrow_share with "HΦ").
iApply lft_incl_refl. }
iSplitL. by iExists 1%Qp; iFrame; auto.
- iIntros "!>H†Hφ!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
+ iIntros "!>H†HΦ!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
iDestruct "Hκ" as (q'') "[_ Hκ]".
iDestruct (lft_own_dead with "Hκ H†") as "[]".
- - iMod ("Hclose" with "*") as "Hφ"; last first.
+ - iMod ("Hclose" with "*") as "HΦ"; last first.
iExists γ, κ. iSplitR. by iApply lft_incl_refl.
iMod (borrow_fake with "LFT H†"). done. by iApply borrow_share.
Qed.
- Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ:
- lft_ctx ⊢ &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖lftN,E}=∗ True))
+ Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ Φ:
+ lft_ctx ⊢ &frac{κ}Φ ={E,E∖lftN}=∗ (∃ q, ▷ Φ q ∗ (▷ Φ q ={E∖lftN,E}=∗ True))
∨ [†κ] ∗ |={E∖lftN,E}=> True.
Proof.
- iIntros "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
- iMod (shr_borrow_acc with "LFT Hshr") as "[[Hφ Hclose]|[H†Hclose]]". done.
- - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
- iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
+ iIntros "#LFT #HΦ". iDestruct "HΦ" as (γ κ') "[Hκκ' Hshr]".
+ iMod (shr_borrow_acc with "LFT Hshr") as "[[HΦ Hclose]|[H†Hclose]]". done.
+ - iLeft. iDestruct "HΦ" as (q) "(HΦ & Hγ & H)". iExists q. iFrame.
+ iIntros "!>HΦ". iApply "Hclose". iExists q. iFrame.
- iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
iApply fupd_intro_mask. set_solver. done.
Qed.
- Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
- lft_ctx ⊢ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗
- &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
+ Lemma frac_borrow_acc_strong `(nclose lftN ⊆ E) q κ Φ:
+ lft_ctx ⊢ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
+ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
Proof.
- iIntros "#LFT #Hφ Hfrac Hκ". unfold frac_borrow.
+ iIntros "#LFT #HΦ Hfrac Hκ". unfold frac_borrow.
iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
- iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
- destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
+ iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & Hq)".
+ destruct (Qp_lower_bound (qκ'/2) (qΦ/2)) as (qq & qκ'0 & qΦ0 & Hqκ' & HqΦ).
iExists qq.
- iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
- { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
- rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
+ iAssert (▷ Φ qq ∗ ▷ Φ (qΦ0 + qΦ / 2))%Qp%I with "[HΦqΦ]" as "[$ HqΦ]".
+ { iNext. rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ. iApply "HΦ". by rewrite assoc. }
+ rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ -assoc {1}Hqκ'.
iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
- iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1".
+ iMod ("Hclose'" with "[HqΦ Hq Hown Hκq]") as "Hκ1".
{ iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
- subst. iExists qq. iIntros "{$Hκq}!%".
- by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2.
+ by rewrite (comm _ qΦ0) -assoc (comm _ qΦ0) -HqΦ Qp_div_2.
- iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
- rewrite lft_own_frac_op. iIntros "{$Hκq $Hq'κ}!%".
- by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. }
- clear Hqφ qφ qφ0. iIntros "!>Hqφ".
+ iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -HqΦ Qp_div_2. }
+ clear HqΦ qΦ qΦ0. iIntros "!>HqΦ".
iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
- iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])".
+ iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & >[%|Hq])".
{ subst. iCombine "Hown" "Hownq" as "Hown".
by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
- iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
- iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'.
+ iDestruct "Hq" as (q') "[HqΦq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
+ iDestruct (own_valid with "Hown") as %Hval. iDestruct "HqΦq'" as %HqΦq'.
assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
- { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'.
- rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
+ { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
+ rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
destruct Hval as [Hval|Hval].
by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
- assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
- iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2".
- { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame.
+ iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
+ { iNext. iExists (qΦ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "HΦ"; iFrame.
iRight. iExists _. iIntros "{$Hq'qκ}!%".
- revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. }
- iApply "Hclose". iFrame. rewrite Hqκ' !lft_own_frac_op. by iFrame.
- - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2".
- { iNext. iExists (qφ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. }
- iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
+ revert HqΦq'. rewrite !Qp_eq. move=>/=<-. ring. }
+ iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
+ - iMod ("Hclose'" with "[HqΦ HΦqΦ Hown]") as "Hqκ2".
+ { iNext. iExists (qΦ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "HΦ"; iFrame. auto. }
+ iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
Qed.
- Lemma frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
+ Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ Φ:
+ Fractional Φ →
+ lft_ctx ⊢ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
+ Proof.
+ iIntros (?) "LFT". iApply (frac_borrow_acc_strong with "LFT"). done.
+ iIntros "!#*". rewrite fractional. iSplit; auto.
+ Qed.
+
+ Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' ⊢ &frac{κ'}Φ -∗ &frac{κ}Φ.
Proof.
iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
iApply lft_incl_trans. iFrame.
@@ -106,9 +113,8 @@ Section frac_borrow.
Proof.
iIntros "#LFT#Hbor!#". iSplitR.
- iIntros (q') "Hκ'".
- iMod (frac_borrow_acc with "LFT [] Hbor Hκ'") as (q'') "[>? Hclose]". done.
- + iIntros "/=!#*". rewrite Qp_mult_plus_distr_r lft_own_frac_op. iSplit; auto.
- + iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
+ iMod (frac_borrow_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
+ iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
- iIntros "H†'".
iMod (frac_borrow_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
iDestruct "H" as (q') "[>Hκ' _]".
diff --git a/theories/heap.v b/theories/heap.v
index 97087b8f529dd3775a849e69f5e64e1007fadafd..021185f02b93d40ce637ea88be16574a562889bf 100644
--- a/theories/heap.v
+++ b/theories/heap.v
@@ -2,6 +2,7 @@ From iris.algebra Require Import cmra_big_op gmap frac dec_agree.
From iris.algebra Require Import csum excl auth.
From iris.base_logic Require Import big_op lib.invariants.
From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export fractional.
From lrust Require Export lifting.
Import uPred.
@@ -117,22 +118,35 @@ Section heap.
Global Instance heap_mapsto_timeless l q v : TimelessP (l↦{q}v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
+ Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
+ Proof.
+ intros p q. by rewrite heap_mapsto_eq -own_op
+ -auth_frag_op op_singleton pair_op dec_agree_idemp.
+ Qed.
+ Global Instance heap_mapsto_as_fractional l q v:
+ AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
+ Proof. done. Qed.
+
Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
Proof. apply _. Qed.
- Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
- Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
-
- Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
+ Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
Proof.
- by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
+ intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
+ by setoid_rewrite (fractional (λ q, _ ↦{q} v)%I).
Qed.
+ Global Instance heap_mapsto_vec_as_fractional l q vl:
+ AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
+ Proof. done. Qed.
+
+ Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
+ Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
- { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
+ { by rewrite -(fractional (λ q, l ↦{q} _)%I) pure_equiv // left_id. }
apply (anti_symm (⊢)); last by apply pure_elim_l.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
eapply pure_elim; [done|]=> /auth_own_valid /=.
@@ -158,12 +172,6 @@ Section heap.
by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
Qed.
- Lemma heap_mapsto_vec_op_eq l q1 q2 vl :
- l ↦∗{q1} vl ∗ l ↦∗{q2} vl ⊣⊢ l ↦∗{q1+q2} vl.
- Proof.
- rewrite /heap_mapsto_vec -big_sepL_sepL. by setoid_rewrite heap_mapsto_op_eq.
- Qed.
-
Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
length vl1 = length vl2 →
l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ vl1 = vl2 ∧ l ↦∗{q1+q2} vl1.
@@ -174,7 +182,7 @@ Section heap.
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
iDestruct (IH (shift_loc l 1) with "[Hvl1 Hvl2]") as "[% $]"; subst; first by iFrame.
rewrite (inj_iff (:: vl2)). iApply heap_mapsto_op. by iFrame.
- - iIntros "[% Hl]"; subst. by iApply heap_mapsto_vec_op_eq.
+ - by iIntros "[% [$ Hl2]]"; subst.
Qed.
Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
@@ -187,19 +195,11 @@ Section heap.
iDestruct (Hlen with "Hown") as %?.
iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
- - iIntros "Hmt". setoid_rewrite <-heap_mapsto_vec_op_eq.
- iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
+ - iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
iDestruct (Hlen with "Hown") as %?.
iSplitL "Hmt1 Hown"; iExists _; by iFrame.
Qed.
- Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ l ↦{q/2} v ∗ l ↦{q/2} v.
- Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
-
- Lemma heap_mapsto_vec_op_split l q vl :
- l ↦∗{q} vl ⊣⊢ l ↦∗{q/2} vl ∗ l ↦∗{q/2} vl.
- Proof. by rewrite heap_mapsto_vec_op_eq Qp_div_2. Qed.
-
Lemma heap_mapsto_vec_combine l q vl :
vl ≠[] →
l ↦∗{q} vl ⊣⊢ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
diff --git a/theories/lft_contexts.v b/theories/lft_contexts.v
new file mode 100644
index 0000000000000000000000000000000000000000..1f78d25a05f871297b04d1f91eecab7feea52964
--- /dev/null
+++ b/theories/lft_contexts.v
@@ -0,0 +1,20 @@
+From iris.proofmode Require Import tactics.
+From lrust Require Export type lifetime.
+
+Section lft_contexts.
+
+ Context `{iris_typeG Σ}.
+
+ Inductive ext_lft_ctx_elt :=
+ |
+
+ Definition ext_lft_ctx := Qp → iProp Σ.
+
+ Global Instance empty_ext_lft_ctx : Empty ext_lft_ctx := λ _, True%I.
+
+
+
+
+ Definition int_lft_ctx := iProp Σ.
+
+
\ No newline at end of file
diff --git a/theories/lifetime.v b/theories/lifetime.v
index 193be22d9c33f4cd72d93a75ae95384bdc37bc1c..c38eea2723ae1138d4fbc66dc9107759d21d6127 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import csum auth frac gmap.
From iris.base_logic.lib Require Export fancy_updates invariants namespaces.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics fractional.
Definition lftN := nroot .@ "lft".
Definition atomic_lft := positive.
@@ -72,10 +72,23 @@ Section lft.
Axiom lft_ctx_alloc : True ={∅}=∗ lft_ctx.
- (*** PersitentP, TimelessP and Proper instances *)
+ (*** PersitentP, TimelessP, Proper and Fractional instances *)
Global Instance lft_own_timeless q κ : TimelessP q.[κ].
Proof. unfold lft_own. apply _. Qed.
+ Global Instance lft_own_fractional κ : Fractional (λ q, q.[κ])%I.
+ Proof.
+ intros p q. rewrite /lft_own -own_op -auth_frag_op.
+ f_equiv. constructor. done. simpl. intros Λ.
+ rewrite lookup_op !lookup_fmap !lookup_omap. apply reflexive_eq.
+ case: (κ !! Λ)=>[[|a]|]//=. rewrite -Some_op Cinl_op. repeat f_equal.
+ induction a as [|a IH]. done.
+ rewrite /= IH /op /cmra_op /= /frac_op !assoc. f_equal.
+ rewrite -!assoc. f_equal. apply (comm _).
+ Qed.
+ Global Instance lft_own_as_fractional κ q :
+ AsFractional q.[κ] (λ q, q.[κ])%I q.
+ Proof. done. Qed.
Global Instance lft_dead_persistent κ : PersistentP [†κ].
Proof. unfold lft_dead. apply _. Qed.
@@ -120,17 +133,6 @@ Section lft.
(iRight + iLeft); iExists Λ; iIntros "{$Hown}!%"; by eauto.
Qed.
- Lemma lft_own_frac_op κ q q':
- (q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
- Proof.
- rewrite /lft_own -own_op -auth_frag_op. f_equiv. constructor. done. simpl.
- intros Λ. rewrite lookup_op !lookup_fmap !lookup_omap. apply reflexive_eq.
- case: (κ !! Λ)=>[[|a]|]//=. rewrite -Some_op Cinl_op. repeat f_equal.
- induction a as [|a IH]. done.
- rewrite /= IH /op /cmra_op /= /frac_op !assoc. f_equal.
- rewrite -!assoc. f_equal. apply (comm _).
- Qed.
-
Axiom lft_create :
∀ `(nclose lftN ⊆ E),
lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]).
@@ -167,7 +169,7 @@ Section lft.
∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
lft_ctx ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Axiom borrow_unnest :
- ∀ `(nclose lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E}▷=∗ &{κ ⋅ κ'}P.
+ ∀ `(nclose lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E, E∖lftN}▷=∗ &{κ ⋅ κ'}P.
(*** Derived lemmas *)
@@ -193,29 +195,6 @@ Section lft.
iIntros "HΛ". iDestruct "HΛ" as (Λ) "[% _]". naive_solver.
Qed.
- Lemma lft_own_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
- Proof. by rewrite -lft_own_frac_op Qp_div_2. Qed.
-
- Global Instance into_and_lft_own_half κ q :
- IntoAnd false q.[κ] (q/2).[κ] (q/2).[κ] | 100.
- Proof. by rewrite /IntoAnd lft_own_split. Qed.
-
- Global Instance from_sep_lft_own_half κ q :
- FromSep q.[κ] (q/2).[κ] (q/2).[κ] | 100.
- Proof. by rewrite /FromSep -lft_own_split. Qed.
-
- Global Instance frame_lft_own_half κ q :
- Frame (q/2).[κ] q.[κ] (q/2).[κ] | 100.
- Proof. by rewrite /Frame -lft_own_split. Qed.
-
- Global Instance into_and_lft_own_frac κ q1 q2 :
- IntoAnd false (q1+q2).[κ] q1.[κ] q2.[κ].
- Proof. by rewrite /IntoAnd lft_own_frac_op. Qed.
-
- Global Instance from_sep_lft_own_frac κ q1 q2 :
- FromSep (q1+q2).[κ] q1.[κ] q2.[κ].
- Proof. by rewrite /FromSep -lft_own_frac_op. Qed.
-
Global Instance into_and_lft_own κ1 κ2 q :
IntoAnd false q.[κ1⋅κ2] q.[κ1] q.[κ2].
Proof. by rewrite /IntoAnd lft_own_op. Qed.
@@ -323,10 +302,9 @@ Section incl.
iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
- iExists qq. rewrite -lft_own_op !lft_own_frac_op.
+ iExists qq. rewrite -lft_own_op.
iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
- iIntros "!>[Hκ'0 Hκ''0]".
- iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
+ iIntros "!>[Hκ'0 Hκ''0]". iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
- rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
Qed.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 4d646f391561e4efcc01630bd7c6b9de769e1b76..53ca8f6127b24c9a000ad756d577421ce66da80f 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -93,9 +93,7 @@ Section props.
Lemma perm_tok_plus κ q1 q2 :
tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
- Proof.
- rewrite /tok /sep /=; split; iIntros (tid) "_ ?"; rewrite lft_own_frac_op //.
- Qed.
+ Proof. rewrite /tok /sep /=; split; by iIntros (tid) "_ [$$]". Qed.
Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
diff --git a/theories/proofmode.v b/theories/proofmode.v
index ade46392b711c4e74f78101efd0c833e3c0d7c29..a5b9a51a5abb699cae7ea3c3b62ba2560fa511b1 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -12,14 +12,6 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
-Global Instance into_and_mapsto l q v :
- IntoAnd false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoAnd heap_mapsto_op_split. Qed.
-
-Global Instance into_and_mapsto_vec l q vl :
- IntoAnd false (l ↦∗{q} vl) (l ↦∗{q/2} vl) (l ↦∗{q/2} vl).
-Proof. by rewrite /IntoAnd heap_mapsto_vec_op_split. Qed.
-
Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
(Δ ⊢ heap_ctx) → nclose heapN ⊆ E → 0 < n →
IntoLaterEnvs Δ Δ' →
diff --git a/theories/tactics.v b/theories/tactics.v
index 91bdc55c60f2d6f96cbcf3cc92087bac4dc06b9c..0b9e0d371a238b24cb411be4b3e406a27c5dbe27 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -195,7 +195,7 @@ Ltac solve_atomic :=
end.
Hint Extern 0 (language.atomic _) => solve_atomic.
(* For the side-condition of elim_vs_pvs_wp_atomic *)
-Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 0 (language.atomic _) => solve_atomic : atomic.
(** Substitution *)
Ltac simpl_subst :=
diff --git a/theories/type.v b/theories/type.v
index ebc124bc32a755adcd645aa66ae94439131b6e1d..b1abff1ea0452cebe4747cc46d5927023f1b0615 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -91,20 +91,16 @@ Qed.
Next Obligation.
intros st κ tid E F l q ??. iIntros "#LFT #Hshr[Hlft $]".
iDestruct "Hshr" as (vl) "[Hf Hown]".
- iMod (frac_borrow_acc with "LFT [] Hf Hlft") as (q') "[Hmt Hclose]";
- first set_solver.
- - iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_vec_op_eq.
- iSplit; auto.
- - iModIntro. rewrite {1}heap_mapsto_vec_op_split. iExists _.
- iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
- + iNext. iExists _. by iFrame.
- + iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
- iAssert (â–· (length vl = length vl'))%I as ">%".
- { iNext.
- iDestruct (st_size_eq with "Hown") as %->.
- iDestruct (st_size_eq with "Hown'") as %->. done. }
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
- iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
+ iMod (frac_borrow_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']".
+ iAssert (â–· (length vl = length vl'))%I as ">%".
+ { iNext.
+ iDestruct (st_size_eq with "Hown") as %->.
+ iDestruct (st_size_eq with "Hown'") as %->. done. }
+ iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+ iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
Qed.
End type.
@@ -213,7 +209,7 @@ Section types.
ty_shr κ' tid E l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
∀ q', □ (q'.[κ ⋅ κ']
- ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I
+ ={mgmtE ∪ E, tlN}▷=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I
|}.
Next Obligation. done. Qed.
Next Obligation.
@@ -232,16 +228,19 @@ Section types.
iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid N l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
+ iApply (step_fupd_mask_mono (mgmtE ∪ N) _ _ ((mgmtE ∪ N) ∖ N ∖ lftN)).
+ { assert (nclose lftN ⊥ tlN) by solve_ndisj. set_solver. } set_solver.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
- replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ rewrite /borrow. eauto. }
iMod (borrow_unnest with "LFT Hb") as "Hb". set_solver.
iIntros "!>". iNext. iMod "Hb".
- iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done.
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
- - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
+ - iMod (step_fupd_mask_mono _ _ _ _ True%I with "[]") as "Hclose'"; last first.
+ iIntros "!>". iNext. iMod "Hclose'" as "_".
+ iMod ("Hclose" with "[]") as "_"; by eauto. eauto. done. set_solver.
Qed.
Next Obligation.
intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
@@ -325,7 +324,7 @@ Section types.
iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". done. 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 -!heap_mapsto_vec_op_eq !split_prod_mt.
+ rewrite !split_prod_mt.
iAssert (â–· (length vl1 = ty1.(ty_size)))%I with "[#]" as ">%".
{ iNext. by iApply ty_size_eq. }
iAssert (â–· (length vl2 = ty2.(ty_size)))%I with "[#]" as ">%".
@@ -412,21 +411,17 @@ Section types.
intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?.
iIntros "#LFT #H[[Htok1 Htok2] Htl]".
setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
- iMod (frac_borrow_acc with "LFT [] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
- { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; eauto. }
+ iMod (frac_borrow_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
iMod ((nth i tyl emp).(ty_shr_acc) with "LFT Hshr [Htok2 $Htl]")
as (q'2) "[Hownq Hclose']"; try done.
{ edestruct nth_in_or_default as [| ->]; last done.
rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left. }
destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
- iExists q'. iModIntro.
- rewrite -{1}heap_mapsto_op_eq -{1}heap_mapsto_vec_prop_op;
- last (by intros; apply sum_size_eq, Hn).
+ rewrite -{1}heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 Hown2]".
- iSplitL "Hown1 Hownq1".
+ iExists q'. iModIntro. iSplitL "Hown1 Hownq1".
- iNext. iExists i. by iFrame.
- iIntros "H". iDestruct "H" as (i') "[Hown1 Hownq1]".
- rewrite (lft_own_split _ q).
iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_op.
iDestruct "Hown" as "[>#Hi Hown]". iDestruct "Hi" as %[= ->%Z_of_nat_inj].
iMod ("Hclose" with "Hown") as "$".
diff --git a/theories/typing.v b/theories/typing.v
index bf0398bf219a0eabc4ffe3958671c293c70740da..a607c2196ddd6da4ebca49697a87b829f83d9d73 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -292,8 +292,7 @@ Section typing.
rewrite has_type_value. iDestruct "Hâ—" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
iDestruct "H↦" as (vl) "[H↦b Hown]".
- iMod (frac_borrow_acc with "LFT [] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
- { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
+ iMod (frac_borrow_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iSpecialize ("Hown" $! _ with "Htok2").
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
- iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ∗ v = #vl)%I); try done.
@@ -319,14 +318,18 @@ Section typing.
iMod (borrow_split with "LFT Hbor") as "[H↦ Hbor]". done.
iMod (borrow_exists with "LFT Hbor") as (l') "Hbor". done.
iMod (borrow_split with "LFT Hbor") as "[Heq Hbor]". done.
- iMod (borrow_unnest with "LFT Hbor") as "Hbor". done.
iMod (borrow_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
iMod (borrow_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
- rewrite heap_mapsto_vec_singleton. wp_read.
- iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
- iMod ("Hclose" with "Htok") as "$". iFrame "#".
- iMod "Hbor". iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
- iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
+ rewrite heap_mapsto_vec_singleton.
+ iApply (wp_strong_mono ⊤ ⊤ _ (λ v, _ ∗ v = #l' ∗ l ↦#l')%I). done.
+ iSplitR "Hbor H↦"; last first.
+ - iApply (wp_frame_step_l with "[-]"); try done; last first.
+ iSplitL "Hbor". by iApply (borrow_unnest with "LFT Hbor"). wp_read. auto.
+ - iIntros (v) "(Hbor & % & H↦)". subst.
+ iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
+ iMod ("Hclose" with "Htok") as "$". iFrame "#".
+ iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
+ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
Qed.
Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
@@ -339,8 +342,7 @@ Section typing.
rewrite has_type_value. iDestruct "Hâ—" as (l) "[Heq Hshr]".
iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
- iMod (frac_borrow_acc with "LFT [] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
- { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
+ iMod (frac_borrow_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
@@ -349,7 +351,7 @@ Section typing.
- iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ∗ v = #l')%I); try done.
iSplitL "Hown"; last by wp_read; eauto.
iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
- last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
+ last iApply "Hown"; (set_solver || rewrite ?disjoint_union_l; solve_ndisj).
- iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
iMod ("Hclose''" with "Htok") as "Htok".
iMod ("Hclose'" with "[$H↦]") as "Htok'".