heap.v 8.03 KB
Newer Older
1
From iris.heap_lang Require Export lifting.
2
From iris.algebra Require Import auth gmap frac dec_agree.
3 4
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import wsat auth.
5
From iris.proofmode Require Import tactics.
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 heapN : namespace := nroot .@ "heap".
12
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
13

14
(** The CMRA we need. *)
15
Class heapG Σ := HeapG {
16
  heapG_iris_inG :> irisG heap_lang Σ;
17
  heap_inG :> authG Σ heapUR;
18 19
  heap_name : gname
}.
20

21
Definition to_heap : state  heapUR := fmap (λ v, (1%Qp, DecAgree v)).
22

23
Section definitions.
24
  Context `{heapG Σ}.
25

26
  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
27
    auth_own heap_name ({[ l := (q, DecAgree v) ]}).
28 29 30 31 32
  Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
  Definition heap_mapsto := proj1_sig heap_mapsto_aux.
  Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
    proj2_sig heap_mapsto_aux.

33
  Definition heap_ctx : iProp Σ := auth_ctx heap_name heapN to_heap ownP.
34
End definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
35

36
Typeclasses Opaque heap_ctx heap_mapsto.
37

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

Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44 45
Notation "l ↦{ q } -" := ( v, l {q} v)%I
  (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.

46
Section heap.
47
  Context {Σ : gFunctors}.
48 49
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
50
  Implicit Types σ : state.
51
  Implicit Types h g : heapUR.
52

53
  (** Conversion to heaps and back *)
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  Lemma to_heap_valid σ :  to_heap σ.
55
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
56 57 58 59
  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, DecAgree v)]}  to_heap σ  σ !! l = Some v.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  Proof.
61 62 63
    rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
    move: Hl. rewrite /to_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
    by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  Qed.
65 66
  Lemma heap_singleton_included' σ l q v :
    {[l := (q, DecAgree v)]}  to_heap σ  to_heap σ !! l = Some (1%Qp,DecAgree v).
67
  Proof.
68
    intros Hl%heap_singleton_included. by rewrite /to_heap lookup_fmap Hl.
69
  Qed.
70 71 72
  Lemma to_heap_insert l v σ :
    to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
  Proof. by rewrite /to_heap fmap_insert. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73

74 75 76
  Context `{heapG Σ}.

  (** General properties of mapsto *)
77 78
  Global Instance heap_ctx_persistent : PersistentP heap_ctx.
  Proof. rewrite /heap_ctx. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  Global Instance heap_mapsto_timeless l q v : TimelessP (l {q} v).
80
  Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
81

82
  Lemma heap_mapsto_op_eq l q1 q2 v : l {q1} v  l {q2} v  l {q1+q2} v.
83
  Proof.
84
    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
85
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87

  Lemma heap_mapsto_op l q1 q2 v1 v2 :
88
    l {q1} v1  l {q2} v2  v1 = v2  l {q1+q2} v1.
89
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
    destruct (decide (v1 = v2)) as [->|].
91 92
    { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
    apply (anti_symm ()); last by apply pure_elim_l.
93 94
    rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
    eapply pure_elim; [done|] =>  /=.
95
    rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
96 97
  Qed.

98 99 100 101 102 103 104 105 106 107 108
  Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
    l {q1} v1  l {q2} v2  v1 = v2  l {q1+q2} v1.
  Proof. by rewrite heap_mapsto_op. Qed.

  Lemma heap_mapsto_op_half l q v1 v2 :
    l {q/2} v1  l {q/2} v2  v1 = v2  l {q} v1.
  Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.

  Lemma heap_mapsto_op_half_1 l q v1 v2 :
    l {q/2} v1  l {q/2} v2  v1 = v2  l {q} v1.
  Proof. by rewrite heap_mapsto_op_half. Qed.
109

Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112 113 114 115 116 117 118 119 120 121
  Lemma heap_ex_mapsto_op l q1 q2 : l {q1} -  l {q2} -  l {q1+q2} -.
  Proof.
    iSplit.
    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
      iDestruct (heap_mapsto_op_1 with "[$H1 $H2]") as "[% ?]"; subst; eauto.
    - iDestruct 1 as (v) "H". rewrite -heap_mapsto_op_eq.
      iDestruct "H" as "[H1 H2]"; iSplitL "H1"; eauto.
  Qed.

  Lemma heap_ex_mapsto_op_half l q : l {q/2} -  l {q/2} -  l {q} -.
  Proof. by rewrite heap_ex_mapsto_op Qp_div_2. Qed.

122
  (** Weakest precondition *)
Ralf Jung's avatar
Ralf Jung committed
123
  Lemma wp_alloc E e v :
124
    to_val e = Some v  nclose heapN  E 
125
    {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l  v }}}.
Ralf Jung's avatar
Ralf Jung committed
126
  Proof.
Ralf Jung's avatar
Ralf Jung committed
127
    iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
128 129
    iMod (auth_empty heap_name) as "Ha".
    iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
Ralf Jung's avatar
Ralf Jung committed
130
    iApply (wp_alloc_pst with "Hσ"). iNext. iIntros (l) "[% Hσ]".
131
    iMod ("Hcl" with "* [Hσ]") as "Ha".
132 133
    { iFrame. iPureIntro. rewrite to_heap_insert.
      eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
134
    iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
135 136
  Qed.

Ralf Jung's avatar
Ralf Jung committed
137
  Lemma wp_load E l q v :
138
    nclose heapN  E 
Ralf Jung's avatar
Ralf Jung committed
139
    {{{ heap_ctx   l {q} v }}} Load (Lit (LitLoc l)) @ E
140
    {{{ RET v; l {q} v }}}.
Ralf Jung's avatar
Ralf Jung committed
141
  Proof.
Ralf Jung's avatar
Ralf Jung committed
142
    iIntros (? Φ) "[#Hinv >Hl] HΦ".
143
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
144
    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
Ralf Jung's avatar
Ralf Jung committed
145 146
    iApply (wp_load_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
    iNext; iIntros "Hσ".
147
    iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
148 149
  Qed.

Ralf Jung's avatar
Ralf Jung committed
150
  Lemma wp_store E l v' e v :
151
    to_val e = Some v  nclose heapN  E 
Ralf Jung's avatar
Ralf Jung committed
152
    {{{ heap_ctx   l  v' }}} Store (Lit (LitLoc l)) e @ E
153
    {{{ RET LitV LitUnit; l  v }}}.
Ralf Jung's avatar
Ralf Jung committed
154
  Proof.
Ralf Jung's avatar
Ralf Jung committed
155
    iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
156
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
157
    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
Ralf Jung's avatar
Ralf Jung committed
158 159
    iApply (wp_store_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
    iNext; iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
160 161
    { iFrame. iPureIntro. rewrite to_heap_insert.
      eapply singleton_local_update, exclusive_local_update; last done.
162
      by eapply heap_singleton_included'. }
163
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
164 165
  Qed.

Ralf Jung's avatar
Ralf Jung committed
166
  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
167
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1  nclose heapN  E 
Ralf Jung's avatar
Ralf Jung committed
168
    {{{ heap_ctx   l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
169
    {{{ RET LitV (LitBool false); l {q} v' }}}.
Ralf Jung's avatar
Ralf Jung committed
170
  Proof.
Ralf Jung's avatar
Ralf Jung committed
171
    iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ".
172
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
173
    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
Ralf Jung's avatar
Ralf Jung committed
174 175
    iApply (wp_cas_fail_pst _ σ with "Hσ"); [eauto using heap_singleton_included|done|].
    iNext; iIntros "Hσ".
176
    iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
177
  Qed.
Ralf Jung's avatar
Ralf Jung committed
178

Ralf Jung's avatar
Ralf Jung committed
179
  Lemma wp_cas_suc E l e1 v1 e2 v2 :
180
    to_val e1 = Some v1  to_val e2 = Some v2  nclose heapN  E 
Ralf Jung's avatar
Ralf Jung committed
181
    {{{ heap_ctx   l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
182
    {{{ RET LitV (LitBool true); l  v2 }}}.
Ralf Jung's avatar
Ralf Jung committed
183
  Proof.
Ralf Jung's avatar
Ralf Jung committed
184
    iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
185
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
186
    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
Ralf Jung's avatar
Ralf Jung committed
187 188
    iApply (wp_cas_suc_pst _ σ with "Hσ"); first by eauto using heap_singleton_included.
    iNext. iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
189 190
    { iFrame. iPureIntro. rewrite to_heap_insert.
      eapply singleton_local_update, exclusive_local_update; last done.
191
      by eapply heap_singleton_included'. }
192
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
193
  Qed.
194
End heap.