(* iris/algebra/dyn_reservation_map.v *)
From iris.algebra Require Export gmap coPset local_updates
From iris.algebra Require Import reservation_map updates proofmode_classes
From iris.prelude Require Import options

Record dyn_reservation_map(A : Type) := DynReservationMap {
  dyn_reservation_map_data_proj : gmap positive A;
  dyn_reservation_map_token_proj : coPset_disj
}.
Add Printing Constructor dyn_reservation_map.

Global ArgumentsDynReservationMap {_} _ _.

Global Argumentsdyn_reservation_map_data_proj {_} _.

Global Argumentsdyn_reservation_map_token_proj {_} _.

Global Instance: Params (@DynReservationMap) 1 := {}.

Global Instance: Params (@dyn_reservation_map_data_proj) 1 := {}.

Global Instance: Params (@dyn_reservation_map_token_proj) 1 := {}.

Definition dyn_reservation_map_data{SI : sidx} {A : cmra}
    (k : positive) (a : A) : dyn_reservation_map A :=
  DynReservationMap {[ k := a ]} ε.

Definition dyn_reservation_map_token{SI : sidx} {A : cmra}
    (E : coPset) : dyn_reservation_map A :=
  DynReservationMap ∅ (CoPset E).

Global Instance: Params (@dyn_reservation_map_data) 3 := {}.

Local Definitionto_reservation_map x : reservation_map A :=
    ReservationMap (dyn_reservation_map_data_proj x) (dyn_reservation_map_token_proj x).

Local Definitionfrom_reservation_map (x : reservation_map A) : dyn_reservation_map A :=
    DynReservationMap (reservation_map_data_proj x) (reservation_map_token_proj x).

Local Instancedyn_reservation_map_equiv : Equiv (dyn_reservation_map A) := λ x y,
    dyn_reservation_map_data_proj x ≡ dyn_reservation_map_data_proj y ∧
    dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.

Local Instancedyn_reservation_map_dist : Dist (dyn_reservation_map A) := λ n x y,
    dyn_reservation_map_data_proj x ≡{n}≡ dyn_reservation_map_data_proj y ∧
    dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.

Global InstanceDynReservationMap_ne :
    NonExpansive2 (@DynReservationMap A).
  Proof. by split. Qed.

Global InstanceDynReservationMap_proper :
    Proper ((≡) ==> (=) ==> (≡)) (@DynReservationMap A).
  Proof. by split. Qed.

Global Instancedyn_reservation_map_data_proj_ne :
    NonExpansive (@dyn_reservation_map_data_proj A).
  Proof. by destruct 1. Qed.

Global Instancedyn_reservation_map_data_proj_proper :
    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data_proj A).
  Proof. by destruct 1. Qed.

Definition dyn_reservation_map_ofe_mixin: OfeMixin (dyn_reservation_map A).
  Proof.
    by apply (iso_ofe_mixin to_reservation_map).
  Qed.
  Canonical Structure dyn_reservation_mapO :=
    Ofe (dyn_reservation_map A) dyn_reservation_map_ofe_mixin.

Global InstanceDynReservationMap_discrete a b :
    Discrete a → Discrete b → Discrete (DynReservationMap a b).
  Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete_0. Qed.

Global Instancedyn_reservation_map_ofe_discrete :
    OfeDiscrete A → OfeDiscrete dyn_reservation_mapO.
  Proof. intros ? [??]; apply _. Qed.

Global Argumentsdyn_reservation_mapO {_} _.

Global Instancedyn_reservation_map_data_ne i :
    NonExpansive (@dyn_reservation_map_data SI A i).
  Proof. intros ? ???. rewrite /dyn_reservation_map_data. solve_proper. Qed.

Global Instancedyn_reservation_map_data_proper N :
    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data SI A N).
  Proof. solve_proper. Qed.

Global Instancedyn_reservation_map_data_discrete N a :
    Discrete a → Discrete (dyn_reservation_map_data N a).
  Proof. intros. apply DynReservationMap_discrete; apply _. Qed.

Global Instancedyn_reservation_map_token_discrete E :
    Discrete (@dyn_reservation_map_token SI A E).
  Proof. intros. apply DynReservationMap_discrete; apply _. Qed.

Local Instancedyn_reservation_map_valid_instance : Valid (dyn_reservation_map A) := λ x,
    match dyn_reservation_map_token_proj x with
    | CoPset E =>
      ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧

Global Argumentsdyn_reservation_map_valid_instance !_ /.

Local Instancedyn_reservation_map_validN_instance : ValidN (dyn_reservation_map A) := λ n x,
    match dyn_reservation_map_token_proj x with
    | CoPset E =>
      ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧

Global Argumentsdyn_reservation_map_validN_instance !_ /.

Local Instancedyn_reservation_map_pcore_instance : PCore (dyn_reservation_map A) := λ x,
    Some (DynReservationMap (core (dyn_reservation_map_data_proj x)) ε).

Local Instancedyn_reservation_map_op_instance : Op (dyn_reservation_map A) := λ x y,
    DynReservationMap (dyn_reservation_map_data_proj x ⋅ dyn_reservation_map_data_proj y)
                   (dyn_reservation_map_token_proj x ⋅ dyn_reservation_map_token_proj y).

Definition dyn_reservation_map_valid_eq:
    valid = λ x, match dyn_reservation_map_token_proj x with
                 | CoPset E =>
                   ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧

Definition dyn_reservation_map_validN_eq:
    validN = λ n x, match dyn_reservation_map_token_proj x with
                    | CoPset E =>
                      ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧

Lemma dyn_reservation_map_includedx y :
    x ≼ y ↔
      dyn_reservation_map_data_proj x ≼ dyn_reservation_map_data_proj y ∧
      dyn_reservation_map_token_proj x ≼ dyn_reservation_map_token_proj y.
  Proof.
    split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (DynReservationMap z1 z2); split; auto.
  Qed.

Lemma dyn_reservation_map_data_proj_validNn x : ✓{n} x → ✓{n} dyn_reservation_map_data_proj x.
  Proof. by destruct x as [? [?|]]=> // -[??]. Qed.

Lemma dyn_reservation_map_token_proj_validNn x : ✓{n} x → ✓{n} dyn_reservation_map_token_proj x.
  Proof. by destruct x as [? [?|]]=> // -[??]. Qed.

Lemma dyn_reservation_map_cmra_mixin: CmraMixin (dyn_reservation_map A).
  Proof.
    apply (iso_cmra_mixin_restrict_validity from_reservation_map to_reservation_map); try done.
    - intros n [m [E|]];
        rewrite dyn_reservation_map_validN_eq reservation_map_validN_eq /=;
        naive_solver.
    - intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[?[??]]; split; simplify_eq/=.
      + by rewrite -Hm.
      + split; first done. intros i. by rewrite -(dist_None n) -Hm dist_None.
    - pose 0ᵢ.
      intros [m [E|]]; rewrite dyn_reservation_map_valid_eq
        dyn_reservation_map_validN_eq /= ?cmra_valid_validN; naive_solver.
    - intros n m [r [E|]]; rewrite dyn_reservation_map_validN_eq /=;
        naive_solver eauto using cmra_validN_le.
    - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite dyn_reservation_map_validN_eq /=.
      rewrite {1}/op /cmra_op /=. case_decide; last done.
      intros [Hm [Hinf Hdisj]]; split; first by eauto using cmra_validN_op_l.
      split.
      + rewrite ->difference_union_distr_r_L in Hinf.
        eapply set_infinite_subseteq, Hinf. set_solver.
      + intros i. move: (Hdisj i). rewrite lookup_op.
        case: (m1 !! i); case: (m2 !! i); set_solver.
  Qed.
  Canonical Structure dyn_reservation_mapR :=
    Cmra (dyn_reservation_map A) dyn_reservation_map_cmra_mixin.

Global Instancedyn_reservation_map_cmra_discrete :
    CmraDiscrete A → CmraDiscrete dyn_reservation_mapR.
  Proof.
    split; first apply _.
    intros [m [E|]]; rewrite dyn_reservation_map_validN_eq dyn_reservation_map_valid_eq //=.
      by intros [?%cmra_discrete_valid ?].
  Qed.

Local Instancedyn_reservation_map_empty_instance : Unit (dyn_reservation_map A) :=
    DynReservationMap ε ε.

Lemma dyn_reservation_map_ucmra_mixin: UcmraMixin (dyn_reservation_map A).
  Proof.
    split; simpl.
    - rewrite dyn_reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. split.
      + rewrite difference_empty_L. apply top_infinite.
      + set_solver.
    - split; simpl; [by rewrite left_id|by rewrite left_id_L].
    - do 2 constructor; [apply (core_id_core _)|done].
  Qed.
  Canonical Structure dyn_reservation_mapUR :=
    Ucmra (dyn_reservation_map A) dyn_reservation_map_ucmra_mixin.

Global Instancedyn_reservation_map_data_core_id k a :
    CoreId a → CoreId (dyn_reservation_map_data k a).
  Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.

Lemma dyn_reservation_map_data_validk a :
    ✓ (dyn_reservation_map_data k a) ↔ ✓ a.
  Proof.
    rewrite dyn_reservation_map_valid_eq /= singleton_valid.
    split; first naive_solver. intros Ha.
    split; first done. split; last set_solver.
    rewrite difference_empty_L. apply top_infinite.
  Qed.

Lemma dyn_reservation_map_token_validE :
    ✓ (dyn_reservation_map_token E) ↔ set_infinite (⊤ ∖ E).
  Proof.
    rewrite dyn_reservation_map_valid_eq /=. split; first naive_solver.
    intros Hinf. do 2 (split; first done). by left.
  Qed.

Lemma dyn_reservation_map_data_opk a b :
    dyn_reservation_map_data k (a ⋅ b) = dyn_reservation_map_data k a ⋅ dyn_reservation_map_data k b.
  Proof.
    by rewrite {2}/op /dyn_reservation_map_op_instance
      /dyn_reservation_map_data /= singleton_op left_id_L.
  Qed.

Lemma dyn_reservation_map_data_monok a b :
    a ≼ b → dyn_reservation_map_data k a ≼ dyn_reservation_map_data k b.
  Proof. intros [c ->]. by rewrite dyn_reservation_map_data_op. Qed.

Global Instancedyn_reservation_map_data_is_op k a b1 b2 :
    IsOp a b1 b2 →
    IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).
  Proof. rewrite /IsOp' /IsOp=> ->. by rewrite dyn_reservation_map_data_op. Qed.

Lemma dyn_reservation_map_token_unionE1 E2 :
    E1 ## E2 →
    dyn_reservation_map_token (E1 ∪ E2) = dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token E2.
  Proof.
    intros. by rewrite /op /dyn_reservation_map_op_instance
      /dyn_reservation_map_token /= coPset_disj_union // left_id_L.
  Qed.

Lemma dyn_reservation_map_token_differenceE1 E2 :
    E1 ⊆ E2 →
    dyn_reservation_map_token E2 = dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token (E2 ∖ E1).
  Proof.
    intros. rewrite -dyn_reservation_map_token_union; last set_solver.
    by rewrite -union_difference_L.
  Qed.

Lemma dyn_reservation_map_token_valid_opE1 E2 :
    ✓ (dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token E2) ↔
      E1 ## E2 ∧ set_infinite (⊤ ∖ (E1 ∪ E2)).
  Proof.
    split.
    - rewrite dyn_reservation_map_valid_eq /= {1}/op /cmra_op /=. case_decide; last done.
      naive_solver.
    - intros [Hdisj Hinf]. rewrite -dyn_reservation_map_token_union //.
      apply dyn_reservation_map_token_valid. done.
  Qed.

Lemma dyn_reservation_map_reserve(Q : dyn_reservation_map A → Prop) :
    (∀ E, set_infinite E → Q (dyn_reservation_map_token E)) →
    ε ~~>: Q.
  Proof.
    intros HQ. apply cmra_total_updateP=> n [mf [Ef|]];
      rewrite left_id {1}dyn_reservation_map_validN_eq /=; last done.
    intros [Hmap [Hinf Hdisj]].

Lemma dyn_reservation_map_reserve':
    ε ~~>: λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E.
  Proof. eauto using dyn_reservation_map_reserve. Qed.

Lemma dyn_reservation_map_allocE k a :
    k ∈ E → ✓ a → dyn_reservation_map_token E ~~> dyn_reservation_map_data k a.
  Proof.
    intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
    rewrite dyn_reservation_map_validN_eq /= {1}/op {1}/cmra_op /=.
    case_decide; last done.
    rewrite !left_id_L. intros [Hmf [Hinf Hdisj]]; split; last split.
    - destruct (Hdisj k) as [Hmfi|]; last set_solver.
      intros j. rewrite lookup_op.
      destruct (decide (k = j)) as [<-|].
      + rewrite Hmfi lookup_singleton_eq right_id_L. by apply cmra_valid_validN.
      + by rewrite lookup_singleton_ne // left_id_L.
    - eapply set_infinite_subseteq, Hinf. set_solver.
    - intros j. destruct (decide (k = j)); first set_solver.
      rewrite lookup_op lookup_singleton_ne //.
      destruct (Hdisj j) as [Hmfi|?]; last set_solver. rewrite Hmfi; auto.
  Qed.

Lemma dyn_reservation_map_updatePP (Q : dyn_reservation_map A → Prop) k a :
    a ~~>: P →
    (∀ a', P a' → Q (dyn_reservation_map_data k a')) →
    dyn_reservation_map_data k a ~~>: Q.
  Proof.
    intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
    rewrite dyn_reservation_map_validN_eq /= left_id_L. intros [Hmf [Hinf Hdisj]].
    destruct (Hup n (mf !! k)) as (a'&?&?).
    { move: (Hmf (k)).
      by rewrite lookup_op lookup_singleton_eq Some_op_opM. }
    exists (dyn_reservation_map_data k a'); split; first by eauto.
    rewrite /= left_id_L. split; last split.
    - intros j. destruct (decide (k = j)) as [<-|].
      + by rewrite lookup_op lookup_singleton_eq Some_op_opM.
      + rewrite lookup_op lookup_singleton_ne // left_id_L.
        move: (Hmf j). rewrite lookup_op. eauto using cmra_validN_op_r.
    - done.
    - intros j. move: (Hdisj j).
      rewrite !lookup_op !op_None !lookup_singleton_None. naive_solver.
  Qed.

Lemma dyn_reservation_map_updatek a b :
    a ~~> b →
    dyn_reservation_map_data k a ~~> dyn_reservation_map_data k b.
  Proof.
    rewrite !cmra_update_updateP. eauto using dyn_reservation_map_updateP with subst.
  Qed.

Global Argumentsdyn_reservation_mapR {_} _.

Global Argumentsdyn_reservation_mapUR {_} _.