spawn.v 5.64 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
From program_logic Require Export global_functor.
From heap_lang Require Export heap.
From heap_lang Require Import wp_tactics notation.
Import uPred.

Definition spawn : val :=
  λ: "f", let: "c" := ref (InjL #0) in
          Fork ('"c" <- InjR ('"f" #())) ;; '"c".
Definition join : val :=
  rec: "join" "c" := match: !'"c" with InjR "x" => '"x"
                                     | InjL <>  => '"join" '"c" end.

(** The monoids we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG {
  spawn_tokG :> inG heap_lang Σ (exclR unitC);
}.
Definition spawnGF : rFunctors := [constRF (exclR unitC)].

Instance inGF_spawnG
  `{inGF heap_lang Σ (constRF (exclR unitC))} : spawnG Σ.
Proof. split. apply: inGF_inG. Qed.

(** Now we come to the Iris part of the proof. *)
Section proof.
Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).

Definition spawn_inv (γ : gname) (l : loc) (Ψ : val  iProp) : iProp :=
  ( lv, l  lv  (lv = InjLV #0   v, lv = InjRV v  (Ψ v  own γ (Excl ()))))%I.

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
45
46
Lemma spawn_spec (Ψ : val  iProp) e (f : val) (Φ : val  iProp) :
  to_val e = Some f 
Ralf Jung's avatar
Ralf Jung committed
47
  heapN  N 
48
  (heap_ctx heapN  #> f #() {{ Ψ }}   l, join_handle l Ψ - Φ (%l))
Ralf Jung's avatar
Ralf Jung committed
49
   #> spawn e {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
50
Proof.
Ralf Jung's avatar
Ralf Jung committed
51
52
53
54
55
56
  intros Hval Hdisj. rewrite /spawn.
  (* TODO: Make this more convenient. *)
  wp_focus e. etransitivity; last by eapply wp_value. wp_let.
  (* FIXME: can we change the ewp notation so that the parentheses become unnecessary? *)
  (ewp eapply wp_alloc); eauto with I. strip_later.
  apply forall_intro=>l. apply wand_intro_l. wp_let.
Ralf Jung's avatar
Ralf Jung committed
57
58
59
60
61
  rewrite (forall_elim l). eapply sep_elim_True_l.
  { eapply (own_alloc (Excl ())). done. }
  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". *)
62
  trans (heap_ctx heapN  #> f #() {{ Ψ }}  (join_handle l Ψ - Φ (%l)%V) 
Ralf Jung's avatar
Ralf Jung committed
63
         own γ (Excl ())   (spawn_inv γ l Ψ))%I.
Ralf Jung's avatar
Ralf Jung committed
64
  { ecancel [ #> _ {{ _ }}; _ - _; heap_ctx _; own _ _]%I.
Ralf Jung's avatar
Ralf Jung committed
65
66
67
68
69
70
71
72
73
    rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
    cancel [l  InjLV #0]%I. apply or_intro_l'. by rewrite const_equiv. }
  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.
  rewrite !assoc [(_  (own _ _))%I]comm !assoc [(_  (inv _ _))%I]comm.
  rewrite !assoc [(_  (_ - _))%I]comm. rewrite -!assoc 3!assoc. apply sep_mono.
  - wp_seq. rewrite -!assoc. eapply wand_apply_l; [done..|].
    rewrite /join_handle. rewrite const_equiv // left_id -(exist_intro γ).
    solve_sep_entails.
Ralf Jung's avatar
Ralf Jung committed
74
75
  - wp_focus (f _). rewrite wp_frame_r wp_frame_l.
    rewrite (of_to_val e) //. apply wp_mono=>v.
Ralf Jung's avatar
Ralf Jung committed
76
77
78
79
    eapply (inv_fsa (wp_fsa _)) with (N0:=N); simpl;
      (* TODO: Collect these in some Hint DB? Or add to an existing one? *)
      eauto using to_val_InjR,to_val_InjL,to_of_val with I ndisj.
    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.
Ralf Jung's avatar
Ralf Jung committed
81
    eapply wp_store; eauto using to_val_InjR,to_val_InjL,to_of_val 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)
Ralf Jung's avatar
Ralf Jung committed
90
91
   #> join (%l) {{ Φ }}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
92
93
94
95
96
97
98
99
100
101
102
  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.
  apply exist_elim=>lv. rewrite later_sep.
  eapply wp_load; eauto with I ndisj. cancel [ (l  lv)]%I. strip_later.
  apply wand_intro_l. rewrite -later_intro -[X in _  (X  _)](exist_intro lv).
  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
    do 2 rewrite const_equiv // left_id. wp_case; eauto.
Ralf Jung's avatar
Ralf Jung committed
104
105
106
107
108
109
110
111
112
113
    wp_seq. rewrite -always_wand_impl always_elim.
    rewrite !assoc. eapply wand_apply_r'; first done.
    rewrite -(exist_intro γ). solve_sep_entails.
  - 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; eauto using to_of_val.
Ralf Jung's avatar
Ralf Jung committed
115
116
117
    wp_let. etransitivity; last by eapply wp_value, to_of_val.
    rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I.
Qed.
Ralf Jung's avatar
Ralf Jung committed
118
119

End proof.