heap.v 7.99 KB
Newer Older
1
From iris.heap_lang Require Export lifting.
2
From iris.algebra Require Import auth gmap frac dec_agree.
3
From iris.base_logic.lib Require Export invariants.
4 5
From iris.base_logic.lib Require Import fractional.
From iris.program_logic Require Import ectx_lifting.
6
From iris.proofmode Require Import tactics.
7 8 9 10 11
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. *)

12
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
13
Definition to_heap : state  heapUR := fmap (λ v, (1%Qp, DecAgree v)).
14

15
(** The CMRA we need. *)
16
Class heapG Σ := HeapG {
17 18
  heapG_invG : invG Σ;
  heap_inG :> inG Σ (authR heapUR);
19 20
  heap_name : gname
}.
21 22 23 24
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
  state_interp σ := own heap_name ( to_heap σ)
}.
25

26
Section definitions.
27
  Context `{heapG Σ}.
28

29
  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
30
    own heap_name ( {[ l := (q, DecAgree v) ]}).
31 32 33 34
  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.
35
End definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

37
Typeclasses Opaque heap_mapsto.
38

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

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

47 48 49 50 51
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.

52
Section heap.
53
  Context {Σ : gFunctors}.
54 55
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
56
  Implicit Types σ : state.
57
  Implicit Types h g : heapUR.
58

59
  (** Conversion to heaps and back *)
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  Lemma to_heap_valid σ :  to_heap σ.
61
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
62 63 64 65
  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
66
  Proof.
67 68 69
    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
70
  Qed.
71 72 73
  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
74

75 76 77
  Context `{heapG Σ}.

  (** General properties of mapsto *)
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  Global Instance heap_mapsto_timeless l q v : TimelessP (l {q} v).
79
  Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
80
  Global Instance heap_mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
81
  Proof.
82 83
    intros p q. by rewrite heap_mapsto_eq -own_op -auth_frag_op
      op_singleton pair_op dec_agree_idemp.
84
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
85 86 87
  Global Instance heap_mapsto_as_fractional l q v :
    AsFractional (l {q} v) (λ q, l {q} v)%I q.
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
88

89
  Lemma heap_mapsto_agree l q1 q2 v1 v2 : l {q1} v1  l {q2} v2  v1 = v2.
90
  Proof.
91 92 93
    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
    f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
    by move=> [_ /= /dec_agree_op_inv [?]].
94 95
  Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
96
  Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
98 99
    intros p q. iSplit.
    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
101
      iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->. iExists v2. by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
103 104 105
  Global Instance heap_ex_mapsto_as_fractional l q :
    AsFractional (l {q} -) (λ q, l {q} -)%I q.
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
106

107 108
  Lemma heap_mapsto_valid l q v : l {q} v   q.
  Proof.
109 110
    rewrite heap_mapsto_eq /heap_mapsto_def own_valid !discrete_valid.
    by apply pure_mono=> /auth_own_valid /singleton_valid [??].
111 112 113
  Qed.
  Lemma heap_mapsto_valid_2 l q1 q2 v1 v2 :
    l {q1} v1  l {q2} v2   (q1 + q2)%Qp.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
114 115 116 117
  Proof.
    iIntros "[H1 H2]". iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->.
    iApply (heap_mapsto_valid l _ v2). by iFrame.
  Qed.
118

119
  (** Weakest precondition *)
Ralf Jung's avatar
Ralf Jung committed
120
  Lemma wp_alloc E e v :
121 122
    to_val e = Some v 
    {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l  v }}}.
Ralf Jung's avatar
Ralf Jung committed
123
  Proof.
124 125 126 127 128 129 130 131
    iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>"; iSplit; first by auto.
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
    iMod (own_update with "Hσ") as "[Hσ Hl]".
    { eapply auth_update_alloc,
        (alloc_singleton_local_update _ _ (1%Qp, DecAgree _))=> //.
      by apply lookup_to_heap_None. }
    iModIntro; iSplit=> //. rewrite to_heap_insert. iFrame.
132
    iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
133 134
  Qed.

Ralf Jung's avatar
Ralf Jung committed
135
  Lemma wp_load E l q v :
136
    {{{  l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l {q} v }}}.
Ralf Jung's avatar
Ralf Jung committed
137
  Proof.
138 139 140 141 142 143 144
    iIntros (Φ) ">Hl HΦ". rewrite heap_mapsto_eq /heap_mapsto_def.
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
      as %[?%heap_singleton_included _]%auth_valid_discrete_2.
    iSplit; first by eauto.
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
145 146
  Qed.

Ralf Jung's avatar
Ralf Jung committed
147
  Lemma wp_store E l v' e v :
148 149
    to_val e = Some v 
    {{{  l  v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l  v }}}.
Ralf Jung's avatar
Ralf Jung committed
150
  Proof.
151 152 153 154 155 156 157 158 159 160 161
    iIntros (<-%of_to_val Φ) ">Hl HΦ". rewrite heap_mapsto_eq /heap_mapsto_def.
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
      as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
    iSplit; first by eauto.
    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
    iMod (own_update_2 with "Hσ Hl") as "[Hσ1 Hl]".
    { eapply auth_update, singleton_local_update,
        (exclusive_local_update _ (1%Qp, DecAgree _))=> //.
      by rewrite /to_heap lookup_fmap Hl. }
    iModIntro. iSplit=>//. rewrite to_heap_insert. iFrame. by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
162 163
  Qed.

Ralf Jung's avatar
Ralf Jung committed
164
  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
165 166
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
    {{{  l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
167
    {{{ RET LitV (LitBool false); l {q} v' }}}.
Ralf Jung's avatar
Ralf Jung committed
168
  Proof.
169 170 171 172 173 174 175 176
    iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
    rewrite heap_mapsto_eq /heap_mapsto_def.
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
      as %[?%heap_singleton_included _]%auth_valid_discrete_2.
    iSplit; first by eauto.
    iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. (* FIXME: this inversion is slow *)
    iModIntro; iSplit=> //. iFrame. 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 181
    to_val e1 = Some v1  to_val e2 = Some v2 
    {{{  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.
184 185 186 187 188 189 190 191 192 193 194 195
    iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
    rewrite heap_mapsto_eq /heap_mapsto_def.
    iApply wp_lift_atomic_head_step_no_fork; auto.
    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
      as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
    iSplit; first by eauto.
    iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
    iMod (own_update_2 with "Hσ Hl") as "[Hσ1 Hl]".
    { eapply auth_update, singleton_local_update,
        (exclusive_local_update _ (1%Qp, DecAgree _))=> //.
      by rewrite /to_heap lookup_fmap Hl. }
    iModIntro. iSplit=>//. rewrite to_heap_insert. iFrame. by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
196
  Qed.
197
End heap.