start proving spawn-join

_CoqProject

@@ -81,6 +81,7 @@ heap_lang/lifting.v
 heap_lang/derived.v
 heap_lang/heap.v
 heap_lang/notation.v
+heap_lang/spawn.v
 heap_lang/tests.v
 heap_lang/substitution.v
 barrier/barrier.v

heap_lang/lang.v

@@ -417,6 +417,17 @@ Proof.
   apply wsubst_closed, not_elem_of_nil.
 Qed.
 
+(** to_val propagation.
+    TODO: automatically appliy in wp_tactics? *)
+Lemma to_val_InjL e v : to_val e = Some v → to_val (InjL e) = Some (InjLV v).
+Proof. move=>H. simpl. by rewrite H. Qed.
+Lemma to_val_InjR e v : to_val e = Some v → to_val (InjR e) = Some (InjRV v).
+Proof. move=>H. simpl. by rewrite H. Qed.
+Lemma to_val_Pair e1 e2 v1 v2 :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  to_val (Pair e1 e2) = Some (PairV v1 v2).
+Proof. move=>H1 H2. simpl. by rewrite H1 H2. Qed.
+
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
 Proof. by induction v; simplify_option_eq. Qed.
@@ -525,7 +536,7 @@ Lemma alloc_fresh e v σ :
   to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
-(** Equality stuff *)
+(** Equality and other typeclass stuff *)
 Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
 Proof. solve_decision. Defined.
 Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
@@ -567,6 +578,9 @@ Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
 Proof.
  refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
 Defined.
+
+Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
+Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
 End heap_lang.
 
 (** Language *)

heap_lang/spawn.v

+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.