Library iris.program_logic.ownership
From iris.program_logic Require Export model.
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
(⧆ (uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅)))%I.
Arguments ownI {_ _} _ _%I.
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := (⧆ (uPred_ownM (Res ∅ (Excl' σ) ∅)))%I.
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := (⧆ (uPred_ownM (Res ∅ ∅ m)))%I.
Definition ownGl {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownMl (Res ∅ ∅ m).
Instance: Params (@ownI) 3.
Instance: Params (@ownP) 2.
Instance: Params (@ownG) 2.
Instance: Params (@ownGl) 2.
Typeclasses Opaque ownI ownG ownP.
Section ownership.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types r : iRes Λ Σ.
Implicit Types σ : state Λ.
Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
Proof.
intros n P Q HPQ. rewrite /ownI.
apply uPred.affine_ne, uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
by apply Next_contractive⇒ j ?; rewrite (HPQ j).
Qed.
Global Instance ownI_relevant i P : RelevantP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Global Instance ownI_affine i P : AffineP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ (False : iProp Λ Σ).
Proof.
rewrite /ownP uPred.sep_affine_1 -uPred.ownM_op Res_op.
rewrite uPred.ownM_invalid; eauto with I.
by intros (_&?&_).
Qed.
Global Instance ownP_affine σ : AffineP (@ownP Λ Σ σ).
Proof. rewrite /ownP. apply _. Qed.
Global Instance ownP_atimeless σ : ATimelessP (@ownP Λ Σ σ).
Proof. rewrite /ownP; apply _. Qed.
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Proof. solve_proper. Qed.
Global Instance ownG_affine m : AffineP (ownG m).
Proof. rewrite /ownG. apply _. Qed.
Global Instance ownG_proper : Proper ((≡) ==> (⊣⊢)) (@ownG Λ Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ⊣⊢ ownG m1 ★ ownG m2.
Proof. by rewrite /ownG -uPred.ownM_op'' Res_op !left_id. Qed.
Global Instance ownG_mono : Proper (flip (≼) ==> (⊢)) (@ownG Λ Σ).
Proof. move⇒a b [c H]. rewrite H ownG_op. eauto with typeclass_instances I. Qed.
Lemma ownG_valid m : ownG m ⊢ ⧆✓ m.
Proof. rewrite /ownG uPred.ownM_valid res_validI /= ?uPred.affine_and; auto with I. Qed.
Lemma ownG_valid_r m : ownG m ⊢ ownG m ★ ⧆✓ m.
Proof. apply (uPred.relevant_entails_r _ _), ownG_valid. Qed.
Lemma ownG_empty : Emp ⊢ (ownG ∅ : iProp Λ Σ).
Proof. apply: uPred.ownM_empty'. Qed.
Global Instance ownG_timeless m : Timeless m → ATimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_relevant m : Persistent m → RelevantP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownGl_ne n : Proper (dist n ==> dist n) (@ownGl Λ Σ).
Proof. solve_proper. Qed.
Global Instance ownGl_proper : Proper ((≡) ==> (⊣⊢)) (@ownGl Λ Σ) := ne_proper _.
Lemma ownGl_op m1 m2 : ownGl (m1 ⋅ m2) ⊣⊢ (ownGl m1 ★ ownGl m2).
Proof. by rewrite /ownGl -uPred.ownMl_op Res_op !left_id. Qed.
Lemma ownGl_valid_r m : ownGl m ⊢ (ownGl m ★ ⧆✓ m).
Proof. rewrite /ownGl {1}uPred.ownMl_valid res_validI /= ?uPred.affine_and; auto with I. Qed.
Lemma ownGl_empty : Emp ⊢ (ownGl ∅ : iProp Λ Σ).
Proof. by rewrite /ownGl uPred.ownMl_empty. Qed.
Global Instance ownGl_relevant m : Persistent m → RelevantP (ownGl m).
Proof. rewrite /ownGl; apply _. Qed.
Lemma ownI_spec n r r' i P :
✓{n} r →
✓{n} r' →
(ownI i P) n r r' ↔ wld r !! i ≡{n}≡ Some (to_agree (Next (iProp_unfold P))) ∧ r' ≡{n}≡ ∅.
Proof.
intros (?&?&?) (?&?&?). rewrite /ownI; uPred.unseal.
rewrite /uPred_holds/=/uPred_holds/=res_includedN/= singleton_includedN; split.
- intros [((P'&Hi&HP)&_) ?]; rewrite Hi.
split; auto. constructor; symmetry; apply agree_valid_includedN.
+ by apply lookup_validN_Some with (wld r) i.
+ by destruct HP as [?| ->].
- intros (?&?); split_and?; try apply ucmra_unit_leastN; eauto.
Qed.
Lemma ownP_spec n r r' σ : ✓{n} r → ✓{n} r' → (ownP σ) n r r' ↔ pst r ≡ Excl' σ ∧ r' ≡{n}≡ ∅.
Proof.
intros (?&?&?) (?&?&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (timeless_iff n). naive_solver (apply ucmra_unit_leastN).
Qed.
Lemma ownP_spec' n r r' σ : ✓{n} r → ✓{n} r' → (ownP σ) n r r' → pst r ≡ Excl' σ.
Proof.
intros (?&?&?) (?&?&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (timeless_iff n). naive_solver (apply cmra_unit_leastN).
Qed.
Lemma ownG_spec n r r' m : (ownG m) n r r' ↔ m ≼{n} gst r ∧ r' ≡{n}≡ ∅.
Proof.
rewrite /ownG; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN; naive_solver (apply ucmra_unit_leastN).
Qed.
Lemma ownGl_spec n r r' m : (ownGl m) n r r' ↔ Res ∅ ∅ m ≡{n}≡ r'.
Proof.
rewrite /ownGl; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds //=.
Qed.
End ownership.
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
(⧆ (uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅)))%I.
Arguments ownI {_ _} _ _%I.
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := (⧆ (uPred_ownM (Res ∅ (Excl' σ) ∅)))%I.
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := (⧆ (uPred_ownM (Res ∅ ∅ m)))%I.
Definition ownGl {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownMl (Res ∅ ∅ m).
Instance: Params (@ownI) 3.
Instance: Params (@ownP) 2.
Instance: Params (@ownG) 2.
Instance: Params (@ownGl) 2.
Typeclasses Opaque ownI ownG ownP.
Section ownership.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types r : iRes Λ Σ.
Implicit Types σ : state Λ.
Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
Proof.
intros n P Q HPQ. rewrite /ownI.
apply uPred.affine_ne, uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
by apply Next_contractive⇒ j ?; rewrite (HPQ j).
Qed.
Global Instance ownI_relevant i P : RelevantP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Global Instance ownI_affine i P : AffineP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ (False : iProp Λ Σ).
Proof.
rewrite /ownP uPred.sep_affine_1 -uPred.ownM_op Res_op.
rewrite uPred.ownM_invalid; eauto with I.
by intros (_&?&_).
Qed.
Global Instance ownP_affine σ : AffineP (@ownP Λ Σ σ).
Proof. rewrite /ownP. apply _. Qed.
Global Instance ownP_atimeless σ : ATimelessP (@ownP Λ Σ σ).
Proof. rewrite /ownP; apply _. Qed.
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Proof. solve_proper. Qed.
Global Instance ownG_affine m : AffineP (ownG m).
Proof. rewrite /ownG. apply _. Qed.
Global Instance ownG_proper : Proper ((≡) ==> (⊣⊢)) (@ownG Λ Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ⊣⊢ ownG m1 ★ ownG m2.
Proof. by rewrite /ownG -uPred.ownM_op'' Res_op !left_id. Qed.
Global Instance ownG_mono : Proper (flip (≼) ==> (⊢)) (@ownG Λ Σ).
Proof. move⇒a b [c H]. rewrite H ownG_op. eauto with typeclass_instances I. Qed.
Lemma ownG_valid m : ownG m ⊢ ⧆✓ m.
Proof. rewrite /ownG uPred.ownM_valid res_validI /= ?uPred.affine_and; auto with I. Qed.
Lemma ownG_valid_r m : ownG m ⊢ ownG m ★ ⧆✓ m.
Proof. apply (uPred.relevant_entails_r _ _), ownG_valid. Qed.
Lemma ownG_empty : Emp ⊢ (ownG ∅ : iProp Λ Σ).
Proof. apply: uPred.ownM_empty'. Qed.
Global Instance ownG_timeless m : Timeless m → ATimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_relevant m : Persistent m → RelevantP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownGl_ne n : Proper (dist n ==> dist n) (@ownGl Λ Σ).
Proof. solve_proper. Qed.
Global Instance ownGl_proper : Proper ((≡) ==> (⊣⊢)) (@ownGl Λ Σ) := ne_proper _.
Lemma ownGl_op m1 m2 : ownGl (m1 ⋅ m2) ⊣⊢ (ownGl m1 ★ ownGl m2).
Proof. by rewrite /ownGl -uPred.ownMl_op Res_op !left_id. Qed.
Lemma ownGl_valid_r m : ownGl m ⊢ (ownGl m ★ ⧆✓ m).
Proof. rewrite /ownGl {1}uPred.ownMl_valid res_validI /= ?uPred.affine_and; auto with I. Qed.
Lemma ownGl_empty : Emp ⊢ (ownGl ∅ : iProp Λ Σ).
Proof. by rewrite /ownGl uPred.ownMl_empty. Qed.
Global Instance ownGl_relevant m : Persistent m → RelevantP (ownGl m).
Proof. rewrite /ownGl; apply _. Qed.
Lemma ownI_spec n r r' i P :
✓{n} r →
✓{n} r' →
(ownI i P) n r r' ↔ wld r !! i ≡{n}≡ Some (to_agree (Next (iProp_unfold P))) ∧ r' ≡{n}≡ ∅.
Proof.
intros (?&?&?) (?&?&?). rewrite /ownI; uPred.unseal.
rewrite /uPred_holds/=/uPred_holds/=res_includedN/= singleton_includedN; split.
- intros [((P'&Hi&HP)&_) ?]; rewrite Hi.
split; auto. constructor; symmetry; apply agree_valid_includedN.
+ by apply lookup_validN_Some with (wld r) i.
+ by destruct HP as [?| ->].
- intros (?&?); split_and?; try apply ucmra_unit_leastN; eauto.
Qed.
Lemma ownP_spec n r r' σ : ✓{n} r → ✓{n} r' → (ownP σ) n r r' ↔ pst r ≡ Excl' σ ∧ r' ≡{n}≡ ∅.
Proof.
intros (?&?&?) (?&?&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (timeless_iff n). naive_solver (apply ucmra_unit_leastN).
Qed.
Lemma ownP_spec' n r r' σ : ✓{n} r → ✓{n} r' → (ownP σ) n r r' → pst r ≡ Excl' σ.
Proof.
intros (?&?&?) (?&?&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (timeless_iff n). naive_solver (apply cmra_unit_leastN).
Qed.
Lemma ownG_spec n r r' m : (ownG m) n r r' ↔ m ≼{n} gst r ∧ r' ≡{n}≡ ∅.
Proof.
rewrite /ownG; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN; naive_solver (apply ucmra_unit_leastN).
Qed.
Lemma ownGl_spec n r r' m : (ownGl m) n r r' ↔ Res ∅ ∅ m ≡{n}≡ r'.
Proof.
rewrite /ownGl; uPred.unseal.
rewrite /uPred_holds /= /uPred_holds //=.
Qed.
End ownership.