proof.v

From prelude Require Import functions.
From algebra Require Import upred_big_op.
From program_logic Require Import sts saved_prop tactics.
From heap_lang Require Export heap wp_tactics.
From barrier Require Export barrier.
From barrier Require Import protocol.
Import uPred.

(** The CMRAs we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class barrierG Σ := BarrierG {
  barrier_stsG :> stsG heap_lang Σ sts;
  barrier_savedPropG :> savedPropG heap_lang Σ (laterCF idCF);
}.
(** The Functors we need. *)
Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF (laterCF idCF)].
(* Show and register that they match. *)
Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ.
Proof. destruct H as (?&?&?). split; apply _. Qed.

(** Now we come to the Iris part of the proof. *)
Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).

Definition ress (P : iProp) (I : gset gname) : iProp :=
  (∃ Ψ : gname → iProp,
    ▷ (P -★ Π★{set I} Ψ) ★ Π★{set I} (λ i, saved_prop_own i (Next (Ψ i))))%I.

Coercion state_to_val (s : state) : val :=
  match s with State Low _ => #0 | State High _ => #1 end.
Arguments state_to_val !_ /.

Definition state_to_prop (s : state) (P : iProp) : iProp :=
  match s with State Low _ => P | State High _ => True%I end.
Arguments state_to_val !_ /.

Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp :=
  (l ↦ s ★ ress (state_to_prop s P) (state_I s))%I.

Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
  (■ (heapN ⊥ N) ★ heap_ctx heapN ★ sts_ctx γ N (barrier_inv l P))%I.

Definition send (l : loc) (P : iProp) : iProp :=
  (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I.

Definition recv (l : loc) (R : iProp) : iProp :=
  (∃ γ P Q i,
    barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
    saved_prop_own i (Next Q) ★ ▷ (Q -★ R))%I.

Global Instance barrier_ctx_always_stable (γ : gname) (l : loc) (P : iProp) :
  AlwaysStable (barrier_ctx γ l P).
Proof. apply _. Qed.

(* TODO: Figure out if this has a "Global" or "Local" effect.
   We want it to be Global. *)
Typeclasses Opaque barrier_ctx send recv.

Implicit Types I : gset gname.

(** Setoids *)
Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
Proof. solve_proper. Qed.
Global Instance state_to_prop_ne n s :
  Proper (dist n ==> dist n) (state_to_prop s).
Proof. solve_proper. Qed.
Global Instance barrier_inv_ne n l :
  Proper (dist n ==> eq ==> dist n) (barrier_inv l).
Proof. solve_proper. Qed.
Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
Proof. solve_proper. Qed. 
Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
Proof. solve_proper. Qed.
Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
Proof. solve_proper. Qed.

(** Helper lemmas *)
Lemma ress_split i i1 i2 Q R1 R2 P I :
  i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
  (saved_prop_own i2 (Next R2) ★
    saved_prop_own i1 (Next R1) ★ saved_prop_own i (Next Q) ★
    (Q -★ R1 ★ R2) ★ ress P I)
  ⊑ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))).
Proof.
  intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ.
  rewrite -(exist_intro (<[i1:=R1]> (<[i2:=R2]> Ψ))).
  rewrite [(Π★{set _} (λ _, saved_prop_own _ _))%I](big_sepS_delete _ I i) //.
  do 4 (rewrite big_sepS_insert; last set_solver).
  rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert.
  set savedQ := _ i _. set savedΨ := _ i _.
  sep_split left: [savedQ; savedΨ; Q -★ _; ▷ (_ -★ Π★{set I} _)]%I.
  - rewrite !assoc saved_prop_agree later_equivI /=. strip_later.
    apply wand_intro_l. to_front [P; P -★ _]%I. rewrite wand_elim_r.
    rewrite (big_sepS_delete _ I i) //.
    sep_split right: [Π★{set _} _]%I.
    + rewrite !assoc.
      eapply wand_apply_r'; first done.
      apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); last by eauto with I.
      rewrite eq_sym. eauto with I.
    + apply big_sepS_mono; [done|] => j.
      rewrite elem_of_difference not_elem_of_singleton=> -[??].
      by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
  - rewrite !assoc [(saved_prop_own i2 _ ★ _)%I]comm; apply sep_mono_r.
    apply big_sepS_mono; [done|]=> j.
    rewrite elem_of_difference not_elem_of_singleton=> -[??].
    by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
Qed.

(** Actual proofs *)
Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
  heapN ⊥ N →
  (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l))
  ⊑ #> newbarrier #() {{ Φ }}.
Proof.
  intros HN. rewrite /newbarrier. wp_seq.
  rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
  apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
  rewrite !assoc. apply pvs_wand_r.
  (* The core of this proof: Allocating the STS and the saved prop. *)
  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=laterCF idCF) _ (Next P)).
  rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
  apply exist_elim=>i.
  trans (pvs ⊤ ⊤ (heap_ctx heapN ★
    ▷ (barrier_inv l P (State Low {[ i ]})) ★ saved_prop_own i (Next P))).
  - rewrite -pvs_intro. cancel [heap_ctx heapN].
    rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i (Next P)].
    rewrite /barrier_inv /ress -later_intro. cancel [l ↦ #0]%I.
    rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I (★)%I).
    by rewrite !big_sepS_singleton /= wand_diag -later_intro.
  - rewrite (sts_alloc (barrier_inv l P) ⊤ N); last by eauto.
    rewrite !pvs_frame_r !pvs_frame_l. 
    rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l.
    apply exist_elim=>γ.
    rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P).
    rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ).
    rewrite always_and_sep_l wand_diag later_True right_id.
    rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
    rewrite /barrier_ctx const_equiv // left_id.
    ecancel_pvs [saved_prop_own i _; heap_ctx _; heap_ctx _;
                 sts_ctx _ _ _; sts_ctx _ _ _].
    rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ 
                            ({[ Change i ]} ∪ {[ Send ]})).
    + apply pvs_mono.
      rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed.
      set_solver.
    + intros []; set_solver.
    + set_solver.
    + auto using sts.closed_op, i_states_closed, low_states_closed.
Qed.

Lemma signal_spec l P (Φ : val → iProp) :
  (send l P ★ P ★ Φ #()) ⊑ #> signal (%l) {{ Φ }}.
Proof.
  rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
  apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let.
  (* I think some evars here are better than repeating *everything* *)
  eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
    eauto with I ndisj.
  ecancel [sts_ownS γ _ _]. 
  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
  apply const_elim_sep_l=>Hs. destruct p; last done.
  rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
  eapply wp_store with (v' := #0); eauto with I ndisj. 
  strip_later. cancel [l ↦ #0]%I.
  apply wand_intro_l. rewrite -(exist_intro (State High I)).
  rewrite -(exist_intro ∅). rewrite const_equiv /=; last by eauto using signal_step.
  rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
  sep_split right: [Φ _]; last first.
  { apply wand_intro_l. eauto with I. }
  (* Now we come to the core of the proof: Updating from waiting to ress. *)
  rewrite /ress sep_exist_r. apply exist_mono=>{Φ} Φ.
  ecancel [Π★{set I} (λ _, saved_prop_own _ _)]%I. strip_later.
  rewrite wand_True. eapply wand_apply_l'; eauto with I.
Qed.

Lemma wait_spec l P (Φ : val → iProp) :
  (recv l P ★ (P -★ Φ #())) ⊑ #> wait (%l) {{ Φ }}.
Proof.
  rename P into R. wp_rec.
  rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
  apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
  rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
  apply exist_elim=>i. rewrite -!(assoc (★)%I). apply const_elim_sep_l=>?.
  wp_focus (! _)%E.
  (* I think some evars here are better than repeating *everything* *)
  eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
    eauto with I ndisj.
  ecancel [sts_ownS γ _ _].
  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
  apply const_elim_sep_l=>Hs.
  rewrite {1}/barrier_inv =>/=. rewrite later_sep.
  eapply wp_load; eauto with I ndisj.
  ecancel [▷ l ↦{_} _]%I. strip_later.
  apply wand_intro_l. destruct p.
  { (* a Low state. The comparison fails, and we recurse. *)
    rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}).
    rewrite [(■ sts.steps _ _ )%I]const_equiv /=; last by apply rtc_refl.
    rewrite left_id -[(▷ barrier_inv _ _ _)%I]later_intro {3}/barrier_inv.
    rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l.
    wp_op; first done. intros _. wp_if. rewrite !assoc.
    rewrite -always_wand_impl always_elim.
    rewrite -{2}pvs_wp. apply pvs_wand_r.
    rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
    rewrite const_equiv // left_id -later_intro.
    ecancel_pvs [heap_ctx _; saved_prop_own _ _; Q -★ _; R -★ _; sts_ctx _ _ _]%I.
    apply sts_own_weaken; eauto using i_states_closed. }
  (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
  rewrite [(_ ★ □ (_ → _ ))%I]sep_elim_l.
  rewrite -(exist_intro (State High (I ∖ {[ i ]}))) -(exist_intro ∅).
  change (i ∈ I) in Hs.
  rewrite const_equiv /=; last by eauto using wait_step.
  rewrite left_id -[(▷ barrier_inv _ _ _)%I]later_intro {2}/barrier_inv.
  rewrite -!assoc. apply sep_mono_r. rewrite /ress.
  rewrite !sep_exist_r. apply exist_mono=>Ψ.
  rewrite !(big_sepS_delete _ I i) //= !wand_True later_sep.
  ecancel [▷ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I.
  apply wand_intro_l.  set savedΨ := _ i _. set savedQ := _ i _.
  to_front [savedΨ; savedQ]. rewrite saved_prop_agree later_equivI /=.
  wp_op; [|done]=> _. wp_if. rewrite !assoc. eapply wand_apply_r'; first done.
  eapply wand_apply_r'; first done.
  apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I.
Qed.

Lemma recv_split E l P1 P2 :
  nclose N ⊆ E → 
  recv l (P1 ★ P2) ⊑ |={E}=> recv l P1 ★ recv l P2.
Proof.
  rename P1 into R1. rename P2 into R2. intros HN.
  rewrite {1}/recv /barrier_ctx. 
  apply exist_elim=>γ. rewrite sep_exist_r.  apply exist_elim=>P. 
  apply exist_elim=>Q. apply exist_elim=>i. rewrite -!(assoc (★)%I).
  apply const_elim_sep_l=>?. rewrite -pvs_trans'.
  (* I think some evars here are better than repeating *everything* *)
  eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl;
    eauto with I ndisj.
  ecancel [sts_ownS γ _ _].
  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
  apply const_elim_sep_l=>Hs. rewrite /pvs_fsa.
  eapply sep_elim_True_l.
  { eapply saved_prop_alloc_strong with (x := Next R1) (G := I). }
  rewrite pvs_frame_r. apply pvs_strip_pvs. rewrite sep_exist_r.
  apply exist_elim=>i1. rewrite always_and_sep_l. rewrite -assoc.
  apply const_elim_sep_l=>Hi1. eapply sep_elim_True_l.
  { eapply saved_prop_alloc_strong with (x := Next R2) (G := I ∪ {[ i1 ]}). }
  rewrite pvs_frame_r. apply pvs_mono. rewrite sep_exist_r.
  apply exist_elim=>i2. rewrite always_and_sep_l. rewrite -assoc.
  apply const_elim_sep_l=>Hi2.
  rewrite ->not_elem_of_union, elem_of_singleton in Hi2.
  destruct Hi2 as [Hi2 Hi12]. change (i ∈ I) in Hs.
  (* Update to new state. *)
  rewrite -(exist_intro (State p ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))))).
  rewrite -(exist_intro ({[Change i1 ]} ∪ {[ Change i2 ]})).
  rewrite [(■ sts.steps _ _)%I]const_equiv; last by eauto using split_step.
  rewrite left_id {1 3}/barrier_inv.
  (* FIXME ssreflect rewrite fails if there are evars around. Also, this is very slow because we don't have a proof mode. *)
  rewrite -(ress_split _ _ _ Q R1 R2); [|done..].
  rewrite {1}[saved_prop_own i1 _]always_sep_dup.
  rewrite {1}[saved_prop_own i2 _]always_sep_dup !later_sep.
  rewrite -![(▷ saved_prop_own _ _)%I]later_intro.
  ecancel [▷ l ↦ _; saved_prop_own i1 _; saved_prop_own i2 _ ;
           ▷ ress _ _ ; ▷ (Q -★ _) ; saved_prop_own i _]%I. 
  apply wand_intro_l. rewrite !assoc. rewrite /recv.
  rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
  rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
  rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
  rewrite /barrier_ctx const_equiv // left_id.
  ecancel_pvs [saved_prop_own i1 _; saved_prop_own i2 _; heap_ctx _; heap_ctx _;
               sts_ctx _ _ _; sts_ctx _ _ _].
  rewrite !wand_diag later_True !right_id.
  rewrite -sts_ownS_op; eauto using i_states_closed.
  - apply sts_own_weaken;
      eauto using sts.closed_op, i_states_closed. set_solver.
  - set_solver.
Qed.

Lemma recv_weaken l P1 P2 :
  (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2).
Proof.
  apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
  rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r.
  apply exist_mono=>Q. rewrite sep_exist_r. apply exist_mono=>i.
  ecancel [barrier_ctx _ _ _; sts_ownS _ _ _; saved_prop_own _ _].
  strip_later. apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r.
Qed.

Lemma recv_mono l P1 P2 :
  P1 ⊑ P2 → recv l P1 ⊑ recv l P2.
Proof.
  intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
Qed.

End proof.