lifting.v 21.6 KB
Newer Older
1
From Coq.Lists Require Import List. (* used for lemma "exists_last" *)
2
From iris.algebra Require Import auth gmap.
3
From iris.base_logic Require Export gen_heap.
4
From iris.base_logic.lib Require Export proph_map.
5
6
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
7
From iris.heap_lang Require Export lang.
8
From iris.heap_lang Require Import tactics.
9
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
10
From stdpp Require Import fin_maps.
11
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
12

13
14
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
15
  heapG_gen_heapG :> gen_heapG loc val Σ;
16
  heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ
17
18
}.

19
Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
20
  iris_invG := heapG_invG;
21
22
  state_interp σ κs _ :=
    (gen_heap_ctx σ.(heap)  proph_map_ctx κs σ.(used_proph_id))%I;
23
  fork_post _ := True%I;
24
25
26
27
}.

(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
29
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
31
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
34

35
36
37
38
39
Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
  ([ list] i  v  vs, loc_add l i  v)%I.
Notation "l ↦∗ vs" := (array l vs)
  (at level 20, format "l  ↦∗  vs") : bi_scope.

40
41
42
43
44
45
46
47
48
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
operations. This tactic is slightly ad-hoc and tuned for proving our lifting
lemmas. *)
Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
49
  | H : head_step ?e _ _ _ _ _ |- _ =>
50
51
52
53
54
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.

Tej Chajed's avatar
Tej Chajed committed
55
56
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
57

58
(* [simpl apply] is too stupid, so we need extern hints here. *)
Tej Chajed's avatar
Tej Chajed committed
59
60
61
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
Amin Timany's avatar
Amin Timany committed
62
Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
Tej Chajed's avatar
Tej Chajed committed
63
64
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
65

66
67
68
69
70
71
72
73
74
75
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.

Local Ltac solve_atomic :=
  apply strongly_atomic_atomic, ectx_language_atomic;
    [inversion 1; naive_solver
    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].

Amin Timany's avatar
Amin Timany committed
76
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
Proof. solve_atomic. Qed.
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
Instance skip_atomic s  : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
92
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
93
94
Proof. solve_atomic. Qed.

95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
Instance proph_resolve_atomic s e v1 v2 :
  Atomic s e  Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
  rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
  simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
  - subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
  - rewrite fill_app. rewrite fill_app in Hfill.
    assert ( v, Val v = fill Ks e1'  False) as fill_absurd.
    { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
      apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
    destruct K; (inversion Hfill; clear Hfill; subst; try
      match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
    refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
    + destruct s; intro Hs; simpl in *.
      * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
      * apply irreducible_resolve. by rewrite fill_app in Hs.
    + econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
Qed.

Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. by apply proph_resolve_atomic, skip_atomic. Qed.

Ralf Jung's avatar
fix TWP    
Ralf Jung committed
117
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
118
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
119
Local Ltac solve_pure_exec :=
120
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
121
    constructor; [solve_exec_safe | solve_exec_puredet].
122

123
124
125
126
127
128
129
130
131
132
133
134
135
136
(** The behavior of the various [wp_] tactics with regard to lambda differs in
the following way:

- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.

To realize this behavior, we define the class [AsRecV v f x erec], which takes a
value [v] as its input, and turns it into a [RecV f x erec] via the instance
[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
not if [v] contains a lambda/rec that is hidden behind a definition.

To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
137
138
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
139
140
141
142
Hint Mode AsRecV ! - - - : typeclass_instances.
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
  apply AsRecV_recv : typeclass_instances.
143

144
145
146
147
148
149
150
151
152
153
154
155
Instance pure_recc f x (erec : expr) :
  PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
Instance pure_pairc (v1 v2 : val) :
  PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
Proof. solve_pure_exec. Qed.
Instance pure_injlc (v : val) :
  PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
Proof. solve_pure_exec. Qed.
Instance pure_injrc (v : val) :
  PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
156

157
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
158
159
160
161
162
  PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.

Instance pure_unop op v v' :
  PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
163
Proof. solve_pure_exec. Qed.
164

165
166
Instance pure_binop op v1 v2 v' :
  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
167
Proof. solve_pure_exec. Qed.
168

169
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
170
Proof. solve_pure_exec. Qed.
171

172
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
173
Proof. solve_pure_exec. Qed.
174

175
176
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
177
Proof. solve_pure_exec. Qed.
178

179
180
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
181
Proof. solve_pure_exec. Qed.
182

183
184
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
185
Proof. solve_pure_exec. Qed.
186

187
188
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
189
Proof. solve_pure_exec. Qed.
190

191
Section lifting.
192
Context `{!heapG Σ}.
193
194
195
196
197
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.

Ralf Jung's avatar
Ralf Jung committed
198
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
199
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
200
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
201
Proof.
202
203
204
  iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
205
Qed.
206

207
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
208
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
209
Proof.
210
211
212
  iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
  iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
  iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
213
214
Qed.

Amin Timany's avatar
Amin Timany committed
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
Lemma array_nil l : l ↦∗ []  emp.
Proof. by rewrite /array. Qed.

Lemma array_singleton l v : l ↦∗ [v]  l  v.
Proof. by rewrite /array /= right_id loc_add_0. Qed.

Lemma array_app l vs ws :
  l ↦∗ (vs ++ ws)  l ↦∗ vs  (loc_add l (length vs)) ↦∗ ws.
Proof.
  rewrite /array big_sepL_app.
  setoid_rewrite Nat2Z.inj_add.
  by setoid_rewrite loc_add_assoc.
Qed.

Lemma array_cons l v vs : l ↦∗ (v :: vs)  l  v  (l + 1) ↦∗ vs.
Proof.
  rewrite /array 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 heap_array_to_array l vs :
  ([ map] i  v  heap_array l vs, i  v)%I - l ↦∗ vs.
Proof.
  iIntros "Hvs".
  iInduction vs as [|v vs] "IH" forall (l); simpl.
  { by rewrite big_opM_empty /array big_opL_nil. }
  rewrite big_opM_union; last first.
  { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
    intros (j&?&Hjl&_)%heap_array_lookup.
    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl;
      apply loc_add_inj in Hjl; lia. }
  rewrite array_cons.
  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
  by iApply "IH".
Qed.

253
(** Heap *)
Amin Timany's avatar
Amin Timany committed
254
255
Lemma wp_allocN s E v n :
  0 < n 
256
257
  {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }}}.
Amin Timany's avatar
Amin Timany committed
258
259
260
261
262
Proof.
  iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
263
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
264
265
266
267
268
269
270
    rewrite replicate_length Z2Nat.id; auto with lia. }
  iModIntro; iSplit; auto.
  iFrame. iApply "HΦ".
  by iApply heap_array_to_array.
Qed.
Lemma twp_allocN s E v n :
  0 < n 
271
272
  [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }]].
Amin Timany's avatar
Amin Timany committed
273
274
275
276
277
Proof.
  iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
278
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
279
280
281
282
283
284
    rewrite replicate_length Z2Nat.id; auto with lia. }
  iModIntro; iSplit; auto.
  iFrame; iSplit; auto. iApply "HΦ".
  by iApply heap_array_to_array.
Qed.

285
286
Lemma wp_alloc s E v :
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
287
Proof.
Amin Timany's avatar
Amin Timany committed
288
289
290
291
292
  iIntros (Φ) "_ HΦ".
  iApply wp_allocN; auto with lia.
  iNext; iIntros (l) "H".
  iApply "HΦ".
  by rewrite array_singleton.
293
Qed.
294
295
Lemma twp_alloc s E v :
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
296
Proof.
Amin Timany's avatar
Amin Timany committed
297
298
299
300
301
  iIntros (Φ) "_ HΦ".
  iApply twp_allocN; auto with lia.
  iIntros (l) "H".
  iApply "HΦ".
  by rewrite array_singleton.
302
Qed.
303

304
Lemma wp_load s E l q v :
305
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
306
307
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
308
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
309
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
310
311
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
312
Lemma twp_load s E l q v :
313
  [[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
314
315
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
316
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
317
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
318
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
319
Qed.
320

321
322
323
Lemma wp_store s E l v' v :
  {{{  l  v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
  {{{ RET LitV LitUnit; l  v }}}.
324
Proof.
325
  iIntros (Φ) ">Hl HΦ".
326
  iApply wp_lift_atomic_head_step_no_fork; auto.
327
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
328
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
329
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
330
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
331
Qed.
332
333
334
Lemma twp_store s E l v' v :
  [[{ l  v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
  [[{ RET LitV LitUnit; l  v }]].
335
Proof.
336
  iIntros (Φ) "Hl HΦ".
337
  iApply twp_lift_atomic_head_step_no_fork; auto.
338
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
339
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
340
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
341
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
342
Qed.
343

344
345
346
Lemma wp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  {{{  l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
347
348
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
349
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
350
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
351
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
352
353
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
354
355
356
Lemma twp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  [[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
357
358
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
359
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
360
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
361
362
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
363
Qed.
364

365
366
367
Lemma wp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  {{{  l  v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
368
369
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
370
  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
371
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
372
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
373
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
374
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
375
Qed.
376
377
378
Lemma twp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  [[{ l  v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
379
380
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
381
  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
382
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
383
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
384
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
385
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
386
Qed.
387

388
389
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
390
391
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
392
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
393
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
394
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
395
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
396
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
397
Qed.
398
399
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
400
401
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
402
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
403
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
404
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
405
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
406
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
407
Qed.
408

409
410
411
412
Lemma wp_new_proph s E :
  {{{ True }}}
    NewProph @ s; E
  {{{ vs p, RET (LitV (LitProphecy p)); proph p vs }}}.
413
414
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
415
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
416
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
417
418
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
419
420
Qed.

421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
(* In the following, strong atomicity is required due to the fact that [e] must
be able to make a head step for [Resolve e _ _] not to be (head) stuck. *)

Lemma resolve_reducible e σ p v :
  Atomic StronglyAtomic e  reducible e σ 
  reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ.
Proof.
  intros A (κ & e' & σ' & efs & H).
  exists (κ ++ [(p, (default v (to_val e'), v))]), e', σ', efs.
  eapply Ectx_step with (K:=[]); try done.
  assert (w, Val w = e') as [w <-].
  { unfold Atomic in A. apply (A σ e' κ σ' efs) in H. unfold is_Some in H.
    destruct H as [w H]. exists w. simpl in H. by apply (of_to_val _ _ H). }
  simpl. constructor. by apply prim_step_to_val_is_head_step.
Qed.

Lemma step_resolve e p v σ1 κ e2 σ2 efs :
  Atomic StronglyAtomic e 
  prim_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs 
  head_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs.
Proof.
  intros A [Ks e1' e2' Hfill -> step]. simpl in *.
  induction Ks as [|K Ks _] using rev_ind.
  + simpl in *. subst. inversion step. by constructor.
  + rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
    - assert (fill_item K (fill Ks e1') = fill (Ks ++ [K]) e1') as Eq1;
        first by rewrite fill_app.
      assert (fill_item K (fill Ks e2') = fill (Ks ++ [K]) e2') as Eq2;
        first by rewrite fill_app.
      rewrite fill_app /=. rewrite Eq1 in A.
      assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as H.
      { apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
      destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
    - assert (to_val (fill Ks e1') = Some p); first by rewrite -H1 //.
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
    - assert (to_val (fill Ks e1') = Some v); first by rewrite -H2 //.
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
Qed.

Lemma wp_resolve s E e Φ p v vs :
  Atomic StronglyAtomic e 
  to_val e = None 
  proph p vs -
  WP e @ s; E {{ r,  vs', vs = (r, v)::vs' - proph p vs' - Φ r }} -
  WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
Proof.
  (* TODO we should try to use a generic lifting lemma (and avoid [wp_unfold])
     here, since this breaks the WP abstraction. *)
  iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre /= He. simpl in *.
  iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct (decide (κ = [])) as [->|HNeq].
  - iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
    { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
    iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done.
    inversion step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
  - apply exists_last in HNeq as [κ' [[p' [w' v']] ->]]. rewrite -app_assoc.
    iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
    { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
    iIntros (e2 σ2 efs step). apply step_resolve in step; last done. inversion step.
    match goal with H: _ ++ _ = _ ++ _ |- _ =>
      apply app_inj_2 in H; last done; destruct H as [-> [=-> -> ->]] end. subst.
    iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe". { eexists [] _ _; try done. }
    iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
    iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs' ->) "[$ HPost]".
    iModIntro. rewrite !wp_unfold /wp_pre /=. iDestruct "WPe" as "[HΦ $]".
    iMod "HΦ". iModIntro. iApply "HΦ"; [ done | iFrame ].
Qed.

Lemma wp_skip s E Φ :  Φ (LitV LitUnit) - WP Skip @ s; E {{ Φ }}.
Proof.
  iIntros "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κ κs n) "Hσ". iModIntro. iSplit.
  - iPureIntro. eexists _, _, _, _. by constructor.
  - iIntros (e2 σ2 efs step) "!>". inversion step. simplify_eq. by iFrame.
Qed.

496
Lemma wp_resolve_proph s E p vs v :
497
  {{{ proph p vs }}}
498
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
499
  {{{ vs', RET (LitV LitUnit); vs = (LitV LitUnit, v)::vs'  proph p vs' }}}.
500
Proof.
501
502
  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
  iApply wp_skip. iNext. iIntros (vs') "HEq Hp". iApply "HΦ". iFrame.
503
Qed.
504

Ralf Jung's avatar
Ralf Jung committed
505
End lifting.