heap.v 7.44 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.program_logic Require Export invariants ghost_ownership.
4
From iris.program_logic Require Import ownership 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

42
Section heap.
43
  Context {Σ : gFunctors}.
44 45
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
46
  Implicit Types σ : state.
47
  Implicit Types h g : heapUR.
48

49
  (** Conversion to heaps and back *)
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  Lemma to_heap_valid σ :  to_heap σ.
51
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
52 53 54 55
  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
56
  Proof.
57 58 59
    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
60
  Qed.
61 62
  Lemma heap_singleton_included' σ l q v :
    {[l := (q, DecAgree v)]}  to_heap σ  to_heap σ !! l = Some (1%Qp,DecAgree v).
63
  Proof.
64
    intros Hl%heap_singleton_included. by rewrite /to_heap lookup_fmap Hl.
65
  Qed.
66 67 68
  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
69

70 71 72
  Context `{heapG Σ}.

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

78
  Lemma heap_mapsto_op_eq l q1 q2 v : l {q1} v  l {q2} v  l {q1+q2} v.
79
  Proof.
80
    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
81
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83

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

94 95 96 97 98 99 100 101 102 103 104
  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.
105

106
  (** Weakest precondition *)
107 108 109
  Lemma wp_alloc E e v Φ :
    to_val e = Some v  nclose heapN  E 
    heap_ctx   ( l, l  v ={E}= Φ (LitV (LitLoc l)))  WP Alloc e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
110
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
    iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113
    iVs (auth_empty heap_name) as "Ha".
    iVs (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
114
    iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>".
Robbert Krebbers's avatar
Robbert Krebbers committed
115
    iVs ("Hcl" with "* [Hσ]") as "Ha".
116 117
    { iFrame. iPureIntro. rewrite to_heap_insert.
      eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
118
    iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
119 120
  Qed.

121 122 123
  Lemma wp_load E l q v Φ :
    nclose heapN  E 
    heap_ctx   l {q} v   (l {q} v ={E}= Φ v)
124
     WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
125
  Proof.
126
    iIntros (?) "[#Hinv [>Hl HΦ]]".
127
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
129
    iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
131
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
132 133
  Qed.

134 135 136
  Lemma wp_store E l v' e v Φ :
    to_val e = Some v  nclose heapN  E 
    heap_ctx   l  v'   (l  v ={E}= Φ (LitV LitUnit))
137
     WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
138
  Proof.
139
    iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
140
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
142
    iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
144 145
    { iFrame. iPureIntro. rewrite to_heap_insert.
      eapply singleton_local_update, exclusive_local_update; last done.
146
      by eapply heap_singleton_included'. }
147
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
148 149
  Qed.

150 151 152
  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2  v'  v1  nclose heapN  E 
    heap_ctx   l {q} v'   (l {q} v' ={E}= Φ (LitV (LitBool false)))
153
     WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
154
  Proof.
155
    iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
156
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
158
    iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
159
    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
160
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
161
  Qed.
Ralf Jung's avatar
Ralf Jung committed
162

163 164 165
  Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
    to_val e1 = Some v1  to_val e2 = Some v2  nclose heapN  E 
    heap_ctx   l  v1   (l  v2 ={E}= Φ (LitV (LitBool true)))
166
     WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
167
  Proof.
168
    iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
169
    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
171
    iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
173 174
    { iFrame. iPureIntro. rewrite to_heap_insert.
      eapply singleton_local_update, exclusive_local_update; last done.
175
      by eapply heap_singleton_included'. }
176
    by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
177
  Qed.
178
End heap.