Library zoo_saturn.mpmc_stack_1

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
  glist.
From zoo_saturn Require Export
  base
  mpmc_stack_1__code.
From zoo Require Import
  options.

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

Class MpmcStack1G Σ `{zoo_G : !ZooG Σ} :=
  { #[local] mpmc_stack_1_G_model_G :: TwinsG Σ (leibnizO (list val))
  }.

Definition mpmc_stack_1_Σ :=
  #[twins_Σ (leibnizO (list val))
  ].
#[global] Instance subG_mpmc_stack_1_Σ Σ `{zoo_G : !ZooG Σ} :
  subG mpmc_stack_1_Σ Σ →
  MpmcStack1G Σ.

Section zoo_G.
  Context `{mpmc_stack_1_G : MpmcStack1G Σ}.

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

  #[local] Definition model₁ γ vs :=
    twins_twin1 γ (DfracOwn 1) vs.
  #[local] Definition model₂ γ vs :=
    twins_twin2 γ vs.

  #[local] Definition inv_inner l γ : iProp Σ :=
    ∃ vs,
    l ↦ᵣ glist_to_val vs ∗
    model₂ γ vs.
  #[local] Instance : CustomIpat "inv_inner" :=
    " ( %vs{} & Hl & Hmodel₂ ) ".
  Definition mpmc_stack_1_inv t ι : iProp Σ :=
    ∃ l γ,
    ⌜t = #l⌝ ∗
    meta l nroot γ ∗
    inv ι (inv_inner l γ).
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & #Hmeta & #Hinv ) ".

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

  #[global] Instance mpmc_stack_1_model_timeless t vs :
    Timeless (mpmc_stack_1_model t vs).

  #[global] Instance mpmc_stack_1_inv_persistent t ι :
    Persistent (mpmc_stack_1_inv t ι).

  #[local] Lemma model_alloc :
    ⊢ |==>
      ∃ γ,
      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 mpmc_stack_1_model_exclusive t vs1 vs2 :
    mpmc_stack_1_model t vs1 -∗
    mpmc_stack_1_model t vs2 -∗
    False.

  Lemma mpmc_stack_1٠create𑁒spec ι :
    {{{
      True
    }}}
      mpmc_stack_1٠create ()
    {{{
      t
    , RET t;
      mpmc_stack_1_inv t ι ∗
      mpmc_stack_1_model t []
    }}}.

  Lemma mpmc_stack_1٠push𑁒spec t ι v :
    <<<
      mpmc_stack_1_inv t ι
    | ∀∀ vs,
      mpmc_stack_1_model t vs
    >>>
      mpmc_stack_1٠push t v @ ↑ι
    <<<
      mpmc_stack_1_model t (v :: vs)
    | RET ();
      True
    >>>.

  Lemma mpmc_stack_1٠pop𑁒spec t ι :
    <<<
      mpmc_stack_1_inv t ι
    | ∀∀ vs,
      mpmc_stack_1_model t vs
    >>>
      mpmc_stack_1٠pop t @ ↑ι
    <<<
      mpmc_stack_1_model t (tail vs)
    | RET head vs;
      True
    >>>.

  Lemma mpmc_stack_1٠snapshot𑁒spec t ι :
    <<<
      mpmc_stack_1_inv t ι
    | ∀∀ vs,
      mpmc_stack_1_model t vs
    >>>
      mpmc_stack_1٠snapshot t @ ↑ι
    <<<
      mpmc_stack_1_model t vs
    | RET glist_to_val vs;
      True
    >>>.
End zoo_G.

From zoo_saturn Require
  mpmc_stack_1__opaque.

#[global] Opaque mpmc_stack_1_inv.
#[global] Opaque mpmc_stack_1_model.