-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathheap_lang_lifting.v
228 lines (205 loc) · 8.61 KB
/
heap_lang_lifting.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
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
94
95
96
97
98
99
100
101
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
128
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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
From iris.base_logic Require Export gen_heap.
From iris_ni.program_logic Require Export dwp classes ectx_lifting.
From iris_ni.program_logic Require Export dwp classes.
From iris.heap_lang Require Export lang notation.
From iris.heap_lang Require Import tactics proofmode.
From iris.proofmode Require Import proofmode.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
Class heapDG Σ := HeapDG {
heapDG_invG :> invGS Σ;
heapDG_proph_mapG1 :> proph_mapGS proph_id (val*val) Σ;
heapDG_proph_mapG2 :> proph_mapGS proph_id (val*val) Σ;
heapDG_gen_heapG1 :> gen_heapGS loc (option val) Σ;
heapDG_gen_heapG2 :> gen_heapGS loc (option val) Σ;
heapDG_inv_heapG1 :> inv_heapGS loc (option val) Σ;
heapDG_inv_heapG2 :> inv_heapGS loc (option val) Σ;
}.
(** heapGS instanecs for both sides *)
Definition heapG1 `{heapDG Σ} : heapGS Σ :=
{| heapGS_invGS := heapDG_invG;
heapGS_gen_heapGS := heapDG_gen_heapG1;
heapGS_inv_heapGS := heapDG_inv_heapG1;
heapGS_proph_mapGS := heapDG_proph_mapG1 |}.
Definition heapG2 `{heapDG Σ} : heapGS Σ :=
{| heapGS_invGS := heapDG_invG;
heapGS_gen_heapGS := heapDG_gen_heapG2;
heapGS_inv_heapGS := heapDG_inv_heapG2;
heapGS_proph_mapGS := heapDG_proph_mapG2 |}.
(** irisGS instances for both sides *)
Definition irisG1 `{!heapDG Σ} : irisGS heap_lang Σ :=
@heapGS_irisGS Σ heapG1.
Definition irisG2 `{!heapDG Σ} : irisGS heap_lang Σ :=
@heapGS_irisGS Σ heapG2.
Definition TWP1 `{!heapDG Σ} (e : expr) (E : coPset) (R : val → iProp Σ) :=
@twp (iProp Σ) expr val stuckness
(@twp' heap_lang Σ irisG1)
NotStuck E e R.
Definition TWP2 `{!heapDG Σ} (e : expr) (E : coPset) (R : val → iProp Σ) :=
@twp (iProp Σ) expr val stuckness
(@twp' heap_lang Σ irisG2)
NotStuck E e R.
Definition mapsto1 `{!heapDG Σ} (l : loc) (q : Qp) (v : val) :=
@mapsto loc _ _ _ Σ heapDG_gen_heapG1 l (DfracOwn q) (Some v%V).
Definition mapsto2 `{!heapDG Σ} (l : loc) (q : Qp) (v : val) :=
@mapsto loc _ _ _ Σ heapDG_gen_heapG2 l (DfracOwn q) (Some v%V).
Notation "l ↦ₗ{ q } v" := (mapsto1 l q v%V)
(at level 20, q at level 50, format "l ↦ₗ{ q } v") : bi_scope.
Notation "l ↦ₗ v" :=
(mapsto1 l 1 v%V) (at level 20) : 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) : bi_scope.
Notation "l ↦ᵣ{ q } v" := (mapsto2 l q v%V)
(at level 20, q at level 50, format "l ↦ᵣ{ q } v") : bi_scope.
Notation "l ↦ᵣ v" :=
(mapsto2 l 1 v%V) (at level 20) : 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) : bi_scope.
Definition array1 `{heapDG Σ} (l : loc) (vs : list val) :=
([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ₗ v)%I.
Definition array2 `{heapDG Σ} (l : loc) (vs : list val) :=
([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ᵣ v)%I.
Notation "l ↦ₗ∗ vs" := (array1 l vs)
(at level 20, format "l ↦ₗ∗ vs") : bi_scope.
Notation "l ↦ᵣ∗ vs" := (array2 l vs)
(at level 20, format "l ↦ᵣ∗ vs") : bi_scope.
Definition meta1 `{heapDG Σ} {A} `{EqDecision A, Countable A}
(l : loc) (N : namespace) (x : A) :=
@meta loc _ _ _ Σ heapDG_gen_heapG1 A _ _ l N x.
Definition meta2 `{heapDG Σ} {A} `{EqDecision A, Countable A}
(l : loc) (N : namespace) (x : A) :=
@meta loc _ _ _ Σ heapDG_gen_heapG2 A _ _ l N x.
#[global] Instance heapDG_irisDG `{!heapDG Σ} : irisDG heap_lang Σ := {
state_rel := (λ σ1 σ2 κs1 κs2,
@gen_heap_interp _ _ _ _ _ heapDG_gen_heapG1 σ1.(heap)
∗ @proph_map_interp _ _ _ _ _ heapDG_proph_mapG1 κs1 σ1.(used_proph_id)
∗ @gen_heap_interp _ _ _ _ _ heapDG_gen_heapG2 σ2.(heap)
∗ @proph_map_interp _ _ _ _ _ heapDG_proph_mapG2 κs2 σ2.(used_proph_id))%I
}.
Section array_liftings.
Context `{!heapDG Σ}.
Lemma array1_cons l v vs : l ↦ₗ∗ (v :: vs) ⊣⊢ l ↦ₗ v ∗ (l +ₗ 1) ↦ₗ∗ vs.
Proof.
rewrite /array1 /mapsto1 big_sepL_cons loc_add_0.
setoid_rewrite loc_add_assoc.
setoid_rewrite Nat2Z.inj_succ.
by setoid_rewrite Z.add_1_l.
Qed.
Lemma array2_cons l v vs : l ↦ᵣ∗ (v :: vs) ⊣⊢ l ↦ᵣ v ∗ (l +ₗ 1) ↦ᵣ∗ vs.
Proof.
rewrite /array2 /mapsto2 big_sepL_cons loc_add_0.
setoid_rewrite loc_add_assoc.
setoid_rewrite Nat2Z.inj_succ.
by setoid_rewrite Z.add_1_l.
Qed.
End array_liftings.
Section lifting.
Context `{!heapDG Σ}.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl : core.
Local Hint Constructors head_step : core.
Lemma dwp_fork E e1 e2 Φ :
▷ dwp ⊤ e1 e2 (λ _ _, True)%I -∗
▷ Φ #() #() -∗
dwp E (Fork e1) (Fork e2) Φ.
Proof.
iIntros "He HΦ".
iApply dwp_lift_pure_det_head_step; [auto| |auto| |].
all: try by (intros; inv_head_step; eauto).
iModIntro. iNext. iModIntro. simpl. iFrame "He".
by iApply dwp_value.
Qed.
Lemma dwp_atomic_lift_wp Ψ1 Ψ2 E2 e1 e2 Φ
`{!Atomic StronglyAtomic e1}
`{!Atomic StronglyAtomic e2}
{NF1 : NoFork e1}
{NF2 : NoFork e2}
{NO1 : NoObs e1}
{NO2 : NoObs e2}
{He1 : NotVal e1}
{He2 : NotVal e2}:
TWP1 e1 E2 Ψ1 -∗
TWP2 e2 ∅ Ψ2 -∗
(∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ▷ Φ v1 v2) -∗
dwp E2 e1 e2 Φ.
Proof.
iIntros "HTWP1 HTWP2 H".
rewrite dwp_unfold /dwp_pre /= He1 He2.
iIntros (σ1 σ2 κ1 κs1 κ2 κs2) "Hσ".
iDestruct "Hσ" as "(Hσ1 & Hκs1 & Hσ2 & Hκs2)".
rewrite /TWP1 /TWP2 !twp_unfold /twp_pre /= !He1 !He2.
iSpecialize ("HTWP1" $! σ1 0 (κ1++κs1) 0 with "[$Hσ1 $Hκs1]").
iSpecialize ("HTWP2" $! σ2 0 (κ2++κs2) 0%nat with "[$Hσ2 $Hκs2]").
iMod "HTWP1" as (Hred1) "HTWP1".
iMod "HTWP2" as (Hred2) "HTWP2".
destruct Hred1 as (? & ? & ? & Hred1).
destruct Hred2 as (? & ? & ? & Hred2).
iModIntro.
iSplit. { iPureIntro. eexists. eauto. }
iSplit. { iPureIntro. eexists. eauto. }
iIntros (e1' σ1' efs e2' σ2' efs2 Hstep1 Hstep2).
iSpecialize ("HTWP1" $! [] e1' σ1' efs with "[//]").
iSpecialize ("HTWP2" with "[//]").
iMod "HTWP2" as "(_ & [Hh2 Hp2] & HTWP2 & _)".
iMod "HTWP1" as "(_ & [Hh1 Hp1] & HTWP1 & _)".
destruct (to_val e1') as [v1|] eqn:Hv1; last first.
{ exfalso. destruct (atomic _ _ _ _ _ Hstep1). naive_solver. }
destruct (to_val e2') as [v2|] eqn:Hv2; last first.
{ exfalso. destruct (atomic _ _ _ _ _ Hstep2). naive_solver. }
rewrite -(of_to_val _ _ Hv1) -(of_to_val _ _ Hv2).
rewrite !twp_value_fupd. iMod "HTWP1".
rewrite (fupd_mask_mono ∅ E2); last by set_solver.
iMod "HTWP2". iFrame "Hh1 Hp1 Hh2 Hp2".
iApply step_fupd_intro; first set_solver.
iSpecialize ("H" with "HTWP1 HTWP2").
iNext. rewrite -dwp_value. iFrame.
rewrite (nofork _ _ _ _ _ Hstep1).
rewrite (nofork _ _ _ _ _ Hstep2).
simpl. eauto with iFrame.
Qed.
Lemma dwp_load E (l1 l2: loc) v1 v2 Φ :
▷l1 ↦ₗ v1 -∗
▷l2 ↦ᵣ v2 -∗
(l1 ↦ₗ v1 -∗ l2 ↦ᵣ v2 -∗ ▷ Φ v1 v2) -∗
dwp E (! #l1) (! #l2) Φ.
Proof.
iIntros ">Hl1 >Hl2 HΦ".
iApply (dwp_atomic_lift_wp
(λ v, ⌜v = v1⌝ ∗ l1 ↦ₗ v1)%I
(λ v, ⌜v = v2⌝ ∗ l2 ↦ᵣ v2)%I
with "[Hl1] [Hl2] [HΦ]").
{ iApply (twp_load _ _ l1 _ v1 with "[Hl1]"); eauto. }
{ iApply (twp_load _ _ l2 _ v2 with "[Hl2]"); eauto. }
iIntros (? ?) "[% Hl1] [% Hl2]". simplify_eq.
iApply ("HΦ" with "Hl1 Hl2").
Qed.
Lemma dwp_alloc E (v1 v2 : val) Φ :
(∀ r1 r2, r1 ↦ₗ v1 -∗ r2 ↦ᵣ v2 -∗ ▷ Φ #r1 #r2) -∗
DWP ref v1 & ref v2 @ E : Φ.
Proof.
iIntros "H".
pose (Ψ1 := (λ v, ∃ r : loc, ⌜v = #r⌝ ∧ r ↦ₗ v1)%I).
pose (Ψ2 := (λ v, ∃ r : loc, ⌜v = #r⌝ ∧ r ↦ᵣ v2)%I).
iApply (dwp_atomic_lift_wp Ψ1 Ψ2 with "[] [] [H]").
{ rewrite /TWP1 /Ψ1. wp_alloc r as "Hr". eauto with iFrame. }
{ rewrite /TWP2 /Ψ2. wp_alloc r as "Hr". eauto with iFrame. }
iIntros (? ?). iDestruct 1 as (r1 ->) "Hr1". iDestruct 1 as (r2 ->) "Hr2".
iApply ("H" with "Hr1 Hr2").
Qed.
Lemma dwp_store E (v1 v2 v1' v2' : val) (l1 l2 : loc) Φ :
▷l1 ↦ₗ v1 -∗
▷l2 ↦ᵣ v2 -∗
(l1 ↦ₗ v1' -∗ l2 ↦ᵣ v2' -∗ ▷Φ #() #()) -∗
DWP #l1 <- v1' & #l2 <- v2' @ E : Φ.
Proof.
iIntros ">Hl1 >Hl2 HΦ".
pose (Ψ1 := (λ v, ⌜v = #()⌝ ∗ l1 ↦ₗ v1')%I).
pose (Ψ2 := (λ v, ⌜v = #()⌝ ∗ l2 ↦ᵣ v2')%I).
iApply (dwp_atomic_lift_wp Ψ1 Ψ2 with "[Hl1] [Hl2] [HΦ]").
{ rewrite /TWP1 /Ψ1. wp_store. eauto with iFrame. }
{ rewrite /TWP2 /Ψ2. wp_store. eauto with iFrame. }
iIntros (? ?). iDestruct 1 as (->) "Hl1". iDestruct 1 as (->) "Hl2".
iApply ("HΦ" with "Hl1 Hl2").
Qed.
End lifting.