prove join and par

heap_lang/lang.v

@@ -417,6 +417,10 @@ Proof.
   apply wsubst_closed, not_elem_of_nil.
 Qed.
 
+Lemma of_val'_closed (v : val) :
+  of_val' v = of_val v.
+Proof. by rewrite /of_val' wexpr_id. 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).

heap_lang/par.v

 From heap_lang Require Export heap.
-From heap_lang Require Import spawn notation.
+From heap_lang Require Import spawn wp_tactics notation.
+Import uPred.
 
 Definition par : val :=
   λ: "f1" "f2", let: "handle" := ^spawn '"f1" in
                 let: "v2" := '"f2" #() in
                 let: "v1" := ^join '"handle" in
                 Pair '"v1" '"v2".
-Notation Par e1 e2 := (^par (λ: <>, e1)%V (λ: <>, e2)%V)%E.
+Notation Par e1 e2 := (^par (λ: <>, e1) (λ: <>, e2))%E.
+Infix "||" := Par : expr_scope.
 
 Section proof.
 Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
 Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
-Lemma par_spec (Ψ1 Ψ2 : val → iProp) (f1 f2 : val) (Φ : val → iProp) :
-  (#> f1 #() {{ Ψ1 }} ★ #> f2 #() {{ Ψ2 }} ★
+Lemma par_spec (Ψ1 Ψ2 : val → iProp) e1 e2 (f1 f2 : val) (Φ : val → iProp) :
+  heapN ⊥ N → to_val e1 = Some f1 → to_val e2 = Some f2 →
+  (* TODO like in spawn.v -- wp about e or f? *)
+  (heap_ctx heapN ★ #> e1 #() {{ Ψ1 }} ★ #> e2 #() {{ Ψ2 }} ★
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ Φ (PairV v1 v2))
-  ⊑ #> par f1 f2 {{ Φ }}.
+  ⊑ #> par e1 e2 {{ Φ }}.
 Proof.
-Abort.
+  intros. rewrite /par.
+  wp_focus e1. etransitivity; last by eapply wp_value. wp_let.
+  wp_focus e2. etransitivity; last by eapply wp_value. wp_let.
+  (ewp eapply spawn_spec); eauto using to_of_val.
+  apply sep_mono_r. rewrite (of_to_val e1) //. apply sep_mono_r.
+  apply forall_intro=>h. apply wand_intro_l. wp_let.
+  wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. rewrite (of_to_val e2) //.
+  apply wp_mono=>v2. wp_let.
+  (ewp eapply join_spec); eauto using to_of_val. apply sep_mono_r.
+  apply forall_intro=>v1. apply wand_intro_l. wp_let.
+  etransitivity; last by (eapply wp_value, to_val_Pair; eapply to_of_val).
+  rewrite (forall_elim v1) (forall_elim v2). rewrite assoc.
+  eapply wand_apply_r'; done.
+Qed.
 
-End proof.
+Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
\ No newline at end of file
+  heapN ⊥ N →
+  (heap_ctx heapN ★ #> e1 {{ Ψ1 }} ★ #> e2 {{ Ψ2 }} ★
+   ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ Φ (PairV v1 v2))
+  ⊑ #> e1 || e2 {{ Φ }}.
+Proof.
+  intros. rewrite of_val'_closed -par_spec //. apply sep_mono_r.
+  apply sep_mono; last apply sep_mono_l; by wp_seq.
+Qed.
+
+End proof.

heap_lang/spawn.v

@@ -42,21 +42,27 @@ Global Instance join_handle_ne n l :
 Proof. solve_proper. Qed.
 
 (** The main proofs. *)
-Lemma spawn_spec (Ψ : val → iProp) (f : val) (Φ : val → iProp) :
+Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
+  to_val e = Some f →
   heapN ⊥ N →
-  (heap_ctx heapN ★ #> f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
-  ⊑ #> spawn f {{ Φ }}.
+  (* TODO: Not sure whether the wp should be about [e] or [f]. Both work. *)
+  (heap_ctx heapN ★ #> e #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
+  ⊑ #> spawn e {{ Φ }}.
 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.
+  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.
   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) ★
+  trans (heap_ctx heapN ★ #> e #() {{ Ψ }} ★ (join_handle l Ψ -★ Φ (%l)%V) ★
          own γ (Excl ()) ★ ▷ (spawn_inv γ l Ψ))%I.
-  { ecancel [ #> f #() {{ _ }}; _ -★ _; heap_ctx _; own _ _]%I.
+  { ecancel [ #> _ {{ _ }}; _ -★ _; 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.
@@ -66,23 +72,49 @@ Proof.
   - 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.
+  - wp_focus (f _). rewrite wp_frame_r wp_frame_l.
+    rewrite (of_to_val e) //. 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.
+    apply exist_elim=>lv. 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.
+    cancel [▷ (l ↦ lv)]%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_handle l Ψ ★ ∀ v, Ψ v -★ Φ v)
   ⊑ #> join (%l) {{ Φ }}.
 Proof.
-Abort.
+  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}.
+    do 2 rewrite const_equiv // left_id. (ewp eapply wp_case_inl); eauto.
+    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 _ _].
+    (ewp apply: wp_case_inr); eauto using to_of_val.
+    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.
 
 End proof.