heap.v 10.1 KB
Newer Older
1
From heap_lang Require Export lifting.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From algebra Require Import upred_big_op frac dec_agree.
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. *)

Robbert Krebbers's avatar
Robbert Krebbers committed
10
Definition heapRA : cmraT := mapRA loc (fracRA (dec_agreeRA val)).
11
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

Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22
Definition to_heap : state  heapRA := fmap (λ v, Frac 1 (DecAgree v)).
Definition of_heap : heapRA  state :=
  omap (mbind (maybe DecAgree  snd)  maybe2 Frac).
23

24 25
(* heap_mapsto is defined strongly opaquely, to prevent unification from
matching it against other forms of ownership. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28
Definition heap_mapsto `{heapG Σ}
    (l : loc)(q : Qp) (v: val) : iPropG heap_lang Σ :=
  auth_own heap_name {[ l := Frac q (DecAgree v) ]}.
29
Typeclasses Opaque heap_mapsto.
30

31 32 33 34 35
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38
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.
39

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

48
  (** Conversion to heaps and back *)
49
  Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
50
  Proof. solve_proper. Qed.
51
  Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
52
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55
    apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
  Qed.
  Lemma to_heap_valid σ :  to_heap σ.
56
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
  Lemma of_heap_insert l v h :
    of_heap (<[l:=Frac 1 (DecAgree v)]> h) = <[l:=v]> (of_heap h).
  Proof. by rewrite /of_heap -(omap_insert _ _ _ (Frac 1 (DecAgree v))). Qed.
  Lemma of_heap_singleton_op l q v h :
     ({[l := Frac q (DecAgree v)]}  h) 
    of_heap ({[l := Frac q (DecAgree v)]}  h) = <[l:=v]> (of_heap h).
  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.
      case _:(h !! l)=>[[q' [v'|]|]|] //=; last by move=> [??].
      move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
    - rewrite /of_heap lookup_insert_ne // !lookup_omap.
      by rewrite (lookup_op _ h) lookup_singleton_ne // left_id.
  Qed.
  Lemma to_heap_insert l v σ :
    to_heap (<[l:=v]> σ) = <[l:=Frac 1 (DecAgree v)]> (to_heap σ).
74
  Proof. by rewrite /to_heap -fmap_insert. Qed.
75
  Lemma of_heap_None h l :
Robbert Krebbers's avatar
Robbert Krebbers committed
76
     h  of_heap h !! l = None  h !! l = None  h !! l  Some FracUnit.
77
  Proof.
78
    move=> /(_ l). rewrite /of_heap lookup_omap.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
    by case: (h !! l)=> [[q [v|]|]|] //=; destruct 1; auto.
80
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82 83
  Lemma heap_store_valid l h v1 v2 :
     ({[l := Frac 1 (DecAgree v1)]}  h) 
     ({[l := Frac 1 (DecAgree v2)]}  h).
84
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87 88
    intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
    - rewrite !lookup_op !lookup_singleton.
      case: (h !! l)=>[x|]; [|done]=> /frac_valid_inv_l=>-> //.
    - by rewrite !lookup_op !lookup_singleton_ne.
89
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  Hint Resolve heap_store_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
91

92
  (** Allocation *)
93 94
  Lemma heap_alloc E N σ :
    authG heap_lang Σ heapRA  nclose N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
95
    ownP σ  (|={E}=>  _ : heapG Σ, heap_ctx N  Π★{map σ} (λ l v, l  v)).
Ralf Jung's avatar
Ralf Jung committed
96
  Proof.
97
    intros. rewrite -{1}(from_to_heap σ). etrans.
98
    { rewrite [ownP _]later_intro.
99 100
      apply (auth_alloc (ownP  of_heap) E N (to_heap σ)); last done.
      apply to_heap_valid. }
101 102
    apply pvs_mono, exist_elim=> γ.
    rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
103
    rewrite /heap_mapsto /heap_name.
104 105 106 107 108
    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
109
    (* FIXME: investigate why we have to unfold auth_own here. *)
110
    by rewrite auth_own_op IH. 
Ralf Jung's avatar
Ralf Jung committed
111
  Qed.
Ralf Jung's avatar
Ralf Jung committed
112

113 114 115 116
  Context `{heapG Σ}.

  (** Propers *)
  Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
117
  Proof. solve_proper. Qed.
118 119

  (** General properties of mapsto *)
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123 124 125
  Lemma heap_mapsto_op_eq l q1 q2 v :
    (l {q1} v  l {q2} v)%I  (l {q1+q2} v)%I.
  Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.

  Lemma heap_mapsto_op l q1 q2 v1 v2 :
    (l {q1} v1  l {q2} v2)%I  (v1 = v2  l {q1+q2} v1)%I.
126
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129 130 131 132
    destruct (decide (v1 = v2)) as [->|].
    { by rewrite heap_mapsto_op_eq const_equiv // left_id. }
    rewrite -auth_own_op map_op_singleton Frac_op dec_agree_ne //.
    apply (anti_symm ()); last by apply const_elim_l.
    rewrite auth_own_valid map_validI (forall_elim l) lookup_singleton.
    rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
133 134
  Qed.

135 136 137 138
  Lemma heap_mapsto_op_split l q v :
    (l {q} v)%I  (l {q/2} v  l {q/2} v)%I.
  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.

139
  (** Weakest precondition *)
140
  Lemma wp_alloc N E e v P Φ :
141 142
    to_val e = Some v 
    P  heap_ctx N  nclose N  E 
143
    P  (  l, l  v - Φ (LocV l)) 
144
    P  || Alloc e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
145
  Proof.
146
    rewrite /heap_ctx /heap_inv=> ??? HP.
147
    trans (|={E}=> auth_own heap_name   P)%I.
148 149 150
    { 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.
151
    rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
152
    rewrite -assoc left_id discrete_valid; apply const_elim_sep_l=> ?.
153
    rewrite -(wp_alloc_pst _ (of_heap h)) //.
154
    apply sep_mono_r; rewrite HP; apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
155
    apply forall_mono=> l; apply wand_intro_l.
156
    rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
    rewrite -(exist_intro (op {[ l := Frac 1 (DecAgree v) ]})).
158
    repeat erewrite <-exist_intro by apply _; simpl.
Ralf Jung's avatar
Ralf Jung committed
159
    rewrite -of_heap_insert left_id right_id.
160
    rewrite /heap_mapsto. ecancel [_ - Φ _]%I.
161
    rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163
    rewrite const_equiv; last by apply (map_insert_valid h).
    by rewrite left_id -later_intro.
164 165
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
166
  Lemma wp_load N E l q v P Φ :
167
    P  heap_ctx N  nclose N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
168
    P  ( l {q} v   (l {q} v - Φ v)) 
169
    P  || Load (Loc l) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
170
  Proof.
171
    rewrite /heap_ctx /heap_inv=> ?? HPΦ.
172
    apply (auth_fsa' heap_inv (wp_fsa _) id)
Robbert Krebbers's avatar
Robbert Krebbers committed
173
      with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
174
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
175
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
176
    rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
177
    rewrite const_equiv // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
    rewrite /heap_inv of_heap_singleton_op //.
179
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
180 181
  Qed.

182
  Lemma wp_store N E l v' e v P Φ :
183 184
    to_val e = Some v 
    P  heap_ctx N  nclose N  E 
185
    P  ( l  v'   (l  v - Φ (LitV LitUnit))) 
186
    P  || Store (Loc l) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
187
  Proof.
188
    rewrite /heap_ctx /heap_inv=> ??? HPΦ.
Robbert Krebbers's avatar
Robbert Krebbers committed
189 190
    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
      with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
191
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
192
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
193
    rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
Robbert Krebbers's avatar
Robbert Krebbers committed
194 195
    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
    rewrite const_equiv; last naive_solver.
196
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Ralf Jung's avatar
Ralf Jung committed
197 198
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
199
  Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 P Φ :
Ralf Jung's avatar
Ralf Jung committed
200
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
201
    P  heap_ctx N  nclose N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
202
    P  ( l {q} v'   (l {q} v' - Φ (LitV (LitBool false)))) 
203
    P  || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
204
  Proof.
205
    rewrite /heap_ctx /heap_inv=>????? HPΦ.
206
    apply (auth_fsa' heap_inv (wp_fsa _) id)
Robbert Krebbers's avatar
Robbert Krebbers committed
207
      with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
208
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
209
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
210
    rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
211
    rewrite const_equiv // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
    rewrite /heap_inv !of_heap_singleton_op //.
213
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
214
  Qed.
Ralf Jung's avatar
Ralf Jung committed
215

216
  Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
Ralf Jung's avatar
Ralf Jung committed
217
    to_val e1 = Some v1  to_val e2 = Some v2 
218
    P  heap_ctx N  nclose N  E 
219
    P  ( l  v1   (l  v2 - Φ (LitV (LitBool true)))) 
220
    P  || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
221
  Proof.
222
    rewrite /heap_ctx /heap_inv=> ???? HPΦ.
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224
    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
      with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
225
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
226
    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
227 228
    rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
      last by rewrite lookup_insert.
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230
    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
    rewrite lookup_insert const_equiv; last naive_solver.
231
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Ralf Jung's avatar
Ralf Jung committed
232
  Qed.
233
End heap.