lifting.v 21.7 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 40 41 42 43
(** 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
44
  | H : head_step ?e _ _ _ _ _ |- _ =>
45 46 47 48 49
     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
50 51
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
52

53
(* [simpl apply] is too stupid, so we need extern hints here. *)
Tej Chajed's avatar
Tej Chajed committed
54 55 56
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
57
Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
Tej Chajed's avatar
Tej Chajed committed
58 59
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
60

61 62 63 64 65 66 67 68 69 70
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
71
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
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.
87
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
88 89
Proof. solve_atomic. Qed.

90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
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
112
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
113
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
114
Local Ltac solve_pure_exec :=
115
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
116
    constructor; [solve_exec_safe | solve_exec_puredet].
117

118 119 120 121 122 123 124 125 126 127 128 129 130 131
(** 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. *)
132 133
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
134 135 136 137
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.
138

139 140 141 142 143 144 145 146 147 148 149 150
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.
151

152
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
153 154 155 156 157
  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').
158
Proof. solve_pure_exec. Qed.
159

160 161
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').
162
Proof. solve_pure_exec. Qed.
163

164
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
165
Proof. solve_pure_exec. Qed.
166

167
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
168
Proof. solve_pure_exec. Qed.
169

170 171
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
172
Proof. solve_pure_exec. Qed.
173

174 175
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
176
Proof. solve_pure_exec. Qed.
177

178 179
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
180
Proof. solve_pure_exec. Qed.
181

182 183
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
184
Proof. solve_pure_exec. Qed.
185

186
Section lifting.
187
Context `{!heapG Σ}.
188 189 190 191 192
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.

Ralf Jung's avatar
Ralf Jung committed
193
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
194
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
195
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
196
Proof.
197 198 199
  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.
200
Qed.
201

202
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
203
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
204
Proof.
205 206 207
  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.
208 209
Qed.

Amin Timany's avatar
Amin Timany committed
210 211 212 213 214 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 253
Definition array (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.

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.

254
(** Heap *)
Amin Timany's avatar
Amin Timany committed
255 256 257 258 259 260 261 262 263
Lemma wp_allocN s E v n :
  0 < n 
  {{{ True }}} AllocN ((Val $ LitV $ LitInt $ n)) (Val v) @ s; E
  {{{ l, RET LitV (LitLoc l); l ↦∗ (replicate (Z.to_nat n) v) }}}.
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]".
264
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
265 266 267 268 269 270 271 272 273 274 275 276 277 278
    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 
  [[{ True }]] AllocN ((Val $ LitV $ LitInt $ n)) (Val v) @ s; E
  [[{ l, RET LitV (LitLoc l); l ↦∗ (replicate (Z.to_nat n) v) }]].
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]".
279
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
280 281 282 283 284 285
    rewrite replicate_length Z2Nat.id; auto with lia. }
  iModIntro; iSplit; auto.
  iFrame; iSplit; auto. iApply "HΦ".
  by iApply heap_array_to_array.
Qed.

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

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

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

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

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

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

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

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 496
(* 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.

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

Ralf Jung's avatar
Ralf Jung committed
506
End lifting.
Amin Timany's avatar
Amin Timany committed
507 508 509

Notation "l ↦∗ vs" := (array l vs)
  (at level 20, format "l  ↦∗  vs") : bi_scope.