lifting.v 16.8 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 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264
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]".
  { symmetry.
    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
    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]".
  { symmetry.
    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
    rewrite replicate_length Z2Nat.id; auto with lia. }
  iModIntro; iSplit; auto.
  iFrame; iSplit; auto. iApply "HΦ".
  by iApply heap_array_to_array.
Qed.

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

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

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

324 325 326
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
327 328
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
329
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
330
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
331
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
332 333
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
334 335 336
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
337 338
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
339
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
340
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
341 342
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
343
Qed.
344

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

368 369
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
370 371
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
372
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
373
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
374
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
375
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
376
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
377
Qed.
378 379
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
380 381
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
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 (κ e2 σ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 391 392
Lemma wp_new_proph s E :
  {{{ True }}}
    NewProph @ s; E
  {{{ vs p, RET (LitV (LitProphecy p)); proph p vs }}}.
393 394
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
395
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
396
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
397 398
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
399 400
Qed.

401
Lemma wp_resolve_proph s E p vs v :
402
  {{{ proph p vs }}}
403
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
404
  {{{ vs', RET (LitV LitUnit); vs = v::vs'  proph p vs' }}}.
405
Proof.
406
  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
407 408 409 410 411 412
  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.
413
Qed.
414

Ralf Jung's avatar
Ralf Jung committed
415
End lifting.
Amin Timany's avatar
Amin Timany committed
416 417 418

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