Library zoo_persistent.pstack

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  option
  list.
From zoo_persistent Require Export
  base
  pstack__code.
From zoo Require Import
  options.

Implicit Types 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.

From zoo_persistent Require
  pstack__opaque.

#[global] Opaque pstack_model.