Library zoo_std.stack

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  stack__code.
From zoo_std Require Import
  dynarray_1.
From zoo Require Import
  options.

Implicit Types v t : val.

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Definition stack_model t vs :=
    dynarray_1_model t (reverse vs).

  #[global] Instance stack_model_timeless t vs :
    Timeless (stack_model t vs).

  Lemma stack٠make𑁒spec :
    {{{
      True
    }}}
      stack٠create ()
    {{{
      t
    , RET t;
      stack_model t []
    }}}.

  Lemma stack٠is_empty𑁒spec t vs :
    {{{
      stack_model t vs
    }}}
      stack٠is_empty t
    {{{
      RET #(bool_decide (vs = []%list));
      stack_model t vs
    }}}.

  Lemma stack٠push𑁒spec t vs v :
    {{{
      stack_model t vs
    }}}
      stack٠push t v
    {{{
      RET ();
      stack_model t (v :: vs)
    }}}.

  Lemma stack٠pop𑁒spec {t vs} v vs' :
    vs = v :: vs' →
    {{{
      stack_model t vs
    }}}
      stack٠pop t
    {{{
      RET v;
      stack_model t vs'
    }}}.
End zoo_G.

From zoo_std Require
  stack__opaque.

#[global] Opaque stack_model.