heap.v 9.76 KB
Newer Older
1
2
3
4
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Ralf Jung's avatar
Ralf Jung committed
5
From iris.proofmode Require Import weakestpre.
6
7
8
9
10
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. *)

11
Definition heapR : cmraT := gmapR loc (fracR (dec_agreeR val)).
12

13
(** The CMRA we need. *)
14
Class heapG Σ := HeapG {
15
  heap_inG :> authG heap_lang Σ heapR;
16
17
  heap_name : gname
}.
18
(** The Functor we need. *)
19
Definition heapGF : gFunctor := authGF heapR.
20

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

25
26
Section definitions.
  Context `{i : heapG Σ}.
27

28
29
30
31
32
33
34
  Definition heap_mapsto (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
    auth_own heap_name {[ l := Frac q (DecAgree v) ]}.
  Definition heap_inv (h : heapR) : iPropG heap_lang Σ :=
    ownP (of_heap h).
  Definition heap_ctx (N : namespace) : iPropG heap_lang Σ :=
    auth_ctx heap_name N heap_inv.

35
  Global Instance heap_inv_proper : Proper (() ==> (⊣⊢)) heap_inv.
36
  Proof. solve_proper. Qed.
37
  Global Instance heap_ctx_persistent N : PersistentP (heap_ctx N).
38
39
40
  Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
41

Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
44
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.
45

46
Section heap.
47
  Context {Σ : gFunctors}.
48
  Implicit Types N : namespace.
49
50
  Implicit Types P Q : iPropG heap_lang Σ.
  Implicit Types Φ : val  iPropG heap_lang Σ.
51
  Implicit Types σ : state.
52
  Implicit Types h g : heapR.
53

54
  (** Conversion to heaps and back *)
55
  Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
56
  Proof. solve_proper. Qed.
57
  Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
58
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
    apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
  Qed.
  Lemma to_heap_valid σ :  to_heap σ.
62
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
  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 σ).
80
  Proof. by rewrite /to_heap -fmap_insert. Qed.
81
  Lemma of_heap_None h l :
Robbert Krebbers's avatar
Robbert Krebbers committed
82
     h  of_heap h !! l = None  h !! l = None  h !! l  Some FracUnit.
83
  Proof.
84
    move=> /(_ l). rewrite /of_heap lookup_omap.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    by case: (h !! l)=> [[q [v|]|]|] //=; destruct 1; auto.
86
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
89
  Lemma heap_store_valid l h v1 v2 :
     ({[l := Frac 1 (DecAgree v1)]}  h) 
     ({[l := Frac 1 (DecAgree v2)]}  h).
90
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
93
94
    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.
95
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  Hint Resolve heap_store_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
97

98
  (** Allocation *)
99
  Lemma heap_alloc N E σ :
100
    authG heap_lang Σ heapR  nclose N  E 
101
    ownP σ  (|={E}=>  _ : heapG Σ, heap_ctx N  Π★{map σ} (λ l v, l  v)).
Ralf Jung's avatar
Ralf Jung committed
102
  Proof.
103
    intros. rewrite -{1}(from_to_heap σ). etrans.
104
    { rewrite [ownP _]later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
      apply (auth_alloc (ownP  of_heap) N E); auto using to_heap_valid. }
106
    apply pvs_mono, exist_elim=> γ.
107
    rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r.
108
    rewrite /heap_mapsto /heap_name.
109
110
111
    induction σ as [|l v σ Hl IH] using map_ind.
    { rewrite big_sepM_empty; apply True_intro. }
    rewrite to_heap_insert big_sepM_insert //.
112
    rewrite (insert_singleton_op (to_heap σ));
Robbert Krebbers's avatar
Robbert Krebbers committed
113
      last by rewrite lookup_fmap Hl; auto.
114
    by rewrite auth_own_op IH.
Ralf Jung's avatar
Ralf Jung committed
115
  Qed.
Ralf Jung's avatar
Ralf Jung committed
116

117
118
119
  Context `{heapG Σ}.

  (** General properties of mapsto *)
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
122
  Global Instance heap_mapsto_timeless l q v : TimelessP (l {q} v).
  Proof. rewrite /heap_mapsto. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
123
  Lemma heap_mapsto_op_eq l q1 q2 v :
124
    (l {q1} v  l {q2} v) ⊣⊢ (l {q1+q2} v).
125
  Proof. by rewrite -auth_own_op op_singleton Frac_op dec_agree_idemp. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127

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

138
  Lemma heap_mapsto_op_split l q v :
139
    (l {q} v) ⊣⊢ (l {q/2} v  l {q/2} v).
140
141
  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.

142
  (** Weakest precondition *)
143
  Lemma wp_alloc N E e v Φ :
Ralf Jung's avatar
Ralf Jung committed
144
145
    to_val e = Some v  nclose N  E 
    (heap_ctx N    l, l  v - Φ (LitV $ LitLoc l))  WP Alloc e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
146
  Proof.
Ralf Jung's avatar
Ralf Jung committed
147
148
    iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
    iPvs (auth_empty heap_name) as "Hheap".
149
    (* TODO: change [auth_fsa] to single turnstile and use [iApply] *)
Ralf Jung's avatar
Ralf Jung committed
150
    apply (auth_fsa heap_inv (wp_fsa (Alloc e)))
151
      with N heap_name ; simpl; eauto with I.
Ralf Jung's avatar
Ralf Jung committed
152
153
154
155
156
157
158
    iFrame "Hheap". iIntros {h}. rewrite [  h]left_id.
    iIntros "[% Hheap]". rewrite /heap_inv.
    iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
    iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _.
    rewrite [{[ _ := _ ]}  ]right_id.
    rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
    iFrame "Hheap". iSplit.
159
160
    { iPureIntro; split; first done. by apply (insert_valid h). }
    iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
161
162
  Qed.

Ralf Jung's avatar
Ralf Jung committed
163
164
165
  Lemma wp_load N E l q v Φ :
    nclose N  E 
    (heap_ctx N   l {q} v   (l {q} v - Φ v))  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
166
  Proof.
Ralf Jung's avatar
Ralf Jung committed
167
    iIntros {?} "[#Hinv [Hmapsto HΦ]]". rewrite /heap_ctx /heap_mapsto.
168
    apply (auth_fsa' heap_inv (wp_fsa _) id)
Robbert Krebbers's avatar
Robbert Krebbers committed
169
      with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
Ralf Jung's avatar
Ralf Jung committed
170
171
172
    iFrame "Hmapsto". iIntros {h} "[% Hheap]". rewrite /heap_inv.
    iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
    rewrite of_heap_singleton_op //. iFrame "Hheap". iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
    iIntros "$". by iSplit.
Ralf Jung's avatar
Ralf Jung committed
174
175
  Qed.

176
  Lemma wp_store N E l v' e v P Φ :
177
    to_val e = Some v 
178
179
    P  heap_ctx N  nclose N  E 
    P  ( l  v'   (l  v - Φ (LitV LitUnit))) 
180
    P  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
181
  Proof.
182
    rewrite /heap_ctx /heap_inv=> ??? HPΦ.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
    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.
185
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
186
    rewrite -assoc; apply const_elim_sep_l=> ?.
187
    rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
    rewrite const_equiv; last naive_solver.
190
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Ralf Jung's avatar
Ralf Jung committed
191
192
  Qed.

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

210
  Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
Ralf Jung's avatar
Ralf Jung committed
211
    to_val e1 = Some v1  to_val e2 = Some v2 
212
213
    P  heap_ctx N  nclose N  E 
    P  ( l  v1   (l  v2 - Φ (LitV (LitBool true)))) 
214
    P  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
215
  Proof.
216
    rewrite /heap_ctx /heap_inv=> ???? HPΦ.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218
    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.
219
    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
220
    rewrite -assoc; apply const_elim_sep_l=> ?.
221
222
    rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
      last by rewrite lookup_insert.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
    rewrite lookup_insert const_equiv; last naive_solver.
225
    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Ralf Jung's avatar
Ralf Jung committed
226
  Qed.
227
End heap.