heap.v 8.71 KB
Newer Older
1
From heap_lang Require Export lifting.
2
From algebra Require Import upred_big_op.
3
From program_logic Require Export invariants ghost_ownership.
4
5
6
7
8
9
From program_logic Require Import ownership auth.
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
15
16
17
Class heapG Σ := HeapG {
  heap_inG : inG heap_lang Σ (authRA heapRA);
  heap_name : gname
}.
Instance heap_authG `{i : heapG Σ} : authG heap_lang Σ heapRA :=
  {| auth_inG := heap_inG |}.
18

19
Definition to_heap : state  heapRA := fmap Excl.
20
Definition of_heap : heapRA  state := omap (maybe Excl).
21

22
23
24
25
26
27
28
29
30
Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
  auth_own heap_name {[ l  Excl v ]}.
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
  ownP (of_heap h).
Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
  auth_ctx heap_name N heap_inv.

(* FIXME:  is already used for the singleton empty map. Resolve that... *)
Notation "l !=> v" := (heap_mapsto l v) (at level 20) : uPred_scope.
31

32
Section heap.
33
  Context {Σ : iFunctorG}.
34
35
36
37
  Implicit Types N : namespace.
  Implicit Types P : iPropG heap_lang Σ.
  Implicit Types σ : state.
  Implicit Types h g : heapRA.
38

39
  (** Conversion to heaps and back *)
40
  Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
41
  Proof. by intros ??; fold_leibniz=>->. Qed.
42
  Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
43
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
48
  Lemma of_heap_insert l v h : of_heap (<[l:=Excl v]> h) = <[l:=v]> (of_heap h).
49
  Proof. by rewrite /of_heap -(omap_insert _ _ _ (Excl v)). Qed.
50
51
  Lemma to_heap_insert l v σ : to_heap (<[l:=v]> σ) = <[l:=Excl v]> (to_heap σ).
  Proof. by rewrite /to_heap -fmap_insert. Qed.
52
53
  Lemma of_heap_None h l :
     h  of_heap h !! l = None  h !! l = None  h !! l  Some ExclUnit.
54
  Proof.
55
    move=> /(_ O l). rewrite /of_heap lookup_omap.
56
57
58
59
60
61
62
63
    by case: (h !! l)=> [[]|]; auto.
  Qed.
  Lemma heap_singleton_inv_l h l v :
     ({[l  Excl v]}  h)  h !! l = None  h !! l  Some ExclUnit.
  Proof.
    move=> /(_ O l). rewrite lookup_op lookup_singleton.
    by case: (h !! l)=> [[]|]; auto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64

65
  (** Allocation *)
66
  Lemma heap_alloc N σ :
67
68
    authG heap_lang Σ heapRA 
    ownP σ  pvs N N ( (_ : heapG Σ), heap_ctx N  Π★{map σ} heap_mapsto).
Ralf Jung's avatar
Ralf Jung committed
69
  Proof.
70
71
72
73
    rewrite -{1}(from_to_heap σ). etransitivity.
    { apply (auth_alloc (ownP  of_heap) N (to_heap σ)), to_heap_valid. }
    apply pvs_mono, exist_elim=> γ.
    rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
74
75
76
77
78
79
    induction σ as [|l v σ Hl IH] using map_ind.
    { rewrite big_sepM_empty; apply True_intro. }
    rewrite to_heap_insert big_sepM_insert //.
    rewrite (map_insert_singleton_op (to_heap σ));
      last rewrite lookup_fmap Hl; auto.
    by rewrite auto_own_op IH.
Ralf Jung's avatar
Ralf Jung committed
80
  Qed.
Ralf Jung's avatar
Ralf Jung committed
81

82
83
84
85
86
87
88
89
90
91
92
93
94
95
  Context `{heapG Σ}.

  (** Propers *)
  Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.

  (** General properties of mapsto *)
  Lemma heap_mapsto_disjoint l v1 v2 : (l !=> v1  l !=> v2)%I  False.
  Proof.
    rewrite /heap_mapsto -auto_own_op auto_own_valid map_op_singleton.
    rewrite map_validI (forall_elim l) lookup_singleton.
    by rewrite option_validI excl_validI.
  Qed.

96
  (** Weakest precondition *)
97
  Lemma wp_alloc N E e v P Q :
98
    to_val e = Some v  nclose N  E 
99
100
    P  heap_ctx N 
    P  (  l, l !=> v - Q (LocV l)) 
Ralf Jung's avatar
Ralf Jung committed
101
102
    P  wp E (Alloc e) Q.
  Proof.
103
    rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
104
105
106
107
    transitivity (pvs E E (auth_own heap_name   P))%I.
    { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
    apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
      with N heap_name ; simpl; eauto with I.
108
    rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
109
110
    rewrite -assoc left_id; apply const_elim_sep_l=> ?.
    rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
111
    rewrite /wp_fsa -(wp_alloc_pst _ (of_heap h)) //.
112
    apply sep_mono_r; rewrite HP; apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
113
    apply forall_mono=> l; apply wand_intro_l.
114
115
116
    rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
    rewrite -(exist_intro (op {[ l  Excl v ]})).
    repeat erewrite <-exist_intro by apply _; simpl.
117
    rewrite -of_heap_insert left_id right_id !assoc.
118
    apply sep_mono_l.
119
    rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
120
121
    rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
    apply later_intro.
122
123
  Qed.

124
  Lemma wp_load N E l v P Q :
Ralf Jung's avatar
Ralf Jung committed
125
    nclose N  E 
126
127
    P  heap_ctx N 
    P  ( l !=> v   (l !=> v - Q v)) 
Ralf Jung's avatar
Ralf Jung committed
128
129
    P  wp E (Load (Loc l)) Q.
  Proof.
130
    rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ.
131
132
133
    apply (auth_fsa' heap_inv (wp_fsa _) id)
      with N heap_name {[ l  Excl v ]}; simpl; eauto with I.
    rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
134
135
    rewrite -assoc; apply const_elim_sep_l=> ?.
    rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
136
    rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
137
138
    rewrite const_equiv // left_id.
    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
139
    rewrite -of_heap_insert.
140
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
141
142
  Qed.

143
  Lemma wp_store N E l v' e v P Q :
144
    to_val e = Some v  nclose N  E  
145
146
    P  heap_ctx N 
    P  ( l !=> v'   (l !=> v - Q (LitV LitUnit))) 
Ralf Jung's avatar
Ralf Jung committed
147
148
    P  wp E (Store (Loc l) e) Q.
  Proof.
149
    rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPQ.
150
151
    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
      with N heap_name {[ l  Excl v' ]}; simpl; eauto with I.
152
153
154
    rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
    rewrite -assoc; apply const_elim_sep_l=> ?.
    rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
155
    rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
156
157
    rewrite /heap_inv alter_singleton insert_insert.
    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
158
    rewrite -!of_heap_insert const_equiv;
159
160
      last (split; [naive_solver|by eapply map_insert_valid, cmra_valid_op_r]).
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Ralf Jung's avatar
Ralf Jung committed
161
162
  Qed.

163
  Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Q :
Ralf Jung's avatar
Ralf Jung committed
164
165
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
    nclose N  E 
166
167
    P  heap_ctx N 
    P  ( l !=> v'   (l !=> v' - Q (LitV (LitBool false)))) 
Ralf Jung's avatar
Ralf Jung committed
168
169
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
170
    rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPQ.
171
172
    apply (auth_fsa' heap_inv (wp_fsa _) id)
      with N heap_name {[ l  Excl v' ]}; simpl; eauto 10 with I.
173
174
175
    rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
    rewrite -assoc; apply const_elim_sep_l=> ?.
    rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
176
    rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
177
178
    rewrite const_equiv // left_id.
    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
179
    rewrite -of_heap_insert.
180
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
181
  Qed.
Ralf Jung's avatar
Ralf Jung committed
182

183
  Lemma wp_cas_suc N E l e1 v1 e2 v2 P Q :
Ralf Jung's avatar
Ralf Jung committed
184
185
    to_val e1 = Some v1  to_val e2 = Some v2 
    nclose N  E 
186
187
    P  heap_ctx N 
    P  ( l !=> v1   (l !=> v2 - Q (LitV (LitBool true)))) 
Ralf Jung's avatar
Ralf Jung committed
188
189
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
190
    rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPQ.
191
192
    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
      with N heap_name {[ l  Excl v1 ]}; simpl; eauto 10 with I.
193
194
195
    rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
    rewrite -assoc; apply const_elim_sep_l=> ?.
    rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
196
    rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) ?lookup_insert //.
197
198
    rewrite /heap_inv alter_singleton insert_insert.
    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
199
    rewrite -!of_heap_insert const_equiv;
200
201
      last (split; [naive_solver|by eapply map_insert_valid, cmra_valid_op_r]).
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Ralf Jung's avatar
Ralf Jung committed
202
  Qed.
203
End heap.