From d38ca7995d93b08d01ced936069c5b11d7d85f5d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Mar 2016 14:35:08 +0100
Subject: [PATCH] prove join and par

---
 heap_lang/lang.v  |  4 ++++
 heap_lang/par.v   | 41 ++++++++++++++++++++++++++++------
 heap_lang/spawn.v | 56 +++++++++++++++++++++++++++++++++++++----------
 3 files changed, 82 insertions(+), 19 deletions(-)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index fbc352ce2..c8c901961 100644
--- a/heap_lang/lang.v
+++ b/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).
diff --git a/heap_lang/par.v b/heap_lang/par.v
index 3bbdda8c5..34332f9ea 100644
--- a/heap_lang/par.v
+++ b/heap_lang/par.v
@@ -1,23 +1,50 @@
 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.
\ No newline at end of file
+Lemma wp_par (Î¨1 Î¨2 : val â†’ iProp) (e1 e2 : expr []) (Î¦ : val â†’ iProp) :
+  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.
diff --git a/heap_lang/spawn.v b/heap_lang/spawn.v
index 84676f004..5bb8fe9d1 100644
--- a/heap_lang/spawn.v
+++ b/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.
-- 
GitLab