From iris.program_logic Require Export weakestpre adequacy ownp.
From iris.base_logic Require Import lib.invariants.
From iris.algebra Require Import auth agree.
Set Default Proof Using "Type".

From igps Require Import lang proofmode.
From igps.base Require Import ghosts.

Class basePreG Σ := BasePreG {
  base_preG_iris :> ownPPreG (ra_lang) Σ;
  base_preG_view :> inG Σ (authR Views);
  base_preG_hist :> inG Σ (authR Hists);
  base_preG_info :> inG Σ (authR Infos);
}.

Definition baseΣ : gFunctors := #[ownPΣ (language.state ra_lang);
      GFunctor (authR Views);
      GFunctor (authR Hists);
      GFunctor (authR Infos)].
Instance subG_basePreG {Σ} : subG baseΣ Σ → basePreG Σ.
Proof. solve_inG. Qed.

(* Definition to_view (σ : language.state ra_lang) : Views := (Excl <$> threads σ). *)
Definition loc_sets (σ : language.state ra_lang) : gmap loc (gset message) :=
  let locs := {[ mloc m | m <- msgs (mem σ) ]} in
  map_imap (λ l _, Some {[ m <- msgs (mem σ) | mloc m = l ]}) (to_gmap () locs).
Definition to_hist (σ : language.state ra_lang) : Hists :=
  let maxsets := (λ M, {[ m <- M | set_Forall (λ m', mtime m' ⊑ mtime m) M ]} )  <$> loc_sets σ in
  let hists := map_vt <$> maxsets in
  let excls := Excl <$> hists in
  excls.
(* TODO: can we avoid this? *)
(* Definition to_info (σ : language.state ra_lang) : Infos := *)
(*   let locs := {[ mloc m | m <- msgs (mem σ) ]} in *)
(*   let infos : gmap loc (frac.fracR * _) := to_gmap (1%Qp, to_agree 1%positive) locs in *)
(*   (infos). *)
Definition to_info (σ : language.state ra_lang) : Infos :=
  (λ _, (1%Qp, to_agree 1%positive)) <$> to_hist σ.

Lemma NoDup_omap {A B : Type} (l : list A) (f : A -> option B) : Inj (=) (=) f -> NoDup l -> NoDup (omap f l).
Proof.
  intros I.
  induction l => //=. constructor.
  inversion 1. case_match; subst; auto.
  constructor; last auto. apply/elem_of_list_omap => [[x [?]]].
  rewrite -Heqo. move/I => ?. subst. auto.
Qed.

Lemma Some_helper {X : Type} (x y : X) : Some x = Some y ↔ x = y.
Proof. naive_solver. Qed.

Lemma dom_map_imap `{Countable K} {B} (f : K -> () -> B) (g: gmap _ _) :
  dom (gset K) (map_imap (λ x y, Some (f x y)) g) ≡ dom _ g.
Proof.
  intros.
  rewrite /map_imap /dom /= /gset_dom /mapset_dom /= => x.
  rewrite !elem_of_mapset_dom_with.
  setoid_rewrite (_ : ∀ P, P ∧ true ↔ P); [|naive_solver|naive_solver].
  setoid_rewrite <-(elem_of_map_of_list _ _ _ _); last first.
  { apply NoDup_fmap_fst; last apply NoDup_omap; last apply NoDup_map_to_list.
    - intros ? ? ?. rewrite !elem_of_list_omap.
      assert (R : ∀ (a : K) (b : B) x, (pair (x.1) <$> curry (λ x y, Some (f x y)) x = Some (a, b)) ↔ (x.1 = a ∧ f (x.1) (x.2) = b)).
      { intros ? ? [? ?]. cbn. naive_solver. }
      repeat setoid_rewrite R.
      move => [[? ?] X] [[? ?] Y]. move: X Y. rewrite !elem_of_map_to_list /=.
      move => [E] [<-] ? [? [? ?]]. by simplify_eq.
    - intros [? ?] [? ?]. simplify_option_eq. inversion 1. simplify_eq. by destruct u, u0.
  }
  setoid_rewrite elem_of_list_omap.
  assert (∀ P, (∃ u : (), P u) ↔ P ()). {
    intros. split; eauto. by move => [[]]. }
  rewrite H0.
  assert (∀ X Y P, (∃ ab : X * Y, P ab) ↔ (∃ a :X, ∃ b :Y , P (a, b))).
  { intros. split. move => [[? ?]]. eauto. move => [? [? ?]]. eauto. }
  setoid_rewrite H1.
  setoid_rewrite elem_of_map_to_list.
  naive_solver.
Qed.

Lemma dom_to_gmap `{Countable K} {B} (g : gset K) (b:B) : dom (gset K) (to_gmap b g) ≡ g.
Proof.
  rewrite /to_gmap dom_fmap => ?. rewrite elem_of_dom.
  split.
  - move => [[] ?]. by do !red.
  - eauto.
Qed.

Lemma loc_sets_dom σ : dom _ (loc_sets σ) ≡ {[ mloc m | m <- mem σ ]}.
  rewrite /loc_sets.
  by rewrite dom_map_imap dom_to_gmap.
Qed.

(* Lemma elements_map_gset `{Countable T} `{Countable B} `{Equiv B} (f : T -> B) g : *)
(*   @equiv (list _) _ (elements (map_gset f g)) (f <$> elements g). *)
(* Proof. *)
(*   rewrite /map_gset. elim: (elements g) => [|? L IHL] /=. *)
(*   - rewrite elements_empty. constructor. *)
(*   - rewrite elements_union.  *)
(*     by rewrite elem_of_elements elem_of_of_list. Qed. *)

(* Instance foldl_proper `{Equiv T} `{Equiv B} (f : B -> list T -> B) : `(Proper ((≡) ==> (≡ₚ) ==> (≡)) f) -> Proper ((≡) ==> (≡ₚ) ==> (≡)) (foldl f). *)
(* Proof. *)
(*   intros P x y Hxy a b Hab. *)
(*   elim: a b Hab x y Hxy => [|? ? IH] b Hab x y Hxy. *)
(*   - case: b Hab => //= ? ?. move => ?. by edestruct (Permutation_nil_cons). *)
(*   - have : (exists c b', b ≡ₚ c :: b') => [|[c [b' P2]]]. *)
(*     { destruct b. by edestruct (Permutation_nil_cons). eauto. } *)
(*     rewrite ->P2 in Hab. *)
(*     rewrite (IH _ Hab). *)
(*     cbn. apply: IH. last by apply P. *)
(* Qed. *)

Lemma loc_sets_lookup σ l h :
  (loc_sets σ) !! l = Some h ↔ l ∈ {[ mloc m | m <- mem σ ]} ∧ h = {[ m <- msgs (mem σ) | mloc m = l ]}.
Proof.
  rewrite /loc_sets.
  rewrite lookup_imap lookup_to_gmap /=.
  case: (decide (l ∈ {[ mloc m | m <- mem σ ]})) => ?.
  - rewrite option_guard_True // /=. naive_solver.
  - rewrite option_guard_False // /=. naive_solver.
Qed.

Lemma to_hist_dom σ : dom _ (to_hist σ) ≡ {[ mloc m | m <- mem σ ]}.
Proof.
  by rewrite /to_hist !dom_fmap loc_sets_dom.
Qed.

Lemma gmap_bigop_lookup `{Countable K} `{Countable X} `(f : gmap.gmapUR K T) `(Ψ : _ -> _ -> gmap.gmapUR X Y) x:
  ([^op map] k ↦ t ∈ f, Ψ k t) !! x ≡ ([^op map] k ↦ t ∈ f, Ψ k t !! x).
Proof.
  rewrite /big_opM /curry.
  assert (tmp := NoDup_map_to_list f). move: tmp.
  elim: (map_to_list f) x => [|[? ?] L /= IHL] x ND.
  - by rewrite lookup_empty.
  - rewrite -IHL; last by apply: NoDup_cons_12.
    by rewrite lookup_merge.
Qed.

Lemma gmap_bigop `{Countable K} `(f : gmap.gmapUR K T) : f ≡ [^op map] k ↦ t ∈ f, {[ k := t ]}.
Proof.
  intros x.
  case Hf: (_ !! _) => [?|] /=.
  - rewrite big_opM_delete // lookup_merge.
    rewrite lookup_singleton.
    rewrite (_ : _ !! _ ≡ None); first by setoid_rewrite (comm op).
    rewrite gmap_bigop_lookup.
    rewrite -(big_opM_proper (λ _ _, None)); last first.
    + intros ? ?. move/lookup_delete_Some => [? ?].
      rewrite lookup_singleton_ne //.
    + rewrite big_opM_dom.
      rewrite /big_opS /curry.
        by elim: (elements _) => [|? L //= ->].
  - rewrite gmap_bigop_lookup.
    rewrite -(big_opM_proper (λ _ _, None)); last first.
    + intros ? ? Hfk.
      rewrite lookup_singleton_ne //.
      move => ?; subst. by rewrite Hf in Hfk.
    + rewrite big_opM_dom.
      rewrite /big_opS /curry.
      by elim: (elements _) => [|? L //= <-].
Qed.

Lemma own_big_op `{C : Countable K} {T} {M : ucmraT} `{i : inG Σ M} {γ} (g : gmap K T) (f : K -> T -> M) :
  @own Σ _ i γ (big_opM op f g) -∗ ([∗ map] k↦x ∈ g, @own Σ _ i γ (f k x)).
Proof.
  rewrite /big_opM /curry /=.
  elim: (map_to_list g) => [/=|[? ?] L /= IHL].
  - iIntros. eauto.
  - iIntros "[$ ?]". by iApply IHL.
Qed.

Lemma auth_big_op `{C : Countable K} {T} (g : gmap K T)  {M : ucmraT} (f : K -> T -> M) :
  ◯ (big_opM op f g) ≡ big_opM op (λ k t, ◯ (f k t)) g.
Proof.
  rewrite /big_opM /curry /=.
  elim: (map_to_list g) => [//=|[? ?] L /= <- //].
Qed.

Definition base_adequacy Σ `{!basePreG Σ} e V σ φ :
  phys_inv σ ->
  view_ok (mem σ) V ->
  (∀ `{!foundationG Σ} π, PSCtx ∗ Seen π V ⊢ WP e {{ v, ⌜φ v⌝ }}) →
  adequate NotStuck e σ φ.
Proof.
  intros Inv VOk Hwp; eapply (ownP_adequacy _ _). iIntros (?).
  iMod (own_alloc (● {[1%positive := Excl V]} ⋅ ◯ {[1%positive:=Excl V]})) as (γV) "HV".
  { rewrite auth_valid_discrete /=. split.
    - exists ∅. intros ?. rewrite !gmap.lookup_op lookup_empty.
      by case: (_ !! _).
    - move => ?.
      case H: (_ !! _) => [?|//] /=.
      move: H. rewrite lookup_singleton_Some => [] [_ <-] //.
  }
  iMod (own_alloc (● to_hist σ ⋅ ◯ to_hist σ)) as (γH) "HH".
  { rewrite auth_valid_discrete /=. split.
    - exists ∅. intros ?. rewrite !gmap.lookup_op lookup_empty.
      by case: (_ !! _).
    - move => ?. rewrite lookup_fmap.
      case: (_ !! _) => [?|//] /=. by constructor. }
  iMod (own_alloc (● to_info σ ⋅ ◯ to_info σ)) as (γI) "HI".
  { rewrite auth_valid_discrete /=. split.
    - exists ∅. intros ?. rewrite !gmap.lookup_op lookup_empty.
      by case: (_ !! _).
    - move => ?. rewrite lookup_fmap.
      case: (_ !! _) => [?|//] /=. by constructor. }
  iDestruct "HV" as "[HV HV']".
  iDestruct "HH" as "[HH HH']".
  iDestruct "HI" as "[HI HI']".
  iIntros "oP".
  (* iModIntro. iExists (λ σ, own γV (to_view σ) ∗ own γH (to_hist σ) ∗ own γI (to_info σ))%I; iFrame. *)
  set (HBase := FoundationG Σ _ _ _ _ γV γH γI).
  iMod (inv_alloc physN top PSInv with "[- HV']"); last first.
  { iApply (Hwp (HBase)). by iFrame. }
  iNext. rewrite /PSInv. iExists _, _, _, _. iFrame (Inv) "∗".
  repeat iSplit; auto.
  - rewrite /DInv.
    rewrite {1}(gmap_bigop (to_hist σ)).
    rewrite {1}(gmap_bigop (to_info σ)).
    rewrite !auth_big_op.
    iDestruct (own_big_op (to_hist σ) (λ k t, ◯ {[ k:= t]}) with "HH'") as "A".
    iDestruct (own_big_op (to_info σ) (λ k t, ◯ {[ k:= t]}) with "HI'") as "B".
    iCombine "A" "B" as "AB".
    rewrite (big_sepM_fmap _ _ (to_hist σ)). rewrite -big_sepM_sepM.
    match goal with
    | |- environments.envs_entails _ (big_opM _ ?f ?g) =>
      iApply (big_sepM_impl _ f with "[$AB]")
    end.
    iIntros "!#". iIntros (? ? ?) "[A B]". destruct a0.
    + iIntros (? ?). iFrame. iExists _. iFrame.
    + iDestruct (own_valid with "A") as "%".
      move: (H a) => /=. by rewrite lookup_singleton.
  - iPureIntro => ? ?. by rewrite lookup_singleton_Some => [] [_ [<-] //].
  - by rewrite to_hist_dom.
  - iPureIntro. intros ? ?. rewrite /to_hist.
    rewrite !lookup_fmap. move/fmap_Some => [?] [].
    move/fmap_Some => [S] [].
    move/fmap_Some => [T] [].
    move => L -> -> [->].
    destruct (minimal_exists (flip $ rel_of (mtime) (⊑)) (T)) as [x [H1 H2]].
    { move/loc_sets_lookup : L => [L ->]. rewrite /map_vt.
      move/elem_of_map_gset:  L => [m [? ?]]. move => /(_ m).
      setoid_rewrite elem_of_filter. abstract set_solver. }
    exists (mval x, mview x). split; [|split; [|split; [|split]]].
    + rewrite elem_of_map_gset.
      exists x. split; auto.
      rewrite elem_of_filter. split; auto. intros y Iny.
      case: (total (⊑) (mtime y) (mtime x)) => //.
      apply (H2 y Iny).
    + intros ?. rewrite elem_of_map_gset. setoid_rewrite elem_of_filter.
      move => [y [-> [FA In]]].
      move/loc_sets_lookup : L => [L ?]. subst T.
      cbn.
      rewrite {1}(_ : l = mloc x); last by abstract set_solver+H1.
      rewrite {1}(_ : l = mloc y); last by abstract set_solver+In.
      rewrite !(_ : msg_ok _) //; first by apply FA.
      * apply Inv. abstract set_solver+In.
      * apply Inv. abstract set_solver+H1.
    + case H: (nats σ !! _) => [?|]; last done.
      move/(INOk _ Inv) : H => [m [? [? <-]]].
      case: (total (⊑) (Some (mtime m)) (mview x !! l)); first auto.
      move/loc_sets_lookup : L => [L ?].
      rewrite -(_ : mloc x = l); last by abstract set_solver.
      rewrite (_ : msg_ok _).
      * apply: H2. subst T. abstract set_solver.
      * apply Inv. abstract set_solver.
    + rewrite /history.hist_from_opt /=.
      f_equiv.
      move/loc_sets_lookup : L => [L ?]. subst T.
      apply set_unfold_2. move => m. split.
      * intuition. rewrite (_ : l = mloc x); last by abstract set_solver+H1.
        rewrite (_ : msg_ok _); last (apply Inv; abstract set_solver+H1).
        apply H0. abstract set_solver.
      * intuition. intros ? ?.
        move : H0.
        rewrite (_ : l = mloc x); last by abstract set_solver+H1.
        rewrite (_ : msg_ok _); last by (apply Inv; abstract set_solver+H1).
        etrans; last apply: H0.
        case: (total (⊑) (mtime x0) (mtime x)); first auto.
        by apply: H2.
    + intros ? ?. apply set_unfold_2. move => [[m [-> /= [FA In]]]].
      move/loc_sets_lookup : L => [L ?].
      edestruct (memory_ok (mem σ) x m).
      { subst. abstract set_solver+H1. }
      { subst. abstract set_solver+In. }
      * by subst.
      * destruct H. abstract set_solver.
        destruct H. apply: (anti_symm (⊑)).
        { by apply FA. }
        { apply H2; last apply FA; auto. }
  - by rewrite /IInv /to_info dom_fmap to_hist_dom.
Qed.