diff --git a/examples/joining_existentials.v b/examples/joining_existentials.v index b40f03c834c272ed17b075a9f15926bbc35f9080..15b8dabccf06498a2d50c555fa3413bad939ab0c 100644 --- a/examples/joining_existentials.v +++ b/examples/joining_existentials.v @@ -9,7 +9,7 @@ Definition client eM eW1 eW2 : expr [] := Section proof. Context (G : cFunctor). -Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !oneShotG heap_lang Σ G}. +Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ G}. Context (heapN N : namespace). Local Notation iProp := (iPropG heap_lang Σ). Local Notation X := (G iProp). @@ -18,33 +18,88 @@ Definition barrier_res γ (P : X → iProp) : iProp := (∃ x:X, one_shot_own γ x ★ P x)%I. -Lemma worker_spec e γ l (P Q : X → iProp) (R : iProp) Φ : +Lemma worker_spec e γ l (P Q : X → iProp) (R : iProp) : R ⊢ (∀ x, {{ P x }} e {{ λ _, Q x }}) → - R ⊢ (recv heapN N l (barrier_res γ P) ★ (∀ v : val, barrier_res γ Q -★ Φ v )) → - R ⊢ WP wait (%l) ;; e {{ Φ }}. + R ⊢ (recv heapN N l (barrier_res γ P)) → + R ⊢ WP wait (%l) ;; e {{ λ _, barrier_res γ Q }}. Proof. intros He HΦ. rewrite -[R](idemp (∧)%I) {1}He HΦ always_and_sep_l {He HΦ}. ewp (eapply wait_spec). ecancel [recv _ _ l _]. apply wand_intro_r. wp_seq. rewrite /barrier_res sep_exist_l. apply exist_elim=>x. rewrite (forall_elim x) /ht always_elim impl_wand !assoc. to_front [P x; _ -★ _]%I. rewrite wand_elim_r !wp_frame_r. - apply wp_mono=>v. rewrite (forall_elim v). rewrite -(exist_intro x). - to_front [one_shot_own _ _; Q _]. by rewrite wand_elim_r. + apply wp_mono=>v. by rewrite -(exist_intro x) comm. Qed. -Context (P' : iProp) (P P1 P2 Q Q1 Q2 : X → iProp). -Context {P_split : (∃ x:X, P x) ⊢ ((∃ x:X, P1 x) ★ (∃ x:X, P2 x))}. -Context {Q_join : ((∃ x:X, Q1 x) ★ (∃ x:X, Q2 x)) ⊢ (∃ x:X, Q x)}. +Context (P' : iProp) (P P1 P2 Q Q1 Q2 : X -n> iProp). +Context {P_split : ∀ x:X, P x ⊢ (P1 x ★ P2 x)}. +Context {Q_join : ∀ x:X, (Q1 x ★ Q2 x) ⊢ Q x}. + +Lemma P_res_split γ : + barrier_res γ P ⊢ (barrier_res γ P1 ★ barrier_res γ P2). +Proof. + rewrite /barrier_res. apply exist_elim=>x. do 2 rewrite -(exist_intro x). + rewrite P_split {1}[one_shot_own _ _]always_sep_dup. + solve_sep_entails. +Qed. + +Lemma Q_res_join γ : + (barrier_res γ Q1 ★ barrier_res γ Q2) ⊢ ▷ barrier_res γ Q. +Proof. + rewrite /barrier_res sep_exist_r. apply exist_elim=>x1. + rewrite sep_exist_l. apply exist_elim=>x2. + rewrite [one_shot_own γ x1]always_sep_dup. + to_front [one_shot_own γ x1; one_shot_own γ x2]. rewrite one_shot_agree. + strip_later. rewrite -(exist_intro x1) -Q_join. + ecancel [one_shot_own γ _; Q1 _]. + eapply (eq_rewrite x2 x1 (λ x, Q2 x)); last by eauto with I. + { (* FIXME typeclass search should find this. *) + apply cofe_mor_ne. } + rewrite eq_sym. eauto with I. +Qed. Lemma client_spec (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) (R : iProp) : - eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 → + heapN ⊥ N → eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 → R ⊢ ({{ P' }} eM {{ λ _, ∃ x, P x }}) → R ⊢ (∀ x, {{ P1 x }} eW1 {{ λ _, Q1 x }}) → R ⊢ (∀ x, {{ P2 x }} eW2 {{ λ _, Q2 x }}) → R ⊢ heap_ctx heapN → + R ⊢ P' → R ⊢ WP client eM' eW1' eW2' {{ λ _, ∃ γ, barrier_res γ Q }}. Proof. -Abort. - + intros HN -> -> -> HeM HeW1 HeW2 Hheap HP'. + rewrite -4!{1}[R](idemp (∧)%I) {1}HeM {1}HeW1 {1}HeW2 {1}Hheap {1}HP' !always_and_sep_l {Hheap} /client. + to_front []. rewrite one_shot_alloc !pvs_frame_r !sep_exist_r. + apply wp_strip_pvs, exist_elim=>γ. rewrite {1}[heap_ctx _]always_sep_dup. + (ewp (eapply (newbarrier_spec heapN N (barrier_res γ P)))); last done. + cancel [heap_ctx heapN]. apply forall_intro=>l. apply wand_intro_r. + set (workers_post (v : val) := (barrier_res γ Q1 ★ barrier_res γ Q2)%I). + wp_let. (ewp (eapply wp_par with (Ψ1 := λ _, True%I) (Ψ2 := workers_post))); last first. + { done. } (* FIXME why does this simple goal even appear? *) + rewrite {1}[heap_ctx _]always_sep_dup. cancel [heap_ctx heapN]. + sep_split left: [one_shot_pending γ; send _ _ _ _ ; P'; {{ _ }} eM {{ _ }}]%I. + { (* Main thread. *) + wp_focus eM. rewrite /ht always_elim impl_wand wand_elim_r !wp_frame_l. + apply wp_mono=>v. wp_seq. rewrite !sep_exist_l. apply exist_elim=>x. + rewrite (one_shot_init _ γ x) !pvs_frame_r. apply wp_strip_pvs. + ewp (eapply signal_spec). ecancel [send _ _ _ _]. + by rewrite /barrier_res -(exist_intro x). } + sep_split right: []. + - (* Worker threads. *) + rewrite recv_mono; last exact: P_res_split. rewrite (recv_split _ _ ⊤) //. + rewrite ?pvs_frame_r !pvs_frame_l. apply wp_strip_pvs. + (ewp (eapply wp_par with (Ψ1 := λ _, barrier_res γ Q1) (Ψ2 := λ _, barrier_res γ Q2))); last first. + { done. } ecancel [heap_ctx _]. + sep_split left: [recv _ _ _ (barrier_res γ P1); ∀ _, {{ _ }} eW1 {{ _ }}]%I. + { eapply worker_spec; eauto with I. } + sep_split left: [recv _ _ _ (barrier_res γ P2); ∀ _, {{ _ }} eW2 {{ _ }}]%I. + { eapply worker_spec; eauto with I. } + rewrite /workers_post. do 2 apply forall_intro=>_. + (* FIXME: this should work: rewrite -later_intro. *) + apply wand_intro_r. rewrite -later_intro. solve_sep_entails. + - (* Merging. *) + rewrite /workers_post. do 2 apply forall_intro=>_. apply wand_intro_r. + rewrite !left_id Q_res_join. strip_later. by rewrite -(exist_intro γ). +Qed. End proof. diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v index 5ecd40c6b68ba13921acf1da79bb5eaf4b0d6481..c3745ea7a2463d9bce44d075c34994013ed7d3fa 100644 --- a/heap_lang/substitution.v +++ b/heap_lang/substitution.v @@ -140,6 +140,17 @@ Proof. apply wsubst_closed, not_elem_of_nil. Qed. +(* Closed expressions *) +Instance do_wsubst_expr_nil' {X} x es (H : X `included` [x]) e : + WSubst x es H (wexpr' e) e | 0. +Proof. by rewrite /WSubst /wexpr' wsubst_wexpr' wsubst_closed_nil. Qed. +Instance do_wsubst_wexpr' X Y x es (H : X `included` x :: Y) e : + WSubst x es H (wexpr' e) (wexpr' e) | 1. +Proof. + rewrite /WSubst /wexpr' wsubst_wexpr'. + apply wsubst_closed, not_elem_of_nil. +Qed. + (* Boring connectives *) Section wsubst. Context {X Y} (x : string) (es : expr []) (H : X `included` x :: Y).