heap.v 8.83 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
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
Definition to_heap : state  heapRA := fmap Excl.
17
Definition of_heap : heapRA  state := omap (maybe Excl).
18

19
Definition heap_mapsto {Σ} (i : gid) `{HeapInG Σ i}
20
21
    (γ : gname) (l : loc) (v : val) : iPropG heap_lang Σ :=
  auth_own i γ {[ l  Excl v ]}.
22
Definition heap_inv {Σ} (i : gid) `{HeapInG Σ i}
23
  (h : heapRA) : iPropG heap_lang Σ := ownP (of_heap h).
24
25
Definition heap_ctx {Σ} (i : gid) `{HeapInG Σ i}
  (γ : gname) (N : namespace) : iPropG heap_lang Σ := auth_ctx i γ N (heap_inv i).
26

27
28
29
30
31
32
33
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.
34

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

61
  (** Propers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Global Instance heap_inv_proper : Proper (() ==> ()) (heap_inv HeapI).
63
  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
64

65
66
67
  (** General properties of mapsto *)
  Lemma heap_mapsto_disjoint γ l v1 v2 :
    (heap_mapsto HeapI γ l v1  heap_mapsto HeapI γ l v2)%I  False.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  Proof.
69
70
71
72
    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.
73

74
  Lemma heap_alloc N σ :
75
    ownP σ  pvs N N ( γ, heap_ctx HeapI γ N  Π★{σ} heap_mapsto HeapI γ).
Ralf Jung's avatar
Ralf Jung committed
76
  Proof.
77
    rewrite -{1}(from_to_heap σ); etransitivity;
78
      first apply (auth_alloc (ownP  of_heap) N (to_heap σ)), to_heap_valid.
79
80
81
82
83
84
85
    apply pvs_mono, exist_mono=> γ; apply and_mono_r.
    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
86
  Qed.
Ralf Jung's avatar
Ralf Jung committed
87

88
  (** Weakest precondition *)
Ralf Jung's avatar
Ralf Jung committed
89
  Lemma wp_alloc N E γ e v P Q :
90
    to_val e = Some v  nclose N  E 
Ralf Jung's avatar
Ralf Jung committed
91
    P  heap_ctx HeapI γ N 
92
    P  (  l, heap_mapsto HeapI γ l v - Q (LocV l)) 
Ralf Jung's avatar
Ralf Jung committed
93
94
    P  wp E (Alloc e) Q.
  Proof.
95
96
97
98
99
100
101
102
    rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
    transitivity (pvs E E (auth_own HeapI γ   P))%I.
    { by rewrite -pvs_frame_r -(auth_empty E γ) left_id. }
    apply wp_strip_pvs, (auth_fsa (heap_inv HeapI) (wp_fsa (Alloc e)))
      with N γ ; simpl; eauto with I.
    apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
    rewrite -assoc left_id; apply const_elim_sep_l=> ?.
    rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
103
    rewrite /wp_fsa -(wp_alloc_pst _ (of_heap h)) //.
104
    apply sep_mono_r; rewrite HP; apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
105
    apply forall_mono=> l; apply wand_intro_l.
106
107
108
    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.
109
    rewrite -of_heap_insert left_id right_id !assoc.
110
    apply sep_mono_l.
111
    rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
112
113
    rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
    apply later_intro.
114
115
  Qed.

116
  Lemma wp_load N E γ l v P Q :
Ralf Jung's avatar
Ralf Jung committed
117
    nclose N  E 
118
119
    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
120
121
    P  wp E (Load (Loc l)) Q.
  Proof.
122
123
124
125
126
127
    rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ.
    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id)
      with N γ {[ l  Excl v ]}; simpl; eauto with I.
    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.
128
    rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
129
130
    rewrite const_equiv // left_id.
    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
131
    rewrite -of_heap_insert.
132
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
133
134
  Qed.

Ralf Jung's avatar
Ralf Jung committed
135
  Lemma wp_store N E γ l v' e v P Q :
136
    to_val e = Some v  nclose N  E  
Ralf Jung's avatar
Ralf Jung committed
137
    P  heap_ctx HeapI γ N 
138
139
    P  (heap_mapsto HeapI γ l v' 
           (heap_mapsto HeapI γ l v - Q (LitV LitUnit))) 
Ralf Jung's avatar
Ralf Jung committed
140
141
    P  wp E (Store (Loc l) e) Q.
  Proof.
142
143
144
145
146
147
    rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPQ.
    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v) l))
      with N γ {[ l  Excl v' ]}; simpl; eauto with I.
    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.
148
    rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
149
150
    rewrite /heap_inv alter_singleton insert_insert.
    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
151
    rewrite -!of_heap_insert const_equiv;
152
153
      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
154
155
156
157
158
159
  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 
160
161
    P  (heap_mapsto HeapI γ l v' 
           (heap_mapsto HeapI γ l v' - Q (LitV (LitBool false)))) 
Ralf Jung's avatar
Ralf Jung committed
162
163
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
164
165
166
167
168
169
    rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPQ.
    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id)
      with N γ {[ l  Excl v' ]}; simpl; eauto 10 with I.
    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.
170
    rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
171
172
    rewrite const_equiv // left_id.
    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
173
    rewrite -of_heap_insert.
174
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
175
  Qed.
Ralf Jung's avatar
Ralf Jung committed
176
177
178
179
180

  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 
181
182
    P  (heap_mapsto HeapI γ l v1 
           (heap_mapsto HeapI γ l v2 - Q (LitV (LitBool true)))) 
Ralf Jung's avatar
Ralf Jung committed
183
184
    P  wp E (Cas (Loc l) e1 e2) Q.
  Proof.
185
186
187
188
189
190
    rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPQ.
    apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v2) l))
      with N γ {[ l  Excl v1 ]}; simpl; eauto 10 with I.
    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.
191
    rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) ?lookup_insert //.
192
193
    rewrite /heap_inv alter_singleton insert_insert.
    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
194
    rewrite -!of_heap_insert const_equiv;
195
196
      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
197
  Qed.
198
End heap.