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

3
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
4
  uPred_own (Res {[ i  to_agree (Later (iProp_unfold P)) ]}  ).
5
Arguments ownI {_ _} _ _%I.
6
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res  (Excl σ) ).
7
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_own (Res   (Some 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 16 17 18 19
Context {Λ : language} {Σ : iFunctor}.
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 inv_contractive i : Contractive (@ownI Λ Σ i).
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25
Proof.
  intros n P Q HPQ.
  apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
26
  by unfold ownI; rewrite HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Qed.
28
Lemma always_inv i P : ( ownI i P)%I  ownI i P.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Proof.
30 31
  apply uPred.always_own.
  by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Qed.
33
Global Instance inv_always_stable i P : AlwaysStable (ownI i P).
34
Proof. by rewrite /AlwaysStable always_inv. Qed.
35
Lemma inv_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 41 42 43
Proof.
  rewrite /ownP -uPred.own_op Res_op.
  by apply uPred.own_invalid; intros (_&?&_).
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. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
50
Global Instance ownG_proper : Proper (() ==> ()) (@ownG Λ Σ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54
Lemma ownG_op m1 m2 : ownG (m1  m2)  (ownG m1  ownG m2)%I.
Proof. by rewrite /ownG -uPred.own_op Res_op !(left_id _ _). Qed.
Lemma always_ownG_unit m : ( ownG (unit m))%I  ownG (unit m).
Proof.
55
  apply uPred.always_own.
56
  by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idempotent m).
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58 59
Qed.
Lemma ownG_valid m : (ownG m)  ( m).
Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
60
Lemma ownG_valid_r m : (ownG m)  (ownG m   m).
61
Proof. apply (uPred.always_entails_r' _ _), ownG_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62 63
Global Instance ownG_timeless m : Timeless m  TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67

(* inversion lemmas *)
Lemma inv_spec r n i P :
  {n} r 
68
  (ownI i P) n r  wld r !! i ={n}= Some (to_agree (Later (iProp_unfold P))).
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71 72 73
Proof.
  intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
  * intros [(P'&Hi&HP) _]; rewrite Hi.
    by apply Some_dist, symmetry, agree_valid_includedN,
      (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
74
  * intros ?; split_ands; try apply cmra_empty_leastN; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
76 77 78
Lemma ownP_spec r n σ : {n} r  (ownP σ) n r  pst r ={n}= Excl σ.
Proof.
  intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
79
  naive_solver (apply cmra_empty_leastN).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Qed.
81
Lemma ownG_spec r n m : (ownG m) n r  Some m {n} gst r.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
83
  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85
Qed.
End ownership.