Skip to content
Snippets Groups Projects
Commit 8602c269 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Derive unnesting and reborrowing from a common principle. 

The common principle is "unnesting an index borrow". This simplifies
the proofs of reborrowing and unnesting, and, moreover, gives a slightly
stronger unnesting rule (the masks are different).
parent 83c446d0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 409 additions and 466 deletions
_CoqProject
+ 1
− 1
View file @ 8602c269
......@@ -5,8 +5,8 @@ theories/lifetime/model/faking.v
theories/lifetime/model/creation.v
theories/lifetime/model/primitive.v
theories/lifetime/model/accessors.v
theories/lifetime/model/raw_reborrow.v
theories/lifetime/model/borrow.v
theories/lifetime/model/borrow_sep.v
theories/lifetime/model/reborrow.v
theories/lifetime/lifetime_sig.v
theories/lifetime/lifetime.v
......
theories/lifetime/lifetime.v
+ 53
− 2
View file @ 8602c269
From lrust.lifetime Require Export lifetime_sig.
From lrust.lifetime.model Require definitions primitive accessors faking borrow
reborrow creation.
borrow_sep reborrow creation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
......@@ -10,6 +10,7 @@ Module Export lifetime : lifetime_sig.
Include primitive.
Include borrow.
Include faking.
Include borrow_sep.
Include reborrow.
Include accessors.
Include creation.
......@@ -25,6 +26,17 @@ Section derived.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
Lemma bor_acc_atomic E κ P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
(▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
Proof.
iIntros (?) "#LFT HP".
iMod (bor_acc_atomic_cons with "LFT HP") as "[[HP Hclose]|[? ?]]"; first done.
- iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "[] HP"); auto.
- iRight. by iFrame.
Qed.
Lemma bor_acc_cons E q κ P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
......@@ -46,6 +58,17 @@ Proof.
iIntros "!>HP". iMod ("Hclose" with "[] HP") as "[$ $]"; auto.
Qed.
Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
Proof.
iIntros (?) "#LFT Hb".
iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
- iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
iExists x. iApply ("Hclose" with "[] HΦ"). iIntros "!> ?"; eauto.
- iExists inhabitant. by iApply (bor_fake with "LFT").
Qed.
Lemma bor_or E κ P Q :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
......@@ -78,6 +101,7 @@ Lemma later_bor_static E P :
Proof.
iIntros (?) "#LFT HP". iMod (bor_create with "LFT HP") as "[$ _]"; done.
Qed.
Lemma bor_static_later E P :
↑lftN ⊆ E →
lft_ctx -∗ &{static} P ={E}=∗ ▷ P.
......@@ -95,6 +119,34 @@ Proof.
iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
Qed.
Lemma rebor E κ κ' P :
↑lftN ⊆ E →
lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Proof.
iIntros (?) "#LFT #Hκ'κ Hbor". rewrite [(&{κ}P)%I]bor_unfold_idx.
iDestruct "Hbor" as (i) "[#Hbor Hidx]".
iMod (bor_create _ κ' with "LFT Hidx") as "[Hidx Hinh]"; first done.
iMod (idx_bor_unnest with "LFT Hbor Hidx") as "Hbor'"; first done.
iDestruct (bor_shorten with "[] Hbor'") as "$".
{ iApply lft_incl_glb. done. iApply lft_incl_refl. }
iIntros "!> H†". iMod ("Hinh" with "H†") as ">Hidx". auto with iFrame.
Qed.
Lemma bor_unnest E κ κ' P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ'} &{κ} P ={E}▷=∗ &{κ ⊓ κ'} P.
Proof.
iIntros (?) "#LFT Hbor".
iMod (bor_acc_atomic_cons with "LFT Hbor") as
"[[Hbor Hclose]|[H† Hclose]]"; first done.
- rewrite ->bor_unfold_idx. iDestruct "Hbor" as (i) "[#Hidx Hbor]".
iMod ("Hclose" with "[] Hbor") as "Hbor".
{ iIntros "!> H". rewrite bor_unfold_idx. auto with iFrame. }
iIntros "!>"; iNext. by iApply (idx_bor_unnest with "LFT Hidx Hbor").
- iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
rewrite -lft_dead_or. auto.
Qed.
Lemma bor_persistent P `{!PersistentP P} E κ :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
......@@ -129,5 +181,4 @@ Proof.
- iApply lft_incl_trans; last iApply IH. (* FIXME: Why does "done" not do this? Looks like "assumption" to me. *)
iApply lft_intersect_incl_r.
Qed.
End derived.
theories/lifetime/lifetime_sig.v
+ 6
− 10
View file @ 8602c269
......@@ -54,6 +54,9 @@ Module Type lifetime_sig.
Context `{invG, lftG Σ}.
(** Instances *)
Global Declare Instance lft_inhabited : Inhabited lft.
Global Declare Instance bor_idx_inhabited : Inhabited bor_idx.
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 κ).
......@@ -109,16 +112,14 @@ Module Type lifetime_sig.
Parameter bor_combine : ∀ E κ P Q,
↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
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.
Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
Parameter idx_bor_iff : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
Parameter idx_bor_unnest : ∀ E κ κ' i P,
↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
Parameter idx_bor_acc : ∀ E q κ i P, ↑lftN ⊆ E →
lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
......@@ -154,15 +155,10 @@ Module Type lifetime_sig.
lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
(lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
(* Same for some of the derived lemmas. *)
Parameter bor_exists : ∀ {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ,
↑lftN ⊆ E → lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
Parameter bor_acc_atomic_cons : ∀ E κ P,
↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
(▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
([†κ] ∗ |={E∖↑lftN,E}=> True).
Parameter bor_acc_atomic : ∀ E κ P,
↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
(▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
End properties.
......
theories/lifetime/model/accessors.v
+ 0
− 11
View file @ 8602c269
......@@ -281,15 +281,4 @@ Proof.
+ iApply (bor_shorten with "Hκκ' Hb").
- iRight. by iFrame.
Qed.
Lemma bor_acc_atomic E κ P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
(▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
Proof.
iIntros (?) "#LFT HP".
iMod (bor_acc_atomic_cons with "LFT HP") as "[[HP Hclose]|[? ?]]"; first done.
- iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "[] HP"); auto.
- iRight. by iFrame.
Qed.
End accessors.
theories/lifetime/model/borrow.v
+ 11
− 133
View file @ 8602c269
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Export faking raw_reborrow.
From lrust.lifetime Require Export faking.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
......@@ -10,9 +10,9 @@ Section borrow.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
Lemma bor_create E κ P :
Lemma raw_bor_create E κ P :
↑lftN ⊆ E →
lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
lft_ctx -∗ ▷ P ={E}=∗ raw_bor κ P ∗ ([†κ] ={E}=∗ ▷ P).
Proof.
iIntros (HE) "#LFT HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
......@@ -43,8 +43,7 @@ Proof.
simpl. iFrame. }
iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
iSplitL "HB◯ HsliceB".
+ rewrite /bor /raw_bor /idx_bor_own. iExists κ; simpl.
iModIntro. iSplit; first by iApply lft_incl_refl. iExists γB. iFrame.
+ rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
iExists P. rewrite -uPred.iff_refl. auto.
+ clear -HE. iIntros "!> H†".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
......@@ -63,137 +62,16 @@ Proof.
- iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
rewrite /lft_inv_dead. iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl -big_sepS_later.
iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iNext.
rewrite /lft_inv. iRight. rewrite /lft_inv_dead. iFrame. eauto.
unfold bor. iFrame. iApply "Hclose". iExists _, _. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iNext. rewrite /lft_inv. iRight.
rewrite /lft_inv_dead. iFrame. eauto.
Qed.
Lemma bor_sep E κ P Q :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
Proof.
iIntros (HE) "#LFT Hbor". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
rewrite {1}/bor. iDestruct "Hbor" as (κ') "[#Hκκ' Hbor]".
rewrite /raw_bor /idx_bor_own. iDestruct "Hbor" as (s) "[Hbor Hslice]".
iDestruct "Hslice" as (P') "[#HPP' Hslice]".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
- rewrite lft_inv_alive_unfold /lft_bor_alive.
iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
iDestruct "H" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_iff _ _ true with "HPP' Hslice Hbox")
as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
{ by rewrite lookup_fmap EQB. }
iAssert (▷ lft_vs κ' Pb' Pi)%I with "[Hvs]" as "Hvs".
{ iNext. iApply (lft_vs_cons false with "[] Hvs"). iIntros "[$ ?]!>".
by iApply "HPbPb'". }
iMod (slice_split _ _ true with "Hslice Hbox")
as (γ1 γ2) "(Hγ1 & Hγ2 & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
{ by rewrite lookup_insert. }
rewrite delete_insert //. iDestruct "Hγ1" as %Hγ1. iDestruct "Hγ2" as %Hγ2.
iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
{ etrans; last etrans.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_alloc,
(alloc_singleton_local_update _ γ1 (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //.
- apply cmra_update_op; last done.
apply auth_update_alloc,
(alloc_singleton_local_update _ γ2 (1%Qp, to_agree Bor_in)); last done.
rewrite lookup_insert_ne // /to_borUR -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
rewrite !big_sepM_insert /=.
+ by rewrite left_id -(big_sepM_delete _ _ _ _ EQB).
+ by rewrite -fmap_None -lookup_fmap fmap_delete.
+ by rewrite lookup_insert_ne // -fmap_None -lookup_fmap fmap_delete.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor1]"; first solve_ndisj.
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor2]"; first solve_ndisj.
iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
{ iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
iRight. iSplit; last by auto. iExists _. iFrame. }
unfold bor. iSplitL "Hbor1"; iExists _; eauto.
Qed.
Lemma bor_combine E κ P Q :
Lemma bor_create E κ P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
lft_ctx -∗ ▷ P ={E}=∗ &{κ}P ∗ ([†κ] ={E}=∗ ▷ P).
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 _]".
done. by apply gmultiset_union_subseteq_l.
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]".
iDestruct "Hslice1" as (P') "[#HPP' Hslice1]".
iDestruct "Hslice2" as (Q') "[#HQQ' Hslice2]".
iDestruct (own_bor_auth with "HI Hbor1") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
- rewrite lft_inv_alive_unfold /lft_bor_alive.
iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
iDestruct "H" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor1")
as %[EQB1%to_borUR_included _]%auth_valid_discrete_2.
iDestruct (own_bor_valid_2 with "Hown Hbor2")
as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
{ iIntros (->).
iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
by intros [[]]. }
iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
{ done. }
{ by rewrite lookup_fmap EQB1. }
{ by rewrite lookup_fmap EQB2. }
iCombine "Hown" "Hbor1" as "Hbor1". iCombine "Hbor1" "Hbor2" as "Hbor".
rewrite -!own_bor_op. iMod (own_bor_update with "Hbor") as "Hbor".
{ etrans; last etrans.
- apply cmra_update_op; last done.
apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_alloc,
(alloc_singleton_local_update _ γ (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR -!fmap_delete lookup_fmap fmap_None
-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).
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'"). }
iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
rewrite !big_sepM_insert /=.
+ rewrite (big_sepM_delete _ _ _ _ EQB1) /=. iNext. simpl.
rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=.
by iDestruct "HB" as "[_ $]". rewrite lookup_delete_ne //.
+ rewrite -fmap_None -lookup_fmap !fmap_delete //.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
iMod ("Hclose" with "[-Hbor]") as "_".
{ iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
iRight. iSplit; last by auto. iExists _. iFrame. }
unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
iIntros (?) "#LFT HP". iMod (raw_bor_create with "LFT HP") as "[HP $]"; [done|].
rewrite /bor. iExists _. iFrame. iApply lft_incl_refl.
Qed.
End borrow.
theories/lifetime/model/borrow_sep.v 0 → 100644
+ 141
− 0
View file @ 8602c269
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Export faking reborrow.
From iris.algebra Require Import csum auth frac gmap agree.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section borrow.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
Lemma bor_sep E κ P Q :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
Proof.
iIntros (HE) "#LFT Hbor". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
rewrite {1}/bor. iDestruct "Hbor" as (κ') "[#Hκκ' Hbor]".
rewrite /raw_bor /idx_bor_own. iDestruct "Hbor" as (s) "[Hbor Hslice]".
iDestruct "Hslice" as (P') "[#HPP' Hslice]".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
- rewrite lft_inv_alive_unfold /lft_bor_alive.
iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
iDestruct "H" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_iff _ _ true with "HPP' Hslice Hbox")
as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
{ by rewrite lookup_fmap EQB. }
iAssert (▷ lft_vs κ' Pb' Pi)%I with "[Hvs]" as "Hvs".
{ iNext. iApply (lft_vs_cons false with "[] Hvs"). iIntros "[$ ?]!>".
by iApply "HPbPb'". }
iMod (slice_split _ _ true with "Hslice Hbox")
as (γ1 γ2) "(Hγ1 & Hγ2 & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
{ by rewrite lookup_insert. }
rewrite delete_insert //. iDestruct "Hγ1" as %Hγ1. iDestruct "Hγ2" as %Hγ2.
iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
{ etrans; last etrans.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_alloc,
(alloc_singleton_local_update _ γ1 (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //.
- apply cmra_update_op; last done.
apply auth_update_alloc,
(alloc_singleton_local_update _ γ2 (1%Qp, to_agree Bor_in)); last done.
rewrite lookup_insert_ne // /to_borUR -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
rewrite !big_sepM_insert /=.
+ by rewrite left_id -(big_sepM_delete _ _ _ _ EQB).
+ by rewrite -fmap_None -lookup_fmap fmap_delete.
+ by rewrite lookup_insert_ne // -fmap_None -lookup_fmap fmap_delete.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor1]"; first solve_ndisj.
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor2]"; first solve_ndisj.
iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
{ iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
iRight. iSplit; last by auto. iExists _. iFrame. }
unfold bor. iSplitL "Hbor1"; iExists _; eauto.
Qed.
Lemma bor_combine E κ P Q :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} P -∗ &{κ} Q ={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 _]".
done. by apply gmultiset_union_subseteq_l.
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]".
iDestruct "Hslice1" as (P') "[#HPP' Hslice1]".
iDestruct "Hslice2" as (Q') "[#HQQ' Hslice2]".
iDestruct (own_bor_auth with "HI Hbor1") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
- rewrite lft_inv_alive_unfold /lft_bor_alive.
iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
iDestruct "H" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor1")
as %[EQB1%to_borUR_included _]%auth_valid_discrete_2.
iDestruct (own_bor_valid_2 with "Hown Hbor2")
as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
{ iIntros (->).
iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
by intros [[]]. }
iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
{ done. }
{ by rewrite lookup_fmap EQB1. }
{ by rewrite lookup_fmap EQB2. }
iCombine "Hown" "Hbor1" as "Hbor1". iCombine "Hbor1" "Hbor2" as "Hbor".
rewrite -!own_bor_op. iMod (own_bor_update with "Hbor") as "Hbor".
{ etrans; last etrans.
- apply cmra_update_op; last done.
apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_alloc,
(alloc_singleton_local_update _ γ (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR -!fmap_delete lookup_fmap fmap_None
-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).
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'"). }
iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
rewrite !big_sepM_insert /=.
+ rewrite (big_sepM_delete _ _ _ _ EQB1) /=. iNext. simpl.
rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=.
by iDestruct "HB" as "[_ $]". rewrite lookup_delete_ne //.
+ rewrite -fmap_None -lookup_fmap !fmap_delete //.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
iMod ("Hclose" with "[-Hbor]") as "_".
{ iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
iRight. iSplit; last by auto. iExists _. iFrame. }
unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
Qed.
End borrow.
\ No newline at end of file
theories/lifetime/model/primitive.v
+ 2
− 0
View file @ 8602c269
......@@ -262,6 +262,8 @@ Proof.
Qed.
(** Basic rules about lifetimes *)
Instance lft_inhabited : Inhabited lft := _.
Instance bor_idx_inhabited : Inhabited bor_idx := _.
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 κ) := _.
......
theories/lifetime/model/raw_reborrow.v deleted 100644 → 0
+ 0
− 200
View file @ 83c446d0
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Import faking.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section rebor.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
(* Notice that taking lft_inv for both κ and κ' already implies
κ ≠ κ'. Still, it is probably more instructing to require
κ ⊂ κ' in this lemma (as opposed to just κ ⊆ κ'), and it
should not increase the burden on the user. *)
Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
↑borN ⊆ E →
let Iinv := (own_ilft_auth I ∗ ▷?q lft_inv A κ)%I in
κ ⊂ κ' →
lft_alive_in A κ' →
Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷?q lft_bor_alive κ' Pb -∗
▷?q lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
Proof.
iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
iMod (own_cnt_update with "Hn●") as "[Hn● H◯]".
{ apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
rewrite {1}/raw_bor /idx_bor_own /=.
iDestruct (own_bor_auth with "HI Hi") as %?.
assert (κ ⊆ κ') by (by apply strict_include).
iDestruct (lft_inv_alive_in with "Hκ") as "Hκ";
first by eauto using lft_alive_in_subseteq.
rewrite lft_inv_alive_unfold;
iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
iDestruct (own_bor_valid_2 with "HB● Hi")
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
{ by rewrite lookup_fmap HB. }
iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
{ eapply auth_update, singleton_local_update; last eapply
(exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
{ iNext. rewrite /lft_inv. iLeft.
iSplit; last by eauto using lft_alive_in_subseteq.
rewrite lft_inv_alive_unfold. iExists Pb', Pi'. iFrame "Hvs' Hinh'".
rewrite /lft_bor_alive. iExists (<[i:=Bor_rebor κ']>B).
rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame; auto. }
clear B HB Pb' Pi'.
rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
iMod (slice_insert_full with "HP Hbox")
as (j) "(HBj & #Hjslice & Hbox)"; first done.
iDestruct "HBj" as %HBj; move: HBj; rewrite lookup_fmap fmap_None=> HBj.
iMod (own_bor_update with "HB●") as "[HB● Hj]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HBj. }
iModIntro. iExists (P ∗ Pb)% I. rewrite /Iinv. iFrame "HI". iFrame.
iSplitL "Hj".
{ rewrite /raw_bor /idx_bor_own. iExists j. iFrame. iExists P.
rewrite -uPred.iff_refl. auto. }
iSplitL "Hbox HB● HB".
{ rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
by rewrite /bor_cnt. }
clear dependent Iinv I.
iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
iIntros (I) "Hinv [HP HPb] #Hκ†".
rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
rewrite lft_inv_alive_unfold.
iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
iDestruct (own_bor_valid_2 with "HB● Hi")
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
{ eapply auth_update, singleton_local_update,
(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.
{ by rewrite lookup_fmap HB. }
iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
rewrite /=. iDestruct "Hcnt" as "[% H1◯]".
iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
[$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
{ rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
iIntros (_). rewrite lft_inv_alive_unfold.
iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
{ rewrite /raw_bor /idx_bor_own /=. auto. }
iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
by iFrame.
Qed.
Lemma raw_bor_unnest' E q A I Pb Pi P κ κ' :
↑borN ⊆ E →
let Iinv := (
own_ilft_auth I ∗
▷?q [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
κ ⊆ κ' →
lft_alive_in A κ' →
Iinv -∗ raw_bor κ P -∗ ▷?q lft_bor_alive κ' Pb -∗
▷?q lft_vs κ' (raw_bor κ P ∗ Pb) Pi ={E}=∗ ∃ Pb',
Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
Proof.
iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hinv) Hraw Hκalive' Hvs".
destruct (decide (κ = κ')) as [<-|Hκneq].
{ iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI Hinv Hκalive' Hraw".
iApply (lft_vs_cons with "[]"); last done.
iIntros "(Hdead & HPb)".
iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
by iFrame. }
assert (κ ⊂ κ') by (by apply strict_spec_alt).
iDestruct (raw_bor_inI with "HI Hraw") as %HI.
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose]".
{ rewrite elem_of_difference elem_of_dom not_elem_of_singleton. done. }
rewrite {1}/raw_bor. iDestruct "Hraw" as (i) "[Hi #Hislice]".
iDestruct "Hislice" as (P') "[#HPP' Hislice]".
iMod (raw_bor_unnest with "[$HI $Hinv] Hi Hislice Hκalive' [Hvs]")
as (Pb') "([HI Hκ] & ? & ? & ?)"; [done..| |].
{ iApply (lft_vs_cons with "[]"); last done.
iIntros "[$ [>? $]]". iModIntro. iNext. rewrite /raw_bor.
iExists i. iFrame. iExists _. iFrame "#". }
iExists Pb'. iModIntro. iFrame. iSplitL "Hclose Hκ". by iApply "Hclose".
by iApply (raw_bor_iff with "HPP'").
Qed.
Lemma raw_rebor E κ κ' P :
↑lftN ⊆ E → κ ⊆ κ' →
lft_ctx -∗ raw_bor κ P ={E}=∗
raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
Proof.
rewrite /lft_ctx. iIntros (??) "#LFT Hκ".
destruct (decide (κ = κ')) as [<-|Hκneq].
{ iFrame. iIntros "!> #Hκ†". by iApply (raw_bor_fake' with "LFT Hκ†"). }
assert (κ ⊂ κ') by (by apply strict_spec_alt).
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iMod (ilft_create _ _ κ' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
clear A I; rename A' into A; rename I' into I.
iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
first by apply elem_of_dom.
rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[? >%]|[Hdead >%]]"; last first.
{ rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & >H● & Hinh)".
iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead $]"; first solve_ndisj.
iMod ("Hclose" with "[-Hκ]") as "_"; last auto.
iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom.
iFrame "Hinv". rewrite /lft_inv /lft_inv_dead. iRight.
iSplit; last done. iExists Pi. by iFrame. }
rewrite lft_inv_alive_unfold; iDestruct "Hκinv'" as (Pb Pi) "(Hbor & Hvs & Hinh)".
rewrite {1}/raw_bor. iDestruct "Hκ" as (i) "[Hi #Hislice]".
iDestruct "Hislice" as (P') "[#HPP' Hislice]".
iMod (lft_inh_extend _ _ (idx_bor_own 1 (κ, i)) with "Hinh")
as "(Hinh & HIlookup & Hinh_close)"; first solve_ndisj.
iDestruct (own_bor_auth with "HI [Hi]") as %?.
{ by rewrite /idx_bor_own. }
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hκ Hκclose]".
{ by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
iMod (raw_bor_unnest _ true _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I
with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
as (Pb') "([HI Hκ] & HP' & Halive & Hvs)"; [solve_ndisj|done|done|..].
{ iNext. by iApply lft_vs_frame. }
iDestruct (raw_bor_iff with "HPP' HP'") as "$".
iDestruct ("Hκclose" with "Hκ") as "Hinv".
iMod ("Hclose" with "[HA HI Hinv Halive Hinh Hvs]") as "_".
{ iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
rewrite /lft_inv. iLeft. iSplit; last done.
rewrite lft_inv_alive_unfold. iExists Pb', (idx_bor_own 1 (κ, i) ∗ Pi)%I.
iFrame. }
clear dependent A I Pb Pb' Pi. iModIntro. iIntros "H†".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iDestruct ("HIlookup" with "HI") as %Hκ'.
iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
first by apply elem_of_dom.
rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >%]|[Hdead >%]]".
- (* the same proof is in bor_fake and bor_create *)
rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
unfold lft_alive_in in *. naive_solver.
- rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
iMod ("Hinh_close" $! Pi with "Hinh") as (Pi') "(Heq & >Hbor & Hinh)".
iMod ("Hclose" with "[HA HI Hinv Hdead Hinh Hcnt]") as "_".
{ iNext. rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
rewrite /lft_inv /lft_inv_dead. iRight. iSplit; last done.
iExists Pi'. iFrame. }
iModIntro. rewrite /raw_bor. iExists i. iFrame. iExists _. auto.
Qed.
End rebor.
theories/lifetime/model/reborrow.v
+ 171
− 85
View file @ 8602c269
From lrust.lifetime Require Export borrow.
From lrust.lifetime Require Import raw_reborrow accessors.
From lrust.lifetime Require Import borrow accessors.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
......@@ -10,96 +9,183 @@ Section reborrow.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
(* This lemma has no good place... and reborrowing is where we need it inside the model. *)
Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
(* Notice that taking lft_inv for both κ and κ' already implies
κ ≠ κ'. Still, it is probably more instructing to require
κ ⊂ κ' in this lemma (as opposed to just κ ⊆ κ'), and it
should not increase the burden on the user. *)
Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
↑borN ⊆ E →
let Iinv := (own_ilft_auth I ∗ ▷?q lft_inv A κ)%I in
κ ⊂ κ' →
lft_alive_in A κ' →
Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷?q lft_bor_alive κ' Pb -∗
▷?q lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
Proof.
iIntros (?) "#LFT Hb".
iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
- iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
iExists x. iApply ("Hclose" with "[] HΦ"). iIntros "!> ?"; eauto.
- iExists inhabitant. by iApply (bor_fake with "LFT").
iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
iMod (own_cnt_update with "Hn●") as "[Hn● H◯]".
{ apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
rewrite {1}/raw_bor /idx_bor_own /=.
iDestruct (own_bor_auth with "HI Hi") as %?.
assert (κ ⊆ κ') by (by apply strict_include).
iDestruct (lft_inv_alive_in with "Hκ") as "Hκ";
first by eauto using lft_alive_in_subseteq.
rewrite lft_inv_alive_unfold;
iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
iDestruct (own_bor_valid_2 with "HB● Hi")
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
{ by rewrite lookup_fmap HB. }
iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
{ eapply auth_update, singleton_local_update; last eapply
(exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
{ iNext. rewrite /lft_inv. iLeft.
iSplit; last by eauto using lft_alive_in_subseteq.
rewrite lft_inv_alive_unfold. iExists Pb', Pi'. iFrame "Hvs' Hinh'".
rewrite /lft_bor_alive. iExists (<[i:=Bor_rebor κ']>B).
rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame; auto. }
clear B HB Pb' Pi'.
rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
iMod (slice_insert_full with "HP Hbox")
as (j) "(HBj & #Hjslice & Hbox)"; first done.
iDestruct "HBj" as %HBj; move: HBj; rewrite lookup_fmap fmap_None=> HBj.
iMod (own_bor_update with "HB●") as "[HB● Hj]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HBj. }
iModIntro. iExists (P ∗ Pb)% I. rewrite /Iinv. iFrame "HI". iFrame.
iSplitL "Hj".
{ rewrite /raw_bor /idx_bor_own. iExists j. iFrame. iExists P.
rewrite -uPred.iff_refl. auto. }
iSplitL "Hbox HB● HB".
{ rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
by rewrite /bor_cnt. }
clear dependent Iinv I.
iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
iIntros (I) "Hinv [HP HPb] #Hκ†".
rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
rewrite lft_inv_alive_unfold.
iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
iDestruct (own_bor_valid_2 with "HB● Hi")
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
{ eapply auth_update, singleton_local_update,
(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.
{ by rewrite lookup_fmap HB. }
iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
rewrite /=. iDestruct "Hcnt" as "[% H1◯]".
iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
[$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
{ rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
iIntros (_). rewrite lft_inv_alive_unfold.
iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
{ rewrite /raw_bor /idx_bor_own /=. auto. }
iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
by iFrame.
Qed.
Lemma rebor E κ κ' P :
↑lftN ⊆ E →
lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Lemma raw_idx_bor_unnest E κ κ' i P :
↑lftN ⊆ E → κ ⊂ κ' →
lft_ctx -∗ slice borN i P -∗ raw_bor κ' (idx_bor_own 1 (κ, i))
={E}=∗ raw_bor κ' P.
Proof.
iIntros (? Hκκ') "#LFT #Hs Hraw".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iDestruct (raw_bor_inI with "HI Hraw") as %HI'.
rewrite (big_sepS_delete _ _ κ') ?elem_of_dom // [_ A κ']/lft_inv.
iDestruct "Hinv" as "[[[Hinvκ >%]|[Hinvκ >%]] Hinv]"; last first.
{ rewrite /lft_inv_dead. iDestruct "Hinvκ" as (Pi) "[Hbordead H]".
iMod (raw_bor_fake _ true with "Hbordead") as "[Hbordead $]";
first solve_ndisj.
iApply "Hclose". iExists _, _. iFrame.
rewrite (big_opS_delete _ (dom _ _) κ') ?elem_of_dom // /lft_inv /lft_inv_dead.
auto 10 with iFrame. }
rewrite {1}/raw_bor. iDestruct "Hraw" as (i') "[Hbor H]".
iDestruct "H" as (P') "[#HP' #Hs']".
rewrite lft_inv_alive_unfold /lft_bor_alive [in _ _ (κ', i')]/idx_bor_own.
iDestruct "Hinvκ" as (Pb Pi) "(Halive & Hvs & Hinh)".
iDestruct "Halive" as (B) "(Hbox & >H● & HB)".
iDestruct (own_bor_valid_2 with "H● Hbor")
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
iDestruct (raw_bor_inI _ _ P with "HI [Hidx]") as %HI;
first by rewrite /raw_bor; auto 10 with I.
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
first by rewrite elem_of_difference elem_of_dom not_elem_of_singleton;
eauto using strict_ne.
iMod (slice_delete_empty with "Hs' Hbox") as (Pb') "[#HeqPb' Hbox]";
[solve_ndisj|by apply lookup_insert|].
iMod (own_bor_update_2 with "H● Hbor") as "H●".
{ apply auth_update_dealloc, delete_singleton_local_update. apply _. }
iMod (raw_bor_unnest _ true with "[$HI $Hinvκ] Hidx Hs [Hbox H● HB] [Hvs]")
as (Pb'') "HH"; [solve_ndisj|done|done| | |].
{ rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
iExists (delete i' B). rewrite -fmap_delete. iFrame.
rewrite fmap_delete -insert_delete delete_insert ?lookup_delete //=. }
{ iNext. iApply (lft_vs_cons false with "[] Hvs"). iIntros "[$ [??]] !>". iNext.
iRewrite "HeqPb'". iFrame. by iApply "HP'". }
iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
iApply "Hclose". iExists _, _. iFrame.
rewrite (big_opS_delete _ (dom _ _) κ') ?elem_of_dom //.
iDestruct ("Hclose'" with "Hinvκ") as "$".
rewrite /lft_inv lft_inv_alive_unfold. auto 10 with iFrame.
Qed.
Lemma raw_rebor E κ κ' P :
↑lftN ⊆ E → κ ⊆ κ' →
lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
Proof.
iIntros (?) "#LFT #H⊑". rewrite {1}/bor; iDestruct 1 as (κ'') "[#H⊑' Hκ'']".
iMod (raw_rebor _ _ (κ' ⊓ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
{ apply gmultiset_union_subseteq_r. }
iModIntro. iSplitL "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κ''".
{ iApply lft_dead_or; auto. }
iModIntro. rewrite /bor. eauto.
iIntros (? Hκκ') "#LFT Hbor".
destruct (decide (κ = κ')) as [<-|Hκneq].
{ iFrame. iIntros "!> H†". by iApply raw_bor_fake'. }
assert (κ ⊂ κ') by (by apply strict_spec_alt).
rewrite [_ κ P]/raw_bor. iDestruct "Hbor" as (s) "[Hbor Hs]".
iDestruct "Hs" as (P') "[#HP'P #Hs]".
iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor Hinh]"; first done.
iSplitR "Hinh"; first last.
{ iIntros "!> #H†". iExists _. iMod ("Hinh" with "H†") as ">$". auto with iFrame. }
iApply (raw_bor_iff with "HP'P"). by iApply raw_idx_bor_unnest.
Qed.
Lemma bor_unnest E κ κ' P :
Lemma idx_bor_unnest E κ κ' i P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ⊓ κ'} P.
lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
Proof.
iIntros (?) "#LFT Hκ". rewrite {2}/bor.
iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
iMod (bor_sep with "LFT Hκ") as "[Hκ⊑ Hκ]"; first done.
rewrite {2}/bor; iDestruct "Hκ" as (κ0') "[#Hκ'⊑ Hκ]".
iMod (bor_acc_atomic with "LFT Hκ⊑") as "[[#Hκ⊑ Hclose]|[#H† Hclose]]"; first done; last first.
{ 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').
iMod (raw_rebor _ _ κ'' with "LFT Hκ") as "[Hκ _]"; first done.
{ apply gmultiset_union_subseteq_r. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iMod (ilft_create _ _ κ'' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
clear A I; rename A' into A; rename I' into I.
iDestruct (big_sepS_delete _ _ κ'' with "Hinv") as "[Hκ'' Hinv]";
first by apply elem_of_dom.
rewrite {1}/lft_inv; iDestruct "Hκ''" as "[[Hinv' >%]|[Hdead >Hdeadin]]"; last first.
{ iDestruct "Hdeadin" as %Hdeadin. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
iMod ("Hclose" with "[-]") as "_".
{ rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
iApply (big_sepS_delete _ _ κ''); first by apply elem_of_dom.
iNext; iFrame "Hinv". rewrite /lft_inv. iRight. iSplit; auto. }
iMod (fupd_intro_mask') as "Hclose"; last iModIntro; first solve_ndisj.
iNext. iMod "Hclose" as "_".
iApply (bor_fake with "LFT [>]"); first done.
iApply (lft_incl_dead with "[] H†"); first done.
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;
iDestruct "Hinv'" as (Pb Pi) "(Halive & Hvs & Hinh)".
rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(Hbox & >HB● & HB)".
iDestruct (own_bor_valid_2 with "HB● Hi")
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_delete_full _ _ true with "Hislice Hbox")
as (Pb') "(HP & #EQ & Hbox)"; first solve_ndisj.
{ by rewrite lookup_fmap HB. }
iDestruct ("HPP'" with "HP") as "HP".
iMod (own_bor_update_2 with "HB● Hi") as "HB●".
{ apply auth_update_dealloc, delete_singleton_local_update. apply _. }
iMod (fupd_intro_mask') as "Hclose'"; last iModIntro; first solve_ndisj.
iNext. iMod "Hclose'" as "_".
iAssert (lft_bor_alive κ'' Pb') with "[Hbox HB● HB]" as "Halive".
{ rewrite /lft_bor_alive. iExists (delete i B).
rewrite fmap_delete. iFrame "Hbox". iSplitL "HB●".
- rewrite /to_borUR fmap_delete. done.
- rewrite big_sepM_delete; last done. iDestruct "HB" as "[_ $]". }
iMod (raw_bor_unnest' _ false with "[$HI $Hinv] HP Halive [Hvs]") as (Pb'') "([HI Hinv] & HP & Halive & Hvs)";
[solve_ndisj|exact: gmultiset_union_subseteq_l|done| |].
{ (* TODO: Use iRewrite supporting contractive rewriting. *)
iApply (lft_vs_cons with "[]"); last done.
iIntros "[$ [Hbor HPb']]". iModIntro. iNext. iRewrite "EQ". iFrame. by iApply "HPP'". }
iMod ("Hclose" with "[-HP]") as "_".
{ iNext. simpl. rewrite /lfts_inv. iExists A, I. iFrame.
rewrite (big_sepS_delete _ (dom _ I) κ''); last by apply elem_of_dom.
iFrame. rewrite /lft_inv lft_inv_alive_unfold. iLeft.
iFrame "%". iExists Pb'', Pi. iFrame. }
iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
by iApply (lft_intersect_mono with "Hκ⊑").
iIntros (?) "#LFT #HP Hbor".
rewrite [(&{κ'}_)%I]/bor. iDestruct "Hbor" as (κ'0) "[#Hκ'κ'0 Hbor]".
destruct (decide (κ'0 = static)) as [->|Hκ'0].
{ iMod (bor_acc_strong with "LFT [Hbor] []") as (?) "(_ & Hbor & _)";
[done| |iApply (lft_tok_static 1)|].
- rewrite /bor. iExists static. iFrame. iApply lft_incl_refl.
- iDestruct "Hbor" as ">Hbor".
iApply bor_shorten; [|by rewrite bor_unfold_idx; auto].
iApply lft_intersect_incl_l. }
rewrite /idx_bor /bor. destruct i as [κ0 i].
iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
iMod (raw_rebor _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "[Hbor _]";
[done|by apply gmultiset_union_subseteq_r|].
iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
[done|by apply gmultiset_union_subset_l|].
iExists _. iDestruct (raw_bor_iff with "HPP' Hbor") as "$".
by iApply lft_intersect_mono.
Qed.
End reborrow.
theories/typing/borrow.v
+ 2
− 3
View file @ 8602c269
......@@ -113,9 +113,8 @@ Section borrow.
try by iMod (bor_persistent_tok with "LFT Hbor Htok") as "[>[] _]".
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
rewrite heap_mapsto_vec_singleton.
iApply (wp_step_fupd _ (⊤∖↑lftN) with "[Hbor]"); try done.
by iApply (bor_unnest with "LFT Hbor").
iApply wp_fupd. wp_read. iIntros "!> Hbor".
iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
iApply wp_fupd. wp_read.
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
iMod ("Hclose" with "Htok") as "($ & $)".
rewrite tctx_interp_singleton tctx_hasty_val' //.
......
theories/typing/lib/mutex/mutexguard.v
+ 3
− 4
View file @ 8602c269
......@@ -41,7 +41,7 @@ Section mguard.
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.[α⊓κ]
={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α⊓κ) tid (shift_loc l' 1) ∗ q.[α⊓κ]
|}%I.
Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed.
(* This is to a large extend copy-pasted from RWLock's write guard. *)
......@@ -219,9 +219,8 @@ Section code.
iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
iMod (bor_persistent_tok with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hclose2]"; first done.
wp_bind (!_)%E. iApply (wp_step_fupd with "[Hlm]");
[done| |by iApply (bor_unnest with "LFT Hlm")|]; first done.
wp_read. iIntros "Hlm !>". wp_let.
wp_bind (!_)%E. iMod (bor_unnest with "LFT Hlm") as "Hlm"; first done.
wp_read. wp_let. iMod "Hlm".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iMod ("Hclose2" with "H↦") as "[_ Hα]".
iMod ("Hclose1" with "Hα HL") as "HL".
......
theories/typing/lib/refcell/refmut.v
+ 1
− 1
View file @ 8602c269
......@@ -33,7 +33,7 @@ Section refmut.
∃ (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, F∖↑shrN}▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
Next Obligation.
iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
Qed.
......
theories/typing/lib/refcell/refmut_code.v
+ 2
− 3
View file @ 8602c269
......@@ -86,9 +86,8 @@ Section refmut_functions.
iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hαν". iClear "H".
rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
[done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
wp_read. iIntros "Hb !>". wp_let.
wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_let. iMod "Hb".
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]
......
theories/typing/lib/rwlock/rwlockwriteguard.v
+ 1
− 1
View file @ 8602c269
......@@ -29,7 +29,7 @@ Section rwlockwriteguard.
ty_shr κ tid l :=
∃ (l' : loc),
&frac{κ} (λ q, l↦∗{q} [ #l']) ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN∖↑lftN}▷=∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN}▷=∗
ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) ∗ q.[α ⊓ κ] |}%I.
Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
Next Obligation.
......
theories/typing/lib/rwlock/rwlockwriteguard_code.v
+ 2
− 3
View file @ 8602c269
......@@ -84,9 +84,8 @@ Section rwlockwriteguard_functions.
iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
[done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
wp_read. iIntros "Hb !>". wp_op. wp_let.
wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_op. wp_let. iMod "Hb".
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]
......
theories/typing/uniq_bor.v
+ 2
− 3
View file @ 8602c269
......@@ -18,7 +18,7 @@ Section uniq_bor.
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.[κ⊓κ']
={F, F∖↑shrN}▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ']
|}%I.
Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
......@@ -35,8 +35,7 @@ Section uniq_bor.
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 solve_ndisj.
iIntros "!# * % Htok". iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); try solve_ndisj.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
......
theories/typing/util.v
+ 11
− 6
View file @ 8602c269
......@@ -12,9 +12,12 @@ Section util.
TODO: Figure out a nice way to generalize that; the two proofs below are too
similar. *)
(* This is somewhat the general pattern here... but it doesn't seem easy to make
this usable in Coq, with the arbitrary quantifiers and things. Also, it actually works
not just for borrows but for anything that you can split into a timeless and a persistent part.
(* This is somewhat the general pattern here... but it doesn't seem
easy to make this usable in Coq, with the arbitrary quantifiers
and things. Also, it actually works not just for borrows but for
anything that you can split into a timeless and a persistent
part.
Lemma delay_borrow_step :
lfeE ⊆ N → (∀ x, PersistentP (Post x)) →
lft_ctx -∗ &{κ} P -∗
......@@ -32,7 +35,8 @@ Section util.
iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
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]"; first solve_ndisj.
iIntros "!> !# * % Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj.
{ rewrite bor_unfold_idx. eauto. }
......@@ -47,13 +51,14 @@ Section util.
lftE ⊆ N →
lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'} &{κ} l ↦∗: ty_own ty tid ={N}=∗
□ ∀ (F : coPset) (q : Qp),
⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN ∖ ↑lftN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
Proof.
iIntros (?) "#LFT #Hincl Hbor". rewrite bor_unfold_idx.
iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
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]"; first solve_ndisj.
iIntros "!> !# * % Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_unnest with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
{ iApply bor_unfold_idx. eauto. }
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment