ghost_ownership.v 4.49 KB
Newer Older
1
2
3
4
From iris.prelude Require Export functions.
From iris.algebra Require Export iprod.
From iris.program_logic Require Export pviewshifts global_functor.
From iris.program_logic Require Import ownership.
5
6
Import uPred.

Ralf Jung's avatar
Ralf Jung committed
7
Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
8
9
10
  ownG (to_globalF γ a).
Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5.
11
12
Typeclasses Opaque to_globalF own.

13
(** Properties about ghost ownership *)
14
Section global.
15
Context `{i : inG Λ Σ A}.
16
17
Implicit Types a : A.

18
(** * Transport empty *)
19
Instance inG_empty `{Empty A} :
20
  Empty (Σ inG_id (iPreProp Λ (globalF Σ))) := cmra_transport inG_prf .
21
Instance inG_empty_spec `{Empty A} :
Ralf Jung's avatar
Ralf Jung committed
22
  CMRAUnit A  CMRAUnit (Σ inG_id (iPreProp Λ (globalF Σ))).
23
24
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
25
  - apply cmra_transport_valid, cmra_unit_valid.
26
27
  - intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
  - apply _.
28
29
30
Qed.

(** * Properties of own *)
31
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Proof. solve_proper. Qed.
33
Global Instance own_proper γ : Proper (() ==> ()) (own γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
34

35
Lemma own_op γ a1 a2 : own γ (a1  a2)  (own γ a1  own γ a2)%I.
36
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
37
Global Instance own_mono γ : Proper (flip () ==> ()) (own γ).
Ralf Jung's avatar
Ralf Jung committed
38
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
Ralf Jung's avatar
Ralf Jung committed
39
40
41
42
Lemma always_own_core γ a : ( own γ (core a))%I  own γ (core a).
Proof. by rewrite /own -to_globalF_core always_ownG_core. Qed.
Lemma always_own γ a : core a  a  ( own γ a)%I  own γ a.
Proof. by intros <-; rewrite always_own_core. Qed.
43
Lemma own_valid γ a : own γ a   a.
44
Proof.
45
  rewrite /own ownG_valid /to_globalF.
46
  rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
47
  rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
48
49
  (* implicit arguments differ a bit *)
  by trans ( cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf.
50
Qed.
51
Lemma own_valid_r γ a : own γ a  (own γ a   a).
52
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
53
Lemma own_valid_l γ a : own γ a  ( a  own γ a).
54
Proof. by rewrite comm -own_valid_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
55
Lemma own_empty `{CMRAUnit A} γ : True  own γ .
56
57
58
59
Proof.
  rewrite ownG_empty /own. apply equiv_spec, ownG_proper.
  (* FIXME: rewrite to_globalF_empty. *)
Abort.
60
Global Instance own_timeless γ a : Timeless a  TimelessP (own γ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Proof. unfold own; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
62
63
Global Instance own_core_always_stable γ a : AlwaysStable (own γ (core a)).
Proof. by rewrite /AlwaysStable always_own_core. Qed.
64

Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
(* 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. *)
67
Lemma own_alloc_strong a E (G : gset gname) :
68
   a  True  (|={E}=>  γ, (γ  G)  own γ a).
69
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
  intros Ha.
71
  rewrite -(pvs_mono _ _ ( m,  ( γ, γ  G  m = to_globalF γ a)  ownG m)%I).
72
  - rewrite ownG_empty. eapply pvs_ownG_updateP, (iprod_singleton_updateP_empty inG_id);
73
74
      first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
      naive_solver.
75
  - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
76
    by rewrite -(exist_intro γ) const_equiv // left_id.
77
Qed.
78
Lemma own_alloc a E :  a  True  (|={E}=>  γ, own γ a).
79
80
81
Proof.
  intros Ha. rewrite (own_alloc_strong a E ) //; []. apply pvs_mono.
  apply exist_mono=>?. eauto with I.
82
Qed.
83

84
Lemma own_updateP P γ a E :
85
  a ~~>: P  own γ a  (|={E}=>  a',  P a'  own γ a').
86
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  intros Ha.
88
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalF γ a'  P a')  ownG m)%I).
89
  - eapply pvs_ownG_updateP, iprod_singleton_updateP;
90
      first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    naive_solver.
92
  - apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
94
95
Qed.

96
Lemma own_update γ a a' E : a ~~> a'  own γ a  (|={E}=> own γ a').
97
Proof.
98
99
100
101
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
  by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
Qed.

Ralf Jung's avatar
Ralf Jung committed
102
Lemma own_empty `{Empty A, !CMRAUnit A} γ E :
103
  True  (|={E}=> own γ ).
104
Proof.
105
106
107
  rewrite ownG_empty /own. apply pvs_ownG_update, cmra_update_updateP.
  eapply iprod_singleton_updateP_empty;
      first by eapply map_singleton_updateP_empty', cmra_transport_updateP',
Ralf Jung's avatar
Ralf Jung committed
108
               cmra_update_updateP, cmra_update_unit.
109
  naive_solver.
110
Qed.
111
End global.