From program_logic Require Export hoare. From barrier Require Export barrier. From barrier Require Import proof. Import uPred. Section spec. Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}. Local Notation iProp := (iPropG heap_lang Σ). (* TODO: Maybe notation for LocV (and Loc)? *) Lemma barrier_spec (heapN N : namespace) : heapN ⊥ N → ∃ recv send : loc → iProp -n> iProp, (∀ P, heap_ctx heapN ⊑ {{ True }} newchan '() {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }}) ∧ (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧ (∀ l P Q, {{ recv l (P ★ Q) }} Skip {{ λ _, recv l P ★ recv l Q }}) ∧ (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)). Proof. intros HN. exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)). split_and?; simpl. - intros P. apply: always_intro. apply impl_intro_r. rewrite -(newchan_spec heapN N P) // always_and_sep_r. apply sep_mono_r, forall_intro=>l; apply wand_intro_l. by rewrite right_id -(exist_intro l) const_equiv // left_id. - intros l P. apply ht_alt. by rewrite -signal_spec right_id. - intros l P. apply ht_alt. by rewrite -(wait_spec heapN N l P) wand_diag right_id. - intros l P Q. apply ht_alt. rewrite -(recv_split heapN N l P Q). apply sep_intro_True_r; first done. apply wand_intro_l. eauto with I. - intros l P Q. apply recv_strengthen. Qed. End spec.