From barrier Require Import barrier.
From program_logic Require Import auth sts saved_prop hoare ownership.
(* FIXME This needs to be imported even though barrier exports it *)
From heap_lang Require Import notation.
Import uPred.

Definition client := (let: "b" := newchan '() in wait "b")%L.

Section client.
  Context {Σ : iFunctorG} (N : namespace).
  Context `{heapG Σ} (heapN : namespace).
  Context `{stsG heap_lang Σ barrier_proto.sts}.
  Context `{savedPropG heap_lang Σ}.

  Local Notation iProp := (iPropG heap_lang Σ).

  Lemma client_safe :
    heapN ⊥ N → heap_ctx heapN ⊑ || client {{ λ _, True }}.
  Proof.
    intros ?. rewrite /client.
    ewp eapply (newchan_spec N heapN True%I); last done.
    apply sep_intro_True_r; first done.
    apply forall_intro=>l. apply wand_intro_l. rewrite right_id.
    wp_let. etrans; last eapply wait_spec.
    apply sep_mono_r. apply wand_intro_r. eauto.
  Qed.

End client.

Section ClosedProofs.
  Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: authF (constF heapRA)
                                     .:: (λ _, constF unitRA) : iFunctorG.
  Notation iProp := (iPropG heap_lang Σ).

  Instance: authG heap_lang Σ heapRA.
  Proof. split; try apply _. by exists 2%nat. Qed.

  Instance: stsG heap_lang Σ barrier_proto.sts.
  Proof. split; try apply _. by exists 1%nat. Qed.

  Instance: savedPropG heap_lang Σ.
  Proof. by exists 0%nat. Qed.

  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
  Proof.
    apply ht_alt. rewrite (heap_alloc ⊤ (ndot nroot "Barrier")); last first.
    { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
      move=>? _. exact I. }
    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
    rewrite -(client_safe (ndot nroot "Heap" ) (ndot nroot "Barrier" )) //.
    (* This, too, should be automated. *)
    apply ndot_ne_disjoint. discriminate.
  Qed.

  Print Assumptions client_safe_closed.
End ClosedProofs.