ghost_ownership.v 5.26 KB
Newer Older
1
From iris.program_logic Require Export model.
2
From iris.algebra Require Import iprod gmap.
3
4
Import uPred.

5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
[Σ]. This class is similar to the [subG] class, but written down in terms of
individual CMRAs instead of lists of CMRA functors. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) :=
  InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) }.
Arguments inG_id {_ _} _.

Lemma subG_inG Σ (F : gFunctor) : subG F Σ  inG Σ (F (iPreProp Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.

(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
  iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4.

22
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
23
  uPred_ownM (iRes_singleton γ a).
24
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
25
Definition own {Σ A i} := proj1_sig own_aux Σ A i.
26
Definition own_eq : @own = @own_def := proj2_sig own_aux.
27
Instance: Params (@own) 4.
28
Typeclasses Opaque own.
29

30
(** * Properties about ghost ownership *)
31
Section global.
32
Context `{i : inG Σ A}.
33
34
Implicit Types a : A.

35
36
37
38
39
40
41
42
43
44
45
(** ** Properties of [iRes_singleton] *)
Global Instance iRes_singleton_ne γ n :
  Proper (dist n ==> dist n) (@iRes_singleton Σ A _ γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma iRes_singleton_op γ a1 a2 :
  iRes_singleton γ (a1  a2)  iRes_singleton γ a1  iRes_singleton γ a2.
Proof.
  by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
Qed.

(** ** Properties of [own] *)
46
Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Σ A _ γ).
47
Proof. rewrite !own_eq. solve_proper. Qed.
48
Global Instance own_proper γ :
49
  Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
50

51
Lemma own_op γ a1 a2 : own γ (a1  a2)  own γ a1  own γ a2.
52
Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
53
Global Instance own_mono γ : Proper (flip () ==> ()) (@own Σ A _ γ).
54
Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
55
Lemma own_valid γ a : own γ a   a.
56
Proof.
57
  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
58
  rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
59
  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
60
  (* implicit arguments differ a bit *)
61
  by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
62
Qed.
63
Lemma own_valid_r γ a : own γ a  own γ a   a.
64
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
65
Lemma own_valid_l γ a : own γ a   a  own γ a.
66
Proof. by rewrite comm -own_valid_r. Qed.
67
Global Instance own_timeless γ a : Timeless a  TimelessP (own γ a).
68
Proof. rewrite !own_eq /own_def; apply _. Qed.
69
Global Instance own_core_persistent γ a : Persistent a  PersistentP (own γ a).
70
Proof. rewrite !own_eq /own_def; apply _. Qed.
71

72
(** ** Allocation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
   assertion. However, the map_updateP_alloc does not suffice to show this. *)
75
76
Lemma own_alloc_strong a (G : gset gname) :
   a  True =r=>  γ,  (γ  G)  own γ a.
77
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  intros Ha.
79
  rewrite -(rvs_mono ( m,  ( γ, γ  G  m = iRes_singleton γ a)  uPred_ownM m)%I).
80
81
  - rewrite ownM_empty.
    eapply rvs_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i));
82
      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
83
      naive_solver.
84
85
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
    by rewrite !own_eq /own_def -(exist_intro γ) pure_equiv // left_id.
86
Qed.
87
Lemma own_alloc a :  a  True =r=>  γ, own γ a.
88
Proof.
89
90
  intros Ha. rewrite (own_alloc_strong a ) //; [].
  apply rvs_mono, exist_mono=>?. eauto with I.
91
Qed.
92

93
(** ** Frame preserving updates *)
94
Lemma own_updateP P γ a : a ~~>: P  own γ a =r=>  a',  P a'  own γ a'.
95
Proof.
96
  intros Ha. rewrite !own_eq.
97
  rewrite -(rvs_mono ( m,  ( a', m = iRes_singleton γ a'  P a')  uPred_ownM m)%I).
98
  - eapply rvs_ownM_updateP, iprod_singleton_updateP;
99
      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
100
    naive_solver.
101
102
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
103
104
Qed.

105
Lemma own_update γ a a' : a ~~> a'  own γ a =r=> own γ a'.
106
Proof.
107
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
108
  by apply rvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
109
Qed.
110
End global.
111

112
113
114
115
116
Arguments own_valid {_ _} [_] _ _.
Arguments own_valid_l {_ _} [_] _ _.
Arguments own_valid_r {_ _} [_] _ _.
Arguments own_updateP {_ _} [_] _ _ _ _.
Arguments own_update {_ _} [_] _ _ _ _.
117

118
Lemma own_empty `{inG Σ (A:ucmraT)} γ : True =r=> own γ .
119
Proof.
120
121
  rewrite ownM_empty !own_eq /own_def.
  apply rvs_ownM_update, iprod_singleton_update_empty.
122
  apply (alloc_unit_singleton_update (cmra_transport inG_prf )); last done.
123
124
  - apply cmra_transport_valid, ucmra_unit_valid.
  - intros x; destruct inG_prf. by rewrite left_id.
125
Qed.