Library zoo_persistent.pstack

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_persistent.pstack__code.
Require Import zoo_persistent.pstack__types.
Require Import zoo.options.

Implicit Type v t : val.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Definition pstack ۰ model t vs : iProp Σ :=
    list ۰ model t vs.

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

  #[global] Instance pstack ۰ model ｰ persistent t vs :
    Persistent (pstack ۰ model t vs).

  Lemma pstack ۰ model ｰ nil :
    ⊢ pstack ۰ model pstack ٠ empty [].

  Lemma pstack ٠ is_empty ｰ spec t vs :
    {{{
      pstack ۰ model t vs
    }}}
      pstack ٠ is_empty t
    {{{
      RET #(bool_decide (vs = []%list));
      True
    }}}.

  Lemma pstack ٠ push ｰ spec t vs v :
    {{{
      pstack ۰ model t vs
    }}}
      pstack ٠ push t v
    {{{
      t'
    , RET t';
      pstack ۰ model t' (v :: vs)
    }}}.

  Lemma pstack ٠ pop ｰ spec t vs :
    {{{
      pstack ۰ model t vs
    }}}
      pstack ٠ pop t
    {{{
      o
    , RET o ;
      match o with
      | None ⇒
          ⌜vs = []⌝
      | Some p ⇒
          ∃ v vs' t',
          ⌜vs = v :: vs'⌝ ∗
          ⌜p = (v , t')%V⌝ ∗
          pstack ۰ model t' vs'
      end
    }}}.
End zoo ۰ G.

Require zoo_persistent.pstack__opaque.

#[global] Opaque pstack ۰ model.