ownership.v 3.21 KB
Newer Older
1
From iris.program_logic Require Export model.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

3
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
4
  uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]}  ).
5
Arguments ownI {_ _} _ _%I.
Ralf Jung's avatar
Ralf Jung committed
6
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_ownM (Res  (Excl σ) ).
7
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownM (Res   m).
8
Instance: Params (@ownI) 3.
9 10
Instance: Params (@ownP) 2.
Instance: Params (@ownG) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12
Typeclasses Opaque ownI ownG ownP.
13

Robbert Krebbers's avatar
Robbert Krebbers committed
14
Section ownership.
15
Context {Λ : language} {Σ : iFunctor}.
16 17 18 19
Implicit Types r : iRes Λ Σ.
Implicit Types σ : state Λ.
Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21

(* Invariants *)
22
Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Proof.
24
  intros n P Q HPQ. rewrite /ownI.
25
  apply uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
26
  by apply Next_contractive=> j ?; rewrite (HPQ j).
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Qed.
28 29
Global Instance ownI_persistent i P : PersistentP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31

(* physical state *)
32
Lemma ownP_twice σ1 σ2 : (ownP σ1  ownP σ2 : iProp Λ Σ)  False.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Proof.
34 35
  rewrite /ownP -uPred.ownM_op Res_op.
  by apply uPred.ownM_invalid; intros (_&?&_).
Robbert Krebbers's avatar
Robbert Krebbers committed
36
Qed.
37
Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ σ).
38
Proof. rewrite /ownP; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40

(* ghost state *)
41
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Proof. solve_proper. Qed.
43 44
Global Instance ownG_proper : Proper (() ==> ()) (@ownG Λ Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1  m2)  (ownG m1  ownG m2).
45
Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
46
Global Instance ownG_mono : Proper (flip () ==> ()) (@ownG Λ Σ).
47
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
48
Lemma ownG_valid m : ownG m   m.
49
Proof. rewrite /ownG uPred.ownM_valid res_validI /=; auto with I. Qed.
50
Lemma ownG_valid_r m : ownG m  (ownG m   m).
51
Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
52
Lemma ownG_empty : True  (ownG  : iProp Λ Σ).
53
Proof. apply uPred.ownM_empty. Qed.
54 55
Global Instance ownG_timeless m : Timeless m  TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
56 57
Global Instance ownG_persistent m : Persistent m  PersistentP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59

(* inversion lemmas *)
60
Lemma ownI_spec n r i P :
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  {n} r 
62
  (ownI i P) n r  wld r !! i {n} Some (to_agree (Next (iProp_unfold P))).
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Proof.
64
  intros (?&?&?). rewrite /ownI; uPred.unseal.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
66
  - intros [(P'&Hi&HP) _]; rewrite Hi.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68
    apply Some_dist, symmetry, agree_valid_includedN; last done.
    by apply map_lookup_validN with (wld r) i.
69
  - intros ?; split_and?; try apply cmra_unit_leastN; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Qed.
71
Lemma ownP_spec n r σ : {n} r  (ownP σ) n r  pst r  Excl σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73 74
  intros (?&?&?). rewrite /ownP; uPred.unseal.
  rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
75
  rewrite (timeless_iff n). naive_solver (apply cmra_unit_leastN).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
77
Lemma ownG_spec n r m : (ownG m) n r  m {n} gst r.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof.
79
  rewrite /ownG; uPred.unseal.
80
  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_unit_leastN).
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
Qed.
End ownership.