heap.v 14 KB
Newer Older
1
From heap_lang Require Export derived.
2
From program_logic Require Export invariants ghost_ownership.
3
From program_logic Require Import ownership auth.
Ralf Jung's avatar
Ralf Jung committed
4
From heap_lang Require Import notation.
5
6
7
8
9
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. *)

10
Definition heapRA := mapRA loc (exclRA (leibnizC val)).
11

12
13
14
Class HeapInG Σ (i : gid) := heap_inG :> InG heap_lang Σ i (authRA heapRA).
Instance heap_inG_auth `{HeapInG Σ i} : AuthInG heap_lang Σ i heapRA.
Proof. split; apply _. Qed.
15

16
17
Definition to_heap : state  heapRA := fmap Excl.
Definition from_heap : heapRA  state := omap (maybe Excl).
18

19
20
21
22
23
24
25
26
27
28
29
(* TODO: Do we want to expose heap ownership based on the state, or the heapRA?
   The former does not expose the annoying "Excl", so for now I am going for
   that. We should be able to derive the lemmas we want for this, too. *)
Definition heap_own {Σ} (i : gid) `{HeapInG Σ i}
  (γ : gname) (σ : state) : iPropG heap_lang Σ := auth_own i γ (to_heap σ).
Definition heap_mapsto {Σ} (i : gid) `{HeapInG Σ i}
  (γ : gname) (l : loc) (v : val) : iPropG heap_lang Σ := heap_own i γ {[ l  v ]}.
Definition heap_inv {Σ} (i : gid) `{HeapInG Σ i}
  (h : heapRA) : iPropG heap_lang Σ := ownP (from_heap h).
Definition heap_ctx {Σ} (i : gid) `{HeapInG Σ i}
  (γ : gname) (N : namespace) : iPropG heap_lang Σ := auth_ctx i γ N (heap_inv i).
30

31
32
33
34
35
36
37
Section heap.
  Context {Σ : iFunctorG} (HeapI : gid) `{!HeapInG Σ HeapI}.
  Implicit Types N : namespace.
  Implicit Types P : iPropG heap_lang Σ.
  Implicit Types σ : state.
  Implicit Types h g : heapRA.
  Implicit Types γ : gname.
38

Robbert Krebbers's avatar
Robbert Krebbers committed
39
  Lemma from_to_heap σ : from_heap (to_heap σ) = σ.
40
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
44
45
46
47
    apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
  Qed.
  Lemma to_heap_valid σ :  to_heap σ.
  Proof. intros n l. rewrite lookup_fmap. by case (σ !! l). Qed.
  Hint Resolve to_heap_valid.

  Global Instance heap_inv_proper : Proper (() ==> ()) (heap_inv HeapI).
48
  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
49
50

  Lemma heap_own_op γ σ1 σ2 :
51
52
    (heap_own HeapI γ σ1  heap_own HeapI γ σ2)%I
     ( (σ1 ⊥ₘ σ2)  heap_own HeapI γ (σ1  σ2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
  Proof.
 (* TODO. *)
55
56
57
58
  Abort.

  Lemma heap_own_mapsto γ σ l v :
    (* TODO: Is this the best way to express "l ∉ dom σ"? *)
59
60
    (heap_own HeapI γ σ  heap_mapsto HeapI γ l v)%I
     ( (σ !! l = None)  heap_own HeapI γ (<[l:=v]>σ))%I.
61
62
63
  Proof. (* TODO. *)
  Abort.

64
  (* TODO: Do we want equivalence to a big sum? *)
65

66
67
  Lemma heap_alloc N σ :
    ownP σ  pvs N N ( γ, heap_ctx HeapI γ N  heap_own HeapI γ σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  Proof. by rewrite -{1}[σ]from_to_heap -(auth_alloc _ N). Qed.
69

Ralf Jung's avatar
Ralf Jung committed
70
71
  (* TODO: Clearly, this is not the right way to obtain these properties about
     fin_maps. This is horrible. *)
Ralf Jung's avatar
Ralf Jung committed
72
73
74
75
76
77
78
  Lemma wp_alloc_heap N E γ σ e v P Q :
    nclose N  E   to_val e = Some v 
    P  heap_ctx HeapI γ N 
    P  (heap_own HeapI γ σ 
          ( l, σ !! l = None  heap_own HeapI γ (<[l:=v]>σ) - Q (LocV l))) 
    P  wp E (Alloc e) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
    rewrite /heap_ctx /heap_own. intros HN Hval Hctx HP.
    set (LU (l : loc) := local_update_op (A:=heapRA) ({[ l  Excl v ]})).
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) _ (LU := LU)); simpl.
    { by eauto. } { by eauto. } { by eauto. }
    rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
    apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
    rewrite -assoc. apply const_elim_sep_l=>Hv /=.
    rewrite {1}[(ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
    rewrite -wp_alloc_pst; first (apply sep_mono; first done); try eassumption.
    apply later_mono, forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
    rewrite -(exist_intro l) !left_id. rewrite always_and_sep_l -assoc.
    apply const_elim_sep_l=>Hfresh.
    assert (σ !! l = None) as Hfresh_σ.
    { move: Hfresh (Hv 0%nat l). rewrite /from_heap /to_heap lookup_omap.
      rewrite lookup_op !lookup_fmap.
      case _:(σ !! l)=>[v'|]/=; case _:(hf !! l)=>[[?||]|]/=; done. }
    rewrite const_equiv // const_equiv; last first.
    { move=>n l'. move:(Hv n l') Hfresh.
      rewrite /from_heap /to_heap !lookup_omap !lookup_op !lookup_fmap !Hfresh_σ /=.
      destruct (decide (l=l')).
      - subst l'. rewrite lookup_singleton !Hfresh_σ.
        case _:(hf !! l)=>[[?||]|]/=; done.
      - rewrite lookup_singleton_ne //.
        case _:(σ !! l')=>[?|]/=; case _:(hf !! l')=>[[?||]|]/=; done. }
    rewrite !left_id -later_intro.
    assert ({[l  Excl v]}  to_heap σ = to_heap (<[l:=v]> σ)) as EQ.
    { apply: map_eq=>l'. rewrite lookup_op !lookup_fmap.
      destruct (decide (l=l')); simplify_map_equality.
      - rewrite lookup_insert. done.
      - rewrite !lookup_insert_ne // lookup_empty left_id. done. }
    rewrite EQ. apply sep_mono; last done. f_equiv. apply: map_eq=>l'. 
    move:(Hv 0%nat l') Hfresh. destruct (decide (l=l')); simplify_map_equality.
    - rewrite lookup_insert !lookup_omap !lookup_op !lookup_fmap lookup_insert.
      case _:(σ !! l')=>[?|]/=; case _:(hf !! l')=>[[?||]|]/=; done.
    - rewrite lookup_insert_ne // !lookup_omap !lookup_op !lookup_fmap lookup_insert_ne //.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
115

Ralf Jung's avatar
Ralf Jung committed
116
117
118
119
120
121
  Lemma wp_alloc N E γ e v P Q :
    nclose N  E   to_val e = Some v 
    P  heap_ctx HeapI γ N 
    P  ( ( l, heap_mapsto HeapI γ l v - Q (LocV l))) 
    P  wp E (Alloc e) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
122
123
124
125
126
127
128
    intros HN ? Hctx HP. rewrite -(right_id True%I ()%I (P)) (auth_empty γ) pvs_frame_l.
    apply wp_strip_pvs. eapply wp_alloc_heap with (σ:=); try eassumption.
    { eauto with I. }
    rewrite HP comm. apply sep_mono.
    - rewrite /heap_own. f_equiv. apply: map_eq=>l. by rewrite lookup_fmap !lookup_empty.
    - apply later_mono, forall_mono=>l. apply wand_mono; last done. eauto with I.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
129

130
  Lemma wp_load_heap N E γ σ l v P Q :
131
    σ !! l = Some v 
Ralf Jung's avatar
Ralf Jung committed
132
    nclose N  E 
133
134
    P  heap_ctx HeapI γ N 
    P  (heap_own HeapI γ σ   (heap_own HeapI γ σ - Q v)) 
135
136
    P  wp E (Load (Loc l)) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
137
    rewrite /heap_ctx /heap_own. intros Hl HN Hctx HP.
138
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), id)); simpl; eauto.
139
140
141
142
143
144
    rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
    apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
    rewrite -assoc. apply const_elim_sep_l=>Hv /=.
    rewrite {1}[(ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
    rewrite -wp_load_pst; first (apply sep_mono; first done); last first.
    { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
Ralf Jung's avatar
Ralf Jung committed
145
      case _:(hf !! l)=>[[?||]|]; by auto. }
146
147
    apply later_mono, wand_intro_l.
    rewrite -(exist_intro ()) left_id const_equiv // left_id.
148
149
150
    by rewrite -later_intro.
  Qed.

151
  Lemma wp_load N E γ l v P Q :
Ralf Jung's avatar
Ralf Jung committed
152
    nclose N  E 
153
154
    P  heap_ctx HeapI γ N 
    P  (heap_mapsto HeapI γ l v   (heap_mapsto HeapI γ l v - Q v)) 
Ralf Jung's avatar
Ralf Jung committed
155
156
    P  wp E (Load (Loc l)) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
157
    intros HN. rewrite /heap_mapsto. apply wp_load_heap; last done.
Ralf Jung's avatar
Ralf Jung committed
158
159
    by simplify_map_equality.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
160

Ralf Jung's avatar
Ralf Jung committed
161
162
163
  Lemma wp_store_heap N E γ σ l v' e v P Q :
    σ !! l = Some v'  to_val e = Some v  
    nclose N  E 
Ralf Jung's avatar
Ralf Jung committed
164
165
166
167
    P  heap_ctx HeapI γ N 
    P  (heap_own HeapI γ σ   (heap_own HeapI γ (<[l:=v]>σ) - Q (LitV LitUnit))) 
    P  wp E (Store (Loc l) e) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
168
    rewrite /heap_ctx /heap_own. intros Hl Hval HN Hctx HP.
169
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), alter (λ _, Excl v) l)); simpl; eauto.
Ralf Jung's avatar
Ralf Jung committed
170
171
172
173
174
175
176
    rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
    apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
    rewrite -assoc. apply const_elim_sep_l=>Hv /=.
    rewrite {1}[(ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
    rewrite -wp_store_pst; first (apply sep_mono; first done); try eassumption; last first.
    { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
      case _:(hf !! l)=>[[?||]|]; by auto. }
177
178
    apply later_mono, wand_intro_l.
    rewrite -(exist_intro ()) const_equiv //; last first.
Ralf Jung's avatar
Ralf Jung committed
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
    (* TODO I think there are some general fin_map lemmas hiding in here. *)
    { split.
      - exists (Excl v'). by rewrite lookup_fmap Hl.
      - move=>n l'. move: (Hv n l'). rewrite !lookup_op.
        destruct (decide (l=l')); simplify_map_equality.
        + rewrite lookup_alter lookup_fmap Hl /=. case (hf !! l')=>[[?||]|]; by auto.
        + rewrite lookup_alter_ne //. }
    rewrite left_id -later_intro.
    assert (alter (λ _ : excl val, Excl v) l (to_heap σ) = to_heap (<[l:=v]> σ)) as EQ.
    { apply: map_eq=>l'. destruct (decide (l=l')); simplify_map_equality.
      + by rewrite lookup_alter /to_heap !lookup_fmap lookup_insert Hl /=.
      + rewrite lookup_alter_ne // !lookup_fmap lookup_insert_ne //. }
    rewrite !EQ. apply sep_mono; last done.
    f_equiv. apply: map_eq=>l'. move: (Hv 0%nat l'). destruct (decide (l=l')); simplify_map_equality.
    - rewrite /from_heap /to_heap lookup_insert lookup_omap !lookup_op.
      rewrite !lookup_fmap lookup_insert Hl.
      case (hf !! l')=>[[?||]|]; auto; contradiction.
    - rewrite /from_heap /to_heap lookup_insert_ne // !lookup_omap !lookup_op !lookup_fmap.
      rewrite lookup_insert_ne //.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
200
201
202
  Lemma wp_store N E γ l v' e v P Q :
    to_val e = Some v  
    nclose N  E  
Ralf Jung's avatar
Ralf Jung committed
203
204
205
206
    P  heap_ctx HeapI γ N 
    P  (heap_mapsto HeapI γ l v'   (heap_mapsto HeapI γ l v - Q (LitV LitUnit))) 
    P  wp E (Store (Loc l) e) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
207
    rewrite /heap_mapsto=>Hval HN Hctx HP. eapply wp_store_heap; try eassumption; last first.
Ralf Jung's avatar
Ralf Jung committed
208
209
210
    - rewrite HP. apply sep_mono; first done. by rewrite insert_singleton.
    - by rewrite lookup_insert.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
211
212
213
214
215
216
217
218
219

  Lemma wp_cas_fail_heap N E γ σ l v' e1 v1 e2 v2 P Q :
    to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
    nclose N  E 
    P  heap_ctx HeapI γ N 
    P  (heap_own HeapI γ σ   (heap_own HeapI γ σ - Q 'false)) 
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
    rewrite /heap_ctx /heap_own. intros He1 He2 Hl Hne HN Hctx HP.
220
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), id)); simpl; eauto.
Ralf Jung's avatar
Ralf Jung committed
221
222
223
224
225
226
227
228
    { split_ands; eexists; eauto. }
    rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
    apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
    rewrite -assoc. apply const_elim_sep_l=>Hv /=.
    rewrite {1}[(ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
    rewrite -wp_cas_fail_pst; first (apply sep_mono; first done); try eassumption; last first.
    { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
      case _:(hf !! l)=>[[?||]|]; by auto. }
229
230
    apply later_mono, wand_intro_l.
    rewrite -(exist_intro ()) left_id const_equiv // left_id.
Ralf Jung's avatar
Ralf Jung committed
231
232
233
234
235
236
237
238
239
240
241
242
243
    by rewrite -later_intro.
  Qed.

  Lemma wp_cas_fail N E γ l v' e1 v1 e2 v2 P Q :
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
    nclose N  E 
    P  heap_ctx HeapI γ N 
    P  (heap_mapsto HeapI γ l v'   (heap_mapsto HeapI γ l v' - Q 'false)) 
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
    rewrite /heap_mapsto=>???. eapply wp_cas_fail_heap; try eassumption.
    by simplify_map_equality.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283

  Lemma wp_cas_suc_heap N E γ σ l e1 v1 e2 v2 P Q :
    to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1  
    nclose N  E 
    P  heap_ctx HeapI γ N 
    P  (heap_own HeapI γ σ   (heap_own HeapI γ (<[l:=v2]>σ) - Q 'true)) 
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
    rewrite /heap_ctx /heap_own. intros Hv1 Hv2 Hl HN Hctx HP.
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), alter (λ _, Excl v2) l)); simpl; eauto.
    { split_ands; eexists; eauto. }
    rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
    apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
    rewrite -assoc. apply const_elim_sep_l=>Hv /=.
    rewrite {1}[(ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
    rewrite -wp_cas_suc_pst; first (apply sep_mono; first done); try eassumption; last first.
    { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
      case _:(hf !! l)=>[[?||]|]; by auto. }
    apply later_mono, wand_intro_l.
    rewrite -(exist_intro ()) const_equiv //; last first.
    (* TODO I think there are some general fin_map lemmas hiding in here. *)
    { split.
      - exists (Excl v1). by rewrite lookup_fmap Hl.
      - move=>n l'. move: (Hv n l'). rewrite !lookup_op.
        destruct (decide (l=l')); simplify_map_equality.
        + rewrite lookup_alter lookup_fmap Hl /=. case (hf !! l')=>[[?||]|]; by auto.
        + rewrite lookup_alter_ne //. }
    rewrite left_id -later_intro.
    assert (alter (λ _ : excl val, Excl v2) l (to_heap σ) = to_heap (<[l:=v2]> σ)) as EQ.
    { apply: map_eq=>l'. destruct (decide (l=l')); simplify_map_equality.
      + by rewrite lookup_alter /to_heap !lookup_fmap lookup_insert Hl /=.
      + rewrite lookup_alter_ne // !lookup_fmap lookup_insert_ne //. }
    rewrite !EQ. apply sep_mono; last done.
    f_equiv. apply: map_eq=>l'. move: (Hv 0%nat l'). destruct (decide (l=l')); simplify_map_equality.
    - rewrite /from_heap /to_heap lookup_insert lookup_omap !lookup_op.
      rewrite !lookup_fmap lookup_insert Hl.
      case (hf !! l')=>[[?||]|]; auto; contradiction.
    - rewrite /from_heap /to_heap lookup_insert_ne // !lookup_omap !lookup_op !lookup_fmap.
      rewrite lookup_insert_ne //.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
284
285
286
287
288
289
290
291
292
293
294
295
296

  Lemma wp_cas_suc N E γ l e1 v1 e2 v2 P Q :
    to_val e1 = Some v1  to_val e2 = Some v2 
    nclose N  E 
    P  heap_ctx HeapI γ N 
    P  (heap_mapsto HeapI γ l v1   (heap_mapsto HeapI γ l v2 - Q 'true)) 
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
    rewrite /heap_mapsto=>???? HP. eapply wp_cas_suc_heap; try eassumption; last first.
    - rewrite HP. apply sep_mono; first done. by rewrite insert_singleton.
    - by simplify_map_equality.
  Qed.

297
End heap.