spawn.v 3.92 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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
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. *)
Lemma spawn_spec (Ψ : val  iProp) (f : val) (Φ : val  iProp) :
  heapN  N 
  (heap_ctx heapN  #> f #() {{ Ψ }}   l, join_handle l Ψ - Φ (%l))
   #> spawn f {{ Φ }}.
Proof.
  intros Hdisj. rewrite /spawn. wp_let. (ewp eapply wp_alloc); eauto with I.
  strip_later. apply forall_intro=>l. apply wand_intro_l. wp_let.
  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". *)
  trans (heap_ctx heapN  #> f #() {{ Ψ }}  (join_handle l Ψ - Φ (%l)%V) 
         own γ (Excl ())   (spawn_inv γ l Ψ))%I.
  { ecancel [ #> f #() {{ _ }}; _ - _; heap_ctx _; own _ _]%I.
    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.
  - wp_focus (f _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v.
    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.
    apply exist_elim=>vl. rewrite later_sep.
    eapply wp_store; eauto using to_val_InjR,to_val_InjL,to_of_val with I ndisj.
    cancel [ (l  vl)]%I. strip_later. apply wand_intro_l.
    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) :
  (join_handle l Ψ   v, Ψ v - Φ (%l))
   #> join (%l) {{ Φ }}.
Proof.
Abort.

End proof.