heap.v 14.6 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6
(** This file defines the basic points-to [↦] connectives for the Iron logic
instantiated with the heap_lang language. As a counter part to this, it defines
the state interpretation [heap_ctx]. *)
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iron.proofmode Require Export fracpred.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
From iris.algebra Require Import excl lib.frac_auth gmap agree gmultiset ufrac lib.ufrac_auth.
8
From iris.base_logic.lib Require Export own.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
From iron.iron_logic Require Export weakestpre.
10
From iron.heap_lang Require Export lang.
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12
Set Default Proof Using "Type".

13
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (agreeR valO)).
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17 18 19
Definition to_heap : gmap loc val  heapUR :=
  fmap (λ v, (1%Qp, to_agree v)).

(** The camera we need. *)
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
20
  heapG_inG :> inG Σ (ufrac_authR heapUR);
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22
  heapG_name : gname;
  heapG_fcinv_cinvG : cinvG Σ;
23
  heapG_fcinv_inG : inG Σ (frac_authR ufracR);
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  heapG_fork_post_name : gname;
25
  heapG_fork_postG :> inG Σ (authR (gmapUR positive (exclR (optionO ufracO))));
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28 29 30
}.
Arguments heapG_name {_} _ : assert.
Arguments heapG_fork_post_name {_} _ : assert.

Definition heap_perm `{hG : heapG Σ} (π : frac) : iProp Σ :=
31
  own (heapG_name hG) (U{π} ε).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Instance perm_fractional `{hG : heapG Σ} : Fractional heap_perm.
33
Proof. intros π1 π2. by rewrite -own_op -ufrac_auth_frag_op left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36 37 38 39 40

Definition heapG_ironInvG `{hG : heapG Σ} : ironInvG Σ := {|
  perm := heap_perm;
  fcinv_cinvG := heapG_fcinv_cinvG;
  fcinv_inG := heapG_fcinv_inG;
|}.

41
Definition heap_ctx `{hG : heapG Σ} (σ : state) (n : nat) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
  ( πfs,
     size πfs = n  
44
    own (heapG_fork_post_name hG) ( (Excl <$> πfs : gmap _ (excl (option ufrac)))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
45
    let πf : option fracR := [^op map] π  πfs, π in
46
    own (heapG_name hG) (U{1%Qp ? πf} (to_heap σ)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49 50 51 52 53 54 55
Definition heap_fork_post `{hG : heapG Σ} : iProp Σ :=
  ( i π,
    from_option heap_perm True π 
    own (heapG_fork_post_name hG) ( ({[ i := Excl π ]})))%I.
Arguments heap_ctx : simpl never.

Instance heapG_ironG `{hG : heapG Σ} : ironG heap_lang Σ := {|
  iron_invG := heapG_invG;
  iron_iron_invG := heapG_ironInvG;
56
  iron_state_interp σ _ := heap_ctx σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58 59 60 61 62 63 64
  iron_fork_post _ := heap_fork_post;
|}.

Section definitions.
  Context `{hG : heapG Σ}.

  Definition mapsto_def (l : loc) (q : Qp) (v : val) : ironProp Σ :=
    FracPred (from_option
65
      (λ π, own (heapG_name hG) (U{π} {[ l := (q, to_agree v) ]}))
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
      False)%I.
  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
  Definition mapsto := mapsto_aux.(unseal).
  Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
End definitions.

Notation "l ↦{ q } v" := (mapsto l q v%V)
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
Notation "l ↦ v" := (mapsto l 1 v)
  (at level 20, format "l  ↦  v") : bi_scope.

Notation "l ↦{ q } -" := ( v, l {q} v)%I
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I
  (at level 20, format "l  ↦  -") : bi_scope.

Section to_heap.
  Implicit Types σ : gmap loc val.
  Implicit Types v : val.

  (** Conversion to heaps and back *)
  Lemma to_heap_valid σ :  to_heap σ.
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
  Lemma lookup_to_heap_None σ l : σ !! l = None  to_heap σ !! l = None.
  Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
  Lemma heap_singleton_included σ l q v :
    {[l := (q, to_agree v)]}  to_heap σ  σ !! l = Some v.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
    rewrite singleton_included_l=> -[[q' av] []].
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97 98 99 100
    rewrite /to_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
    move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
  Qed.
  Lemma to_heap_empty : to_heap  = .
  Proof. by rewrite /to_heap fmap_empty. Qed.
  Lemma to_heap_insert l v σ :
101
    to_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizO val))]> (to_heap σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
  Proof. by rewrite /to_heap fmap_insert. Qed.
  Lemma to_heap_delete l σ :
    to_heap (delete l σ) = delete l (to_heap σ).
  Proof. by rewrite /to_heap fmap_delete. Qed.
  Global Instance to_heap_inj : Inj (=) () to_heap.
  Proof.
    intros σ1 σ2. rewrite /to_heap=> Hσ. apply map_eq=> i.
    move: Hσ=> /(_ i). rewrite !lookup_fmap.
    case: (σ1 !! i)=> [v|]; case: (σ2 !! i)=> [v'|] /=; try by inversion 1.
    rewrite (inj_iff Some)=> -[_] /=.
    by rewrite (inj_iff to_agree) leibniz_equiv_iff=> ->.
  Qed.
End to_heap.

Section heap.
  Context `{heapG Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
  Implicit Types σ : gmap loc val.
  Implicit Types l : loc.
  Implicit Types v : val.

  (** General properties of mapsto *)
  Global Instance mapsto_uniform l q v : Uniform (l {q} v).
  Proof.
    intros π1 π2. rewrite mapsto_eq /perm /mapsto_def /=.
128
    by rewrite -own_op -ufrac_auth_frag_op right_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  Qed.
  Global Instance mapsto_exist_perm l q v : ExistPerm (l {q} v).
  Proof. by rewrite /ExistPerm mapsto_eq. Qed.

  Global Instance mapsto_timeless l q v : Timeless (l {q} v).
  Proof. apply fracPred_at_timeless_alt. rewrite mapsto_eq. apply _. Qed.

  Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
  Proof.
    intros p q. rewrite mapsto_eq /mapsto_def.
    iStartProof (iProp _); iIntros ([π|]) "/=".
    - iSplit.
      + iIntros "[??]". iExists (Some (π / 2)%Qp), (Some (π / 2)%Qp).	 iFrame.
        by rewrite -Some_op frac_op' Qp_div_2.
      + iDestruct 1 as ([?|] [?|] Hπ) "[H1 H2]"; simpl; try done.
        move: Hπ. rewrite -Some_op. intros [=->]. by iSplitL "H1".
    - iSplit; first by iIntros "[]". by iDestruct 1 as ([?|] [?|] ?) "[??]".
  Qed.
  Global Instance mapsto_as_fractional l q v :
    AsFractional (l {q} v) (λ q, l {q} v)%I q.
  Proof. split. done. apply _. Qed.

  Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
  Proof.
    iStartProof (iProp _). rewrite mapsto_eq /mapsto_def /=.
    iIntros ([π1|]) "H1"; iIntros ([π2|]) "H2 //=".
    iDestruct (own_valid_2 with "H1 H2") as %Hv.
156
    move: Hv. rewrite -ufrac_auth_frag_op ufrac_auth_frag_valid=>Hv.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
    move: Hv. rewrite op_singleton singleton_valid -pair_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175
    by intros [_ ?%agree_op_invL'].
  Qed.

  Global Instance ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
  Proof.
    intros p q. iSplit.
    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
      iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
  Qed.
  Global Instance ex_mapsto_as_fractional l q :
    AsFractional (l {q} -) (λ q, l {q} -)%I q.
  Proof. split. done. apply _. Qed.

  Lemma mapsto_valid l q v : l {q} v -   q .
  Proof.
    iStartProof (iProp _). rewrite mapsto_eq /mapsto_def /=.
    iIntros ([π1|]) "H1 //=". iDestruct (own_valid with "H1") as %Hv.
176
    move: Hv. rewrite ufrac_auth_frag_valid=> Hv.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
    move: Hv. by rewrite singleton_valid=> -[? _].
  Qed.
  Lemma mapsto_valid_2 l q1 q2 v1 v2 :
    l {q1} v1 - l {q2} v2 -   (q1 + q2)%Qp .
  Proof.
    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
    iApply (mapsto_valid l _ v2). by iFrame.
  Qed.

  Lemma big_mapsto_None σ :
    ([ map] l  v  σ, l  v) None   σ =  .
  Proof.
    iIntros "Hσ". destruct (decide (σ = )); first done.
    destruct (map_choose σ) as (k & w & ?); first done.
    rewrite big_sepM_lookup_acc; last done. rewrite fracPred_at_sep.
    by iDestruct "Hσ" as ([π3|] [π4|] ?) "[? _]".
  Qed.
  Lemma big_mapsto_alt_1 σ π :
195
    ([ map] l  v  σ, l  v) (Some π)  own (heapG_name H) (U{π} (to_heap σ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197 198 199 200 201 202 203 204 205 206 207
  Proof.
    revert π. induction σ as [|l v σ Hl IH] using map_ind=> π.
    { rewrite big_sepM_empty fracPred_at_emp. iIntros ([=]). }
    rewrite big_sepM_insert // to_heap_insert fracPred_at_sep.
    rewrite insert_singleton_op; last by apply lookup_to_heap_None.
    iDestruct 1 as ([π1|] [π2|] Hπ) "[Hl Hσ]"=>//.
    - rewrite IH // mapsto_eq. apply (inj Some) in Hπ as ->. by iSplitL "Hl".
    - iDestruct (big_mapsto_None with "Hσ") as %->. apply (inj Some) in Hπ as ->.
      by rewrite to_heap_empty right_id mapsto_eq.
  Qed.
  Lemma big_mapsto_alt_2 σ π :
    σ   
208
    own (heapG_name H) (U{π} (to_heap σ))  ([ map] l  v  σ, l  v) (Some π).
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210 211 212 213 214 215 216 217 218 219 220
  Proof.
    revert π. induction σ as [|l v σ Hl IH] using map_ind; [done|intros π _].
    rewrite to_heap_insert. destruct (decide (σ = )) as [->|].
    { by rewrite to_heap_empty insert_empty big_sepM_singleton mapsto_eq. }
    rewrite big_sepM_insert // fracPred_at_sep.
    rewrite insert_singleton_op; last by apply lookup_to_heap_None.
    iIntros "[Hl Hh]". iExists (Some (π / 2))%Qp, (Some (π / 2))%Qp.
    iSplit; first by rewrite -Some_op frac_op' Qp_div_2.
    rewrite IH // mapsto_eq. by iSplitL "Hl".
  Qed.

  (* heap_ctx manipulating lemmas *)
221
  Lemma heap_thread_adequacy σ n π1 π2 σ' :
Robbert Krebbers's avatar
Robbert Krebbers committed
222
    π1 ? π2 = 1%Qp 
223
    heap_ctx σ n -
Robbert Krebbers's avatar
Robbert Krebbers committed
224 225 226 227 228 229
    [] replicate n heap_fork_post -
    heap_perm π1 -
    ([ map] lv  σ', l  v) π2 ==
     σ = σ' .
  Proof.
    iIntros (Hπ). iDestruct 1 as (πfs <-) "[Hn Hσ]". iIntros "HQs Hp Hσ'".
230
    iAssert (own (heapG_name H) (U{1%Qp ? ([^op map] π  πfs, π)} (to_heap σ')))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
231
      with "[> Hn HQs Hp Hσ']" as "Hσ'"; last first.
232
    { by iDestruct (own_valid_2 with "Hσ Hσ'") as %?%ufrac_auth_agree%(inj _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
233 234 235 236 237 238 239 240 241 242 243
    iInduction (map_wf πfs) as [πfs _] "IH".
    destruct (size πfs) as [|m'] eqn:Hsize; simpl.
    { apply map_size_empty_iff in Hsize as ->.
      rewrite big_opM_empty /=. destruct π2 as [π2|]; simpl in *; last first.
      - iDestruct (big_mapsto_None with "Hσ'") as %->.
        by rewrite to_heap_empty -Hπ.
      - iDestruct (big_mapsto_alt_1 with "Hσ'") as "Hσ'".
        iCombine "Hp Hσ'" as "Hσ'". by rewrite left_id Hπ. }
    iDestruct "HQs" as "[HQ HQs]". iDestruct "HQ" as (j π) "[Hp' Hj]".
    iAssert  πfs !! j = Some π %I as %Hj.
    { iDestruct (own_valid_2 with "Hn Hj")
Robbert Krebbers's avatar
Robbert Krebbers committed
244
        as %[Hj%singleton_included_l Hvalid]%auth_both_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263
      destruct Hj as (eπ'&Hj%leibniz_equiv&[[=]|(?&?&[= <-]&[= <-]&Heπ)]%option_included).
      destruct Heπ as [<-%leibniz_equiv|Hincl]; last first.
      { exfalso. move: (Hvalid j). rewrite Hj. destruct eπ'=> //.
        by destruct Hincl as [[] ?%leibniz_equiv]. }
      move: Hj; rewrite lookup_fmap fmap_Some=> -[π' [Hj ?]]; by simplify_eq. }
    rewrite (big_opM_delete (o:=op) _ πfs) //.
    iMod (own_update_2 with "Hn Hj") as "Hn".
    { apply auth_update_dealloc, delete_singleton_local_update, _. }
    rewrite -fmap_delete.
    iMod ("IH" with "[%] Hn [HQs] Hp Hσ'") as "Hσ'".
    { apply delete_subset; eauto. }
    { replace m' with (size (delete j πfs)); first done.
      apply (inj S). rewrite -Hsize -{2}(insert_id πfs j π) // -insert_delete.
      by rewrite map_size_insert ?lookup_delete. }
    destruct π as [π|]; last by rewrite left_id_L.
    iCombine "Hp' Hσ'" as "Hσ'". rewrite left_id.
    by rewrite -cmra_opM_opM_assoc_L /= -(comm_L _ π) cmra_op_opM_assoc_L.
  Qed.

264 265 266
  Lemma heap_thread_alloc σ n π :
    heap_ctx σ n ==  i,
      heap_ctx σ (S n) 
Robbert Krebbers's avatar
Robbert Krebbers committed
267 268 269 270 271
      from_option perm True π 
      own (heapG_fork_post_name _) ( {[ i := Excl π ]}).
  Proof.
    iDestruct 1 as (πfs Hsize) "[Hn Hσ]".
    set (i := fresh (dom (gset positive) πfs)).
272
    assert (πfs !! i = None) by (by eapply (not_elem_of_dom (D:=gset positive)), is_fresh).
Robbert Krebbers's avatar
Robbert Krebbers committed
273 274 275 276 277 278 279 280 281
    iMod (own_update with "Hn") as "[Hn Hi]".
    { apply auth_update_alloc, (alloc_singleton_local_update _ i (Excl π))=> //.
      by rewrite lookup_fmap fmap_None. }
    iExists i. iFrame "Hi".
    destruct π as [π|]; last first.
    { iModIntro. iSplitL=> //. iExists (<[i:=None]> πfs).
      iSplit; first (by rewrite map_size_insert // Hsize).
      rewrite fmap_insert. iFrame "Hn". by rewrite big_opM_insert // left_id. }
    iMod (own_update with "Hσ") as "[Hσ Hp]".
282
    { apply (ufrac_auth_update_surplus _ π _ (ε : heapUR)).
Robbert Krebbers's avatar
Robbert Krebbers committed
283 284 285 286 287 288 289
      rewrite right_id. apply to_heap_valid. }
    rewrite right_id. iModIntro. iFrame "Hp".
    iExists (<[i:=Some π]> πfs). iSplit; first (by rewrite map_size_insert // Hsize).
    rewrite big_opM_insert // (comm op).
    rewrite -cmra_opM_opM_assoc_L fmap_insert. iFrame.
  Qed.

290
  Lemma heap_alloc σ n l v π :
Robbert Krebbers's avatar
Robbert Krebbers committed
291
    σ !! l = None 
292 293
    heap_ctx σ n - perm π ==
    heap_ctx (<[l:=v]>σ) n  (l  v) (Some π).
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295 296 297
  Proof.
    iIntros (?). rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
    iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hp".
    iMod (own_update_2 with "Hσ Hp") as "[Hσ Hl]".
298
    { eapply ufrac_auth_update,
299
        (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizO _))) => //.
Robbert Krebbers's avatar
Robbert Krebbers committed
300 301 302 303
      by apply lookup_to_heap_None. }
    iModIntro. iFrame "Hl". iExists πfs. rewrite to_heap_insert. by iFrame.
  Qed.

304 305 306
  Lemma heap_dealloc σ n l v π :
    heap_ctx σ n - (l  v) (Some π) ==
    heap_ctx (delete l σ) n  perm π.
Robbert Krebbers's avatar
Robbert Krebbers committed
307 308 309 310
  Proof.
    rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
    iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl".
    iDestruct (own_valid_2 with "Hσ Hl")
311
      as %Hl%ufrac_auth_included_total%heap_singleton_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
312
    rewrite to_heap_delete. iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
313
    { eapply ufrac_auth_update,
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315 316 317 318
        (delete_singleton_local_update_cancelable _ _ _).
      by rewrite /to_heap lookup_fmap Hl. }
    iModIntro. iFrame "Hl". iExists πfs. by iFrame.
  Qed.

319 320
  Lemma heap_valid σ n l q v π :
    heap_ctx σ n - (l {q} v) π - ⌜σ !! l = Some v.
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322 323 324
  Proof.
    rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
    iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl". destruct π as [π|]=>//.
    by iDestruct (own_valid_2 with "Hσ Hl")
325
      as %Hl%ufrac_auth_included%Some_included_total%heap_singleton_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
326 327
  Qed.

328 329 330
  Lemma heap_update σ n l v1 v2 π :
    heap_ctx σ n - (l  v1) π ==
    heap_ctx (<[l:=v2]>σ) n  (l  v2) π.
Robbert Krebbers's avatar
Robbert Krebbers committed
331 332 333 334
  Proof.
    rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
    iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl". destruct π as [π|]=>//.
    iDestruct (own_valid_2 with "Hσ Hl")
335
      as %Hl%ufrac_auth_included%Some_included_total%heap_singleton_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
337
    { eapply ufrac_auth_update, singleton_local_update,
Robbert Krebbers's avatar
Robbert Krebbers committed
338 339 340 341 342
        (exclusive_local_update _ (1%Qp, to_agree v2))=> //.
      by rewrite /to_heap lookup_fmap Hl. }
    iModIntro. iFrame "Hl". iExists πfs. rewrite to_heap_insert. by iFrame.
  Qed.
End heap.