spawn.v 3.46 KB
Newer Older
1
From iris.program_logic Require Export global_functor.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation.
Ralf Jung's avatar
Ralf Jung committed
4 5 6
Import uPred.

Definition spawn : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  λ: "f",
8 9
    let: "c" := ref (InjL #0) in
    Fork ('"c" <- InjR ('"f" #())) ;; '"c".
Ralf Jung's avatar
Ralf Jung committed
10
Definition join : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15
  rec: "join" "c" :=
    match: !'"c" with
      InjR "x" => '"x"
    | InjL <>  => '"join" '"c"
    end.
Ralf Jung's avatar
Ralf Jung committed
16

17
(** The CMRA we need. *)
Ralf Jung's avatar
Ralf Jung committed
18 19 20 21
(* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG {
  spawn_tokG :> inG heap_lang Σ (exclR unitC);
}.
22
(** The functor we need. *)
23
Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
24
(* Show and register that they match. *)
Ralf Jung's avatar
Ralf Jung committed
25
Instance inGF_spawnG
26 27
  `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
Ralf Jung's avatar
Ralf Jung committed
28 29 30

(** Now we come to the Iris part of the proof. *)
Section proof.
31
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
Ralf Jung's avatar
Ralf Jung committed
32 33 34 35
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).

Definition spawn_inv (γ : gname) (l : loc) (Ψ : val  iProp) : iProp :=
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37
  ( lv, l  lv  (lv = InjLV #0 
                    v, lv = InjRV v  (Ψ v  own γ (Excl ()))))%I.
Ralf Jung's avatar
Ralf Jung committed
38 39

Definition join_handle (l : loc) (Ψ : val  iProp) : iProp :=
40 41
  (heapN  N   γ, heap_ctx heapN  own γ (Excl ()) 
                    inv N (spawn_inv γ l Ψ))%I.
Ralf Jung's avatar
Ralf Jung committed
42

Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
Typeclasses Opaque join_handle.

Ralf Jung's avatar
Ralf Jung committed
45 46 47 48 49 50 51 52
Global Instance spawn_inv_ne n γ l :
  Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
Proof. solve_proper. Qed.
Global Instance join_handle_ne n l :
  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle l).
Proof. solve_proper. Qed.

(** The main proofs. *)
Ralf Jung's avatar
Ralf Jung committed
53 54
Lemma spawn_spec (Ψ : val  iProp) e (f : val) (Φ : val  iProp) :
  to_val e = Some f 
Ralf Jung's avatar
Ralf Jung committed
55
  heapN  N 
56
  (heap_ctx heapN  WP f #() {{ Ψ }}   l, join_handle l Ψ - Φ #l)
57
   WP spawn e {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
58
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61
  iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
  wp_let; wp_alloc l as "Hl"; wp_let.
  iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
62
  iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64
  { iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. }
  wp_apply wp_fork. iSplitR "Hf".
65 66
  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle.
    iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69 70
  - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
    iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]".
    wp_store. iSplit; [iNext|done].
    iExists (InjRV v); iFrame "Hl"; iRight; iExists v; iSplit; [done|by iLeft].
Ralf Jung's avatar
Ralf Jung committed
71 72 73
Qed.

Lemma join_spec (Ψ : val  iProp) l (Φ : val  iProp) :
74
  (join_handle l Ψ   v, Ψ v - Φ v)  WP join #l {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
75
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
77
  iLöb as "IH". wp_rec. wp_focus (! _)%E.
Robbert Krebbers's avatar
Robbert Krebbers committed
78 79 80
  iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
  - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
81
    wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84 85 86
  - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
    + iSplitL "Hl Hγ".
      { iNext. iExists _; iFrame "Hl"; iRight.
        iExists _; iSplit; [done|by iRight]. }
      wp_case. wp_let. iPvsIntro. by iApply "Hv".
87
    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Ralf Jung's avatar
Ralf Jung committed
88
Qed.
Ralf Jung's avatar
Ralf Jung committed
89
End proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
90 91

Typeclasses Opaque join_handle.