spawn.v 3.29 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.
16
Global Opaque spawn join.
Ralf Jung's avatar
Ralf Jung committed
17

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

(** Now we come to the Iris part of the proof. *)
Section proof.
32
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
Ralf Jung's avatar
Ralf Jung committed
33 34 35 36
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
37 38
  ( lv, l  lv  (lv = InjLV #0 
                    v, lv = InjRV v  (Ψ v  own γ (Excl ()))))%I.
Ralf Jung's avatar
Ralf Jung committed
39 40

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

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

Ralf Jung's avatar
Ralf Jung committed
46 47 48 49 50 51 52 53
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
54 55
Lemma spawn_spec (Ψ : val  iProp) e (f : val) (Φ : val  iProp) :
  to_val e = Some f 
Ralf Jung's avatar
Ralf Jung committed
56
  heapN  N 
57
  heap_ctx heapN  WP f #() {{ Ψ }}  ( l, join_handle l Ψ - Φ #l)
58
   WP spawn e {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
59
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
61
  wp_let. wp_alloc l as "Hl". wp_let.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
63
  iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
64
  { iNext. iExists (InjLV #0). iFrame "Hl"; eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  wp_apply wp_fork. iSplitR "Hf".
66
  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
68
    iInv N as {v'} "[Hl _]"; first wp_done.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
    wp_store. iSplit; [iNext|done].
70
    iExists (InjRV v); iFrame "Hl"; eauto.
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. iInv N as {v} "[Hl Hinv]".
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
79
  - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; eauto|].
80
    wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
  - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
    + iSplitL "Hl Hγ".
83
      { iNext. iExists _; iFrame "Hl"; eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
84
      wp_case. wp_let. iPvsIntro. by iApply "Hv".
85
    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Ralf Jung's avatar
Ralf Jung committed
86
Qed.
Ralf Jung's avatar
Ralf Jung committed
87
End proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
88 89

Typeclasses Opaque join_handle.