heap.v 9.89 KB
Newer Older
1 2 3 4
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
5
From iris.proofmode Require Import weakestpre.
6 7 8 9 10
Import uPred.
(* TODO: The entire construction could be generalized to arbitrary languages that have
   a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
   predicates over finmaps instead of just ownP. *)

11
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
12

13
(** The CMRA we need. *)
14
Class heapG Σ := HeapG {
15
  heap_inG :> authG heap_lang Σ heapUR;
16 17
  heap_name : gname
}.
18
(** The Functor we need. *)
19
Definition heapGF : gFunctor := authGF heapUR.
20

21 22
Definition to_heap : state  heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Definition of_heap : heapUR  state := omap (maybe DecAgree  snd).
23

24 25
Section definitions.
  Context `{i : heapG Σ}.
26

27
  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
28
    auth_own heap_name {[ l := (q, DecAgree v) ]}.
29 30 31 32 33
  Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
  Definition heap_mapsto := proj1_sig heap_mapsto_aux.
  Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
    proj2_sig heap_mapsto_aux.

34
  Definition heap_inv (h : heapUR) : iPropG heap_lang Σ :=
35 36 37 38
    ownP (of_heap h).
  Definition heap_ctx (N : namespace) : iPropG heap_lang Σ :=
    auth_ctx heap_name N heap_inv.

39
  Global Instance heap_inv_proper : Proper (() ==> (⊣⊢)) heap_inv.
40
  Proof. solve_proper. Qed.
41
  Global Instance heap_ctx_persistent N : PersistentP (heap_ctx N).
42 43
  Proof. apply _. Qed.
End definitions.
44

45
Typeclasses Opaque heap_ctx heap_mapsto.
46 47 48
Instance: Params (@heap_inv) 1.
Instance: Params (@heap_mapsto) 4.
Instance: Params (@heap_ctx) 2.
49

Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52
Notation "l ↦{ q } v" := (heap_mapsto l q v)
  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
53

54
Section heap.
55
  Context {Σ : gFunctors}.
56
  Implicit Types N : namespace.
57 58
  Implicit Types P Q : iPropG heap_lang Σ.
  Implicit Types Φ : val  iPropG heap_lang Σ.
59
  Implicit Types σ : state.
60
  Implicit Types h g : heapUR.
61

62
  (** Conversion to heaps and back *)
63
  Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
64
  Proof. solve_proper. Qed.
65
  Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
66
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69
    apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
  Qed.
  Lemma to_heap_valid σ :  to_heap σ.
70
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  Lemma of_heap_insert l v h :
72 73
    of_heap (<[l:=(1%Qp, DecAgree v)]> h) = <[l:=v]> (of_heap h).
  Proof. by rewrite /of_heap -(omap_insert _ _ _ (1%Qp, DecAgree v)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Lemma of_heap_singleton_op l q v h :
75 76
     ({[l := (q, DecAgree v)]}  h) 
    of_heap ({[l := (q, DecAgree v)]}  h) = <[l:=v]> (of_heap h).
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80
  Proof.
    intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|].
    - move: (Hv l). rewrite /of_heap lookup_insert
        lookup_omap (lookup_op _ h) lookup_singleton.
81
      case _:(h !! l)=>[[q' [v'|]]|] //=; last by move=> [??].
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83
      move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
    - rewrite /of_heap lookup_insert_ne // !lookup_omap.
84
      by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
  Qed.
  Lemma to_heap_insert l v σ :
87
    to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
88
  Proof. by rewrite /to_heap -fmap_insert. Qed.
89
  Lemma of_heap_None h l :  h  of_heap h !! l = None  h !! l = None.
90
  Proof.
91
    move=> /(_ l). rewrite /of_heap lookup_omap.
92
    by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto.
93
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  Lemma heap_store_valid l h v1 v2 :
95 96
     ({[l := (1%Qp, DecAgree v1)]}  h) 
     ({[l := (1%Qp, DecAgree v2)]}  h).
97
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99
    intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
    - rewrite !lookup_op !lookup_singleton.
100
      by case: (h !! l)=> [x|] // /Some_valid/exclusive_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
    - by rewrite !lookup_op !lookup_singleton_ne.
102
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  Hint Resolve heap_store_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
104

105
  (** Allocation *)
106
  Lemma heap_alloc N E σ :
107
    authG heap_lang Σ heapUR  nclose N  E 
108
    ownP σ ={E}=>  _ : heapG Σ, heap_ctx N  [ map] lv  σ, l  v.
Ralf Jung's avatar
Ralf Jung committed
109
  Proof.
110
    intros. rewrite -{1}(from_to_heap σ). etrans.
111
    { rewrite [ownP _]later_intro.
112
      apply (auth_alloc (ownP  of_heap) N E); auto using to_heap_valid. }
113
    apply pvs_mono, exist_elim=> γ.
114
    rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r.
115
    rewrite heap_mapsto_eq /heap_mapsto_def /heap_name.
116 117 118
    induction σ as [|l v σ Hl IH] using map_ind.
    { rewrite big_sepM_empty; apply True_intro. }
    rewrite to_heap_insert big_sepM_insert //.
119
    rewrite (insert_singleton_op (to_heap σ));
120
      last by rewrite lookup_fmap Hl; auto.
121
    by rewrite auth_own_op IH.
Ralf Jung's avatar
Ralf Jung committed
122
  Qed.
Ralf Jung's avatar
Ralf Jung committed
123

124 125 126
  Context `{heapG Σ}.

  (** General properties of mapsto *)
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  Global Instance heap_mapsto_timeless l q v : TimelessP (l {q} v).
128
  Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
129

130
  Lemma heap_mapsto_op_eq l q1 q2 v : l {q1} v  l {q2} v ⊣⊢ l {q1+q2} v.
131 132 133
  Proof.
    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135

  Lemma heap_mapsto_op l q1 q2 v1 v2 :
136
    l {q1} v1  l {q2} v2 ⊣⊢ v1 = v2  l {q1+q2} v1.
137
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
    destruct (decide (v1 = v2)) as [->|].
139
    { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
140
    rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
141
    apply (anti_symm ()); last by apply pure_elim_l.
142
    rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
143
    rewrite option_validI prod_validI frac_validI discrete_valid.
144
    by apply pure_elim_r.
145 146
  Qed.

147
  Lemma heap_mapsto_op_split l q v : l {q} v ⊣⊢ (l {q/2} v  l {q/2} v).
148 149
  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.

150
  (** Weakest precondition *)
Ralf Jung's avatar
Ralf Jung committed
151
  (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
152
  Lemma wp_alloc N E e v Φ :
153
    to_val e = Some v  nclose N  E 
154
    heap_ctx N   ( l, l  v ={E}= Φ (LitV (LitLoc l)))  WP Alloc e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
155
  Proof.
156
    iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx.
157
    iPvs (auth_empty heap_name) as "Hheap".
158
    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
159
    iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
160 161
    iIntros "[% Hheap]". rewrite /heap_inv.
    iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
162
    iIntros (l) "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
163
    rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
164
    iFrame "Hheap". iSplitR; first iPureIntro.
165
    { by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
166
    iIntros "Hheap". iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
167 168
  Qed.

Ralf Jung's avatar
Ralf Jung committed
169 170
  Lemma wp_load N E l q v Φ :
    nclose N  E 
171
    heap_ctx N   l {q} v   (l {q} v ={E}= Φ v)
172
     WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
173
  Proof.
174
    iIntros (?) "[#Hh [Hl HΦ]]".
175
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
176
    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
177
    iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
Ralf Jung's avatar
Ralf Jung committed
178
    iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
179
    rewrite of_heap_singleton_op //. iFrame "Hl".
180
    iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
181
    rewrite of_heap_singleton_op //. by iFrame.
Ralf Jung's avatar
Ralf Jung committed
182 183
  Qed.

184 185
  Lemma wp_store N E l v' e v Φ :
    to_val e = Some v  nclose N  E 
186
    heap_ctx N   l  v'   (l  v ={E}= Φ (LitV LitUnit))
187
     WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
188
  Proof.
189
    iIntros (??) "[#Hh [Hl HΦ]]".
190
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
191
    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
192
    iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
193
    iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
194
    rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
195
    iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
196 197
    { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
    rewrite of_heap_singleton_op //; eauto. by iFrame.
Ralf Jung's avatar
Ralf Jung committed
198 199
  Qed.

200 201
  Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1  nclose N  E 
202
    heap_ctx N   l {q} v'   (l {q} v' ={E}= Φ (LitV (LitBool false)))
203
     WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
204
  Proof.
205
    iIntros (????) "[#Hh [Hl HΦ]]".
206
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
207
    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
208
    iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
209
    iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
210
    rewrite of_heap_singleton_op //. iFrame "Hl".
211
    iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
212
    rewrite of_heap_singleton_op //. by iFrame.
Ralf Jung's avatar
Ralf Jung committed
213
  Qed.
Ralf Jung's avatar
Ralf Jung committed
214

215 216
  Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2  nclose N  E 
217
    heap_ctx N   l  v1   (l  v2 ={E}= Φ (LitV (LitBool true)))
218
     WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
219
  Proof.
220
    iIntros (???) "[#Hh [Hl HΦ]]".
221
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
222
    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
223
    iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
224
    iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
225
    rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
226
    iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
227 228
    { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
    rewrite of_heap_singleton_op //; eauto. by iFrame.
Ralf Jung's avatar
Ralf Jung committed
229
  Qed.
230
End heap.