ownership.v 3.81 KB
Newer Older
1
From 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Lemma always_ownI i P : ( ownI i P)%I  ownI i P.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Proof.
30
  apply uPred.always_ownM.
31
  by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Qed.
33 34 35
Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
Proof. by rewrite /AlwaysStable always_ownI. Qed.
Lemma ownI_sep_dup i P : ownI i P  (ownI i P  ownI i P)%I.
36
Proof. apply (uPred.always_sep_dup _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38

(* physical state *)
39
Lemma ownP_twice σ1 σ2 : (ownP σ1  ownP σ2 : iProp Λ Σ)  False.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Proof.
41 42
  rewrite /ownP -uPred.ownM_op Res_op.
  by apply uPred.ownM_invalid; intros (_&?&_).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
Qed.
44
Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Proof. rewrite /ownP; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47

(* ghost state *)
48
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
49
Proof. solve_proper. Qed.
50
Global Instance ownG_proper : Proper (() ==> ()) (@ownG Λ Σ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Lemma ownG_op m1 m2 : ownG (m1  m2)  (ownG m1  ownG m2)%I.
52
Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
53 54
Global Instance ownG_mono : Proper (flip () ==> ()) (@ownG Λ Σ).
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
Lemma always_ownG_unit m : ( ownG (unit m))%I  ownG (unit m).
Proof.
57
  apply uPred.always_ownM.
58
  by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Qed.
60 61
Lemma always_ownG m : unit m  m  ( ownG m)%I  ownG m.
Proof. by intros <-; rewrite always_ownG_unit. Qed.
62 63
Lemma ownG_valid m : ownG m   m.
Proof.
64
  rewrite /ownG uPred.ownM_valid res_validI /=; auto with I.
65 66
Qed.
Lemma ownG_valid_r m : ownG m  (ownG m   m).
67
Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
68 69
Lemma ownG_empty : True  (ownG  : iProp Λ Σ).
Proof. apply uPred.ownM_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
Global Instance ownG_timeless m : Timeless m  TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
72 73
Global Instance ownG_unit_always_stable m : AlwaysStable (ownG (unit m)).
Proof. by rewrite /AlwaysStable always_ownG_unit. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75

(* inversion lemmas *)
76
Lemma ownI_spec n r i P :
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  {n} r 
78
  (ownI i P) n r  wld r !! i {n} Some (to_agree (Next (iProp_unfold P))).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof.
80 81
  intros (?&?&?). rewrite /ownI; uPred.unseal.
  rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
82
  - intros [(P'&Hi&HP) _]; rewrite Hi.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
    by apply Some_dist, symmetry, agree_valid_includedN,
      (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
85
  - intros ?; split_and?; try apply cmra_empty_leastN; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Qed.
87
Lemma ownP_spec n r σ : {n} r  (ownP σ) n r  pst r  Excl σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Proof.
89 90
  intros (?&?&?). rewrite /ownP; uPred.unseal.
  rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
91
  rewrite (timeless_iff n). naive_solver (apply cmra_empty_leastN).
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Qed.
93
Lemma ownG_spec n r m : (ownG m) n r  m {n} gst r.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
Proof.
95
  rewrite /ownG; uPred.unseal.
96
  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98
Qed.
End ownership.