Library zoo_boxroot.boxroot

Require Import iris.base_logic.lib.ghost_map.

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.common.fin_maps.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo_std.xdeque.
Require Export zoo_boxroot.gc.
Require Import zoo.options.

Section list_to_set.
  Lemma list_to_set ｰ delete `{Countable A} {l i} x :
    NoDup l →
    l !! i = Some x →
    list_to_set (C := gset A) (delete i l) ≡ list_to_set l ∖ {[x ]}.
End list_to_set.

Section list_to_map.
  Lemma list_to_map ｰ zip ｰ list_to_set `{Countable K} `{!Inhabited A} (m : gmap K A) (l : list K) :
    NoDup l →
    dom m ≡ list_to_set l →
    list_to_map (zip l ((λ x, m !!! x ) <$> l)) = m.
End list_to_map.

Implicit Type l l_global root : location.
Implicit Type roots : list location.
Implicit Type v t global : val.
Implicit Type ω : gc ۰ location.
Implicit Type map : gmap location gc ۰ location.

Definition boxroot ٠ init : val :=
  𝗳𝘂𝗻 ⎽ →
    𝗹𝗲𝘁 "global" = xdeque ٠ create () 𝗶𝗻
    gc ٠ set_roots (𝗳𝘂𝗻 "fn" → xdeque ٠ iter "fn" "global") #2%nat ⍮
    "global".

Definition boxroot ٠ create : val :=
  𝗳𝘂𝗻 "global" "v" →
    𝗹𝗲𝘁 "t" = { (), (), "v" } 𝗶𝗻
    xdeque ٠ push_back "global" "t" ⍮
    "t".

Definition boxroot ٠ remove : val :=
  𝗳𝘂𝗻 "global" "t" →
    xdeque ٠ remove "t".

Definition boxroot ٠ get : val :=
  𝗳𝘂𝗻 "t" →
    "t".{xdeque ٠ data }.

Definition boxroot ٠ set : val :=
  𝗳𝘂𝗻 "t" "v" →
    "t" <-{xdeque ٠ data } "v".

Class BoxrootG Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] boxroot ۰ G ۰ roots ۰ G :: ghost_mapG Σ location gc ۰ location
  }.

Definition boxroot ۰ Σ :=
  #[ghost_mapΣ location gc ۰ location
  ].
#[global] Instance subG ｰ boxroot ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG boxroot ۰ Σ Σ →
  BoxrootG Σ.

Section boxroot ۰ G.
  Context `{boxroot ۰ G : BoxrootG Σ}.

  #[local] Definition metadata :=
    gname.
  Implicit Type γ : metadata.

  #[local] Definition roots ۰ auth γ map :=
    ghost_map_auth γ 1 map.
  #[local] Definition roots ۰ elem γ root ω :=
    ghost_map_elem γ root (DfracOwn 1) ω.

  Definition boxroot ۰ global global gc : iProp Σ :=
    ∃ l_global γ roots map ,
    ⌜global = #l_global ⌝ ∗
    l_global ↪ γ ∗
    ⌜dom map ≡ list_to_set roots ⌝ ∗
    roots ۰ auth γ map ∗
    xdeque ۰ model global roots ∗
    [∗ map ] root ↦ ω ∈ map ,
      root .[xdeque ٠ data ] ↦root [gc ] ω.

  Definition boxroot ۰ model t global ω : iProp Σ :=
    ∃ root l_global γ ,
    ⌜t = #root ⌝ ∗
    ⌜global = #l_global ⌝ ∗
    l_global ↪ γ ∗
    roots ۰ elem γ root ω.

  #[local] Lemma roots ｰ alloc :
    ⊢ |==>
      ∃ γ ,
      roots ۰ auth γ ∅.
  #[local] Lemma roots ｰ lookup γ map root ω :
    roots ۰ auth γ map -∗
    roots ۰ elem γ root ω -∗
    ⌜map !! root = Some ω ⌝.
  #[local] Lemma roots ｰ insert {γ map} root ω :
    map !! root = None →
    roots ۰ auth γ map ⊢ |==>
      roots ۰ auth γ (<[root := ω ]> map) ∗
      roots ۰ elem γ root ω.
  #[local] Lemma roots ｰ delete γ map root ω :
    roots ۰ auth γ map -∗
    roots ۰ elem γ root ω ==∗
      roots ۰ auth γ (delete root map).
  #[local] Lemma roots ｰ update {γ map root ω} ω' :
    roots ۰ auth γ map -∗
    roots ۰ elem γ root ω ==∗
      roots ۰ auth γ (<[root := ω']> map) ∗
      roots ۰ elem γ root ω'.

  Lemma boxroot ٠ init ｰ spec gc Χ :
    {{{
      gc ۰ model gc ∗
      gc ۰ roots Χ
    }}}
      boxroot ٠ init ()
    {{{
      global
    , RET global ;
      gc ۰ model gc ∗
      gc ۰ roots (boxroot ۰ global global) ∗
      boxroot ۰ global global gc
    }}}.

  Lemma boxroot ٠ create ｰ spec {gc global l} ω :
    ω ↦gc [gc ] l →
    {{{
      boxroot ۰ global global gc
    }}}
      boxroot ٠ create global #l
    {{{
      t
    , RET t ;
      boxroot ۰ global global gc ∗
      boxroot ۰ model t global ω
    }}}.

  Lemma boxroot ٠ remove ｰ spec gc global t ω :
    {{{
      boxroot ۰ global global gc ∗
      boxroot ۰ model t global ω
    }}}
      boxroot ٠ remove global t
    {{{
      RET ();
      boxroot ۰ global global gc
    }}}.

  Lemma boxroot ٠ get ｰ spec gc global t ω :
    {{{
      boxroot ۰ global global gc ∗
      boxroot ۰ model t global ω
    }}}
      boxroot ٠ get t
    {{{
      l
    , RET #l ;
      ⌜ω ↦gc [gc ] l ⌝ ∗
      boxroot ۰ global global gc ∗
      boxroot ۰ model t global ω
    }}}.

  Lemma boxroot ٠ set ｰ spec {gc global t ω'} ω l :
    ω ↦gc [gc ] l →
    {{{
      boxroot ۰ global global gc ∗
      boxroot ۰ model t global ω'
    }}}
      boxroot ٠ set t #l
    {{{
      RET ();
      boxroot ۰ global global gc ∗
      boxroot ۰ model t global ω
    }}}.
End boxroot ۰ G.

#[global] Opaque boxroot ٠ create.
#[global] Opaque boxroot ٠ remove.
#[global] Opaque boxroot ٠ get.
#[global] Opaque boxroot ٠ set.

#[global] Opaque boxroot ۰ global.
#[global] Opaque boxroot ۰ model.