spawn.v 3.22 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2 3
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris.heap_lang Require Import proofmode notation.
5
From iris.algebra Require Import excl.
Ralf Jung's avatar
Ralf Jung committed
6 7

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

19
(** The CMRA we need. *)
Ralf Jung's avatar
Ralf Jung committed
20
(* Not bundling heapG, as it may be shared with other users. *)
21
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
22 23 24 25 26

(** The functor we need and register that they match. *)
Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ  spawnG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
27 28 29

(** Now we come to the Iris part of the proof. *)
Section proof.
30
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Ralf Jung's avatar
Ralf Jung committed
31

32
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val  iProp Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
  ( lv, l  lv  (lv = NONEV 
                    v, lv = SOMEV v  (Ψ v  own γ (Excl ()))))%I.
Ralf Jung's avatar
Ralf Jung committed
35

36
Definition join_handle (l : loc) (Ψ : val  iProp Σ) : iProp Σ :=
37 38
  (heapN  N   γ, heap_ctx  own γ (Excl ()) 
                    inv N (spawn_inv γ l Ψ))%I.
Ralf Jung's avatar
Ralf Jung committed
39

Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
Typeclasses Opaque join_handle.

Ralf Jung's avatar
Ralf Jung committed
42 43 44 45 46 47 48 49
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. *)
50
Lemma spawn_spec (Ψ : val  iProp Σ) e (f : val) (Φ : val  iProp Σ) :
Ralf Jung's avatar
Ralf Jung committed
51
  to_val e = Some f 
52
  heapN  N 
53
  heap_ctx  WP f #() {{ Ψ }}  ( l, join_handle l Ψ - Φ #l)
54
   WP spawn e {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
55
Proof.
56
  iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
57
  wp_let. wp_alloc l as "Hl". wp_let.
58 59
  iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
  iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  { iNext. iExists NONEV. iFrame; eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  wp_apply wp_fork. iSplitR "Hf".
62
  - iVsIntro. wp_seq. iVsIntro. iApply "HΦ". rewrite /join_handle. eauto.
63
  - wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
64 65
    iInv N as (v') "[Hl _]" "Hclose".
    wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Ralf Jung's avatar
Ralf Jung committed
66 67
Qed.

68
Lemma join_spec (Ψ : val  iProp Σ) l (Φ : val  iProp Σ) :
69
  join_handle l Ψ  ( v, Ψ v - Φ v)  WP join #l {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
70
Proof.
71
  rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
72
  iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
74 75
  - iVs ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
    iVsIntro. wp_match. iApply ("IH" with "Hγ Hv").
76
  - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
77 78
    + iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
      iVsIntro. wp_match. by iApply "Hv".
79
    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Ralf Jung's avatar
Ralf Jung committed
80
Qed.
Ralf Jung's avatar
Ralf Jung committed
81
End proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83

Typeclasses Opaque join_handle.