Library zoo_saturn.mpmc_stack_2

From zoo Require Import
  prelude.
From zoo.iris.base_logic Require Import
  lib.twins.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  option
  optional
  clist.
From zoo_saturn Require Export
  base
  mpmc_stack_2__code.
From zoo Require Import
  options.

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

Class MpmcStack2G Σ `{zoo_G : !ZooG Σ} :=
  { #[local] mpmc_stack_2_G_model_G :: TwinsG Σ (leibnizO (option $ list val))
  }.

Definition mpmc_stack_2_Σ :=
  #[twins_Σ (leibnizO (option $ list val))
  ].
#[global] Instance subG_mpmc_stack_2_Σ Σ `{zoo_G : !ZooG Σ} :
  subG mpmc_stack_2_Σ Σ →
  MpmcStack2G Σ.

Section zoo_G.
  Context `{mpmc_stack_2_G : MpmcStack2G Σ}.

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

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

  #[local] Definition inv_inner l γ : iProp Σ :=
    ∃ vs,
    l ↦ᵣ from_option (clist_to_val ∘ list_to_clist_open) §ClistClosed vs ∗
    model₂ γ vs.
  #[local] Instance : CustomIpat "inv_inner" :=
    " ( %vs & Hl & Hmodel₂ ) ".
  Definition mpmc_stack_2_inv t ι : iProp Σ :=
    ∃ l γ,
    ⌜t = #l⌝ ∗
    meta l nroot γ ∗
    inv ι (inv_inner l γ).
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & #Hmeta & #Hinv ) ".

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

  Definition mpmc_stack_2_closed t :=
    mpmc_stack_2_model t None.

  #[global] Instance mpmc_stack_2_model_timeless t vs :
    Timeless (mpmc_stack_2_model t vs).

  #[global] Instance mpmc_stack_2_inv_persistent t ι :
    Persistent (mpmc_stack_2_inv t ι).
  #[global] Instance mpmc_stack_2_model_persistent t :
    Persistent (mpmc_stack_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 mpmc_stack_2_model_exclusive t vs1 vs2 :
    mpmc_stack_2_model t (Some vs1) -∗
    mpmc_stack_2_model t vs2 -∗
    False.

  Lemma mpmc_stack_2٠create𑁒spec ι :
    {{{
      True
    }}}
      mpmc_stack_2٠create ()
    {{{
      t
    , RET t;
      mpmc_stack_2_inv t ι ∗
      mpmc_stack_2_model t (Some [])
    }}}.

  Lemma mpmc_stack_2٠push𑁒spec t ι v :
    <<<
      mpmc_stack_2_inv t ι
    | ∀∀ vs,
      mpmc_stack_2_model t vs
    >>>
      mpmc_stack_2٠push t v @ ↑ι
    <<<
      mpmc_stack_2_model t (cons v <$> vs)
    | RET #(bool_decide (vs = None));
      £ 1
    >>>.
  Lemma mpmc_stack_2٠push𑁒spec_closed t ι v :
    {{{
      mpmc_stack_2_inv t ι ∗
      mpmc_stack_2_closed t
    }}}
      mpmc_stack_2٠push t v
    {{{
      RET true;
      True
    }}}.

  Lemma mpmc_stack_2٠pop𑁒spec t ι :
    <<<
      mpmc_stack_2_inv t ι
    | ∀∀ vs,
      mpmc_stack_2_model t vs
    >>>
      mpmc_stack_2٠pop t @ ↑ι
    <<<
      mpmc_stack_2_model t (tail <$> vs)
    | RET default Anything (option_to_optional ∘ head <$> vs);
      £ 1
    >>>.
  Lemma mpmc_stack_2٠pop𑁒spec_closed t ι v :
    {{{
      mpmc_stack_2_inv t ι ∗
      mpmc_stack_2_closed t
    }}}
      mpmc_stack_2٠pop t
    {{{
      RET §Anything;
      True
    }}}.

  Lemma mpmc_stack_2٠is_closed𑁒spec t ι :
    <<<
      mpmc_stack_2_inv t ι
    | ∀∀ vs,
      mpmc_stack_2_model t vs
    >>>
      mpmc_stack_2٠is_closed t @ ↑ι
    <<<
      mpmc_stack_2_model t vs
    | RET #(bool_decide (vs = None));
      £ 1
    >>>.
  Lemma mpmc_stack_2٠is_closed𑁒spec_closed t ι :
    {{{
      mpmc_stack_2_inv t ι ∗
      mpmc_stack_2_closed t
    }}}
      mpmc_stack_2٠is_closed t
    {{{
      RET true;
      True
    }}}.

  Lemma mpmc_stack_2٠close𑁒spec t ι :
    <<<
      mpmc_stack_2_inv t ι
    | ∀∀ vs,
      mpmc_stack_2_model t vs
    >>>
      mpmc_stack_2٠close t @ ↑ι
    <<<
      mpmc_stack_2_model t None
    | RET from_option list_to_clist_open ClistClosed vs;
      £ 1
    >>>.
  Lemma mpmc_stack_2٠closed𑁒spec_closed t ι v :
    {{{
      mpmc_stack_2_inv t ι ∗
      mpmc_stack_2_closed t
    }}}
      mpmc_stack_2٠close t
    {{{
      RET §ClistClosed;
      True
    }}}.
End zoo_G.

From zoo_saturn Require
  mpmc_stack_2__opaque.

#[global] Opaque mpmc_stack_2_inv.
#[global] Opaque mpmc_stack_2_model.