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.
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
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 Λ Σ σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
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 Λ Σ).
Ralf Jung's avatar
Ralf Jung committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Ralf Jung's avatar
Ralf Jung committed
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 //.
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
80
  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_unit_leastN).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
Qed.
End ownership.