spawn.v 5.26 KB
Newer Older
1 2 3
From iris.program_logic Require Export global_functor.
From iris.heap_lang Require Export heap.
From iris.heap_lang Require Import wp_tactics 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 :=
36
  ( lv, l  lv  (lv = InjLV #0   v, lv = InjRV v  (Ψ v  own γ (Excl ()))))%I.
Ralf Jung's avatar
Ralf Jung committed
37 38 39 40 41 42 43 44 45 46 47 48 49

Definition join_handle (l : loc) (Ψ : val  iProp) : iProp :=
  ( (heapN  N)   γ, heap_ctx heapN  own γ (Excl ()) 
                        inv N (spawn_inv γ l Ψ))%I.

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
50 51
Lemma spawn_spec (Ψ : val  iProp) e (f : val) (Φ : val  iProp) :
  to_val e = Some f 
Ralf Jung's avatar
Ralf Jung committed
52
  heapN  N 
53
  (heap_ctx heapN  WP f #() {{ Ψ }}   l, join_handle l Ψ - Φ (%l))
54
   WP spawn e {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
55
Proof.
56 57
  intros Hval Hdisj. rewrite /spawn. ewp (by eapply wp_value). wp_let.
  wp eapply wp_alloc; eauto with I.
Ralf Jung's avatar
Ralf Jung committed
58
  apply forall_intro=>l. apply wand_intro_l. wp_let.
Ralf Jung's avatar
Ralf Jung committed
59
  rewrite (forall_elim l). eapply sep_elim_True_l.
60
  { by eapply (own_alloc (Excl ())). }
Ralf Jung's avatar
Ralf Jung committed
61 62 63
  rewrite !pvs_frame_r. eapply wp_strip_pvs. rewrite !sep_exist_r.
  apply exist_elim=>γ.
  (* TODO: Figure out a better way to say "I want to establish ▷ spawn_inv". *)
64
  trans (heap_ctx heapN  WP f #() {{ Ψ }}  (join_handle l Ψ - Φ (%l)%V) 
Ralf Jung's avatar
Ralf Jung committed
65
         own γ (Excl ())   (spawn_inv γ l Ψ))%I.
66
  { ecancel [ WP _ {{ _ }}; _ - _; heap_ctx _; own _ _]%I.
67 68
    rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
    cancel [l  InjLV #0]%I. by apply or_intro_l', const_intro. }
Ralf Jung's avatar
Ralf Jung committed
69 70
  rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
  ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup.
71
  sep_split left: [_ - _; inv _ _; own _ _; heap_ctx _]%I.
72
  - wp_seq. rewrite -pvs_intro. eapply wand_apply_l; [done..|].
Ralf Jung's avatar
Ralf Jung committed
73 74
    rewrite /join_handle. rewrite const_equiv // left_id -(exist_intro γ).
    solve_sep_entails.
Ralf Jung's avatar
Ralf Jung committed
75 76
  - wp_focus (f _). rewrite wp_frame_r wp_frame_l.
    rewrite (of_to_val e) //. apply wp_mono=>v.
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78
    eapply (inv_fsa (wp_fsa _)) with (N0:=N);
      rewrite /= ?to_of_val; eauto with I ndisj.
Ralf Jung's avatar
Ralf Jung committed
79
    apply wand_intro_l. rewrite /spawn_inv {1}later_exist !sep_exist_r.
Ralf Jung's avatar
Ralf Jung committed
80
    apply exist_elim=>lv. rewrite later_sep.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    eapply wp_store; rewrite /= ?to_of_val; eauto with I ndisj.
Ralf Jung's avatar
Ralf Jung committed
82
    cancel [ (l  lv)]%I. strip_later. apply wand_intro_l.
Ralf Jung's avatar
Ralf Jung committed
83 84 85 86 87 88
    rewrite right_id -later_intro -{2}[( _, _  _  _)%I](exist_intro (InjRV v)).
    ecancel [l  _]%I. apply or_intro_r'. rewrite sep_elim_r sep_elim_r sep_elim_l.
    rewrite -(exist_intro v). rewrite const_equiv // left_id. apply or_intro_l.
Qed.

Lemma join_spec (Ψ : val  iProp) l (Φ : val  iProp) :
Ralf Jung's avatar
Ralf Jung committed
89
  (join_handle l Ψ   v, Ψ v - Φ v)
90
   WP join (%l) {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
91
Proof.
Ralf Jung's avatar
Ralf Jung committed
92 93 94 95 96
  wp_rec. wp_focus (! _)%E.
  rewrite {1}/join_handle sep_exist_l !sep_exist_r. apply exist_elim=>γ.
  rewrite -!assoc. apply const_elim_sep_l=>Hdisj.
  eapply (inv_fsa (wp_fsa _)) with (N0:=N); simpl; eauto with I ndisj.
  apply wand_intro_l. rewrite /spawn_inv {1}later_exist !sep_exist_r.
97 98
  apply exist_elim=>lv.
  wp eapply wp_load; eauto with I ndisj. cancel [l  lv]%I.
99
  apply wand_intro_l. rewrite -later_intro -[X in _  (X  _)](exist_intro lv).
Ralf Jung's avatar
Ralf Jung committed
100 101 102
  cancel [l  lv]%I. rewrite sep_or_r. apply or_elim.
  - (* Case 1 : nothing sent yet, we wait. *)
    rewrite -or_intro_l. apply const_elim_sep_l=>-> {lv}.
103
    rewrite (const_equiv (_ = _)) // left_id. wp_case.
Ralf Jung's avatar
Ralf Jung committed
104 105
    wp_seq. rewrite -always_wand_impl always_elim.
    rewrite !assoc. eapply wand_apply_r'; first done.
106
    rewrite -(exist_intro γ) const_equiv //. solve_sep_entails.
Ralf Jung's avatar
Ralf Jung committed
107 108 109 110 111 112 113
  - rewrite [(_   _)%I]sep_elim_l -or_intro_r !sep_exist_r. apply exist_mono=>v.
    rewrite -!assoc. apply const_elim_sep_l=>->{lv}. rewrite const_equiv // left_id.
    rewrite sep_or_r. apply or_elim; last first.
    { (* contradiction: we have the token twice. *)
      rewrite [(heap_ctx _  _)%I]sep_elim_r !assoc. rewrite -own_op own_valid_l.
      rewrite -!assoc discrete_valid. apply const_elim_sep_l=>-[]. }
    rewrite -or_intro_r. ecancel [own _ _].
114
    wp_case. wp_let. ewp (eapply wp_value; wp_done).
Ralf Jung's avatar
Ralf Jung committed
115 116
    rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I.
Qed.
Ralf Jung's avatar
Ralf Jung committed
117
End proof.