From program_logic Require Export hoare.
From barrier Require Export barrier.
From barrier Require Import proof.
Import uPred.

Section spec.
Context {Σ : gFunctors} `{!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 }} newbarrier #() {{ λ v,
                             ∃ l : loc, 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) ={N}=> 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 -(newbarrier_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 vs_alt. rewrite -(recv_split heapN N N l P Q) //.
  - intros l P Q. apply recv_weaken.
Qed.
End spec.