Library zoo_saturn.stack_mpmc_2

Require Import zoo.prelude.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_saturn.stack_mpmc_2__code.
Require Import zoo_saturn.stack_mpmc_2__types.
Require Import zoo.options.

Implicit Type l : location.
Implicit Type v t : val.
Implicit Type ws : list val.

Class StackMpmc2G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] stack_mpmc_2 ۰ G ۰ model ۰ G :: TwinsG Σ (leibnizO (option $ list val))
  }.

Definition stack_mpmc_2 ۰ Σ :=
  #[twins ۰ Σ (leibnizO (option $ list val))
  ].
#[global] Instance subG ｰ stack_mpmc_2 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG stack_mpmc_2 ۰ Σ Σ →
  StackMpmc2G Σ.

Section zoo ۰ G.
  Context `{stack_mpmc_2 ۰ G : StackMpmc2G Σ}.

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

  #[local] Definition model₁ γ vs :=
    twins ۰ twin₁ γ (if vs is None then DfracDiscarded else DfracOwn 1) vs.
  #[local] Definition model₂ γ vs :=
    twins ۰ twin₂ γ vs.

  #[local] Definition inv ۰ inner l γ : iProp Σ :=
    ∃ vs ,
    l ↦ᵣ from_option (clist ۰ to_val ∘ list ۰ to_clist_open) §clist ٠ Closed vs ∗
    model₂ γ vs.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %vs & Hl & Hmodel₂ ) ".
  Definition stack_mpmc_2 ۰ inv t ι : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    inv ι (inv ۰ inner l γ).
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & #Hmeta & #Hinv ) ".

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

  Definition stack_mpmc_2 ۰ closed t :=
    stack_mpmc_2 ۰ model t None.

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

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

  #[local] Lemma model ｰ alloc :
    ⊢ |==>
      ∃ γ ,
      model₁ γ (Some []) ∗
      model₂ γ (Some []).
  #[local] Lemma model₁ ｰ exclusive γ vs1 vs2 :
    model₁ γ (Some vs1) -∗
    model₁ γ vs2 -∗
    False.
  #[local] Lemma model ｰ agree γ vs1 vs2 :
    model₁ γ vs1 -∗
    model₂ γ vs2 -∗
    ⌜vs1 = vs2 ⌝.
  #[local] Lemma model ｰ update {γ ws1 ws2} ws :
    model₁ γ (Some ws1) -∗
    model₂ γ (Some ws2) ==∗
      model₁ γ (Some ws) ∗
      model₂ γ (Some ws).
  #[local] Lemma model ｰ close γ ws1 ws2 :
    model₁ γ (Some ws1) -∗
    model₂ γ (Some ws2) ==∗
      model₁ γ None ∗
      model₂ γ None.

  Lemma stack_mpmc_2 ۰ model ｰ exclusive t vs1 vs2 :
    stack_mpmc_2 ۰ model t (Some vs1) -∗
    stack_mpmc_2 ۰ model t vs2 -∗
    False.

  Lemma stack_mpmc_2 ٠ create ｰ spec ι :
    {{{
      True
    }}}
      stack_mpmc_2 ٠ create ()
    {{{
      t
    , RET t ;
      stack_mpmc_2 ۰ inv t ι ∗
      stack_mpmc_2 ۰ model t (Some [])
    }}}.

  Lemma stack_mpmc_2 ٠ push ｰ spec t ι v :
    <<<
      stack_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      stack_mpmc_2 ۰ model t vs
    >>>
      stack_mpmc_2 ٠ push t v @ ↑ι
    <<<
      stack_mpmc_2 ۰ model t (cons v <$> vs)
    | RET #(bool_decide (vs = None));
      £ 1
    >>>.
  Lemma stack_mpmc_2 ٠ push ｰ spec ｰ closed t ι v :
    {{{
      stack_mpmc_2 ۰ inv t ι ∗
      stack_mpmc_2 ۰ closed t
    }}}
      stack_mpmc_2 ٠ push t v
    {{{
      RET true ;
      True
    }}}.

  Lemma stack_mpmc_2 ٠ pop ｰ spec t ι :
    <<<
      stack_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      stack_mpmc_2 ۰ model t vs
    >>>
      stack_mpmc_2 ٠ pop t @ ↑ι
    <<<
      stack_mpmc_2 ۰ model t (tail <$> vs)
    | RET default Anything (option ۰ to_optional ∘ head <$> vs);
      £ 1
    >>>.
  Lemma stack_mpmc_2 ٠ pop ｰ spec ｰ closed t ι v :
    {{{
      stack_mpmc_2 ۰ inv t ι ∗
      stack_mpmc_2 ۰ closed t
    }}}
      stack_mpmc_2 ٠ pop t
    {{{
      RET §optional ٠ Anything ;
      True
    }}}.

  Lemma stack_mpmc_2 ٠ is_closed ｰ spec t ι :
    <<<
      stack_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      stack_mpmc_2 ۰ model t vs
    >>>
      stack_mpmc_2 ٠ is_closed t @ ↑ι
    <<<
      stack_mpmc_2 ۰ model t vs
    | RET #(bool_decide (vs = None));
      £ 1
    >>>.
  Lemma stack_mpmc_2 ٠ is_closed ｰ spec ｰ closed t ι :
    {{{
      stack_mpmc_2 ۰ inv t ι ∗
      stack_mpmc_2 ۰ closed t
    }}}
      stack_mpmc_2 ٠ is_closed t
    {{{
      RET true ;
      True
    }}}.

  Lemma stack_mpmc_2 ٠ close ｰ spec t ι :
    <<<
      stack_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      stack_mpmc_2 ۰ model t vs
    >>>
      stack_mpmc_2 ٠ close t @ ↑ι
    <<<
      stack_mpmc_2 ۰ model t None
    | RET from_option list ۰ to_clist_open Closed vs ;
      £ 1
    >>>.
  Lemma stack_mpmc_2 ٠ closed ｰ spec ｰ closed t ι v :
    {{{
      stack_mpmc_2 ۰ inv t ι ∗
      stack_mpmc_2 ۰ closed t
    }}}
      stack_mpmc_2 ٠ close t
    {{{
      RET §clist ٠ Closed ;
      True
    }}}.
End zoo ۰ G.

Require zoo_saturn.stack_mpmc_2__opaque.

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