Library zoo_saturn.bag_1

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.common.list.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Export zoo_saturn.bag_1__code.
Require Import zoo_saturn.bag_1__types.
Require Import zoo.options.

Implicit Type front back : nat.
Implicit Type l slot : location.
Implicit Type slots : list location.
Implicit Type v t data : val.
Implicit Type vs : gmultiset val.
Implicit Type o : option val.
Implicit Type os : list (option val).

Class Bag1G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] bag_1 ۰ G ۰ model ۰ G :: TwinsG Σ (leibnizO (gmultiset val))
  }.

Definition bag_1 ۰ Σ :=
  #[twins ۰ Σ (leibnizO (gmultiset val))
  ].
#[global] Instance subG ｰ bag_1 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG bag_1 ۰ Σ Σ →
  Bag1G Σ.

Section consistent.
  #[local] Definition consistent vs os :=
    vs = ⋃+ (singletonMS <$> oflatten os ).

  #[local] Lemma consistent ｰ lookup vs os i v :
    os !! i = Some $ Some v →
    consistent vs os →
    v ∈ vs.
  #[local] Lemma consistent ｰ insert {vs os i} v :
    os !! i = Some None →
    consistent vs os →
    consistent ({[+v +]} ⊎ vs) (<[i := Some v ]> os).
  #[local] Lemma consistent ｰ remove vs os i v :
    os !! i = Some $ Some v →
    consistent vs os →
    consistent (vs ∖ {[+v +]}) (<[i := None ]> os).
End consistent.

Opaque consistent.

Section bag_1 ۰ G.
  Context `{bag_1 ۰ G : Bag1G Σ}.

  Record metadata :=
    { metadata ۰ data : val
    ; metadata ۰ slots : list location
    ; metadata ۰ inv : namespace
    ; metadata ۰ model : gname
    }.
  Implicit Type γ : metadata.

  #[local] Instance metadata ｰ eq_dec : EqDecision metadata :=
    ltac:(solve_decision).
  #[local] Instance metadata ｰ countable :
    Countable metadata.

  #[local] Definition model₁' γ_model vs :=
    twins ۰ twin₁ γ_model (DfracOwn 1) vs.
  #[local] Definition model₁ γ vs :=
    model₁' γ.(metadata ۰ model) vs.
  #[local] Definition model₂' γ_model vs :=
    twins ۰ twin₂ γ_model vs.
  #[local] Definition model₂ γ vs :=
    model₂' γ.(metadata ۰ model) vs.

  #[local] Definition inv ۰ inner l γ : iProp Σ :=
    ∃ front back vs os ,
    l .[front ] ↦ #front ∗
    l .[back ] ↦ #back ∗
    model₂ γ vs ∗
    ⌜consistent vs os ⌝ ∗
    [∗ list ] slot ; o ∈ γ.(metadata ۰ slots); os ,
      slot ↦ᵣ (o : val ).
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %front & %back & %vs & %os & Hfront & Hback & Hmodel₂ & >%Hconsistent & Hslots ) ".
  #[local] Definition inv' l γ :=
    inv γ.(metadata ۰ inv) (inv ۰ inner l γ).
  Definition bag_1 ۰ inv t ι : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    ⌜ι = γ.(metadata ۰ inv)⌝ ∗
    ⌜0 < length γ.(metadata ۰ slots)⌝ ∗
    l ↪ γ ∗
    l .[data ] ↦□ γ.(metadata ۰ data) ∗
    array ۰ model γ.(metadata ۰ data) DfracDiscarded (#*@{location } γ .(metadata ۰ slots )) ∗
    inv' l γ.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & -> & %Hsz & #Hmeta & #Hdata & #Hdata_model & #Hinv ) ".

  Definition bag_1 ۰ model t vs : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    model₁ γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} ) ".

  #[global] Instance bag_1 ۰ model ｰ timeless t vs :
    Timeless (bag_1 ۰ model t vs).

  #[global] Instance bag_1 ۰ inv ｰ persistent t ι :
    Persistent (bag_1 ۰ inv t ι).

  #[local] Lemma model ｰ alloc :
    ⊢ |==>
      ∃ γ_model ,
      model₁' γ_model ∅ ∗
      model₂' γ_model ∅.
  #[local] Lemma model₁ ｰ exclusive γ vs1 vs2 :
    model₁ γ vs1 -∗
    model₁ γ vs2 -∗
    False.
  #[local] Lemma model ｰ agree γ vs1 vs2 :
    model₁ γ vs1 -∗
    model₂ γ vs2 -∗
    ⌜vs1 = vs2 ⌝.
  #[local] Lemma model ｰ update {γ vs1 vs2} vs :
    model₁ γ vs1 -∗
    model₂ γ vs2 ==∗
      model₁ γ vs ∗
      model₂ γ vs.

  Lemma bag_1 ۰ model ｰ exclusive t vs1 vs2 :
    bag_1 ۰ model t vs1 -∗
    bag_1 ۰ model t vs2 -∗
    False.

  Lemma bag_1 ٠ create ｰ spec ι (sz : Z) :
    (0 < sz)%Z →
    {{{
      True
    }}}
      bag_1 ٠ create #sz
    {{{
      t
    , RET t ;
      bag_1 ۰ inv t ι ∗
      bag_1 ۰ model t ∅
    }}}.

  #[local] Lemma bag_1 ٠ push₁ ｰ spec slot v l γ :
    slot ∈ γ.(metadata ۰ slots) →
    <<<
      l ↪ γ ∗
      inv' l γ
    | ∀∀ vs ,
      bag_1 ۰ model #l vs
    >>>
      bag_1 ٠ push₁ #slot ’Some [ v ] @ ↑γ.(metadata ۰ inv)
    <<<
      bag_1 ۰ model #l ({[+v +]} ⊎ vs)
    | RET ();
      True
    >>>.
  Lemma bag_1 ٠ push ｰ spec t ι v :
    <<<
      bag_1 ۰ inv t ι
    | ∀∀ vs ,
      bag_1 ۰ model t vs
    >>>
      bag_1 ٠ push t v @ ↑ι
    <<<
      bag_1 ۰ model t ({[+v +]} ⊎ vs)
    | RET ();
      True
    >>>.

  #[local] Lemma bag_1 ٠ pop₁ ｰ spec slot l γ :
    slot ∈ γ.(metadata ۰ slots) →
    <<<
      l ↪ γ ∗
      inv' l γ
    | ∀∀ vs ,
      bag_1 ۰ model #l vs
    >>>
      bag_1 ٠ pop₁ #slot @ ↑γ.(metadata ۰ inv)
    <<<
      ∃∃ v vs',
      ⌜vs = {[+v +]} ⊎ vs'⌝ ∗
      bag_1 ۰ model #l vs'
    | RET v ;
      True
    >>>.
  Lemma bag_1 ٠ pop ｰ spec t ι :
    <<<
      bag_1 ۰ inv t ι
    | ∀∀ vs ,
      bag_1 ۰ model t vs
    >>>
      bag_1 ٠ pop t @ ↑ι
    <<<
      ∃∃ v vs',
      ⌜vs = {[+v +]} ⊎ vs'⌝ ∗
      bag_1 ۰ model t vs'
    | RET v ;
      True
    >>>.
End bag_1 ۰ G.

Require zoo_saturn.bag_1__opaque.

#[global] Opaque bag_1 ۰ inv.
#[global] Opaque bag_1 ۰ model.