Library zoo_saturn.bstack_mpmc

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_saturn.bstack_mpmc__code.
Require Import zoo_saturn.bstack_mpmc__types.
Require Import zoo.options.

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

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

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

Section bstack_mpmc ۰ G.
  Context `{bstack_mpmc ۰ G : BstackMpmcG Σ}.

  Record metadata :=
    { metadata ۰ capacity : nat
    ; metadata ۰ model : gname
    }.
  Implicit Type γ : 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 ۰ 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 Σ :=
    ∃ vs ,
    l .[front ] ↦ list ۰ to_val (length vs) vs ∗
    model₂ γ vs.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %vs{} & Hl_front & Hmodel₂ ) ".
  Definition bstack_mpmc ۰ inv t ι cap : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    ⌜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 bstack_mpmc ۰ model t vs : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    ⌜length vs ≤ γ.(metadata ۰ capacity)⌝ ∗
    model₁ γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %l{;_} & %γ{;_} & %Heq{} & Hmeta_{} & %Hvs{} & Hmodel₁{_{}} ) ".

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

  #[global] Instance bstack_mpmc ۰ inv ｰ persistent t ι cap :
    Persistent (bstack_mpmc ۰ 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 bstack_mpmc ۰ model ｰ valid t ι cap vs :
    bstack_mpmc ۰ inv t ι cap -∗
    bstack_mpmc ۰ model t vs -∗
    ⌜length vs ≤ cap ⌝.
  Lemma bstack_mpmc ۰ model ｰ exclusive t vs1 vs2 :
    bstack_mpmc ۰ model t vs1 -∗
    bstack_mpmc ۰ model t vs2 -∗
    False.

  Lemma bstack_mpmc ٠ create ｰ spec ι (cap : Z) :
    (0 < cap)%Z →
    {{{
      True
    }}}
      bstack_mpmc ٠ create #cap
    {{{
      t
    , RET t ;
      bstack_mpmc ۰ inv t ι ₊cap ∗
      bstack_mpmc ۰ model t []
    }}}.

  Lemma bstack_mpmc ٠ size ｰ spec t ι cap :
    <<<
      bstack_mpmc ۰ inv t ι cap
    | ∀∀ vs ,
      bstack_mpmc ۰ model t vs
    >>>
      bstack_mpmc ٠ size t @ ↑ι
    <<<
      bstack_mpmc ۰ model t vs
    | RET #(length vs );
      True
    >>>.

  Lemma bstack_mpmc ٠ is_empty ｰ spec t ι cap :
    <<<
      bstack_mpmc ۰ inv t ι cap
    | ∀∀ vs ,
      bstack_mpmc ۰ model t vs
    >>>
      bstack_mpmc ٠ is_empty t @ ↑ι
    <<<
      bstack_mpmc ۰ model t vs
    | RET #(bool_decide (vs = []%list));
      True
    >>>.

  #[local] Lemma bstack_mpmc ٠ push_aux_push ｰ spec t ι cap v :
    ⊢ (
      ∀ (sz : Z) front ws ,
      <<<
        ⌜sz = length ws ⌝ ∗
        ⌜front = list ۰ to_val (length ws) ws ⌝ ∗
        ⌜length ws < cap ⌝ ∗
        bstack_mpmc ۰ inv t ι cap
      | ∀∀ vs ,
        bstack_mpmc ۰ model t vs
      >>>
        bstack_mpmc ٠ push_aux t #sz v front @ ↑ι
      <<<
        ∃∃ b ,
        ⌜b = bool_decide (length vs < cap)⌝ ∗
        bstack_mpmc ۰ model t (if b then v :: vs else vs)
      | RET #b ;
        True
      >>>
    ) ∧ (
      <<<
        bstack_mpmc ۰ inv t ι cap
      | ∀∀ vs ,
        bstack_mpmc ۰ model t vs
      >>>
        bstack_mpmc ٠ push t v @ ↑ι
      <<<
        ∃∃ b ,
        ⌜b = bool_decide (length vs < cap)⌝ ∗
        bstack_mpmc ۰ model t (if b then v :: vs else vs)
      | RET #b ;
        True
      >>>
    ).
  Lemma bstack_mpmc ٠ push ｰ spec t ι cap v :
    <<<
      bstack_mpmc ۰ inv t ι cap
    | ∀∀ vs ,
      bstack_mpmc ۰ model t vs
    >>>
      bstack_mpmc ٠ push t v @ ↑ι
    <<<
      ∃∃ b ,
      ⌜b = bool_decide (length vs < cap)⌝ ∗
      bstack_mpmc ۰ model t (if b then v :: vs else vs)
    | RET #b ;
      True
    >>>.

  Lemma bstack_mpmc ٠ pop ｰ spec t ι cap :
    <<<
      bstack_mpmc ۰ inv t ι cap
    | ∀∀ vs ,
      bstack_mpmc ۰ model t vs
    >>>
      bstack_mpmc ٠ pop t @ ↑ι
    <<<
      bstack_mpmc ۰ model t (tail vs)
    | RET head vs ;
      True
    >>>.
End bstack_mpmc ۰ G.

Require zoo_saturn.bstack_mpmc__opaque.

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