heap.v 9.08 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
11
Definition heapRA : cmraT := mapRA loc (exclRA (leibnizC val)).
Definition heapGF : iFunctor := authGF heapRA.
12

13
14
15
16
17
18
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 |}.
19

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

23
24
25
(* heap_mapsto is defined strongly opaquely, to prevent unification from
matching it against other forms of ownership. *)
Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
26
  auth_own heap_name {[ l := Excl v ]}.
27
(* Perform sealing *)
28
29
30
31
32
Definition heap_mapsto_aux : { x : _ & x = @heap_mapsto_def }.
  exact (existT _ Logic.eq_refl). Qed.
Definition heap_mapsto := projT1 heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def := projT2 heap_mapsto_aux.
Arguments heap_mapsto {_ _} _ _.
33

34
35
36
37
38
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.

39
Notation "l ↦ v" := (heap_mapsto l v) (at level 20) : uPred_scope.
40

41
Section heap.
42
  Context {Σ : iFunctorG}.
43
  Implicit Types N : namespace.
44
45
  Implicit Types P Q : iPropG heap_lang Σ.
  Implicit Types Φ : val  iPropG heap_lang Σ.
46
47
  Implicit Types σ : state.
  Implicit Types h g : heapRA.
48

49
  (** Conversion to heaps and back *)
50
  Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
51
  Proof. by intros ??; fold_leibniz=>->. Qed.
52
  Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
53
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
56
    apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
  Qed.
  Lemma to_heap_valid σ :  to_heap σ.
57
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
58
  Lemma of_heap_insert l v h : of_heap (<[l:=Excl v]> h) = <[l:=v]> (of_heap h).
59
  Proof. by rewrite /of_heap -(omap_insert _ _ _ (Excl v)). Qed.
60
61
  Lemma to_heap_insert l v σ : to_heap (<[l:=v]> σ) = <[l:=Excl v]> (to_heap σ).
  Proof. by rewrite /to_heap -fmap_insert. Qed.
62
63
  Lemma of_heap_None h l :
     h  of_heap h !! l = None  h !! l = None  h !! l  Some ExclUnit.
64
  Proof.
65
    move=> /(_ l). rewrite /of_heap lookup_omap.
66
67
68
    by case: (h !! l)=> [[]|]; auto.
  Qed.
  Lemma heap_singleton_inv_l h l v :
69
     ({[l := Excl v]}  h)  h !! l = None  h !! l  Some ExclUnit.
70
  Proof.
71
    move=> /(_ l). rewrite lookup_op lookup_singleton.
72
73
    by case: (h !! l)=> [[]|]; auto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
74

75
  (** Allocation *)
76
77
  Lemma heap_alloc E N σ :
    authG heap_lang Σ heapRA  nclose N  E 
78
    ownP σ  (|={E}=>  _ : heapG Σ, heap_ctx N  Π★{map σ} heap_mapsto).
Ralf Jung's avatar
Ralf Jung committed
79
  Proof.
Ralf Jung's avatar
Ralf Jung committed
80
    intros. rewrite heap_mapsto_eq -{1}(from_to_heap σ). etrans.
81
    { rewrite [ownP _]later_intro.
82
83
      apply (auth_alloc (ownP  of_heap) E N (to_heap σ)); last done.
      apply to_heap_valid. }
84
85
    apply pvs_mono, exist_elim=> γ.
    rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
Ralf Jung's avatar
Ralf Jung committed
86
    rewrite /heap_mapsto_def /heap_name.
87
88
89
90
91
    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.
Ralf Jung's avatar
Ralf Jung committed
92
93
    (* FIXME: investigate why we have to unfold auth_own here. *)
    by rewrite auth_own_op IH auth_own_eq. 
Ralf Jung's avatar
Ralf Jung committed
94
  Qed.
Ralf Jung's avatar
Ralf Jung committed
95

96
97
98
99
100
101
102
  Context `{heapG Σ}.

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

  (** General properties of mapsto *)
103
  Lemma heap_mapsto_disjoint l v1 v2 : (l  v1  l  v2)%I  False.
104
  Proof.
Ralf Jung's avatar
Ralf Jung committed
105
    rewrite heap_mapsto_eq -auth_own_op auth_own_valid map_op_singleton.
106
107
108
109
    rewrite map_validI (forall_elim l) lookup_singleton.
    by rewrite option_validI excl_validI.
  Qed.

110
  (** Weakest precondition *)
111
  Lemma wp_alloc N E e v P Φ :
112
113
    to_val e = Some v 
    P  heap_ctx N  nclose N  E 
114
    P  (  l, l  v - Φ (LocV l)) 
115
    P  || Alloc e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
116
  Proof.
117
    rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ??? HP.
118
    trans (|={E}=> auth_own heap_name   P)%I.
119
120
121
    { 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.
122
    rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
123
    rewrite -assoc left_id discrete_valid; apply const_elim_sep_l=> ?.
124
    rewrite -(wp_alloc_pst _ (of_heap h)) //.
125
    apply sep_mono_r; rewrite HP; apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
126
    apply forall_mono=> l; apply wand_intro_l.
127
    rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
128
    rewrite -(exist_intro (op {[ l := Excl v ]})).
129
    repeat erewrite <-exist_intro by apply _; simpl.
Ralf Jung's avatar
Ralf Jung committed
130
    rewrite -of_heap_insert left_id right_id.
131
    ecancel [_ - Φ _]%I.
132
    rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
133
134
    rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
    apply later_intro.
135
136
  Qed.

137
  Lemma wp_load N E l v P Φ :
138
    P  heap_ctx N  nclose N  E 
139
    P  ( l  v   (l  v - Φ v)) 
140
    P  || Load (Loc l) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
141
  Proof.
142
    rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ?? HPΦ.
143
    apply (auth_fsa' heap_inv (wp_fsa _) id)
144
      with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
145
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
146
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
147
    rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
148
149
    rewrite const_equiv // left_id.
    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
150
    rewrite -of_heap_insert.
151
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
152
153
  Qed.

154
  Lemma wp_store N E l v' e v P Φ :
155
156
    to_val e = Some v 
    P  heap_ctx N  nclose N  E 
157
    P  ( l  v'   (l  v - Φ (LitV LitUnit))) 
158
    P  || Store (Loc l) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
159
  Proof.
160
    rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ??? HPΦ.
161
    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
162
      with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
163
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
164
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
165
    rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
166
167
    rewrite /heap_inv alter_singleton insert_insert.
    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
168
    rewrite -!of_heap_insert const_equiv;
169
170
      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
171
172
  Qed.

173
  Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Φ :
Ralf Jung's avatar
Ralf Jung committed
174
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
175
    P  heap_ctx N  nclose N  E 
176
    P  ( l  v'   (l  v' - Φ (LitV (LitBool false)))) 
177
    P  || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
178
  Proof.
179
    rewrite /heap_ctx /heap_inv heap_mapsto_eq=>????? HPΦ.
180
    apply (auth_fsa' heap_inv (wp_fsa _) id)
181
      with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
182
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
183
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
184
    rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
185
186
    rewrite const_equiv // left_id.
    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
187
    rewrite -of_heap_insert.
188
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
189
  Qed.
Ralf Jung's avatar
Ralf Jung committed
190

191
  Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
Ralf Jung's avatar
Ralf Jung committed
192
    to_val e1 = Some v1  to_val e2 = Some v2 
193
    P  heap_ctx N  nclose N  E 
194
    P  ( l  v1   (l  v2 - Φ (LitV (LitBool true)))) 
195
    P  || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
196
  Proof.
197
    rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ???? HPΦ.
198
    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
199
      with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
200
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
201
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
202
    rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) ?lookup_insert //.
203
204
    rewrite /heap_inv alter_singleton insert_insert.
    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
205
    rewrite -!of_heap_insert const_equiv;
206
207
      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
208
  Qed.
209
End heap.