Library zoo_saturn.mpmc_bstack

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
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.
From zoo_saturn Require Export
  base
  mpmc_bstack__code.
From zoo_saturn Require Import
  mpmc_bstack__types.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types cap sz : nat.
Implicit Types l : location.
Implicit Types v t front : val.
Implicit Types vs : list val.

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

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

Section mpmc_bstack_G.
  Context `{mpmc_bstack_G : MpmcBstackG Σ}.

  Record metadata :=
    { metadata_capacity : nat
    ; metadata_model : gname
    }.
  Implicit Types γ : metadata.

  #[local] Instance metadata_eq_dec : EqDecision metadata :=
    ltac:(solve_decision).
  #[local] Instance metadata_countable :
    Countable metadata.

  #[local] Fixpoint list_to_val sz vs :=
    match vs with
    | [] ⇒
        §Nil%V
    | v :: vs ⇒
        ‘Cons[ #sz, v, list_to_val (sz - 1) vs ]%V
    end.

  #[local] Instance list_to_val_inj_similar sz :
    Inj (=) (≈@{val}) (list_to_val sz).
  #[local] Instance list_to_val_inj sz :
    Inj (=) (=) (list_to_val sz).

  Lemma list_to_val_inj' vs1 vs2 :
    list_to_val (length vs1) vs1 ≈ list_to_val (length vs2) vs2 →
    vs1 = vs2.

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

  #[local] Definition inv_inner l γ : iProp Σ :=
    ∃ vs,
    l.[front] ↦ list_to_val (length vs) vs ∗
    model₂ γ vs.
  #[local] Instance : CustomIpat "inv_inner" :=
    " ( %vs{} & Hl_front & Hmodel₂ ) ".
  Definition mpmc_bstack_inv t ι cap : iProp Σ :=
    ∃ l γ,
    ⌜t = #l⌝ ∗
    meta l nroot γ ∗
    ⌜cap = γ.(metadata_capacity)⌝ ∗
    ⌜0 < γ.(metadata_capacity)⌝ ∗
    l.[capacity] ↦□ #γ.(metadata_capacity) ∗
    inv ι (inv_inner l γ).
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & #Hmeta & -> & %Hcapacity & #Hl_capacity & #Hinv ) ".

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

  #[global] Instance mpmc_bstack_model_timeless t vs :
    Timeless (mpmc_bstack_model t vs).

  #[global] Instance mpmc_bstack_inv_persistent t ι cap :
    Persistent (mpmc_bstack_inv t ι cap).

  #[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 mpmc_bstack_model_valid t ι cap vs :
    mpmc_bstack_inv t ι cap -∗
    mpmc_bstack_model t vs -∗
    ⌜length vs ≤ cap⌝.
  Lemma mpmc_bstack_model_exclusive t vs1 vs2 :
    mpmc_bstack_model t vs1 -∗
    mpmc_bstack_model t vs2 -∗
    False.

  Lemma mpmc_bstack٠create𑁒spec ι (cap : Z) :
    (0 < cap)%Z →
    {{{
      True
    }}}
      mpmc_bstack٠create #cap
    {{{
      t
    , RET t;
      mpmc_bstack_inv t ι ₊cap ∗
      mpmc_bstack_model t []
    }}}.

  Lemma mpmc_bstack٠size𑁒spec t ι cap :
    <<<
      mpmc_bstack_inv t ι cap
    | ∀∀ vs,
      mpmc_bstack_model t vs
    >>>
      mpmc_bstack٠size t @ ↑ι
    <<<
      mpmc_bstack_model t vs
    | RET #(length vs);
      True
    >>>.

  Lemma mpmc_bstack٠is_empty𑁒spec t ι cap :
    <<<
      mpmc_bstack_inv t ι cap
    | ∀∀ vs,
      mpmc_bstack_model t vs
    >>>
      mpmc_bstack٠is_empty t @ ↑ι
    <<<
      mpmc_bstack_model t vs
    | RET #(bool_decide (vs = []%list));
      True
    >>>.

  #[local] Lemma mpmc_bstack٠push_aux_push𑁒spec t ι cap v :
    ⊢ (
      ∀ (sz : Z) front ws,
      <<<
        ⌜sz = length ws⌝ ∗
        ⌜front = list_to_val (length ws) ws⌝ ∗
        ⌜length ws < cap⌝ ∗
        mpmc_bstack_inv t ι cap
      | ∀∀ vs,
        mpmc_bstack_model t vs
      >>>
        mpmc_bstack٠push_aux t #sz v front @ ↑ι
      <<<
        ∃∃ b,
        ⌜b = bool_decide (length vs < cap)⌝ ∗
        mpmc_bstack_model t (if b then v :: vs else vs)
      | RET #b;
        True
      >>>
    ) ∧ (
      <<<
        mpmc_bstack_inv t ι cap
      | ∀∀ vs,
        mpmc_bstack_model t vs
      >>>
        mpmc_bstack٠push t v @ ↑ι
      <<<
        ∃∃ b,
        ⌜b = bool_decide (length vs < cap)⌝ ∗
        mpmc_bstack_model t (if b then v :: vs else vs)
      | RET #b;
        True
      >>>
    ).
  Lemma mpmc_bstack٠push𑁒spec t ι cap v :
    <<<
      mpmc_bstack_inv t ι cap
    | ∀∀ vs,
      mpmc_bstack_model t vs
    >>>
      mpmc_bstack٠push t v @ ↑ι
    <<<
      ∃∃ b,
      ⌜b = bool_decide (length vs < cap)⌝ ∗
      mpmc_bstack_model t (if b then v :: vs else vs)
    | RET #b;
      True
    >>>.

  Lemma mpmc_bstack٠pop𑁒spec t ι cap :
    <<<
      mpmc_bstack_inv t ι cap
    | ∀∀ vs,
      mpmc_bstack_model t vs
    >>>
      mpmc_bstack٠pop t @ ↑ι
    <<<
      mpmc_bstack_model t (tail vs)
    | RET head vs;
      True
    >>>.
End mpmc_bstack_G.

From zoo_saturn Require
  mpmc_bstack__opaque.

#[global] Opaque mpmc_bstack_inv.
#[global] Opaque mpmc_bstack_model.