Skip to content
Snippets Groups Projects
Commit d0f2c02e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Split lifetime logic into multiple files.

parent 7209ca51
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 5
− 20
View file @ d0f2c02e
-Q theories lrust -Q theories lrust
-Q iris-enabled iris -Q iris-enabled iris
theories/adequacy.v theories/lifetime/definitions.v
theories/derived.v theories/lifetime/derived.v
theories/heap.v theories/lifetime/creation.v
theories/lang.v theories/lifetime/primitive.v
theories/lifting.v theories/lifetime/todo.v
theories/memcpy.v
theories/notation.v
theories/proofmode.v
theories/races.v
theories/tactics.v
theories/wp_tactics.v
theories/lifetime.v
theories/tl_borrow.v
theories/shr_borrow.v
theories/frac_borrow.v
theories/type.v
theories/type_incl.v
theories/perm.v
theories/perm_incl.v
theories/typing.v
theories/lifetime.v → theories/lifetime/creation.v
+ 294
− 0
View file @ d0f2c02e
From lrust.lifetime Require Export primitive.
From iris.algebra Require Import csum auth frac gmap dec_agree gset. From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.prelude Require Import gmultiset.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Import uPred.
Definition lftN : namespace := nroot .@ "lft".
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 := ∅.
Inductive bor_state :=
| Bor_in
| Bor_open (q : frac)
| Bor_rebor (κ : lft).
Instance bor_state_eq_dec : EqDecision bor_state.
Proof. solve_decision. Defined.
Definition bor_filled (s : bor_state) : bool :=
match s with Bor_in => true | _ => false end.
Definition lft_stateR := csumR fracR unitR.
Definition to_lft_stateR (b : bool) : lft_stateR :=
if b then Cinl 1%Qp else Cinr ().
Record lft_names := LftNames {
bor_name : gname;
cnt_name : gname;
inh_name : gname
}.
Instance lft_names_eq_dec : EqDecision lft_names.
Proof. solve_decision. Defined.
Class lftG Σ := LftG {
lft_box :> boxG Σ;
alft_inG :> inG Σ (authR (gmapUR atomic_lft lft_stateR));
alft_name : gname;
ilft_inG :> inG Σ (authR (gmapUR lft (dec_agreeR lft_names)));
ilft_name : gname;
lft_bor_box :>
inG Σ (authR (gmapUR slice_name (prodR fracR (dec_agreeR bor_state))));
lft_cnt_inG :> inG Σ (authR natUR);
lft_inh_box :> inG Σ (authR (gset_disjUR slice_name));
}.
Section defs.
Context `{invG Σ, lftG Σ}.
Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
Definition lft_dead (κ : lft) : iProp Σ :=
(∃ Λ, ⌜Λ ∈ κ⌝ ∗ own alft_name (◯ {[ Λ := Cinr () ]}))%I.
Definition own_alft_auth (A : gmap atomic_lft bool) : iProp Σ :=
own alft_name (● (to_lft_stateR <$> A)).
Definition own_ilft_auth (I : gmap lft lft_names) : iProp Σ :=
own ilft_name (● (DecAgree <$> I)).
Definition own_bor (κ : lft)
(x : auth (gmap slice_name (frac * dec_agree bor_state))) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own (bor_name γs) x)%I.
Definition own_cnt (κ : lft) (x : auth nat) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own (cnt_name γs) x)%I.
Definition own_inh (κ : lft) (x : auth (gset_disj slice_name)) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own (inh_name γs) x)%I.
Definition bor_cnt (κ : lft) (s : bor_state) : iProp Σ :=
match s with
| Bor_in => True
| Bor_open q => lft_tok q κ
| Bor_rebor κ' => ⌜κ ⊂ κ'⌝ ∗ own_cnt κ' (◯ 1)
end%I.
Definition lft_bor_alive (κ : lft) (P : iProp Σ) : iProp Σ :=
(∃ B : gmap slice_name bor_state,
box borN (bor_filled <$> B) P ∗
own_bor κ (● ((1%Qp,) ∘ DecAgree <$> B)) ∗
[∗ map] s ∈ B, bor_cnt κ s)%I.
Definition lft_bor_dead (κ : lft) : iProp Σ :=
(∃ (B: gset slice_name) (P : iProp Σ),
own_bor κ (● to_gmap (1%Qp, DecAgree Bor_in) B) ∗
box borN (to_gmap false B) P)%I.
Definition lft_inh (κ : lft) (s : bool) (P : iProp Σ) : iProp Σ :=
(∃ E : gset slice_name,
own_inh κ (● GSet E) ∗
box inhN (to_gmap s E) P)%I.
Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
(I : gmap lft lft_names) : iProp Σ :=
(lft_bor_dead κ ∗
own_ilft_auth I ∗
[∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
(P Q : iProp Σ) : iProp Σ :=
(∃ n : nat,
own_cnt κ (● n) ∗
∀ I : gmap lft lft_names,
lft_vs_inv_go κ lft_inv_alive I -∗ ▷ P -∗ lft_dead κ
={⊤∖↑mgmtN}=∗
lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Q ∗ own_cnt κ (◯ n))%I.
Definition lft_inv_alive_go (κ : lft) Section creation.
(lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ) : iProp Σ :=
(∃ P Q,
lft_bor_alive κ P ∗
lft_vs_go κ lft_inv_alive P Q ∗
lft_inh κ false Q)%I.
Definition lft_inv_alive (κ : lft) : iProp Σ :=
Fix_F _ lft_inv_alive_go (gmultiset_wf κ).
Definition lft_vs_inv (κ : lft) (I : gmap lft lft_names) : iProp Σ :=
lft_vs_inv_go κ (λ κ' _, lft_inv_alive κ') I.
Definition lft_vs (κ : lft) (P Q : iProp Σ) : iProp Σ :=
lft_vs_go κ (λ κ' _, lft_inv_alive κ') P Q.
Definition lft_inv_dead (κ : lft) : iProp Σ :=
(∃ P,
lft_bor_dead κ ∗
own_cnt κ (● 0) ∗
lft_inh κ true P)%I.
Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
∀ Λ, Λ ∈ κ → A !! Λ = Some true.
Definition lft_dead_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
∃ Λ, Λ ∈ κ ∧ A !! Λ = Some false.
Definition lft_inv (A : gmap atomic_lft bool) (κ : lft) : iProp Σ :=
(lft_inv_alive κ ∗ ⌜lft_alive_in A κ⌝ ∨
lft_inv_dead κ ∗ ⌜lft_dead_in A κ⌝)%I.
Definition lfts_inv : iProp Σ :=
(∃ (A : gmap atomic_lft bool) (I : gmap lft lft_names),
own_alft_auth A ∗
own_ilft_auth I ∗
[∗ set] κ ∈ dom _ I, lft_inv A κ)%I.
Definition lft_ctx : iProp Σ := inv mgmtN lfts_inv.
Definition lft_incl (κ κ' : lft) : iProp Σ :=
(□ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
(lft_dead κ' ={↑lftN}=∗ lft_dead κ)))%I.
Definition bor_idx := (lft * slice_name)%type.
Definition idx_bor_own (q : frac) (i : bor_idx) : iProp Σ :=
own_bor (i.1) (◯ {[ i.2 := (q,DecAgree Bor_in) ]}).
Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
(lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
Definition raw_bor (i : bor_idx) (P : iProp Σ) : iProp Σ :=
(idx_bor_own 1 i ∗ slice borN (i.2) P)%I.
Definition bor (κ : lft) (P : iProp Σ) : iProp Σ :=
(∃ i, lft_incl κ (i.1) ∗ raw_bor i P)%I.
End defs.
Instance: Params (@lft_bor_alive) 4.
Instance: Params (@lft_inh) 5.
Instance: Params (@lft_vs) 4.
Instance: Params (@idx_bor) 5.
Instance: Params (@raw_bor) 4.
Instance: Params (@bor) 4.
Notation "q .[ κ ]" := (lft_tok q κ)
(format "q .[ κ ]", at level 0) : uPred_scope.
Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
Notation "&{ κ } P" := (bor κ P)
(format "&{ κ } P", at level 20, right associativity) : uPred_scope.
Notation "&{ κ , i } P" := (idx_bor κ i P)
(format "&{ κ , i } P", at level 20, right associativity) : uPred_scope.
Infix "⊑" := lft_incl (at level 70) : uPred_scope.
Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
idx_bor_own idx_bor raw_bor bor.
Section theorems.
Context `{invG Σ, lftG Σ}. Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft. Implicit Types κ : lft.
(* Unfolding lemmas *)
Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
Proof.
intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
by apply forall_ne=> Hκ.
Qed.
Lemma lft_vs_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) P P' Q Q' n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
P ≡{n}≡ P' → Q ≡{n}≡ Q' →
lft_vs_go κ f P Q ≡{n}≡ lft_vs_go κ f' P' Q'.
Proof.
intros Hf HP HQ. apply exist_ne=> n'.
apply sep_ne, forall_ne=> // I. rewrite lft_vs_inv_go_ne //. solve_proper.
Qed.
Lemma lft_inv_alive_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_inv_alive_go κ f ≡{n}≡ lft_inv_alive_go κ f'.
Proof.
intros Hf. apply exist_ne=> P; apply exist_ne=> Q. by rewrite lft_vs_go_ne.
Qed.
Lemma lft_inv_alive_unfold κ :
lft_inv_alive κ ⊣⊢ ∃ P Q, lft_bor_alive κ P ∗ lft_vs κ P Q ∗ lft_inh κ false Q.
Proof.
apply equiv_dist=> n. rewrite /lft_inv_alive -Fix_F_eq.
apply lft_inv_alive_go_ne=> κ' Hκ.
apply (Fix_F_proper _ (λ _, dist n)); auto using lft_inv_alive_go_ne.
Qed.
Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
lft_vs_inv κ I ⊣⊢ lft_bor_dead κ ∗
own_ilft_auth I ∗
[∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
Proof.
rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
Qed.
Lemma lft_vs_unfold κ P Q :
lft_vs κ P Q ⊣⊢ ∃ n : nat,
own_cnt κ (● n) ∗
∀ I : gmap lft lft_names,
lft_vs_inv κ I -∗ ▷ P -∗ lft_dead κ ={⊤∖↑mgmtN}=∗
lft_vs_inv κ I ∗ ▷ Q ∗ own_cnt κ (◯ n).
Proof. done. Qed.
Global Instance lft_bor_alive_ne κ n : Proper (dist n ==> dist n) (lft_bor_alive κ).
Proof. solve_proper. Qed.
Global Instance lft_bor_alive_proper κ : Proper ((≡) ==> (≡)) (lft_bor_alive κ).
Proof. apply (ne_proper _). Qed.
Global Instance lft_inh_ne κ s n : Proper (dist n ==> dist n) (lft_inh κ s).
Proof. solve_proper. Qed.
Global Instance lft_inh_proper κ s : Proper ((≡) ==> (≡)) (lft_inh κ s).
Proof. apply (ne_proper _). Qed.
Global Instance lft_vs_ne κ n :
Proper (dist n ==> dist n ==> dist n) (lft_vs κ).
Proof. intros P P' HP Q Q' HQ. by apply lft_vs_go_ne. Qed.
Global Instance lft_vs_proper κ : Proper ((≡) ==> (≡) ==> (≡)) (lft_vs κ).
Proof. apply (ne_proper_2 _). Qed.
Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
Proof. solve_proper. Qed.
Global Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
Proof. apply (ne_proper _). Qed.
Global Instance raw_bor_ne i n : Proper (dist n ==> dist n) (raw_bor i).
Proof. solve_proper. Qed.
Global Instance raw_bor_proper i : Proper ((≡) ==> (≡)) (raw_bor i).
Proof. apply (ne_proper _). Qed.
Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
Proof. solve_proper. Qed.
Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
Proof. apply (ne_proper _). Qed.
(*** PersistentP and TimelessP instances *)
Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
Proof. rewrite /lft_tok. apply _. Qed.
Global Instance lft_dead_persistent κ : PersistentP [†κ].
Proof. rewrite /lft_dead. apply _. Qed.
Global Instance lft_dead_timeless κ : PersistentP [†κ].
Proof. rewrite /lft_tok. apply _. Qed.
Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
Proof. rewrite /lft_incl. apply _. Qed.
Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
Proof. rewrite /idx_bor. apply _. Qed.
Global Instance idx_borrow_own_timeless q i : TimelessP (idx_bor_own q i).
Proof. rewrite /idx_bor_own. apply _. Qed.
Global Instance lft_ctx_persistent : PersistentP lft_ctx.
Proof. rewrite /lft_ctx. apply _. Qed.
(** Alive and dead *)
Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
Proof.
refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
(dom (gset atomic_lft) κ))));
rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
Qed.
Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
Proof.
refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
(dom (gset atomic_lft) κ))));
rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
Qed.
Lemma lft_alive_or_dead_in A κ :
(∃ Λ, Λ ∈ κ ∧ A !! Λ = None) ∨ (lft_alive_in A κ ∨ lft_dead_in A κ).
Proof.
rewrite /lft_alive_in /lft_dead_in.
destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
right; left. intros Λ HΛ%gmultiset_elem_of_dom.
move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
Qed.
Lemma lft_alive_and_dead_in A κ : lft_alive_in A κ → lft_dead_in A κ → False.
Proof. intros Halive (Λ&HΛ&?). generalize (Halive _ HΛ). naive_solver. Qed.
Lemma lft_alive_in_subseteq A κ κ' :
lft_alive_in A κ → κ' ⊆ κ → lft_alive_in A κ'.
Proof. intros Halive ? Λ ?. by eapply Halive, gmultiset_elem_of_subseteq. Qed.
Lemma lft_alive_in_insert A κ Λ b :
A !! Λ = None → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
Proof.
intros HΛ Halive Λ' HΛ'.
assert (Λ ≠ Λ') by (intros ->; move:(Halive _ HΛ'); by rewrite HΛ).
rewrite lookup_insert_ne; eauto.
Qed.
Lemma lft_alive_in_insert_false A κ Λ b :
Λ ∉ κ → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
Proof.
intros HΛ Halive Λ' HΛ'.
rewrite lookup_insert_ne; last (by intros ->); auto.
Qed.
Lemma lft_dead_in_insert A κ Λ b :
A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
Proof.
intros HΛ (Λ'&?&HΛ').
assert (Λ ≠ Λ') by (intros ->; move:HΛ'; by rewrite HΛ).
exists Λ'. by rewrite lookup_insert_ne.
Qed.
Lemma lft_dead_in_insert_false A κ Λ :
lft_dead_in A κ → lft_dead_in (<[Λ:=false]> A) κ.
Proof.
intros (Λ'&?&HΛ'). destruct (decide (Λ = Λ')) as [<-|].
- exists Λ. by rewrite lookup_insert.
- exists Λ'. by rewrite lookup_insert_ne.
Qed.
Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
Proof. exists Λ. by rewrite lookup_insert. Qed.
(** Silly stuff *)
Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
own_ilft_auth I ⊢
own ilft_name (◯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
as %[[? [??]]%singleton_included _]%auth_valid_discrete_2.
simplify_map_eq; simplify_option_eq; eauto.
Qed.
Lemma own_bor_auth I κ x : own_ilft_auth I ⊢ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
Qed.
Lemma own_bor_op κ x y : own_bor κ (x ⋅ y) ⊣⊢ own_bor κ x ∗ own_bor κ y.
Proof.
iSplit.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Lemma own_bor_valid κ x : own_bor κ x ⊢ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_bor_valid_2 κ x y : own_bor κ x ⊢ own_bor κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
Qed.
Lemma own_cnt_auth I κ x : own_ilft_auth I ⊢ own_cnt κ x -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
Qed.
Lemma own_cnt_op κ x y : own_cnt κ (x ⋅ y) ⊣⊢ own_cnt κ x ∗ own_cnt κ y.
Proof.
iSplit.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
Lemma own_cnt_valid κ x : own_cnt κ x ⊢ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_cnt_valid_2 κ x y : own_cnt κ x ⊢ own_cnt κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
Qed.
Lemma own_cnt_update_2 κ x1 x2 y :
x1 ⋅ x2 ~~> y → own_cnt κ x1 ⊢ own_cnt κ x2 ==∗ own_cnt κ y.
Proof.
intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
Qed.
Lemma own_inh_auth I κ x : own_ilft_auth I ⊢ own_inh κ x -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
Qed.
Lemma own_inh_op κ x y : own_inh κ (x ⋅ y) ⊣⊢ own_inh κ x ∗ own_inh κ y.
Proof.
iSplit.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Lemma own_inh_valid κ x : own_inh κ x ⊢ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_inh_valid_2 κ x y : own_inh κ x ⊢ own_inh κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
Qed.
Lemma lft_inv_alive_twice κ : lft_inv_alive κ ⊢ lft_inv_alive κ -∗ False.
Proof.
rewrite lft_inv_alive_unfold /lft_inh.
iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
iDestruct "Hinh" as (E) "[HE _]"; iDestruct "Hinh'" as (E') "[HE' _]".
by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
Qed.
(** Basic rules about lifetimes *)
Lemma lft_tok_op 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].
Proof.
rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
Qed.
Lemma lft_tok_frac_op κ q q' : (q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
Proof.
rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper=> Λ _.
by rewrite -own_op -auth_frag_op op_singleton.
Qed.
Lemma lft_tok_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
Proof. by rewrite -lft_tok_frac_op Qp_div_2. Qed.
Lemma lft_tok_dead_own q κ : q.[κ] ⊢ [† κ] -∗ False.
Proof.
rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
iDestruct (own_valid_2 with "H H'") as %Hvalid.
move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
Qed.
Lemma lft_tok_static q : True ⊢ q.[static].
Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
Lemma lft_dead_static : [† static] ⊢ False.
Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
(* Lifetime creation *) (* Lifetime creation *)
Lemma lft_inh_kill E κ Q : Lemma lft_inh_kill E κ Q :
↑inhN ⊆ E → ↑inhN ⊆ E →
...@@ -768,180 +291,4 @@ Proof. ...@@ -768,180 +291,4 @@ Proof.
contradict H7. apply elem_of_dom. set_solver +HI Hκ. contradict H7. apply elem_of_dom. set_solver +HI Hκ.
+ iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false. + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
Qed. Qed.
End creation.
(** Basic borrows *)
Lemma bor_create E κ P :
↑lftN ⊆ E →
lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
Proof. Admitted.
Lemma bor_fake E κ P :
↑lftN ⊆ E →
lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
Proof.
iIntros (?) "#?". (* iDestruct 1 as (Λ) "[% ?]". *)
Admitted.
Lemma bor_sep E κ P Q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
Proof.
iIntros (?) "#? Hbor".
Admitted.
Lemma bor_combine E κ P Q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
Proof. Admitted.
Lemma bor_acc_strong E q κ P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
Proof. Admitted.
Lemma bor_acc_atomic_strong E κ P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} P ={E,E∖↑lftN}=∗
(▷ P ∗ ∀ Q, ▷ Q ∗ ▷ ([†κ] -∗ ▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
Proof. Admitted.
Lemma bor_reborrow' E κ κ' P :
↑lftN ⊆ E → κ ⊆ κ' →
lft_ctx ⊢ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
Proof. Admitted.
Lemma bor_unnest E κ κ' P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
Proof. Admitted.
(** Indexed borrow *)
Lemma idx_bor_acc E q κ i P :
↑lftN ⊆ E →
lft_ctx ⊢ idx_bor κ i P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
Proof. Admitted.
Lemma idx_bor_atomic_acc E q κ i P :
↑lftN ⊆ E →
lft_ctx ⊢ idx_bor κ i P -∗ idx_bor_own q i ={E,E∖↑lftN}=∗
▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i) ∨
[†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
Proof. Admitted.
Lemma idx_bor_shorten κ κ' i P :
κ ⊑ κ' ⊢ idx_bor κ' i P -∗ idx_bor κ i P.
Proof. Admitted.
(*** Derived lemmas *)
Lemma bor_acc E q κ P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
Proof.
iIntros (?) "#LFT HP Htok".
iMod (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
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_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]"; first done.
- iDestruct "HΦ" as (x) "HΦ". iExists x.
iApply "Hclose". iIntros "{$HΦ} !> _ ?"; eauto.
- iMod "Hclose" as "_". iExists inhabitant. by iApply (bor_fake with "LFT").
Qed.
Lemma bor_or E κ P Q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
Proof.
iIntros (?) "#LFT H". rewrite uPred.or_alt.
iMod (bor_exists with "LFT H") as ([]) "H"; auto.
Qed.
Lemma bor_persistent `{!PersistentP P} E κ q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
Proof.
iIntros (?) "#LFT Hb Htok".
iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
by iMod ("Hob" with "HP") as "[_$]".
Qed.
Lemma lft_incl_acc E κ κ' q :
↑lftN ⊆ E →
κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Proof.
rewrite /lft_incl.
iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
iMod ("H" with "* Hq") as (q') "[Hq' Hclose]". iExists q'.
iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
Qed.
Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
Proof.
rewrite /lft_incl.
iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
Qed.
Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
Proof. (*
iIntros (->%gmultiset_union_difference) "!#". iSplitR.
- iIntros (q). rewrite -lft_tok_op. iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
- iIntros "? !>". iApply lft_dead_or. auto.
Qed. *) Admitted.
Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
Proof. by apply lft_le_incl. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
Proof.
rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
- iIntros (q) "Hκ".
iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
iExists q''. iIntros "{$Hκ''} !> Hκ''".
iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
- iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
Qed.
Lemma bor_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
Proof.
iIntros "Hκκ' H". rewrite /bor. iDestruct "H" as (i) "[??]".
iExists i. iFrame. (*
Check idx_bor_shorten.
by iApply (idx_bor_shorten with "Hκκ'").
Qed. *) Admitted.
Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ∪ κ''.
Proof. (*
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'']".
destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
iExists qq. rewrite -lft_tok_op !lft_tok_frac_op.
iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
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. *) Admitted.
Lemma lft_incl_static κ : True ⊢ κ ⊑ static.
Proof.
iIntros "!#". iSplitR.
- iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
Lemma reborrow E P κ κ' :
↑lftN ⊆ E →
lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Proof.
iIntros (?) "#LFT #H⊑ HP". iMod (bor_reborrow' with "LFT HP") as "[Hκ' H∋]".
done. (* by exists κ'.
iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
Qed.
*)
Admitted.
theories/lifetime/definitions.v 0 → 100644
+ 192
− 0
View file @ d0f2c02e
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.prelude Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes.
From iris.base_logic Require Import big_op.
Definition lftN : namespace := nroot .@ "lft".
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 := ∅.
Inductive bor_state :=
| Bor_in
| Bor_open (q : frac)
| Bor_rebor (κ : lft).
Instance bor_state_eq_dec : EqDecision bor_state.
Proof. solve_decision. Defined.
Definition bor_filled (s : bor_state) : bool :=
match s with Bor_in => true | _ => false end.
Definition lft_stateR := csumR fracR unitR.
Definition to_lft_stateR (b : bool) : lft_stateR :=
if b then Cinl 1%Qp else Cinr ().
Record lft_names := LftNames {
bor_name : gname;
cnt_name : gname;
inh_name : gname
}.
Instance lft_names_eq_dec : EqDecision lft_names.
Proof. solve_decision. Defined.
Class lftG Σ := LftG {
lft_box :> boxG Σ;
alft_inG :> inG Σ (authR (gmapUR atomic_lft lft_stateR));
alft_name : gname;
ilft_inG :> inG Σ (authR (gmapUR lft (dec_agreeR lft_names)));
ilft_name : gname;
lft_bor_box :>
inG Σ (authR (gmapUR slice_name (prodR fracR (dec_agreeR bor_state))));
lft_cnt_inG :> inG Σ (authR natUR);
lft_inh_box :> inG Σ (authR (gset_disjUR slice_name));
}.
Section defs.
Context `{invG Σ, lftG Σ}.
Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
Definition lft_dead (κ : lft) : iProp Σ :=
(∃ Λ, ⌜Λ ∈ κ⌝ ∗ own alft_name (◯ {[ Λ := Cinr () ]}))%I.
Definition own_alft_auth (A : gmap atomic_lft bool) : iProp Σ :=
own alft_name (● (to_lft_stateR <$> A)).
Definition own_ilft_auth (I : gmap lft lft_names) : iProp Σ :=
own ilft_name (● (DecAgree <$> I)).
Definition own_bor (κ : lft)
(x : auth (gmap slice_name (frac * dec_agree bor_state))) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own (bor_name γs) x)%I.
Definition own_cnt (κ : lft) (x : auth nat) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own (cnt_name γs) x)%I.
Definition own_inh (κ : lft) (x : auth (gset_disj slice_name)) : iProp Σ :=
(∃ γs,
own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
own (inh_name γs) x)%I.
Definition bor_cnt (κ : lft) (s : bor_state) : iProp Σ :=
match s with
| Bor_in => True
| Bor_open q => lft_tok q κ
| Bor_rebor κ' => ⌜κ ⊂ κ'⌝ ∗ own_cnt κ' (◯ 1)
end%I.
Definition lft_bor_alive (κ : lft) (P : iProp Σ) : iProp Σ :=
(∃ B : gmap slice_name bor_state,
box borN (bor_filled <$> B) P ∗
own_bor κ (● ((1%Qp,) ∘ DecAgree <$> B)) ∗
[∗ map] s ∈ B, bor_cnt κ s)%I.
Definition lft_bor_dead (κ : lft) : iProp Σ :=
(∃ (B: gset slice_name) (P : iProp Σ),
own_bor κ (● to_gmap (1%Qp, DecAgree Bor_in) B) ∗
box borN (to_gmap false B) P)%I.
Definition lft_inh (κ : lft) (s : bool) (P : iProp Σ) : iProp Σ :=
(∃ E : gset slice_name,
own_inh κ (● GSet E) ∗
box inhN (to_gmap s E) P)%I.
Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
(I : gmap lft lft_names) : iProp Σ :=
(lft_bor_dead κ ∗
own_ilft_auth I ∗
[∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
(P Q : iProp Σ) : iProp Σ :=
(∃ n : nat,
own_cnt κ (● n) ∗
∀ I : gmap lft lft_names,
lft_vs_inv_go κ lft_inv_alive I -∗ ▷ P -∗ lft_dead κ
={⊤∖↑mgmtN}=∗
lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Q ∗ own_cnt κ (◯ n))%I.
Definition lft_inv_alive_go (κ : lft)
(lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ) : iProp Σ :=
(∃ P Q,
lft_bor_alive κ P ∗
lft_vs_go κ lft_inv_alive P Q ∗
lft_inh κ false Q)%I.
Definition lft_inv_alive (κ : lft) : iProp Σ :=
Fix_F _ lft_inv_alive_go (gmultiset_wf κ).
Definition lft_vs_inv (κ : lft) (I : gmap lft lft_names) : iProp Σ :=
lft_vs_inv_go κ (λ κ' _, lft_inv_alive κ') I.
Definition lft_vs (κ : lft) (P Q : iProp Σ) : iProp Σ :=
lft_vs_go κ (λ κ' _, lft_inv_alive κ') P Q.
Definition lft_inv_dead (κ : lft) : iProp Σ :=
(∃ P,
lft_bor_dead κ ∗
own_cnt κ (● 0) ∗
lft_inh κ true P)%I.
Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
∀ Λ, Λ ∈ κ → A !! Λ = Some true.
Definition lft_dead_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
∃ Λ, Λ ∈ κ ∧ A !! Λ = Some false.
Definition lft_inv (A : gmap atomic_lft bool) (κ : lft) : iProp Σ :=
(lft_inv_alive κ ∗ ⌜lft_alive_in A κ⌝ ∨
lft_inv_dead κ ∗ ⌜lft_dead_in A κ⌝)%I.
Definition lfts_inv : iProp Σ :=
(∃ (A : gmap atomic_lft bool) (I : gmap lft lft_names),
own_alft_auth A ∗
own_ilft_auth I ∗
[∗ set] κ ∈ dom _ I, lft_inv A κ)%I.
Definition lft_ctx : iProp Σ := inv mgmtN lfts_inv.
Definition lft_incl (κ κ' : lft) : iProp Σ :=
(□ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
(lft_dead κ' ={↑lftN}=∗ lft_dead κ)))%I.
Definition bor_idx := (lft * slice_name)%type.
Definition idx_bor_own (q : frac) (i : bor_idx) : iProp Σ :=
own_bor (i.1) (◯ {[ i.2 := (q,DecAgree Bor_in) ]}).
Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
(lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
Definition raw_bor (i : bor_idx) (P : iProp Σ) : iProp Σ :=
(idx_bor_own 1 i ∗ slice borN (i.2) P)%I.
Definition bor (κ : lft) (P : iProp Σ) : iProp Σ :=
(∃ i, lft_incl κ (i.1) ∗ raw_bor i P)%I.
End defs.
Instance: Params (@lft_bor_alive) 4.
Instance: Params (@lft_inh) 5.
Instance: Params (@lft_vs) 4.
Instance: Params (@idx_bor) 5.
Instance: Params (@raw_bor) 4.
Instance: Params (@bor) 4.
Notation "q .[ κ ]" := (lft_tok q κ)
(format "q .[ κ ]", at level 0) : uPred_scope.
Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
Notation "&{ κ } P" := (bor κ P)
(format "&{ κ } P", at level 20, right associativity) : uPred_scope.
Notation "&{ κ , i } P" := (idx_bor κ i P)
(format "&{ κ , i } P", at level 20, right associativity) : uPred_scope.
Infix "⊑" := lft_incl (at level 70) : uPred_scope.
Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
idx_bor_own idx_bor raw_bor bor.
theories/lifetime/derived.v 0 → 100644
+ 125
− 0
View file @ d0f2c02e
From lrust.lifetime Require Export primitive todo.
From iris.proofmode Require Import tactics.
Section derived.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
(*** Derived lemmas *)
Lemma bor_acc E q κ P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
Proof.
iIntros (?) "#LFT HP Htok".
iMod (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
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_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]"; first done.
- iDestruct "HΦ" as (x) "HΦ". iExists x.
iApply "Hclose". iIntros "{$HΦ} !> _ ?"; eauto.
- iMod "Hclose" as "_". iExists inhabitant. by iApply (bor_fake with "LFT").
Qed.
Lemma bor_or E κ P Q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
Proof.
iIntros (?) "#LFT H". rewrite uPred.or_alt.
iMod (bor_exists with "LFT H") as ([]) "H"; auto.
Qed.
Lemma bor_persistent `{!PersistentP P} E κ q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
Proof.
iIntros (?) "#LFT Hb Htok".
iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
by iMod ("Hob" with "HP") as "[_$]".
Qed.
Lemma lft_incl_acc E κ κ' q :
↑lftN ⊆ E →
κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Proof.
rewrite /lft_incl.
iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
iMod ("H" with "* Hq") as (q') "[Hq' Hclose]". iExists q'.
iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
Qed.
Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
Proof.
rewrite /lft_incl.
iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
Qed.
Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
Proof. (*
iIntros (->%gmultiset_union_difference) "!#". iSplitR.
- iIntros (q). rewrite -lft_tok_op. iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
- iIntros "? !>". iApply lft_dead_or. auto.
Qed. *) Admitted.
Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
Proof. by apply lft_le_incl. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
Proof.
rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
- iIntros (q) "Hκ".
iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
iExists q''. iIntros "{$Hκ''} !> Hκ''".
iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
- iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
Qed.
Lemma bor_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
Proof.
iIntros "Hκκ' H". rewrite /bor. iDestruct "H" as (i) "[??]".
iExists i. iFrame. (*
Check idx_bor_shorten.
by iApply (idx_bor_shorten with "Hκκ'").
Qed. *) Admitted.
Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ∪ κ''.
Proof. (*
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'']".
destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
iExists qq. rewrite -lft_tok_op !lft_tok_frac_op.
iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
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. *) Admitted.
Lemma lft_incl_static κ : True ⊢ κ ⊑ static.
Proof.
iIntros "!#". iSplitR.
- iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
Lemma reborrow E P κ κ' :
↑lftN ⊆ E →
lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Proof.
iIntros (?) "#LFT #H⊑ HP". iMod (bor_reborrow' with "LFT HP") as "[Hκ' H∋]".
done. (* by exists κ'.
iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
Qed.
*)
Admitted.
End derived.
theories/lifetime/primitive.v 0 → 100644
+ 298
− 0
View file @ d0f2c02e
From lrust.lifetime Require Export definitions.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
Import uPred.
Section primitive.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
(* Unfolding lemmas *)
Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
Proof.
intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
by apply forall_ne=> Hκ.
Qed.
Lemma lft_vs_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) P P' Q Q' n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
P ≡{n}≡ P' → Q ≡{n}≡ Q' →
lft_vs_go κ f P Q ≡{n}≡ lft_vs_go κ f' P' Q'.
Proof.
intros Hf HP HQ. apply exist_ne=> n'.
apply sep_ne, forall_ne=> // I. rewrite lft_vs_inv_go_ne //. solve_proper.
Qed.
Lemma lft_inv_alive_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_inv_alive_go κ f ≡{n}≡ lft_inv_alive_go κ f'.
Proof.
intros Hf. apply exist_ne=> P; apply exist_ne=> Q. by rewrite lft_vs_go_ne.
Qed.
Lemma lft_inv_alive_unfold κ :
lft_inv_alive κ ⊣⊢ ∃ P Q, lft_bor_alive κ P ∗ lft_vs κ P Q ∗ lft_inh κ false Q.
Proof.
apply equiv_dist=> n. rewrite /lft_inv_alive -Fix_F_eq.
apply lft_inv_alive_go_ne=> κ' Hκ.
apply (Fix_F_proper _ (λ _, dist n)); auto using lft_inv_alive_go_ne.
Qed.
Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
lft_vs_inv κ I ⊣⊢ lft_bor_dead κ ∗
own_ilft_auth I ∗
[∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
Proof.
rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
Qed.
Lemma lft_vs_unfold κ P Q :
lft_vs κ P Q ⊣⊢ ∃ n : nat,
own_cnt κ (● n) ∗
∀ I : gmap lft lft_names,
lft_vs_inv κ I -∗ ▷ P -∗ lft_dead κ ={⊤∖↑mgmtN}=∗
lft_vs_inv κ I ∗ ▷ Q ∗ own_cnt κ (◯ n).
Proof. done. Qed.
Global Instance lft_bor_alive_ne κ n : Proper (dist n ==> dist n) (lft_bor_alive κ).
Proof. solve_proper. Qed.
Global Instance lft_bor_alive_proper κ : Proper ((≡) ==> (≡)) (lft_bor_alive κ).
Proof. apply (ne_proper _). Qed.
Global Instance lft_inh_ne κ s n : Proper (dist n ==> dist n) (lft_inh κ s).
Proof. solve_proper. Qed.
Global Instance lft_inh_proper κ s : Proper ((≡) ==> (≡)) (lft_inh κ s).
Proof. apply (ne_proper _). Qed.
Global Instance lft_vs_ne κ n :
Proper (dist n ==> dist n ==> dist n) (lft_vs κ).
Proof. intros P P' HP Q Q' HQ. by apply lft_vs_go_ne. Qed.
Global Instance lft_vs_proper κ : Proper ((≡) ==> (≡) ==> (≡)) (lft_vs κ).
Proof. apply (ne_proper_2 _). Qed.
Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
Proof. solve_proper. Qed.
Global Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
Proof. apply (ne_proper _). Qed.
Global Instance raw_bor_ne i n : Proper (dist n ==> dist n) (raw_bor i).
Proof. solve_proper. Qed.
Global Instance raw_bor_proper i : Proper ((≡) ==> (≡)) (raw_bor i).
Proof. apply (ne_proper _). Qed.
Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
Proof. solve_proper. Qed.
Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
Proof. apply (ne_proper _). Qed.
(*** PersistentP and TimelessP instances *)
Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
Proof. rewrite /lft_tok. apply _. Qed.
Global Instance lft_dead_persistent κ : PersistentP [†κ].
Proof. rewrite /lft_dead. apply _. Qed.
Global Instance lft_dead_timeless κ : PersistentP [†κ].
Proof. rewrite /lft_tok. apply _. Qed.
Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
Proof. rewrite /lft_incl. apply _. Qed.
Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
Proof. rewrite /idx_bor. apply _. Qed.
Global Instance idx_borrow_own_timeless q i : TimelessP (idx_bor_own q i).
Proof. rewrite /idx_bor_own. apply _. Qed.
Global Instance lft_ctx_persistent : PersistentP lft_ctx.
Proof. rewrite /lft_ctx. apply _. Qed.
(** Alive and dead *)
Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
Proof.
refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
(dom (gset atomic_lft) κ))));
rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
Qed.
Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
Proof.
refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
(dom (gset atomic_lft) κ))));
rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
Qed.
Lemma lft_alive_or_dead_in A κ :
(∃ Λ, Λ ∈ κ ∧ A !! Λ = None) ∨ (lft_alive_in A κ ∨ lft_dead_in A κ).
Proof.
rewrite /lft_alive_in /lft_dead_in.
destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
right; left. intros Λ HΛ%gmultiset_elem_of_dom.
move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
Qed.
Lemma lft_alive_and_dead_in A κ : lft_alive_in A κ → lft_dead_in A κ → False.
Proof. intros Halive (Λ&HΛ&?). generalize (Halive _ HΛ). naive_solver. Qed.
Lemma lft_alive_in_subseteq A κ κ' :
lft_alive_in A κ → κ' ⊆ κ → lft_alive_in A κ'.
Proof. intros Halive ? Λ ?. by eapply Halive, gmultiset_elem_of_subseteq. Qed.
Lemma lft_alive_in_insert A κ Λ b :
A !! Λ = None → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
Proof.
intros HΛ Halive Λ' HΛ'.
assert (Λ ≠ Λ') by (intros ->; move:(Halive _ HΛ'); by rewrite HΛ).
rewrite lookup_insert_ne; eauto.
Qed.
Lemma lft_alive_in_insert_false A κ Λ b :
Λ ∉ κ → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
Proof.
intros HΛ Halive Λ' HΛ'.
rewrite lookup_insert_ne; last (by intros ->); auto.
Qed.
Lemma lft_dead_in_insert A κ Λ b :
A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
Proof.
intros HΛ (Λ'&?&HΛ').
assert (Λ ≠ Λ') by (intros ->; move:HΛ'; by rewrite HΛ).
exists Λ'. by rewrite lookup_insert_ne.
Qed.
Lemma lft_dead_in_insert_false A κ Λ :
lft_dead_in A κ → lft_dead_in (<[Λ:=false]> A) κ.
Proof.
intros (Λ'&?&HΛ'). destruct (decide (Λ = Λ')) as [<-|].
- exists Λ. by rewrite lookup_insert.
- exists Λ'. by rewrite lookup_insert_ne.
Qed.
Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
Proof. exists Λ. by rewrite lookup_insert. Qed.
(** Silly stuff *)
Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
own_ilft_auth I ⊢
own ilft_name (◯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
as %[[? [??]]%singleton_included _]%auth_valid_discrete_2.
simplify_map_eq; simplify_option_eq; eauto.
Qed.
Lemma own_bor_auth I κ x : own_ilft_auth I ⊢ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
Qed.
Lemma own_bor_op κ x y : own_bor κ (x ⋅ y) ⊣⊢ own_bor κ x ∗ own_bor κ y.
Proof.
iSplit.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Lemma own_bor_valid κ x : own_bor κ x ⊢ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_bor_valid_2 κ x y : own_bor κ x ⊢ own_bor κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
Qed.
Lemma own_cnt_auth I κ x : own_ilft_auth I ⊢ own_cnt κ x -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
Qed.
Lemma own_cnt_op κ x y : own_cnt κ (x ⋅ y) ⊣⊢ own_cnt κ x ∗ own_cnt κ y.
Proof.
iSplit.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
Lemma own_cnt_valid κ x : own_cnt κ x ⊢ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_cnt_valid_2 κ x y : own_cnt κ x ⊢ own_cnt κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
Qed.
Lemma own_cnt_update_2 κ x1 x2 y :
x1 ⋅ x2 ~~> y → own_cnt κ x1 ⊢ own_cnt κ x2 ==∗ own_cnt κ y.
Proof.
intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
Qed.
Lemma own_inh_auth I κ x : own_ilft_auth I ⊢ own_inh κ x -∗ ⌜is_Some (I !! κ)⌝.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
Qed.
Lemma own_inh_op κ x y : own_inh κ (x ⋅ y) ⊣⊢ own_inh κ x ∗ own_inh κ y.
Proof.
iSplit.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Lemma own_inh_valid κ x : own_inh κ x ⊢ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_inh_valid_2 κ x y : own_inh κ x ⊢ own_inh κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
Qed.
Lemma lft_inv_alive_twice κ : lft_inv_alive κ ⊢ lft_inv_alive κ -∗ False.
Proof.
rewrite lft_inv_alive_unfold /lft_inh.
iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
iDestruct "Hinh" as (E) "[HE _]"; iDestruct "Hinh'" as (E') "[HE' _]".
by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
Qed.
(** Basic rules about lifetimes *)
Lemma lft_tok_op 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].
Proof.
rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
Qed.
Lemma lft_tok_frac_op κ q q' : (q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
Proof.
rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper=> Λ _.
by rewrite -own_op -auth_frag_op op_singleton.
Qed.
Lemma lft_tok_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
Proof. by rewrite -lft_tok_frac_op Qp_div_2. Qed.
Lemma lft_tok_dead_own q κ : q.[κ] ⊢ [† κ] -∗ False.
Proof.
rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
iDestruct (own_valid_2 with "H H'") as %Hvalid.
move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
Qed.
Lemma lft_tok_static q : True ⊢ q.[static].
Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
Lemma lft_dead_static : [† static] ⊢ False.
Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
End primitive.
theories/lifetime/todo.v 0 → 100644
+ 63
− 0
View file @ d0f2c02e
From lrust.lifetime Require Export definitions.
Section todo.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
(** Basic borrows *)
Lemma bor_create E κ P :
↑lftN ⊆ E →
lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
Proof. Admitted.
Lemma bor_fake E κ P :
↑lftN ⊆ E →
lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
Proof.
Admitted.
Lemma bor_sep E κ P Q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
Proof.
Admitted.
Lemma bor_combine E κ P Q :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
Proof. Admitted.
Lemma bor_acc_strong E q κ P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
Proof. Admitted.
Lemma bor_acc_atomic_strong E κ P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ} P ={E,E∖↑lftN}=∗
(▷ P ∗ ∀ Q, ▷ Q ∗ ▷ ([†κ] -∗ ▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
Proof. Admitted.
Lemma bor_reborrow' E κ κ' P :
↑lftN ⊆ E → κ ⊆ κ' →
lft_ctx ⊢ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
Proof. Admitted.
Lemma bor_unnest E κ κ' P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
Proof. Admitted.
(** Indexed borrow *)
Lemma idx_bor_acc E q κ i P :
↑lftN ⊆ E →
lft_ctx ⊢ idx_bor κ i P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
Proof. Admitted.
Lemma idx_bor_atomic_acc E q κ i P :
↑lftN ⊆ E →
lft_ctx ⊢ idx_bor κ i P -∗ idx_bor_own q i ={E,E∖↑lftN}=∗
▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i) ∨
[†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
Proof. Admitted.
Lemma idx_bor_shorten κ κ' i P :
κ ⊑ κ' ⊢ idx_bor κ' i P -∗ idx_bor κ i P.
Proof. Admitted.
End todo.
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment