(* iris/base_logic/lib/gen_inv_heap.v *)
From iris.algebra Require Import auth excl gmap
From iris.base_logic.lib Require Import own invariants gen_heap
From iris.proofmode Require Import proofmode
From iris.prelude Require Import options

Definition inv_heapN: namespace := nroot .@ "inv_heap".

Local Notation"l ↦ v" := (pointsto l (DfracOwn 1) v) (at level 20) : bi_scope.

Definition inv_heap_mapUR(L V : Type) `{Countable L} : ucmra := gmapUR L $ prodR
  (optionR $ exclR $ leibnizO V)
  (agreeR (V -d> PropO)).

Definition to_inv_heap{L V : Type} `{Countable L}
    (h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
  prod_map (λ x, Excl' x) to_agree <$> h.

Class inv_heapGpreS(L V : Type) (Σ : gFunctors) `{Countable L} := {
  #[local] inv_heapGpreS_inG :: inG Σ (authR (inv_heap_mapUR L V))
}.

Class inv_heapGS(L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
  #[local] inv_heap_inG :: inv_heapGpreS L V Σ;
  inv_heap_name : gname
}.

Global ArgumentsInv_HeapG _ _ {_ _ _ _}.

Global Argumentsinv_heap_name {_ _ _ _ _} _ : assert.

Definition inv_heapΣ(L V : Type) `{Countable L} : gFunctors :=
  #[ GFunctor (authR (inv_heap_mapUR L V)) ].

Global InstancesubG_inv_heapGpreS (L V : Type) `{Countable L} {Σ} :
  subG (inv_heapΣ L V) Σ → inv_heapGpreS L V Σ.
Proof. solve_inG. Qed.

Definition inv_heap_inv_P: iProp Σ :=
    ∃ h : gmap L (V * (V -d> PropO)),
       own (inv_heap_name gG) (● to_inv_heap h) ∗
       [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1.

Definition inv_heap_inv: iProp Σ := inv inv_heapN inv_heap_inv_P.

Definition inv_pointsto_own(l : L) (v : V) (I : V → Prop) : iProp Σ :=
    own (inv_heap_name gG) (◯ {[l := (Excl' v, to_agree I) ]}).

Definition inv_pointsto(l : L) (I : V → Prop) : iProp Σ :=
    own (inv_heap_name gG) (◯ {[l := (None, to_agree I)]}).

Local Notation"l '↦_' I v" := (inv_pointsto_own l v I%stdpp%type)
  (at level 20, I at level 9, format "l  '↦_' I  v") : bi_scope.

Local Notation"l '↦_' I □" := (inv_pointsto l I%stdpp%type)
  (at level 20, I at level 9, format "l  '↦_' I  '□'") : bi_scope.

Global Argumentsinv_heap_inv _ _ {_ _ _ _ _ _ _}.

Global Instance: Params (@inv_pointsto_own) 8 := {}.

Global Instance: Params (@inv_pointsto) 7 := {}.

Lemma to_inv_heap_validh : ✓ to_inv_heap h.
  Proof. intros l. rewrite lookup_fmap. by case: (h !! l). Qed.

Lemma to_inv_heap_singletonl v I :
    to_inv_heap {[l := (v, I)]} =@{inv_heap_mapUR L V} {[l := (Excl' v, to_agree I)]}.
  Proof. by rewrite /to_inv_heap fmap_insert fmap_empty. Qed.

Lemma to_inv_heap_insertl v I h :
    to_inv_heap (<[l := (v, I)]> h) = <[l := (Excl' v, to_agree I)]> (to_inv_heap h).
  Proof. by rewrite /to_inv_heap fmap_insert. Qed.

Lemma lookup_to_inv_heap_Noneh l :
    h !! l = None → to_inv_heap h !! l = None.
  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.

Lemma lookup_to_inv_heap_Someh l v I :
    h !! l = Some (v, I) → to_inv_heap h !! l = Some (Excl' v, to_agree I).
  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.

Lemma lookup_to_inv_heap_Some_2h l v' I' :
    to_inv_heap h !! l ≡ Some (v', I') →
    ∃ v I, v' = Excl' v ∧ I' ≡ to_agree I ∧ h !! l = Some (v, I).
  Proof.
    rewrite /to_inv_heap /prod_map lookup_fmap. rewrite fmap_Some_equiv.
    intros ([] & Hsome & [Heqv HeqI]); simplify_eq/=; eauto.
  Qed.

Lemma inv_heap_init(L V : Type) `{Countable L, !invGS_gen hlc Σ, !gen_heapGS L V Σ, !inv_heapGpreS L V Σ} E :
  ⊢ |==> ∃ _ : inv_heapGS L V Σ, |={E}=> inv_heap_inv L V.
Proof.
  iMod (own_alloc (● (to_inv_heap ∅))) as (γ) "H●".
  { rewrite auth_auth_valid. exact: to_inv_heap_valid. }
  iModIntro.
  iExists (Inv_HeapG L V γ).
  iAssert (inv_heap_inv_P (gG := Inv_HeapG L V γ)) with "[H●]" as "P".
  { iExists _. iFrame. done. }
  iApply (inv_alloc inv_heapN E inv_heap_inv_P with "P").
Qed.

Lemma inv_pointsto_lookup_Somel h I :
    l ↦_I □ -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
    ⌜∃ v I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
  Proof.
    iIntros "Hl_inv H◯".
    iCombine "H◯ Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
    iPureIntro.
    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
    move: Hincl; rewrite HI Some_included_total pair_included
      to_agree_included; intros [??]; eauto.
  Qed.

Lemma inv_pointsto_own_lookup_Somel v h I :
    l ↦_I v -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
    ⌜ ∃ I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
  Proof.
    iIntros "Hl_inv H●".
    iCombine "H● Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
    iPureIntro.
    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
    move: Hincl; rewrite HI Some_included_total pair_included
      Excl_included to_agree_included; intros [-> ?]; eauto.
  Qed.

Global Instanceinv_pointsto_own_proper l v :
    Proper (pointwise_relation _ iff ==> (≡)) (inv_pointsto_own l v).
  Proof.
    intros I1 I2 ?. rewrite /inv_pointsto_own. do 2 f_equiv.
    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
  Qed.

Global Instanceinv_pointsto_proper l :
    Proper (pointwise_relation _ iff ==> (≡)) (inv_pointsto l).
  Proof.
    intros I1 I2 ?. rewrite /inv_pointsto. do 2 f_equiv.
    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
  Qed.

Global Instanceinv_heap_inv_persistent : Persistent (inv_heap_inv L V).
  Proof. apply _. Qed.

Global Instanceinv_pointsto_persistent l I : Persistent (l ↦_I □).
  Proof. apply _. Qed.

Global Instanceinv_pointsto_timeless l I : Timeless (l ↦_I □).
  Proof. apply _. Qed.

Global Instanceinv_pointsto_own_timeless l v I : Timeless (l ↦_I v).
  Proof. apply _. Qed.

Lemma make_inv_pointstol v I E :
    ↑inv_heapN ⊆ E →
    I v →
    inv_heap_inv L V -∗ l ↦ v ={E}=∗ l ↦_I v.
  Proof.
    iIntros (HN HI) "#Hinv Hl".
    iMod (inv_acc_timeless _ inv_heapN with "Hinv") as "[HP Hclose]"; first done.
    iDestruct "HP" as (h) "[H● HsepM]".
    destruct (h !! l) as [v'| ] eqn: Hlookup.
    -
      iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
      by iCombine "Hl Hl'" gives %[??].
    - iMod (own_update with "H●") as "[H● H◯]".
      { apply lookup_to_inv_heap_None in Hlookup.
        apply (auth_update_alloc _
          (to_inv_heap (<[l:=(v,I)]> h)) (to_inv_heap ({[l:=(v,I)]}))).
        rewrite to_inv_heap_insert to_inv_heap_singleton.
        by apply: alloc_singleton_local_update. }
      iMod ("Hclose" with "[H● HsepM Hl]").
      + iExists _.
        iDestruct (big_sepM_insert _ _ _ (_,_) with "[$HsepM $Hl]")
          as "HsepM"; auto with iFrame.
      + iModIntro. by rewrite /inv_pointsto_own to_inv_heap_singleton.
  Qed.

Lemma inv_pointsto_own_invl v I : l ↦_I v -∗ l ↦_I □.
  Proof.
    iApply own_mono. apply auth_frag_mono.
    rewrite singleton_included_total pair_included.
    split; [apply: ucmra_unit_least|done].
  Qed.

Lemma inv_pointsto_own_acc_strongE :
    ↑inv_heapN ⊆ E →
    inv_heap_inv L V ={E, E ∖ ↑inv_heapN}=∗ ∀ l v I, l ↦_I v -∗
      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗
        inv_pointsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
  Proof.
    iIntros (HN) "#Hinv".
    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
    iIntros "!>" (l v I) "Hl_inv".
    iDestruct "HP" as (h) "[H● HsepM]".
    iDestruct (inv_pointsto_own_lookup_Some with "Hl_inv H●") as %(I'&?&HI').
    setoid_rewrite HI'.
    iDestruct (big_sepM_delete with "HsepM") as "[[HI Hl] HsepM]"; first done.
    iIntros "{$HI $Hl}" (w ?) "Hl".
    iMod (own_update_2 with "H● Hl_inv") as "[H● H◯]".
    { apply (auth_update _ _ (<[l := (Excl' w, to_agree I')]> (to_inv_heap h))
             {[l := (Excl' w, to_agree I)]}).
      apply: singleton_local_update.
      { by apply lookup_to_inv_heap_Some. }
      apply: prod_local_update_1. apply: option_local_update.
      apply: exclusive_local_update. done. }
    iDestruct (big_sepM_insert _ _ _ (w, I') with "[$HsepM $Hl //]") as "HsepM".
    { apply lookup_delete_eq. }
    rewrite insert_delete_eq -to_inv_heap_insert. iIntros "!> {$H◯}".
    iApply ("Hclose" with "[H● HsepM]"). iExists _; by iFrame.
  Qed.

Lemma inv_pointsto_own_accE l v I:
    ↑inv_heapN ⊆ E →
    inv_heap_inv L V -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
  Proof.
    iIntros (?) "#Hinv Hl".
    iMod (inv_pointsto_own_acc_strong with "Hinv") as "Hacc"; first done.
    iDestruct ("Hacc" with "Hl") as "(HI & Hl & Hclose)".
    iIntros "!> {$HI $Hl}" (w) "HI Hl".
    iMod ("Hclose" with "HI Hl") as "[$ $]".
  Qed.

Lemma inv_pointsto_accl I E :
    ↑inv_heapN ⊆ E →
    inv_heap_inv L V -∗ l ↦_I □ ={E, E ∖ ↑inv_heapN}=∗
    ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
  Proof.
    iIntros (HN) "#Hinv Hl_inv".
    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
    iModIntro.
    iDestruct "HP" as (h) "[H● HsepM]".
    iDestruct (inv_pointsto_lookup_Some with "Hl_inv H●") as %(v&I'&?&HI').
    iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"; first done.
    setoid_rewrite HI'.
    iExists _. iIntros "{$HI $Hl} Hl".
    iMod ("Hclose" with "[H● HsepM Hl]"); last done.
    iExists _. iFrame "H●". iApply ("HsepM" with "[$Hl //]").
  Qed.

Global TypeclassesOpaque inv_heap_inv inv_pointsto inv_pointsto_own.