concurrent_runners.v 16.4 KB
Newer Older
1 2 3 4 5
(** Concurrent Runner example from
    "Modular Reasoning about Separation of Concurrent Data Structures"
    <http://www.kasv.dk/articles/hocap-ext.pdf>
*)
From iris.heap_lang Require Import proofmode notation.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.bi.lib Require Import fractional.
7
From iris.algebra Require Import cmra agree frac csum excl.
8
From iris.heap_lang.lib Require Import assert.
9
From iris_examples.hocap Require Export abstract_bag shared_bag lib.oneshot.
10 11
Set Default Proof Using "Type".

12 13 14 15 16
(** RA describing the evolution of a task *)
(** INIT = task has been initiated
    SET_RES v = the result of the task has been computed and it is v
    FIN v = the task has been completed with the result v *)
(* We use this RA to verify the Task.run() method *)
17
Definition saR := csumR fracR (csumR (prodR fracR (agreeR valO)) (agreeR valO)).
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
Class saG Σ := { sa_inG :> inG Σ saR }.
Definition INIT `{saG Σ} γ (q: Qp) := own γ (Cinl q%Qp).
Definition SET_RES `{saG Σ} γ (q: Qp) (v: val) := own γ (Cinr (Cinl (q%Qp, to_agree v))).
Definition FIN `{saG Σ} γ (v: val) := own γ (Cinr (Cinr (to_agree v))).
Global Instance INIT_fractional `{saG Σ} γ : Fractional (INIT γ)%I.
Proof.
  intros p q. rewrite /INIT.
  rewrite -own_op. f_equiv.
Qed.
Global Instance INIT_as_fractional `{saG Σ} γ q:
  AsFractional (INIT γ q) (INIT γ)%I q.
Proof.
  split; [done | apply _].
Qed.
Global Instance SET_RES_fractional `{saG Σ} γ v : Fractional (fun q => SET_RES γ q v)%I.
Proof.
  intros p q. rewrite /SET_RES.
35
  rewrite -own_op Cinr_op Cinl_op pair_op agree_idemp. f_equiv.
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
Qed.
Global Instance SET_RES_as_fractional `{saG Σ} γ q v:
  AsFractional (SET_RES γ q v) (fun q => SET_RES γ q v)%I q.
Proof.
  split; [done | apply _].
Qed.

Lemma new_INIT `{saG Σ} : (|==>  γ, INIT γ 1%Qp)%I.
Proof. by apply own_alloc. Qed.
Lemma INIT_not_SET_RES `{saG Σ} γ q q' v :
  (INIT γ q - SET_RES γ q' v - False)%I.
Proof.
  iIntros "Hs Hp".
  iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma INIT_not_FIN `{saG Σ} γ q v :
  (INIT γ q - FIN γ v - False)%I.
Proof.
  iIntros "Hs Hp".
  iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma SET_RES_not_FIN `{saG Σ} γ q v v' :
  (SET_RES γ q v - FIN γ v' - False)%I.
Proof.
  iIntros "Hs Hp".
  iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma SET_RES_agree `{saG Σ} (γ: gname) (q q': Qp) (v w: val) :
  SET_RES γ q v - SET_RES γ q' w - v = w.
Proof.
  iIntros "Hs1 Hs2".
  iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
  iPureIntro. rewrite Cinr_op Cinl_op pair_op in Hfoo.
  by destruct Hfoo as [_ ?%agree_op_invL'].
Qed.
Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) :
  FIN γ v - FIN γ w - v = w.
Proof.
  iIntros "Hs1 Hs2".
  iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
  iPureIntro. rewrite Cinr_op Cinr_op in Hfoo.
  by apply agree_op_invL'.
Qed.
Lemma INIT_SET_RES `{saG Σ} (v: val) γ :
  INIT γ 1%Qp == SET_RES γ 1%Qp v.
Proof.
  apply own_update.
  by apply cmra_update_exclusive.
Qed.
Lemma SET_RES_FIN `{saG Σ} (v w: val) γ :
  SET_RES γ 1%Qp v == FIN γ w.
Proof.
  apply own_update.
  by apply cmra_update_exclusive.
Qed.

Section contents.
  Context `{heapG Σ, !oneshotG Σ, !saG Σ}.
  Variable b : bag Σ.
  Variable N : namespace.

  (* new Task : Runner<A,B> -> A -> Task<A,B> *)
  Definition newTask : val := λ: "r" "a", ("r", "a", ref #0, ref NONEV).
  (* task_runner == Fst Fst Fst *)
  (* task_arg    == Snd Fst Fst *)
  (* task_state  == Snd Fst *)
  (* task_res    == Snd *)
  (* Task.Run : Task<A,B> -> () *)
  Definition task_Run : val := λ: "t",
    let: "runner" := Fst (Fst (Fst "t")) in
    let: "arg"    := Snd (Fst (Fst "t")) in
    let: "state"  := Snd (Fst "t") in
    let: "res"    := Snd "t" in
    let: "tmp" := (Fst "runner") "runner" "arg"
                  (* runner.body(runner,arg)*) in
    "res" <- (SOME "tmp");;
    "state" <- #1.

  (* Task.Join : Task<A,B> -> B *)
  Definition task_Join : val := rec: "join" "t" :=
    let: "runner" := Fst (Fst (Fst "t")) in
    let: "arg"    := Snd (Fst (Fst "t")) in
    let: "state"  := Snd (Fst "t") in
    let: "res"    := Snd "t" in
120 121 122 123 124 125
    if: (!"state" = #1)
    then match: !"res" with
           NONE => assert #false
         | SOME "v" => "v"
         end
    else "join" "t".
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

  (* runner_body == Fst *)
  (* runner_bag  == Snd *)

  (* Runner.Fork : Runner<A,B> -> A -> Task<A,B> *)
  Definition runner_Fork : val := λ: "r" "a",
    let: "bag" := Snd "r" in
    let: "t" := newTask "r" "a" in
    pushBag b "bag" "t";;
    "t".

  (* Runner.runTask : Runner<A,B> -> () *)
  Definition runner_runTask : val := λ: "r",
    let: "bag" := Snd "r" in
    match: popBag b "bag" with
      NONE => #()
    | SOME "t" => task_Run "t"
    end.

  (* Runner.runTasks : Runner<A,B> -> () *)
  Definition runner_runTasks : val := rec: "runTasks" "r" :=
    runner_runTask "r";; "runTasks" "r".

  (* newRunner : (Runner<A,B> -> A -> B) -> nat -> Runner<A,B> *)
  Definition newRunner : val := λ: "body" "n",
    let: "bag" := newBag b #() in
    let: "r" := ("body", "bag") in
    let: "loop" :=
       (rec: "loop" "i" :=
          if: ("i" < "n")
          then Fork (runner_runTasks "r");; "loop" ("i"+#1)
          else "r"
       ) in
    "loop" #0.

  Definition task_inv (γ γ': gname) (state res: loc) (Q: val  iProp Σ) : iProp Σ :=
    ((state  #0  res  NONEV  pending γ (1/2)%Qp  INIT γ' (1/2)%Qp)
    ( v, state  #0  res  SOMEV v  pending γ (1/2)%Qp  SET_RES γ' (1/2)%Qp v)
    ( v, state  #1  res  SOMEV v  FIN γ' v  (Q v  pending γ (1/2)%Qp  shot γ v)))%I.
165
  Definition isTask (r: val) (γ γ': gname) (t: val) (P: val  iProp Σ) (Q: val  val  iProp Σ) : iProp Σ :=
166 167 168
    ( (arg : val) (state res : loc),
     t = (r, arg, #state, #res)%V
      P arg  INIT γ' (1/2)%Qp
169 170 171
      inv (N.@"task") (task_inv γ γ' state res (Q arg)))%I.
  Definition task (γ γ': gname) (t arg: val) (P: val  iProp Σ) (Q: val  val  iProp Σ) : iProp Σ :=
    ( (r: val) (state res : loc),
172 173
     t = (r, arg, #state, #res)%V
      pending γ (1/2)%Qp
174
      inv (N.@"task") (task_inv γ γ' state res (Q arg)))%I.
175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190

  Ltac auto_equiv :=
    (* Deal with "pointwise_relation" *)
    repeat lazymatch goal with
           | |- pointwise_relation _ _ _ _ => intros ?
           end;
    (* Normalize away equalities. *)
    repeat match goal with
           | H : _ {_} _ |-  _ => apply (discrete_iff _ _) in H
           | _ => progress simplify_eq
           end;
    (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
    try (f_equiv; fast_done || auto_equiv).

  Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).

Dan Frumin's avatar
Dan Frumin committed
191
  Program Definition pre_runner (γ : name Σ b) (P: val  iProp Σ) (Q: val  val  iProp Σ) :
192
    (valO -n> iProp Σ) -n> (valO -n> iProp Σ) := λne R r,
193 194
    ( (body bag : val), r = (body, bag)%V
      bagS b (N.@"bag") (λ x y,  γ γ', isTask (body,x) γ γ' y P Q) γ bag
195
        r a: val,  (R r  P a - WP body r a {{ v, Q a v }}))%I.
196 197
  Solve Obligations with solve_proper.

Dan Frumin's avatar
Dan Frumin committed
198 199 200
  Global Instance pre_runner_contractive (γ : name Σ b) P Q :
    Contractive (pre_runner γ P Q).
  Proof. unfold pre_runner. solve_contractive. Qed.
201

Dan Frumin's avatar
Dan Frumin committed
202
  Definition runner (γ: name Σ b) (P: val  iProp Σ) (Q: val  val  iProp Σ) :
203
    valO -n> iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
204
    (fixpoint (pre_runner γ P Q))%I.
205

Dan Frumin's avatar
Dan Frumin committed
206 207
  Lemma runner_unfold γ r P Q :
    runner γ P Q r 
208 209
      ( (body bag : val), r = (body, bag)%V
        bagS b (N.@"bag") (λ x y,  γ γ', isTask (body,x) γ γ' y P Q) γ bag
Dan Frumin's avatar
Dan Frumin committed
210
          r a: val,  (runner γ P Q r  P a - WP body r a {{ v, Q a v }}))%I.
Ralf Jung's avatar
Ralf Jung committed
211
  Proof. rewrite /runner. by rewrite {1}(fixpoint_unfold (pre_runner _ _ _) r). Qed.
212

Dan Frumin's avatar
Dan Frumin committed
213 214
  Global Instance runner_persistent γ r P Q :
    Persistent (runner γ P Q r).
Ralf Jung's avatar
Ralf Jung committed
215
  Proof. rewrite /runner (fixpoint_unfold (pre_runner _ _ _) r). apply _. Qed.
216

217
  Lemma newTask_spec γb (r a : val) P (Q : val  val  iProp Σ) :
Dan Frumin's avatar
Dan Frumin committed
218
    {{{ runner γb P Q r  P a }}}
219
      newTask r a
220
    {{{ γ γ' t, RET t; isTask r γ γ' t P Q  task γ γ' t a P Q }}}.
221 222
  Proof.
    iIntros (Φ) "[#Hrunner HP] HΦ".
223
    wp_rec. wp_pures. iApply wp_fupd.
224
    wp_alloc res as "Hres".
Robbert Krebbers's avatar
Robbert Krebbers committed
225
    wp_alloc status as "Hstatus".
226 227
    iMod (new_pending) as (γ) "[Htoken Htask]".
    iMod (new_INIT) as (γ') "[Hinit Hinit']".
228
    iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
229
    { iNext. iLeft. iFrame. }
230
    wp_pures. iModIntro. iApply "HΦ".
231
    iFrame. iSplitL; iExists _,_,_; iFrame "Hinv"; eauto.
232 233
  Qed.

234
  Lemma task_Join_spec γb γ γ' (r t a : val) P Q :
Dan Frumin's avatar
Dan Frumin committed
235
    {{{ runner γb P Q r  task γ γ' t a P Q }}}
236
       task_Join t
237
    {{{ res, RET res; Q a res }}}.
238
  Proof.
239
    iIntros (Φ) "[#Hrunner Htask] HΦ".
240 241
    iLöb as "IH".
    rewrite {2}/task_Join.
242
    iDestruct "Htask" as (r' state res) "(% & Htoken & #Htask)". simplify_eq.
243
    wp_rec. wp_pures.
244
    wp_bind (! #state)%E. iInv (N.@"task") as "Hstatus" "Hcl".
245
    rewrite {2}/task_inv.
246
    iDestruct "Hstatus" as "[>(Hstate & Hres)|[Hstatus|Hstatus]]".
247 248 249 250 251
    - wp_load.
      iMod ("Hcl" with "[Hstate Hres]") as "_".
      { iNext; iLeft; iFrame. }
      iModIntro. wp_op. wp_if.
      rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
252 253
      iExists _,_,_; iFrame "Htask"; eauto.
    - iDestruct "Hstatus" as (v) "(>Hstate & >Hres & HQ)".
254 255 256 257 258
      wp_load.
      iMod ("Hcl" with "[Hstate Hres HQ]") as "_".
      { iNext; iRight; iLeft. iExists _; iFrame. }
      iModIntro. wp_op. wp_if.
      rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
259 260
      iExists _,_,_; iFrame "Htask"; eauto.
    - iDestruct "Hstatus" as (v) "(>Hstate & >Hres & #HFIN & HQ)".
261 262 263 264 265 266 267 268 269 270
      wp_load.
      iDestruct "HQ" as "[[HQ Htoken2]|Hshot]"; last first.
      { iExFalso. iApply (shot_not_pending with "Hshot Htoken"). }
      iMod (shoot v γ with "[Htoken Htoken2]") as "#Hshot".
      { iApply (fractional_split_2 with "Htoken Htoken2").
        assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
        apply _. }
      iMod ("Hcl" with "[Hstate Hres]") as "_".
      { iNext. iRight. iRight. iExists _. iFrame. iFrame "HFIN".
        iRight. eauto. }
271 272
      iModIntro. wp_op. wp_if. wp_bind (!#res)%E.
      iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT)|[Hstatus|Hstatus]]" "Hcl".
273
      { iExFalso. iApply (shot_not_pending with "Hshot Hpending"). }
274
      { iDestruct "Hstatus" as (v') "(Hstate & Hres & Hpending & >HSETRES)".
275 276
        iExFalso. iApply (SET_RES_not_FIN with "HSETRES HFIN"). }
      iDestruct "Hstatus" as (v') "(Hstate & Hres & _ & HQ')".
277 278 279 280
      iDestruct "HQ'" as "[[? >Hpending]|>Hshot']".
      { iExFalso. iApply (shot_not_pending with "Hshot Hpending"). }
      iDestruct (shot_agree with "Hshot Hshot'") as %->.
      wp_load.
281 282
      iMod ("Hcl" with "[Hres Hstate]") as "_".
      { iNext. iRight. iRight. iExists _; iFrame. iFrame "HFIN". by iRight. }
283
      iModIntro. wp_match. iApply "HΦ"; eauto.
284 285
  Qed.

286
  Lemma task_Run_spec γb γ γ' r t P Q :
Dan Frumin's avatar
Dan Frumin committed
287
    {{{ runner γb P Q r  isTask r γ γ' t P Q }}}
288 289 290 291
       task_Run t
    {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "[#Hrunner Htask] HΦ".
Dan Frumin's avatar
Dan Frumin committed
292
    rewrite runner_unfold.
293 294 295
    iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)".
    iDestruct "Htask" as (arg state res) "(% & HP & HINIT & #Htask)".
    simplify_eq. rewrite /task_Run.
296
    wp_rec. wp_pures.
297 298 299
    wp_bind (body _ arg).
    iDestruct ("Hbody" $! (PairV body bag) arg) as "Hbody'".
    iSpecialize ("Hbody'" with "[HP]").
Dan Frumin's avatar
Dan Frumin committed
300
    { iFrame. rewrite runner_unfold.
301 302 303
      iExists _,_; iSplitR; eauto. }
    iApply (wp_wand with "Hbody'").
    iIntros (v) "HQ". wp_let.
304
    wp_bind (#res <- SOME v)%E. wp_inj.
305
    iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT')|[Hstatus|Hstatus]]" "Hcl".
306 307 308 309 310 311 312
    - wp_store.
      iMod (INIT_SET_RES v γ' with "[HINIT HINIT']") as "[HSETRES HSETRES']".
      { iApply (fractional_split_2 with "HINIT HINIT'").
        assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
        apply _. }
      iMod ("Hcl" with "[HSETRES Hstate Hres Hpending]") as "_".
      { iNext. iRight. iLeft. iExists _; iFrame. }
313
      iModIntro. wp_seq.
314
      iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT')|[Hstatus|Hstatus]]" "Hcl".
315 316 317 318 319 320 321 322 323 324 325
      { iExFalso. iApply (INIT_not_SET_RES with "HINIT' HSETRES'"). }
      + iDestruct "Hstatus" as (v') "(Hstate & Hres & Hpending & HSETRES)".
        wp_store.
        iDestruct (SET_RES_agree with "HSETRES HSETRES'") as %->.
        iMod (SET_RES_FIN v v with "[HSETRES HSETRES']") as "#HFIN".
        { iApply (fractional_split_2 with "HSETRES HSETRES'").
          assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
          apply _. }
        iMod ("Hcl" with "[-HΦ]") as "_".
        { iNext. do 2 iRight. iExists _; iFrame. iFrame "HFIN". iLeft. iFrame.  }
        iModIntro. by iApply "HΦ".
326
      + iDestruct "Hstatus" as (v') "(Hstate & Hres & >HFIN & HQ')".
327
        iExFalso. iApply (SET_RES_not_FIN with "HSETRES' HFIN").
328
    - iDestruct "Hstatus" as (v') "(Hstate & Hres & Hpending & >HSETRES)".
329
      iExFalso. iApply (INIT_not_SET_RES with "HINIT HSETRES").
330
    - iDestruct "Hstatus" as (v') "(Hstate & Hres & >HFIN & HQ')".
331 332 333
      iExFalso. iApply (INIT_not_FIN with "HINIT HFIN").
  Qed.

334
  Lemma runner_runTask_spec γb P Q r:
Dan Frumin's avatar
Dan Frumin committed
335
    {{{ runner γb P Q r }}}
336 337 338 339
      runner_runTask r
    {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "#Hrunner HΦ".
Dan Frumin's avatar
Dan Frumin committed
340
    rewrite runner_unfold /runner_runTask.
341
    iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)"; simplify_eq.
342
    wp_rec. wp_pures.
343 344 345 346 347 348 349 350
    wp_bind (popBag b _).
    iApply (popBag_spec with "Hbag").
    iNext. iIntros (t') "[_ [%|Ht]]"; simplify_eq.
    - wp_match. by iApply "HΦ".
    - iDestruct "Ht" as (t) "[% Ht]".
      iDestruct "Ht" as (γ γ') "Htask".
      simplify_eq. wp_match.
      iApply (task_Run_spec with "[Hbag Hbody Htask]"); last done.
Dan Frumin's avatar
Dan Frumin committed
351
      iFrame "Htask". rewrite runner_unfold.
352 353 354
      iExists _,_; iSplit; eauto.
  Qed.

355
  Lemma runner_runTasks_spec γb P Q r:
Dan Frumin's avatar
Dan Frumin committed
356
    {{{ runner γb P Q r }}}
357 358 359 360 361 362 363
      runner_runTasks r
    {{{ RET #(); False }}}.
  Proof.
    iIntros (Φ) "#Hrunner HΦ".
    iLöb as "IH". rewrite /runner_runTasks.
    wp_rec. wp_bind (runner_runTask r).
    iApply runner_runTask_spec; eauto.
364
    iNext. iIntros "_". wp_seq. by iApply "IH".
365 366
  Qed.

367
  Lemma loop_spec (n i : nat) P Q γb r:
Dan Frumin's avatar
Dan Frumin committed
368
    {{{ runner γb P Q r }}}
369
      (RecV "loop" "i" (
370 371
         if: "i" < #n
         then Fork (runner_runTasks r);; "loop" ("i" + #1)
372
         else r)) #i
Dan Frumin's avatar
Dan Frumin committed
373
    {{{ r, RET r; runner γb P Q r }}}.
374 375 376 377 378
  Proof.
    iIntros (Φ) "#Hrunner HΦ".
    iLöb as "IH" forall (i).
    wp_rec. wp_op. case_bool_decide; wp_if; last first.
    { by iApply "HΦ". }
Robbert Krebbers's avatar
Robbert Krebbers committed
379 380
    wp_bind (Fork _). iApply (wp_fork with "[]").
    - iNext. by iApply runner_runTasks_spec.
381
    - iNext. wp_seq. wp_op.
382 383 384 385 386
      (* Set Printing Coercions. *)
      assert ((Z.of_nat i + 1) = Z.of_nat (i + 1)) as -> by lia.
      iApply ("IH" with "HΦ").
  Qed.

387
  Lemma newRunner_spec P Q (f : val) (n : nat) :
388
    {{{  (γ: name Σ b) (r: val),
Dan Frumin's avatar
Dan Frumin committed
389
            a: val, (runner γ P Q r  P a - WP f r a {{ v, Q a v }}) }}}
390
       newRunner f #n
Dan Frumin's avatar
Dan Frumin committed
391
    {{{ γb r, RET r; runner γb P Q r }}}.
392
  Proof.
393
    iIntros (Φ) "#Hf HΦ".
394
    unfold newRunner. iApply wp_fupd.
395
    wp_lam. wp_pures.
396 397 398
    wp_bind (newBag b #()).
    iApply (newBag_spec b (N.@"bag") (λ x y,  γ γ', isTask (f,x) γ γ' y P Q)%I); auto.
    iNext. iIntros (bag). iDestruct 1 as (γb) "#Hbag".
399
    wp_let. wp_pair. wp_let. wp_closure. wp_let.
Dan Frumin's avatar
Dan Frumin committed
400 401
    iAssert (runner γb P Q (PairV f bag))%I with "[]" as "#Hrunner".
    { rewrite runner_unfold. iExists _,_. iSplit; eauto. }
402 403 404 405
    iApply (loop_spec n 0 with "Hrunner [HΦ]"); eauto.
    iNext. iIntros (r) "Hr". by iApply "HΦ".
  Qed.

406
  Lemma runner_Fork_spec γb (r a:val) P Q :
Dan Frumin's avatar
Dan Frumin committed
407
    {{{ runner γb P Q r  P a }}}
408
       runner_Fork r a
409
    {{{ γ γ' t, RET t; task γ γ' t a P Q }}}.
410
  Proof.
411
    iIntros (Φ) "[#Hrunner HP] HΦ".
Dan Frumin's avatar
Dan Frumin committed
412
    rewrite /runner_Fork runner_unfold.
413 414
    iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)". simplify_eq.
    Local Opaque newTask.
415
    wp_lam. wp_pures. wp_bind (newTask _ _).
416
    iApply (newTask_spec γb (body,bag) a P Q with "[Hbag Hbody HP]").
Dan Frumin's avatar
Dan Frumin committed
417
    { iFrame "HP". rewrite runner_unfold.
418 419 420 421
      iExists _,_; iSplit; eauto. }
    iNext. iIntros (γ γ' t) "[Htask Htask']". wp_let.
    wp_bind (pushBag _ _ _).
    iApply (pushBag_spec with "[$Hbag Htask]"); eauto.
422
    iNext. iIntros "_". wp_seq. by iApply "HΦ".
423 424
  Qed.
End contents.
425

Dan Frumin's avatar
Dan Frumin committed
426
Opaque runner task newRunner runner_Fork task_Join.