ghost_ownership.v 6.23 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
(** 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
7
individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
8 9 10 11 12 13 14 15 16 17 18 19 20 21
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55
Lemma own_mono γ a1 a2 : a2  a1  own γ a1  own γ a2.
Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed.

56 57
Global Instance own_cmra_homomorphism : CMRAHomomorphism (own γ).
Proof. split. apply _. apply own_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
Global Instance own_mono' γ : Proper (flip () ==> ()) (@own Σ A _ γ).
Proof. intros a1 a2. apply own_mono. Qed.
60

61
Lemma own_valid γ a : own γ a   a.
62
Proof.
63
  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
64
  rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
65
  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
66
  (* implicit arguments differ a bit *)
67
  by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
68
Qed.
69 70 71 72 73
Lemma own_valid_2 γ a1 a2 : own γ a1  own γ a2   (a1  a2).
Proof. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1  own γ a2  own γ a3   (a1  a2  a3).
Proof. by rewrite -!own_op assoc own_valid. Qed.

74
Lemma own_valid_r γ a : own γ a  own γ a   a.
75
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
76
Lemma own_valid_l γ a : own γ a   a  own γ a.
77
Proof. by rewrite comm -own_valid_r. Qed.
78

79
Global Instance own_timeless γ a : Timeless a  TimelessP (own γ a).
80
Proof. rewrite !own_eq /own_def; apply _. Qed.
81
Global Instance own_core_persistent γ a : Persistent a  PersistentP (own γ a).
82
Proof. rewrite !own_eq /own_def; apply _. Qed.
83

84
(** ** Allocation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
(* 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. *)
87 88
Lemma own_alloc_strong a (G : gset gname) :
   a  True =r=>  γ,  (γ  G)  own γ a.
89
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  intros Ha.
91
  rewrite -(rvs_mono ( m,  ( γ, γ  G  m = iRes_singleton γ a)  uPred_ownM m)%I).
92 93
  - rewrite ownM_empty.
    eapply rvs_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i));
94
      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
95
      naive_solver.
96 97
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
    by rewrite !own_eq /own_def -(exist_intro γ) pure_equiv // left_id.
98
Qed.
99
Lemma own_alloc a :  a  True =r=>  γ, own γ a.
100
Proof.
101 102
  intros Ha. rewrite (own_alloc_strong a ) //; [].
  apply rvs_mono, exist_mono=>?. eauto with I.
103
Qed.
104

105
(** ** Frame preserving updates *)
106
Lemma own_updateP P γ a : a ~~>: P  own γ a =r=>  a',  P a'  own γ a'.
107
Proof.
108
  intros Ha. rewrite !own_eq.
109
  rewrite -(rvs_mono ( m,  ( a', m = iRes_singleton γ a'  P a')  uPred_ownM m)%I).
110
  - eapply rvs_ownM_updateP, iprod_singleton_updateP;
111
      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
112
    naive_solver.
113 114
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
115 116
Qed.

117
Lemma own_update γ a a' : a ~~> a'  own γ a =r=> own γ a'.
118
Proof.
119
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
120
  by apply rvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
121
Qed.
122 123 124 125 126 127
Lemma own_update_2 γ a1 a2 a' :
  a1  a2 ~~> a'  own γ a1  own γ a2 =r=> own γ a'.
Proof. intros. rewrite -own_op. by apply own_update. Qed.
Lemma own_update_3 γ a1 a2 a3 a' :
  a1  a2  a3 ~~> a'  own γ a1  own γ a2  own γ a3 =r=> own γ a'.
Proof. intros. rewrite -!own_op assoc. by apply own_update. Qed.
128
End global.
129

130
Arguments own_valid {_ _} [_] _ _.
131 132
Arguments own_valid_2 {_ _} [_] _ _ _.
Arguments own_valid_3 {_ _} [_] _ _ _ _.
133 134 135 136
Arguments own_valid_l {_ _} [_] _ _.
Arguments own_valid_r {_ _} [_] _ _.
Arguments own_updateP {_ _} [_] _ _ _ _.
Arguments own_update {_ _} [_] _ _ _ _.
137 138
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
139

140
Lemma own_empty `{inG Σ (A:ucmraT)} γ : True =r=> own γ .
141
Proof.
142 143
  rewrite ownM_empty !own_eq /own_def.
  apply rvs_ownM_update, iprod_singleton_update_empty.
144
  apply (alloc_unit_singleton_update (cmra_transport inG_prf )); last done.
145 146
  - apply cmra_transport_valid, ucmra_unit_valid.
  - intros x; destruct inG_prf. by rewrite left_id.
147
Qed.