heap.v 10 KB
Newer Older
1
From iris.heap_lang Require Export lifting.
2
From iris.algebra Require Import upred_big_op gmap frac dec_agree.
3
4
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Ralf Jung's avatar
Ralf Jung committed
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 heapN : namespace := nroot .@ "heap".
12
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
13

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

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

26
Section definitions.
27
  Context `{heapG Σ}.
28

29
  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
30
    auth_own heap_name {[ l := (q, DecAgree v) ]}.
31
32
33
34
35
  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.

36
  Definition heap_inv (h : heapUR) : iProp Σ :=
37
    ownP (of_heap h).
38
  Definition heap_ctx : iProp Σ :=
39
    auth_ctx heap_name heapN heap_inv.
40

41
  Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
42
  Proof. solve_proper. Qed.
43
  Global Instance heap_ctx_persistent : PersistentP heap_ctx.
44
45
  Proof. apply _. Qed.
End definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
46

47
Typeclasses Opaque heap_ctx heap_mapsto.
48
Instance: Params (@heap_inv) 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
57
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
58
  Implicit Types σ : state.
59
  Implicit Types h g : heapUR.
60

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

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

122
123
124
  Context `{heapG Σ}.

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

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

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

145
146
147
148
149
150
151
152
153
154
155
  Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
    l {q1} v1  l {q2} v2  v1 = v2  l {q1+q2} v1.
  Proof. by rewrite heap_mapsto_op. Qed.

  Lemma heap_mapsto_op_half l q v1 v2 :
    l {q/2} v1  l {q/2} v2  v1 = v2  l {q} v1.
  Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.

  Lemma heap_mapsto_op_half_1 l q v1 v2 :
    l {q/2} v1  l {q/2} v2  v1 = v2  l {q} v1.
  Proof. by rewrite heap_mapsto_op_half. Qed.
156

157
  (** Weakest precondition *)
158
159
160
  Lemma wp_alloc E e v Φ :
    to_val e = Some v  nclose heapN  E 
    heap_ctx   ( l, l  v ={E}= Φ (LitV (LitLoc l)))  WP Alloc e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
161
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
    iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
163
164
165
166
167
168
169
170
171
172
    iVs (auth_empty heap_name) as "Hh".
    iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto.
    rewrite left_id /heap_inv. iDestruct "Hv" as %?.
    iApply wp_alloc_pst. iFrame "Hh". iNext.
    iIntros (l) "[% Hh]"; iVsIntro.
    iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]").
    { rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
      iFrame "Hh". iPureIntro.
      by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
    iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
173
174
  Qed.

175
176
177
  Lemma wp_load E l q v Φ :
    nclose heapN  E 
    heap_ctx   l {q} v   (l {q} v ={E}= Φ v)
178
     WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
179
  Proof.
180
    iIntros (?) "[#Hinv [Hl HΦ]]".
181
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
182
183
    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
    rewrite /heap_inv.
Ralf Jung's avatar
Ralf Jung committed
184
    iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
185
    rewrite of_heap_singleton_op //. iFrame "Hl".
186
187
188
    iIntros "> Hown". iVsIntro. iVs ("Hclose" with "* [Hown]").
    { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
189
190
  Qed.

191
192
193
  Lemma wp_store E l v' e v Φ :
    to_val e = Some v  nclose heapN  E 
    heap_ctx   l  v'   (l  v ={E}= Φ (LitV LitUnit))
194
     WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
195
  Proof.
196
    iIntros (<-%of_to_val ?) "[#Hinv [Hl HΦ]]".
197
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
198
199
    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
    rewrite /heap_inv.
200
    iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
201
    rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
202
203
204
205
206
207
    iIntros "> Hl". iVsIntro.
    iVs ("Hclose" $! {[l := (1%Qp, DecAgree v)]} with "[Hl]").
    { iSplit.
      - iPureIntro; by apply singleton_local_update, exclusive_local_update.
      - rewrite of_heap_singleton_op //; eauto. }
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
208
209
  Qed.

210
211
212
  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1  nclose heapN  E 
    heap_ctx   l {q} v'   (l {q} v' ={E}= Φ (LitV (LitBool false)))
213
     WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
214
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
    iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
216
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
217
218
    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
    rewrite /heap_inv.
219
    iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
220
    rewrite of_heap_singleton_op //. iFrame "Hl".
221
222
223
    iIntros "> Hown". iVsIntro. iVs ("Hclose" with "* [Hown]").
    { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
224
  Qed.
Ralf Jung's avatar
Ralf Jung committed
225

226
227
228
  Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2  nclose heapN  E 
    heap_ctx   l  v1   (l  v2 ={E}= Φ (LitV (LitBool true)))
229
     WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
230
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
    iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
232
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
233
234
    iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
    rewrite /heap_inv.
235
    iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
236
    rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
237
238
239
240
241
242
    iIntros "> Hl". iVsIntro.
    iVs ("Hclose" $! {[l := (1%Qp, DecAgree v2)]} with "[Hl]").
    { iSplit.
      - iPureIntro; by apply singleton_local_update, exclusive_local_update.
      - rewrite of_heap_singleton_op //; eauto. }
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
243
  Qed.
244
End heap.