lifting.v 16.7 KB
Newer Older
1
From iris.algebra Require Import auth gmap.
2
From iris.base_logic Require Export gen_heap.
3
From iris.base_logic.lib Require Export proph_map.
4 5
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
6
From iris.heap_lang Require Export lang.
7
From iris.heap_lang Require Import tactics.
8
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
9
From stdpp Require Import fin_maps.
10
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
11

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

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

(** 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
27
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
28
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
30
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
33

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

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

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

Ralf Jung's avatar
fix TWP  
Ralf Jung committed
89
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
90
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
91
Local Ltac solve_pure_exec :=
92
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
93
    constructor; [solve_exec_safe | solve_exec_puredet].
94

95 96 97 98 99 100 101 102 103 104 105 106 107 108
(** 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. *)
109 110
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
111 112 113 114
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.
115

116 117 118 119 120 121 122 123 124 125 126 127
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.
128

129
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
130 131 132 133 134
  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').
135
Proof. solve_pure_exec. Qed.
136

137 138
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').
139
Proof. solve_pure_exec. Qed.
140

141
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
142
Proof. solve_pure_exec. Qed.
143

144
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
145
Proof. solve_pure_exec. Qed.
146

147 148
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
149
Proof. solve_pure_exec. Qed.
150

151 152
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
153
Proof. solve_pure_exec. Qed.
154

155 156
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
157
Proof. solve_pure_exec. Qed.
158

159 160
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
161
Proof. solve_pure_exec. Qed.
162

163
Section lifting.
164
Context `{!heapG Σ}.
165 166 167 168 169
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.

Ralf Jung's avatar
Ralf Jung committed
170
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
171
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
172
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
173
Proof.
174 175 176
  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.
177
Qed.
178

179
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
180
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
181
Proof.
182 183 184
  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.
185 186
Qed.

Amin Timany's avatar
Amin Timany committed
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 229 230
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.

231
(** Heap *)
Amin Timany's avatar
Amin Timany committed
232 233 234 235 236 237 238 239 240
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]".
241
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
242 243 244 245 246 247 248 249 250 251 252 253 254 255
    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]".
256
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
257 258 259 260 261 262
    rewrite replicate_length Z2Nat.id; auto with lia. }
  iModIntro; iSplit; auto.
  iFrame; iSplit; auto. iApply "HΦ".
  by iApply heap_array_to_array.
Qed.

263 264
Lemma wp_alloc s E v :
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
265
Proof.
Amin Timany's avatar
Amin Timany committed
266 267 268 269 270
  iIntros (Φ) "_ HΦ".
  iApply wp_allocN; auto with lia.
  iNext; iIntros (l) "H".
  iApply "HΦ".
  by rewrite array_singleton.
271
Qed.
272 273
Lemma twp_alloc s E v :
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
274
Proof.
Amin Timany's avatar
Amin Timany committed
275 276 277 278 279
  iIntros (Φ) "_ HΦ".
  iApply twp_allocN; auto with lia.
  iIntros (l) "H".
  iApply "HΦ".
  by rewrite array_singleton.
280
Qed.
281

282
Lemma wp_load s E l q v :
283
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
284 285
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
286
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
287
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
288 289
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
290
Lemma twp_load s E l q v :
291
  [[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
292 293
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
294
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
295
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
296
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
297
Qed.
298

299 300 301
Lemma wp_store s E l v' v :
  {{{  l  v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
  {{{ RET LitV LitUnit; l  v }}}.
302
Proof.
303
  iIntros (Φ) ">Hl HΦ".
304
  iApply wp_lift_atomic_head_step_no_fork; auto.
305
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
306
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
307
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
308
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
309
Qed.
310 311 312
Lemma twp_store s E l v' v :
  [[{ l  v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
  [[{ RET LitV LitUnit; l  v }]].
313
Proof.
314
  iIntros (Φ) "Hl HΦ".
315
  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.
318
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
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_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
325 326
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
327
  iIntros (?? Φ) ">Hl HΦ". 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 331
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
332 333 334
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
335 336
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
337
  iIntros (?? Φ) "Hl HΦ". 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 %?.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
339 340
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
341
Qed.
342

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

366 367
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
368 369
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
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
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
378 379
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
380
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
381
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
382
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
383
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
384
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
385
Qed.
386

387 388 389 390
Lemma wp_new_proph s E :
  {{{ True }}}
    NewProph @ s; E
  {{{ vs p, RET (LitV (LitProphecy p)); proph p vs }}}.
391 392
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
393
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
394
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
395 396
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
397 398
Qed.

399
Lemma wp_resolve_proph s E p vs v :
400
  {{{ proph p vs }}}
401
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
402
  {{{ vs', RET (LitV LitUnit); vs = v::vs'  proph p vs' }}}.
403
Proof.
404
  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
405 406 407 408 409 410
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
  iMod (proph_map_resolve_proph p v κs with "[HR Hp]") as "HPost"; first by iFrame.
  iModIntro. iFrame. iSplitR; first done.
  iDestruct "HPost" as (vs') "[HEq [HR Hp]]". iFrame.
  iApply "HΦ". iFrame.
411
Qed.
412

Ralf Jung's avatar
Ralf Jung committed
413
End lifting.
Amin Timany's avatar
Amin Timany committed
414 415 416

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