Library zoo_boxroot.boxroot

From iris.base_logic Require Import
  lib.ghost_map.

From zoo Require Import
  prelude.
From zoo.common Require Import
  list
  fin_maps.
From zoo.iris.bi Require Import
  big_op.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  xdeque.
From zoo_boxroot Require Export
  gc.
From zoo Require Import
  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 Types l l_global root : location.
Implicit Types roots : list location.
Implicit Types v t global : val.
Implicit Types ω : gc_location.
Implicit Types map : gmap location gc_location.

Definition boxroot٠init : val :=
  fun: ≠ ⇒
    let: "global" := xdeque٠create () in
    gc٠set_roots (fun: "fn" ⇒ xdeque٠iter "fn" "global") #2%nat ;;
    "global".

Definition boxroot٠create : val :=
  fun: "global" "v" ⇒
    let: "t" := { (), (), "v" } in
    xdeque٠push_back "global" "t" ;;
    "t".

Definition boxroot٠remove : val :=
  fun: "global" "t" ⇒
    xdeque٠remove "t".

Definition boxroot٠get : val :=
  fun: "t" ⇒
    "t".{xdeque_data}.

Definition boxroot٠set : val :=
  fun: "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 Types γ : 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⌝ ∗
    meta l_global nroot γ ∗
    ⌜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⌝ ∗
    meta l_global nroot γ ∗
    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.