heap.v 7.18 KB
Newer Older
1
2
3
4
5
6
7
From heap_lang Require Export derived.
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. *)

8
Definition heapRA := mapRA loc (exclRA (leibnizC val)).
9

10
11
12
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.
13

14
15
Definition to_heap : state  heapRA := fmap Excl.
Definition from_heap : heapRA  state := omap (maybe Excl).
16

17
18
19
20
21
22
23
24
25
26
27
(* 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).
28

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

Robbert Krebbers's avatar
Robbert Krebbers committed
37
  Lemma from_to_heap σ : from_heap (to_heap σ) = σ.
38
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
41
42
43
44
45
    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).
46
  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
47
48

  Lemma heap_own_op γ σ1 σ2 :
49
50
    (heap_own HeapI γ σ1  heap_own HeapI γ σ2)%I
     ( (σ1 ⊥ₘ σ2)  heap_own HeapI γ (σ1  σ2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
  Proof.
 (* TODO. *)
53
54
55
56
  Abort.

  Lemma heap_own_mapsto γ σ l v :
    (* TODO: Is this the best way to express "l ∉ dom σ"? *)
57
58
    (heap_own HeapI γ σ  heap_mapsto HeapI γ l v)%I
     ( (σ !! l = None)  heap_own HeapI γ (<[l:=v]>σ))%I.
59
60
61
  Proof. (* TODO. *)
  Abort.

62
  (* TODO: Do we want equivalence to a big sum? *)
63

64
65
  Lemma heap_alloc N σ :
    ownP σ  pvs N N ( γ, heap_ctx HeapI γ N  heap_own HeapI γ σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  Proof. by rewrite -{1}[σ]from_to_heap -(auth_alloc _ N). Qed.
67

Ralf Jung's avatar
Ralf Jung committed
68
69
70
71
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.
    rewrite /heap_ctx /heap_own. intros HN Hval Hl Hctx HP.
    Fail eapply (auth_fsa (heap_inv HeapI) (wp_fsa _ _) (alter (λ _, Excl v) l)).
  Abort.

79
  Lemma wp_load_heap N E γ σ l v P Q :
80
81
    nclose N  E 
    σ !! l = Some v 
82
83
    P  heap_ctx HeapI γ N 
    P  (heap_own HeapI γ σ   (heap_own HeapI γ σ - Q v)) 
84
85
86
    P  wp E (Load (Loc l)) Q.
  Proof.
    rewrite /heap_ctx /heap_own. intros HN Hl Hctx HP.
Ralf Jung's avatar
Ralf Jung committed
87
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _ _) id).
88
89
90
91
92
93
94
    { eassumption. } { eassumption. }
    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
95
      case _:(hf !! l)=>[[?||]|]; by auto. }
96
97
98
    apply later_mono, wand_intro_l. rewrite left_id const_equiv // left_id.
    by rewrite -later_intro.
  Unshelve.
Ralf Jung's avatar
Ralf Jung committed
99
  (* TODO Make it so that this becomes a goal, not shelved. *)
Ralf Jung's avatar
Ralf Jung committed
100
  { eexists; eauto. }
101
102
  Qed.

103
  Lemma wp_load N E γ l v P Q :
Ralf Jung's avatar
Ralf Jung committed
104
    nclose N  E 
105
106
    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
107
108
109
110
111
    P  wp E (Load (Loc l)) Q.
  Proof.
    intros HN. rewrite /heap_mapsto. apply wp_load_heap; first done.
    by simplify_map_equality.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164

  Lemma wp_store_heap N E γ σ l e v v' P Q :
    nclose N  E  to_val e = Some v  
    σ !! l = Some v' 
    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.
    rewrite /heap_ctx /heap_own. intros HN Hval Hl Hctx HP.
    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _ _) (alter (λ _, Excl v) l)).
    { eassumption. } { eassumption. }
    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_store_pst; first (apply sep_mono; first done); try eassumption; last first.
    { 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 const_equiv //; last first.
    (* 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.
    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 //.
  Unshelve.
  (* TODO Make it so that this becomes a goal, not shelved. *)
  { eexists; eauto. }
  Qed.

  Lemma wp_store N E γ l e v v' P Q :
    nclose N  E  to_val e = Some v  
    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.
    intros HN. rewrite /heap_mapsto=>Hval Hctx HP. eapply wp_store_heap; try eassumption; last first.
    - rewrite HP. apply sep_mono; first done. by rewrite insert_singleton.
    - by rewrite lookup_insert.
  Qed.
165
End heap.