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
    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.
Ralf Jung's avatar
Ralf Jung committed
87
    rewrite -wp_alloc_pst; first (apply sep_mono; first done); try done; [].
Ralf Jung's avatar
Ralf Jung committed
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
    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.
122 123 124
    intros HN ? Hctx HP. eapply sep_elim_True_r.
    { eapply (auth_empty γ). }
    rewrite pvs_frame_l. apply wp_strip_pvs.
Ralf Jung's avatar
Ralf Jung committed
125
    eapply wp_alloc_heap with (σ:=); try done; [|].
Ralf Jung's avatar
Ralf Jung committed
126 127 128 129 130
    { 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
131

132
  Lemma wp_load_heap N E γ σ l v P Q :
133
    σ !! l = Some v 
Ralf Jung's avatar
Ralf Jung committed
134
    nclose N  E 
135 136
    P  heap_ctx HeapI γ N 
    P  (heap_own HeapI γ σ   (heap_own HeapI γ σ - Q v)) 
137 138
    P  wp E (Load (Loc l)) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
139
    rewrite /heap_ctx /heap_own. intros Hl HN Hctx HP.
140
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), id)); simpl; eauto.
141 142 143 144 145 146
    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
147
      case _:(hf !! l)=>[[?||]|]; by auto. }
148 149
    apply later_mono, wand_intro_l.
    rewrite -(exist_intro ()) left_id const_equiv // left_id.
150 151 152
    by rewrite -later_intro.
  Qed.

153
  Lemma wp_load N E γ l v P Q :
Ralf Jung's avatar
Ralf Jung committed
154
    nclose N  E 
155 156
    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
157 158
    P  wp E (Load (Loc l)) Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
159
    intros HN. rewrite /heap_mapsto. apply wp_load_heap; last done.
Ralf Jung's avatar
Ralf Jung committed
160 161
    by simplify_map_equality.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
162

Ralf Jung's avatar
Ralf Jung committed
163 164 165
  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
166 167 168 169
    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
170
    rewrite /heap_ctx /heap_own. intros Hl Hval HN Hctx HP.
171 172
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _)
                     (λ _:(), alter (λ _, Excl v) l)); simpl; eauto.
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
177
    rewrite -wp_store_pst; first (apply sep_mono; first done); try done; last first.
Ralf Jung's avatar
Ralf Jung committed
178 179
    { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
      case _:(hf !! l)=>[[?||]|]; by auto. }
180 181
    apply later_mono, wand_intro_l.
    rewrite -(exist_intro ()) const_equiv //; last first.
Ralf Jung's avatar
Ralf Jung committed
182 183 184 185 186 187 188 189 190 191 192 193 194
    (* 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.
195 196
    f_equiv. apply: map_eq=>l'. move: (Hv 0%nat l').
    destruct (decide (l=l')); simplify_map_equality.
Ralf Jung's avatar
Ralf Jung committed
197 198 199
    - rewrite /from_heap /to_heap lookup_insert lookup_omap !lookup_op.
      rewrite !lookup_fmap lookup_insert Hl.
      case (hf !! l')=>[[?||]|]; auto; contradiction.
200 201
    - rewrite /from_heap /to_heap lookup_insert_ne // !lookup_omap.
      rewrite !lookup_op !lookup_fmap lookup_insert_ne //.
Ralf Jung's avatar
Ralf Jung committed
202 203
  Qed.

Ralf Jung's avatar
Ralf Jung committed
204 205 206
  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
207 208 209 210
    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.
211
    rewrite /heap_mapsto=>Hval HN Hctx HP.
Ralf Jung's avatar
Ralf Jung committed
212
    eapply wp_store_heap; try done; last first.
Ralf Jung's avatar
Ralf Jung committed
213 214 215
    - rewrite HP. apply sep_mono; first done. by rewrite insert_singleton.
    - by rewrite lookup_insert.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
216 217 218 219 220 221 222 223 224

  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.
225
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), id)); simpl; eauto.
Ralf Jung's avatar
Ralf Jung committed
226 227 228 229 230
    { 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.
Ralf Jung's avatar
Ralf Jung committed
231
    rewrite -wp_cas_fail_pst; first (apply sep_mono; first done); try done; last first.
Ralf Jung's avatar
Ralf Jung committed
232 233
    { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
      case _:(hf !! l)=>[[?||]|]; by auto. }
234 235
    apply later_mono, wand_intro_l.
    rewrite -(exist_intro ()) left_id const_equiv // left_id.
Ralf Jung's avatar
Ralf Jung committed
236 237 238 239 240 241 242 243 244 245
    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.
Ralf Jung's avatar
Ralf Jung committed
246
    rewrite /heap_mapsto=>???. eapply wp_cas_fail_heap; try done; [].
Ralf Jung's avatar
Ralf Jung committed
247 248
    by simplify_map_equality.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263

  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.
Ralf Jung's avatar
Ralf Jung committed
264
    rewrite -wp_cas_suc_pst; first (apply sep_mono; first done); try done; last first.
Ralf Jung's avatar
Ralf Jung committed
265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288
    { 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
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.
Ralf Jung's avatar
Ralf Jung committed
297
    rewrite /heap_mapsto=>???? HP. eapply wp_cas_suc_heap; try done; last first.
Ralf Jung's avatar
Ralf Jung committed
298 299 300 301
    - rewrite HP. apply sep_mono; first done. by rewrite insert_singleton.
    - by simplify_map_equality.
  Qed.

302
End heap.