Library zoo.iris.base_logic.lib.ghost_list

From iris.base_logic Require Import
  lib.ghost_map.

From zoo Require Import
  prelude.
From zoo.common Require Import
  list.
From zoo.iris.bi Require Import
  big_op.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  options.

Class GhostListG Σ A :=
  { #[local] ghost_list_G_map_G :: ghost_mapG Σ nat A
  }.

Definition ghost_list_Σ A :=
  #[ghost_mapΣ nat A
  ].
#[global] Instance subG_ghost_list_Σ Σ A :
  subG (ghost_list_Σ A) Σ →
  GhostListG Σ A.

Section ghost_list_G.
  Context `{ghost_list_G : !GhostListG Σ A}.

  Implicit Types x : A.
  Implicit Types xs : list A.

  Definition ghost_list_auth γ xs :=
    ghost_map_auth γ 1 (map_seq 0 xs).
  Definition ghost_list_at γ :=
    ghost_map_elem γ.

  #[global] Instance ghost_list_auth_timeless γ vs :
    Timeless (ghost_list_auth γ vs).
  #[global] Instance ghost_list_at_timeless γ i dq x :
    Timeless (ghost_list_at γ i dq x).

  #[global] Instance ghost_list_at_persistent γ i x :
    Persistent (ghost_list_at γ i DfracDiscarded x).

  #[global] Instance ghost_list_at_fractional γ i x :
    Fractional (λ q, ghost_list_at γ i (DfracOwn q) x).
  #[global] Instance ghost_list_at_as_fractional γ i q x :
    AsFractional (ghost_list_at γ i (DfracOwn q) x) (λ q, ghost_list_at γ i (DfracOwn q) x) q.

  Lemma ghost_list_alloc xs :
    ⊢ |==>
      ∃ γ,
      ghost_list_auth γ xs ∗
      [∗ list] i ↦ x ∈ xs,
        ghost_list_at γ i (DfracOwn 1) x.

  Lemma ghost_list_auth_exclusive γ xs1 xs2 :
    ghost_list_auth γ xs1 -∗
    ghost_list_auth γ xs2 -∗
    False.

  Lemma ghost_list_at_valid γ i dq x :
    ghost_list_at γ i dq x ⊢
    ⌜✓ dq⌝.
  Lemma ghost_list_at_combine γ i dq1 x1 dq2 x2 :
    ghost_list_at γ i dq1 x1 -∗
    ghost_list_at γ i dq2 x2 -∗
      ⌜x1 = x2⌝ ∗
      ghost_list_at γ i (dq1 ⋅ dq2) x1.
  Lemma ghost_list_at_valid_2 γ i dq1 x1 dq2 x2 :
    ghost_list_at γ i dq1 x1 -∗
    ghost_list_at γ i dq2 x2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜x1 = x2⌝.
  Lemma ghost_list_at_agree γ i dq1 x1 dq2 x2 :
    ghost_list_at γ i dq1 x1 -∗
    ghost_list_at γ i dq2 x2 -∗
    ⌜x1 = x2⌝.
  Lemma ghost_list_at_dfrac_ne γ1 i1 dq1 x1 γ2 i2 dq2 x2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    ghost_list_at γ1 i1 dq1 x1 -∗
    ghost_list_at γ2 i2 dq2 x2 -∗
    ⌜γ1 ≠ γ2 ∨ i1 ≠ i2⌝.
  Lemma ghost_list_at_ne γ1 i1 x1 γ2 i2 dq2 x2 :
    ghost_list_at γ1 i1 (DfracOwn 1) x1 -∗
    ghost_list_at γ2 i2 dq2 x2 -∗
    ⌜γ1 ≠ γ2 ∨ i1 ≠ i2⌝.
  Lemma ghost_list_at_exclusive γ i x1 dq2 x2 :
    ghost_list_at γ i (DfracOwn 1) x1 -∗
    ghost_list_at γ i dq2 x2 -∗
    False.
  Lemma ghost_list_at_persist γ i dq x :
    ghost_list_at γ i dq x ⊢ |==>
    ghost_list_at γ i DfracDiscarded x.

  Lemma ghost_list_lookup γ xs i dq x :
    ghost_list_auth γ xs -∗
    ghost_list_at γ i dq x -∗
    ⌜xs !! i = Some x⌝.
  Lemma ghost_list_auth_ats γ xs1 dq xs2 :
    length xs1 = length xs2 →
    ghost_list_auth γ xs1 -∗
    ([∗ list] i ↦ x ∈ xs2, ghost_list_at γ i dq x) -∗
    ⌜xs1 = xs2⌝.

  Lemma ghost_list_update_push {γ xs} x :
    ghost_list_auth γ xs ⊢ |==>
      ghost_list_auth γ (xs ++ [x]) ∗
      ghost_list_at γ (length xs) (DfracOwn 1) x.
  Lemma ghost_list_update_at {γ xs i x} x' :
    ghost_list_auth γ xs -∗
    ghost_list_at γ i (DfracOwn 1) x ==∗
      ghost_list_auth γ (<[i := x']> xs) ∗
      ghost_list_at γ i (DfracOwn 1) x'.
End ghost_list_G.

#[global] Opaque ghost_list_auth.
#[global] Opaque ghost_list_at.